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.

Equations

• H.toFiniteIndexNormalSubgroup = FiniteIndexNormalSubgroup.ofSubgroup ↑H.toOpenSubgroup

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.

Equations

• H.toFiniteIndexNormalAddSubgroup = FiniteIndexNormalAddSubgroup.ofAddSubgroup ↑H.toOpenAddSubgroup

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.

Equations

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

def ProfiniteAddGrp.ProfiniteCompletion.finiteAddGrpDiagram (G : AddGrpCat) : CategoryTheory.Functor (FiniteIndexNormalAddSubgroup ↑G) FiniteAddGrp.{u}

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

Equations

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

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

The finite-quotient diagram viewed in ProfiniteGrp.

Equations

• ProfiniteGrp.ProfiniteCompletion.diagram G = (ProfiniteGrp.ProfiniteCompletion.finiteGrpDiagram G).comp (CategoryTheory.forget₂ FiniteGrp.{?u.1} ProfiniteGrp.{?u.1})

def ProfiniteAddGrp.ProfiniteCompletion.diagram (G : AddGrpCat) : CategoryTheory.Functor (FiniteIndexNormalAddSubgroup ↑G) ProfiniteAddGrp.{u}

The finite-quotient diagram viewed in ProfiniteAddGrp.

Equations

• ProfiniteAddGrp.ProfiniteCompletion.diagram G = (ProfiniteAddGrp.ProfiniteCompletion.finiteAddGrpDiagram G).comp (CategoryTheory.forget₂ FiniteAddGrp.{?u.1} ProfiniteAddGrp.{?u.1})

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

The profinite completion of G as a projective limit.

Equations

• ProfiniteGrp.ProfiniteCompletion.completion G = ProfiniteGrp.limit (ProfiniteGrp.ProfiniteCompletion.diagram G)

def ProfiniteAddGrp.ProfiniteCompletion.completion (G : AddGrpCat) : ProfiniteAddGrp.{u}

The profinite completion of G as a projective limit.

Equations

• ProfiniteAddGrp.ProfiniteCompletion.completion G = ProfiniteAddGrp.limit (ProfiniteAddGrp.ProfiniteCompletion.diagram G)

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

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

Equations

• ProfiniteGrp.ProfiniteCompletion.etaFn G x = ⟨fun (x_1 : FiniteIndexNormalSubgroup ↑G) => ↑x, ⋯⟩

def ProfiniteAddGrp.ProfiniteCompletion.etaFn (G : AddGrpCat) (x : ↑G) : ↑(completion G).toProfinite.toTop

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

Equations

• ProfiniteAddGrp.ProfiniteCompletion.etaFn G x = ⟨fun (x_1 : FiniteIndexNormalAddSubgroup ↑G) => ↑x, ⋯⟩

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

The canonical morphism from G to its profinite completion.

Equations

• ProfiniteGrp.ProfiniteCompletion.eta G = GrpCat.ofHom { toFun := ProfiniteGrp.ProfiniteCompletion.etaFn G, map_one' := ⋯, map_mul' := ⋯ }

def ProfiniteAddGrp.ProfiniteCompletion.eta (G : AddGrpCat) : G ⟶ AddGrpCat.of ↑(completion G).toProfinite.toTop

The canonical morphism from G to its profinite completion.

Equations

• ProfiniteAddGrp.ProfiniteCompletion.eta G = AddGrpCat.ofHom { toFun := ProfiniteAddGrp.ProfiniteCompletion.etaFn G, map_zero' := ⋯, map_add' := ⋯ }

theorem ProfiniteGrp.ProfiniteCompletion.mono_eta_iff_residuallyFinite (G : GrpCat) : CategoryTheory.Mono (eta G) ↔ Group.ResiduallyFinite ↑G

theorem ProfiniteAddGrp.ProfiniteCompletion.mono_eta_iff_residuallyFinite (G : AddGrpCat) : CategoryTheory.Mono (eta G) ↔ AddGroup.ResiduallyFinite ↑G

theorem ProfiniteGrp.ProfiniteCompletion.etaFn_injective_iff_residuallyFinite (G : GrpCat) : Function.Injective (etaFn G) ↔ Group.ResiduallyFinite ↑G

theorem ProfiniteAddGrp.ProfiniteCompletion.etaFn_injective_iff_residuallyFinite (G : AddGrpCat) : Function.Injective (etaFn G) ↔ AddGroup.ResiduallyFinite ↑G

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

theorem ProfiniteAddGrp.ProfiniteCompletion.denseRange (G : AddGrpCat) : 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.

Equations

• ProfiniteGrp.ProfiniteCompletion.preimage f H = FiniteIndexNormalSubgroup.comap (GrpCat.Hom.hom f) H.toFiniteIndexNormalSubgroup

def ProfiniteAddGrp.ProfiniteCompletion.preimage {G : AddGrpCat} {P : ProfiniteAddGrp.{u}} (f : G ⟶ AddGrpCat.of ↑P.toProfinite.toTop) (H : OpenNormalAddSubgroup ↑P.toProfinite.toTop) : FiniteIndexNormalAddSubgroup ↑G

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

Equations

• ProfiniteAddGrp.ProfiniteCompletion.preimage f H = FiniteIndexNormalAddSubgroup.comap (AddGrpCat.Hom.hom f) H.toFiniteIndexNormalAddSubgroup

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

theorem ProfiniteAddGrp.ProfiniteCompletion.preimage_le {G : AddGrpCat} {P : ProfiniteAddGrp.{u}} {f : G ⟶ AddGrpCat.of ↑P.toProfinite.toTop} {H K : OpenNormalAddSubgroup ↑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.

Equations

• ProfiniteGrp.ProfiniteCompletion.quotientMap f H = FiniteGrp.ofHom (QuotientGroup.map (ProfiniteGrp.ProfiniteCompletion.preimage f H).toSubgroup (↑H.toOpenSubgroup) (GrpCat.Hom.hom f) ⋯)

def ProfiniteAddGrp.ProfiniteCompletion.quotientMap {G : AddGrpCat} {P : ProfiniteAddGrp.{u}} (f : G ⟶ AddGrpCat.of ↑P.toProfinite.toTop) (H : OpenNormalAddSubgroup ↑P.toProfinite.toTop) : FiniteAddGrp.of (↑G ⧸ (preimage f H).toAddSubgroup) ⟶ FiniteAddGrp.of (↑P.toProfinite.toTop ⧸ ↑H.toOpenAddSubgroup)

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

Equations

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

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.

Equations

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

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

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

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

The profinite completion functor.

Equations

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

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

Equations

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

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

The profinite completion is left adjoint to the forgetful functor.

Equations

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