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)

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.

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

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

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

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