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.

instance ProfiniteGrp.instSmallCategoryOpenNormalSubgroupCarrierToTopTotallyDisconnectedSpaceToProfinite (P : ProfiniteGrp.{u_1}) : CategoryTheory.SmallCategory (OpenNormalSubgroup ↑P.toProfinite.toTop)

Equations

• P.instSmallCategoryOpenNormalSubgroupCarrierToTopTotallyDisconnectedSpaceToProfinite = Preorder.smallCategory (OpenNormalSubgroup ↑P.toProfinite.toTop)

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 ProfiniteGrp.toLimit_fun (P : ProfiniteGrp.{u}) : ↑P.toProfinite.toTop →* ↑(limit (P.toFiniteQuotientFunctor.comp (CategoryTheory.forget₂ FiniteGrp.{u} ProfiniteGrp.{u}))).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.toLimit_fun = { toFun := fun (p : ↑P.toProfinite.toTop) => ⟨fun (x : OpenNormalSubgroup ↑P.toProfinite.toTop) => ↑p, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

theorem ProfiniteGrp.toLimit_fun_continuous (P : ProfiniteGrp.{u}) : Continuous ⇑P.toLimit_fun

def ProfiniteGrp.toLimit (P : ProfiniteGrp.{u}) : P ⟶ limit (P.toFiniteQuotientFunctor.comp (CategoryTheory.forget₂ FiniteGrp.{u} ProfiniteGrp.{u}))

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.toLimit_fun; { toMonoidHom := __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)

noncomputable def ProfiniteGrp.continuousMulEquivLimittoFiniteQuotientFunctor (P : ProfiniteGrp.{u}) : ↑P.toProfinite.toTop ≃ₜ* ↑(limit (P.toFiniteQuotientFunctor.comp (CategoryTheory.forget₂ FiniteGrp.{u} ProfiniteGrp.{u}))).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.toFiniteQuotientFunctor.comp (CategoryTheory.forget₂ FiniteGrp.{u} ProfiniteGrp.{u}))

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