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.instSmallCategoryOpenNormalSubgroupαTopologicalSpaceToTopTotallyDisconnectedSpaceToProfinite (P : ProfiniteGrp.{u_1}) : CategoryTheory.SmallCategory (OpenNormalSubgroup ↑P.toProfinite.toTop)

Equations

• P.instSmallCategoryOpenNormalSubgroupαTopologicalSpaceToTopTotallyDisconnectedSpaceToProfinite = 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 = { toMonoidHom := P.toLimit_fun, continuous_toFun := ⋯ }

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

An auxiliary result, superceded by toLimit_surjective.

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

theorem ProfiniteGrp.toLimit_injective (P : ProfiniteGrp.{u}) : Function.Injective ⇑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 := ⋯ }

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

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