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.

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

The diagram of finite quotients of P viewed in ProfiniteGrp.

@[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)

@[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)

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

theorem ProfiniteGrp.toLimitFun_continuous (P : ProfiniteGrp.{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

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.diagram).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.diagram

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

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.

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

The canonical cone over diagram P with point P.

@[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

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

The canonical cone over diagram P is a limit cone.