A profinite group is the projective limit of finite groups

We define the topological group isomorphism between a profinite group and the projective limit of its quotients by open normal subgroups.

Main definitions

• toFiniteQuotientFunctor : The functor from OpenNormalSubgroup P to FiniteGrp sending an open normal subgroup U to P ⧸ U, where P : ProfiniteGrp.

• toLimit : The continuous homomorphism from a profinite group P to the projective limit of its quotients by open normal subgroups ordered by inclusion.

• ContinuousMulEquivLimittoFiniteQuotientFunctor : The toLimit is a ContinuousMulEquiv

Main Statements

• OpenNormalSubgroupSubClopenNhdsOfOne : For any open neighborhood of 1 there is an open normal subgroup contained in it.

def ProfiniteGrp.toFiniteQuotientFunctor (P : ProfiniteGrp.{u_1}) : CategoryTheory.Functor (OpenNormalSubgroup ↑P.toProfinite.toTop) FiniteGrp.{u_1}

The functor from OpenNormalSubgroup P to FiniteGrp sending U to P ⧸ U, where P : ProfiniteGrp.

Equations

• One or more equations did not get rendered due to their size.

def ProfiniteAddGrp.toFiniteQuotientFunctor (P : ProfiniteAddGrp.{u_1}) : CategoryTheory.Functor (OpenNormalAddSubgroup ↑P.toProfinite.toTop) FiniteAddGrp.{u_1}

The functor from OpenNormalAddSubgroup P to FiniteAddGrp sending U to P ⧸ U, where P : ProfiniteAddGrp.

Equations

• One or more equations did not get rendered due to their size.

def ProfiniteGrp.diagram (P : ProfiniteGrp.{u}) : CategoryTheory.Functor (OpenNormalSubgroup ↑P.toProfinite.toTop) ProfiniteGrp.{u}

The diagram of finite quotients of P viewed in ProfiniteGrp.

Equations

• P.diagram = P.toFiniteQuotientFunctor.comp (CategoryTheory.forget₂ FiniteGrp.{?u.1} ProfiniteGrp.{?u.1})

def ProfiniteAddGrp.diagram (P : ProfiniteAddGrp.{u}) : CategoryTheory.Functor (OpenNormalAddSubgroup ↑P.toProfinite.toTop) ProfiniteAddGrp.{u}

The diagram of finite quotients of P viewed in ProfiniteAddGrp.

Equations

• P.diagram = P.toFiniteQuotientFunctor.comp (CategoryTheory.forget₂ FiniteAddGrp.{?u.1} ProfiniteAddGrp.{?u.1})

@[simp]

theorem ProfiniteAddGrp.diagram_obj (P : ProfiniteAddGrp.{u}) (X : OpenNormalAddSubgroup ↑P.toProfinite.toTop) : P.diagram.obj X = (CategoryTheory.forget₂ FiniteAddGrp.{u} ProfiniteAddGrp.{u}).obj (P.toFiniteQuotientFunctor.obj X)

@[simp]

theorem ProfiniteGrp.diagram_map (P : ProfiniteGrp.{u}) {X✝ Y✝ : OpenNormalSubgroup ↑P.toProfinite.toTop} (f : X✝ ⟶ Y✝) : P.diagram.map f = (CategoryTheory.forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).map (P.toFiniteQuotientFunctor.map f)

@[simp]

theorem ProfiniteAddGrp.diagram_map (P : ProfiniteAddGrp.{u}) {X✝ Y✝ : OpenNormalAddSubgroup ↑P.toProfinite.toTop} (f : X✝ ⟶ Y✝) : P.diagram.map f = (CategoryTheory.forget₂ FiniteAddGrp.{u} ProfiniteAddGrp.{u}).map (P.toFiniteQuotientFunctor.map f)

@[simp]

