Profinite completion of groups

We define the profinite completion of a group as the limit of its finite quotients, and prove its universal property.

def OpenNormalSubgroup.toFiniteIndexNormalSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [ContinuousMul G] (H : OpenNormalSubgroup G) : FiniteIndexNormalSubgroup G

An open normal subgroup of a compact topological group has finite index.

def OpenNormalAddSubgroup.toFiniteIndexNormalAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] [CompactSpace G] [ContinuousAdd G] (H : OpenNormalAddSubgroup G) : FiniteIndexNormalAddSubgroup G

An open normal additive subgroup of a compact topological additive group has finite index.

theorem OpenNormalSubgroup.toFiniteIndexNormalSubgroup_mono {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [ContinuousMul G] {H K : OpenNormalSubgroup G} (h : H ≤ K) : H.toFiniteIndexNormalSubgroup ≤ K.toFiniteIndexNormalSubgroup

theorem OpenNormalAddSubgroup.toFiniteIndexNormalAddSubgroup_mono {G : Type u_1} [AddGroup G] [TopologicalSpace G] [CompactSpace G] [ContinuousAdd G] {H K : OpenNormalAddSubgroup G} (h : H ≤ K) : H.toFiniteIndexNormalAddSubgroup ≤ K.toFiniteIndexNormalAddSubgroup

theorem OpenNormalSubgroup.toFiniteIndexNormalSubgroup_injective {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [ContinuousMul G] : Function.Injective toFiniteIndexNormalSubgroup

theorem OpenNormalAddSubgroup.toFiniteIndexNormalAddSubgroup_injective {G : Type u_1} [AddGroup G] [TopologicalSpace G] [CompactSpace G] [ContinuousAdd G] : Function.Injective toFiniteIndexNormalAddSubgroup

def ProfiniteGrp.ProfiniteCompletion.finiteGrpDiagram (G : GrpCat) : CategoryTheory.Functor (FiniteIndexNormalSubgroup ↑G) FiniteGrp.{u}

The diagram of finite quotients indexed by finite-index normal subgroups of G.

def ProfiniteGrp.ProfiniteCompletion.diagram (G : GrpCat) : CategoryTheory.Functor (FiniteIndexNormalSubgroup ↑G) ProfiniteGrp.{u}

The finite-quotient diagram viewed in ProfiniteGrp.

def ProfiniteGrp.ProfiniteCompletion.completion (G : GrpCat) : ProfiniteGrp.{u}

The profinite completion of G as a projective limit.

def ProfiniteGrp.ProfiniteCompletion.etaFn (G : GrpCat) (x : ↑G) : ↑(completion G).toProfinite.toTop

The canonical map from G to its profinite completion, as a function.

def ProfiniteGrp.ProfiniteCompletion.eta (G : GrpCat) : G ⟶ GrpCat.of ↑(completion G).toProfinite.toTop

The canonical morphism from G to its profinite completion.

theorem ProfiniteGrp.ProfiniteCompletion.denseRange (G : GrpCat) : DenseRange (etaFn G)

def ProfiniteGrp.ProfiniteCompletion.preimage {G : GrpCat} {P : ProfiniteGrp.{u}} (f : G ⟶ GrpCat.of ↑P.toProfinite.toTop) (H : OpenNormalSubgroup ↑P.toProfinite.toTop) : FiniteIndexNormalSubgroup ↑G

The preimage of an open normal subgroup under a morphism to a profinite group.

theorem ProfiniteGrp.ProfiniteCompletion.preimage_le {G : GrpCat} {P : ProfiniteGrp.{u}} {f : G ⟶ GrpCat.of ↑P.toProfinite.toTop} {H K : OpenNormalSubgroup ↑P.toProfinite.toTop} (h : H ≤ K) : preimage f H ≤ preimage f K

def ProfiniteGrp.ProfiniteCompletion.quotientMap {G : GrpCat} {P : ProfiniteGrp.{u}} (f : G ⟶ GrpCat.of ↑P.toProfinite.toTop) (H : OpenNormalSubgroup ↑P.toProfinite.toTop) : FiniteGrp.of (↑G ⧸ (preimage f H).toSubgroup) ⟶ FiniteGrp.of (↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup)

The induced map on finite quotients coming from a morphism to P.

noncomputable def ProfiniteGrp.ProfiniteCompletion.lift {G : GrpCat} {P : ProfiniteGrp.{u}} (f : G ⟶ GrpCat.of ↑P.toProfinite.toTop) : completion G ⟶ P

The universal morphism from the profinite completion to P.

@[simp]

theorem ProfiniteGrp.ProfiniteCompletion.lift_eta {G : GrpCat} {P : ProfiniteGrp.{u}} (f : G ⟶ GrpCat.of ↑P.toProfinite.toTop) : CategoryTheory.CategoryStruct.comp (eta G) ((CategoryTheory.forget₂ ProfiniteGrp.{u} GrpCat).map (lift f)) = f

@[simp]

theorem ProfiniteGrp.ProfiniteCompletion.lift_eta_assoc {G : GrpCat} {P : ProfiniteGrp.{u}} (f : G ⟶ GrpCat.of ↑P.toProfinite.toTop) {Z : GrpCat} (h : (CategoryTheory.forget₂ ProfiniteGrp.{u} GrpCat).obj P ⟶ Z) : CategoryTheory.CategoryStruct.comp (eta G) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget₂ ProfiniteGrp.{u} GrpCat).map (lift f)) h) = CategoryTheory.CategoryStruct.comp f h

theorem ProfiniteGrp.ProfiniteCompletion.lift_unique {G : GrpCat} {P : ProfiniteGrp.{u}} (f g : completion G ⟶ P) (h : CategoryTheory.CategoryStruct.comp (eta G) ((CategoryTheory.forget₂ ProfiniteGrp.{u} GrpCat).map f) = CategoryTheory.CategoryStruct.comp (eta G) ((CategoryTheory.forget₂ ProfiniteGrp.{u} GrpCat).map g)) : f = g

noncomputable def ProfiniteGrp.profiniteCompletion : CategoryTheory.Functor GrpCat ProfiniteGrp.{u}

The profinite completion functor.

@[simp]

theorem ProfiniteGrp.profiniteCompletion_map {X✝ Y✝ : GrpCat} (f : X✝ ⟶ Y✝) : profiniteCompletion.map f = ProfiniteCompletion.lift (CategoryTheory.CategoryStruct.comp f (ProfiniteCompletion.eta Y✝))

@[simp]

theorem ProfiniteGrp.profiniteCompletion_obj (G : GrpCat) : profiniteCompletion.obj G = ProfiniteCompletion.completion G

noncomputable def ProfiniteGrp.ProfiniteCompletion.homEquiv (G : GrpCat) (P : ProfiniteGrp.{u}) : (completion G ⟶ P) ≃ (G ⟶ GrpCat.of ↑P.toProfinite.toTop)

The hom-set equivalence exhibiting the adjunction.

noncomputable def ProfiniteGrp.ProfiniteCompletion.adjunction : profiniteCompletion ⊣ CategoryTheory.forget₂ ProfiniteGrp.{u_1} GrpCat

The profinite completion is left adjoint to the forgetful functor.