theorem ProfiniteGrp.diagram_obj (P : ProfiniteGrp.{u}) (X : OpenNormalSubgroup ↑P.toProfinite.toTop) : P.diagram.obj X = (CategoryTheory.forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj (P.toFiniteQuotientFunctor.obj X)

def ProfiniteGrp.toLimitFun (P : ProfiniteGrp.{u}) : ↑P.toProfinite.toTop →* ↑(limit P.diagram).toProfinite.toTop

The MonoidHom from a profinite group P to the projective limit of its quotients by open normal subgroups ordered by inclusion

Equations

• P.toLimitFun = { toFun := fun (p : ↑P.toProfinite.toTop) => ⟨fun (x : OpenNormalSubgroup ↑P.toProfinite.toTop) => ↑p, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

def ProfiniteAddGrp.toLimitFun (P : ProfiniteAddGrp.{u}) : ↑P.toProfinite.toTop →+ ↑(limit P.diagram).toProfinite.toTop

The AddMonoidHom from a profinite additive group P to the projective limit of its quotients by open normal subgroups ordered by inclusion

Equations

• P.toLimitFun = { toFun := fun (p : ↑P.toProfinite.toTop) => ⟨fun (x : OpenNormalAddSubgroup ↑P.toProfinite.toTop) => ↑p, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

theorem ProfiniteGrp.toLimitFun_continuous (P : ProfiniteGrp.{u}) : Continuous ⇑P.toLimitFun

theorem ProfiniteAddGrp.toLimitFun_continuous (P : ProfiniteAddGrp.{u}) : Continuous ⇑P.toLimitFun

def ProfiniteGrp.toLimit (P : ProfiniteGrp.{u}) : P ⟶ limit P.diagram

The morphism in the category of ProfiniteGrp from a profinite group P to the projective limit of its quotients by open normal subgroups ordered by inclusion

Equations

• P.toLimit = ProfiniteGrp.ofHom (let __src := P.toLimitFun; { toMonoidHom := __src, continuous_toFun := ⋯ })

def ProfiniteAddGrp.toLimit (P : ProfiniteAddGrp.{u}) : P ⟶ limit P.diagram

The morphism in the category of ProfiniteAddGrp from a profinite additive group P to the projective limit of its quotients by open normal subgroups ordered by inclusion

Equations

• P.toLimit = ProfiniteAddGrp.ofHom (let __src := P.toLimitFun; { toAddMonoidHom := __src, continuous_toFun := ⋯ })

theorem ProfiniteGrp.denseRange_toLimit (P : ProfiniteGrp.{u}) : DenseRange ⇑(Hom.hom P.toLimit)

An auxiliary result, superseded by toLimit_surjective

theorem ProfiniteGrp.toLimit_surjective (P : ProfiniteGrp.{u}) : Function.Surjective ⇑(Hom.hom P.toLimit)

theorem ProfiniteGrp.toLimit_injective (P : ProfiniteGrp.{u}) : Function.Injective ⇑(Hom.hom P.toLimit)

theorem ProfiniteAddGrp.toLimit_injective (P : ProfiniteAddGrp.{u}) : Function.Injective ⇑(Hom.hom P.toLimit)

noncomputable def ProfiniteGrp.continuousMulEquivLimittoFiniteQuotientFunctor (P : ProfiniteGrp.{u}) : ↑P.toProfinite.toTop ≃ₜ* ↑(limit P.diagram).toProfinite.toTop

The topological group isomorphism between a profinite group and the projective limit of its quotients by open normal subgroups

Equations

• P.continuousMulEquivLimittoFiniteQuotientFunctor = { toEquiv := ⋯.homeoOfEquivCompactToT2.toEquiv, map_mul' := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

instance ProfiniteGrp.isIso_toLimit (P : ProfiniteGrp.{u}) : CategoryTheory.IsIso P.toLimit

noncomputable def ProfiniteGrp.isoLimittoFiniteQuotientFunctor (P : ProfiniteGrp.{u}) : P ≅ limit P.diagram

The isomorphism in the category of profinite group between a profinite group and the projective limit of its quotients by open normal subgroups

Equations

• P.isoLimittoFiniteQuotientFunctor = ProfiniteGrp.ContinuousMulEquiv.toProfiniteGrpIso P.continuousMulEquivLimittoFiniteQuotientFunctor

def ProfiniteGrp.proj {P : ProfiniteGrp.{u}} (U : OpenNormalSubgroup ↑P.toProfinite.toTop) : P ⟶ P.diagram.obj U

The projection from P to the quotient by an open normal subgroup.

Equations

• ProfiniteGrp.proj U = ProfiniteGrp.ofHom { toFun := QuotientGroup.mk, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }

def ProfiniteAddGrp.proj {P : ProfiniteAddGrp.{u}} (U : OpenNormalAddSubgroup ↑P.toProfinite.toTop) : P ⟶ P.diagram.obj U

The projection from P to the quotient by an open normal subgroup.

Equations

• ProfiniteAddGrp.proj U = ProfiniteAddGrp.ofHom { toFun := QuotientAddGroup.mk, map_zero' := ⋯, map_add' := ⋯, continuous_toFun := ⋯ }

def ProfiniteGrp.cone (P : ProfiniteGrp.{u}) : CategoryTheory.Limits.Cone P.diagram

The canonical cone over diagram P with point P.

Equations

• P.cone = { pt := P, π := { app := ProfiniteGrp.proj, naturality := ⋯ } }

def ProfiniteAddGrp.cone (P : ProfiniteAddGrp.{u}) : CategoryTheory.Limits.Cone P.diagram

The canonical cone over diagram P with point P.

Equations

• P.cone = { pt := P, π := { app := ProfiniteAddGrp.proj, naturality := ⋯ } }

@[simp]

theorem ProfiniteGrp.cone_pt (P : ProfiniteGrp.{u}) : P.cone.pt = P

@[simp]

theorem ProfiniteGrp.cone_π_app (P : ProfiniteGrp.{u}) (U : OpenNormalSubgroup ↑P.toProfinite.toTop) : P.cone.π.app U = proj U

@[simp]

theorem ProfiniteAddGrp.cone_π_app (P : ProfiniteAddGrp.{u}) (U : OpenNormalAddSubgroup ↑P.toProfinite.toTop) : P.cone.π.app U = proj U

@[simp]

theorem ProfiniteAddGrp.cone_pt (P : ProfiniteAddGrp.{u}) : P.cone.pt = P

noncomputable def ProfiniteGrp.isLimitCone (P : ProfiniteGrp.{u}) : CategoryTheory.Limits.IsLimit P.cone

The canonical cone over diagram P is a limit cone.

Equations

• P.isLimitCone = (ProfiniteGrp.limitConeIsLimit P.diagram).ofIsoLimit (CategoryTheory.Limits.Cone.ext P.cone.pt.isoLimittoFiniteQuotientFunctor ⋯).symm