Category of Profinite Groups

We say G is a profinite group if it is a topological group which is compact and totally disconnected.

Main definitions and results

• ProfiniteGrp is the category of profinite groups.

• ProfiniteGrp.pi : The pi-type of profinite groups is also a profinite group.

• ofFiniteGrp : A FiniteGrp when given the discrete topology can be considered as a profinite group.

• ofClosedSubgroup : A closed subgroup of a profinite group is profinite.

structure ProfiniteGrp : Type (u_1 + 1)

The category of profinite groups. A term of this type consists of a profinite set with a topological group structure.

• toProfinite : Profinite

  The underlying profinite topological space.

• group : Group ↑self.toProfinite.toTop

  The group structure.

• topologicalGroup : TopologicalGroup ↑self.toProfinite.toTop

  The above data together form a topological group.

theorem ProfiniteGrp.topologicalGroup (self : ProfiniteGrp.{u_1}) : TopologicalGroup ↑self.toProfinite.toTop

The above data together form a topological group.

structure ProfiniteAddGrp : Type (u_1 + 1)

The category of profinite additive groups. A term of this type consists of a profinite set with a topological additive group structure.

• toProfinite : Profinite

  The underlying profinite topological space.

• addGroup : AddGroup ↑self.toProfinite.toTop

  The additive group structure.

• topologicalAddGroup : TopologicalAddGroup ↑self.toProfinite.toTop

  The above data together form a topological additive group.

theorem ProfiniteAddGrp.topologicalAddGroup (self : ProfiniteAddGrp.{u_1}) : TopologicalAddGroup ↑self.toProfinite.toTop

The above data together form a topological additive group.

instance ProfiniteGrp.instCoeSortType : CoeSort ProfiniteGrp.{u} (Type u)

Equations

• ProfiniteGrp.instCoeSortType = { coe := fun (G : ProfiniteGrp.{?u.1}) => ↑G.toProfinite.toTop }

instance ProfiniteAddGrp.instCoeSortType : CoeSort ProfiniteAddGrp.{u} (Type u)

Equations

• ProfiniteAddGrp.instCoeSortType = { coe := fun (G : ProfiniteAddGrp.{?u.1}) => ↑G.toProfinite.toTop }

instance ProfiniteGrp.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} ProfiniteGrp.{u_1}

Equations

• ProfiniteGrp.instCategory = CategoryTheory.Category.mk @ProfiniteGrp.instCategory.proof_1 @ProfiniteGrp.instCategory.proof_2 @ProfiniteGrp.instCategory.proof_3

instance ProfiniteAddGrp.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} ProfiniteAddGrp.{u_1}

Equations

• ProfiniteAddGrp.instCategory = CategoryTheory.Category.mk @ProfiniteAddGrp.instCategory.proof_1 @ProfiniteAddGrp.instCategory.proof_2 @ProfiniteAddGrp.instCategory.proof_3

instance ProfiniteGrp.instFunLikeHomαTopologicalSpaceToTopTotallyDisconnectedSpaceToProfinite (G : ProfiniteGrp.{u_1}) (H : ProfiniteGrp.{u_1}) : FunLike (G ⟶ H) ↑G.toProfinite.toTop ↑H.toProfinite.toTop

Equations

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

instance ProfiniteAddGrp.instFunLikeHomαTopologicalSpaceToTopTotallyDisconnectedSpaceToProfinite (G : ProfiniteAddGrp.{u_1}) (H : ProfiniteAddGrp.{u_1}) : FunLike (G ⟶ H) ↑G.toProfinite.toTop ↑H.toProfinite.toTop

Equations

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

instance ProfiniteGrp.instMonoidHomClassHomαTopologicalSpaceToTopTotallyDisconnectedSpaceToProfinite (G : ProfiniteGrp.{u_1}) (H : ProfiniteGrp.{u_1}) : MonoidHomClass (G ⟶ H) ↑G.toProfinite.toTop ↑H.toProfinite.toTop

Equations

• ⋯ = ⋯

instance ProfiniteAddGrp.instAddMonoidHomClassHomαTopologicalSpaceToTopTotallyDisconnectedSpaceToProfinite (G : ProfiniteAddGrp.{u_1}) (H : ProfiniteAddGrp.{u_1}) : AddMonoidHomClass (G ⟶ H) ↑G.toProfinite.toTop ↑H.toProfinite.toTop

Equations

• ⋯ = ⋯

instance ProfiniteGrp.instContinuousMapClassHomαTopologicalSpaceToTopTotallyDisconnectedSpaceToProfinite (G : ProfiniteGrp.{u_1}) (H : ProfiniteGrp.{u_1}) : ContinuousMapClass (G ⟶ H) ↑G.toProfinite.toTop ↑H.toProfinite.toTop

Equations

• ⋯ = ⋯

instance ProfiniteAddGrp.instContinuousMapClassHomαTopologicalSpaceToTopTotallyDisconnectedSpaceToProfinite (G : ProfiniteAddGrp.{u_1}) (H : ProfiniteAddGrp.{u_1}) : ContinuousMapClass (G ⟶ H) ↑G.toProfinite.toTop ↑H.toProfinite.toTop

Equations

• ⋯ = ⋯

instance ProfiniteGrp.instConcreteCategory : CategoryTheory.ConcreteCategory ProfiniteGrp.{u_1}

Equations

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

instance ProfiniteAddGrp.instConcreteCategory : CategoryTheory.ConcreteCategory ProfiniteAddGrp.{u_1}

Equations

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

def ProfiniteGrp.of (G : Type u) [Group G] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : ProfiniteGrp.{u}

Construct a term of ProfiniteGrp from a type endowed with the structure of a compact and totally disconnected topological group. (The condition of being Hausdorff can be omitted here because totally disconnected implies that {1} is a closed set, thus implying Hausdorff in a topological group.)

Equations

• ProfiniteGrp.of G = ProfiniteGrp.mk (Profinite.of G)

def ProfiniteAddGrp.of (G : Type u) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : ProfiniteAddGrp.{u}

Construct a term of ProfiniteAddGrp from a type endowed with the structure of a compact and totally disconnected topological additive group. (The condition of being Hausdorff can be omitted here because totally disconnected implies that {0} is a closed set, thus implying Hausdorff in a topological additive group.)

Equations

• ProfiniteAddGrp.of G = ProfiniteAddGrp.mk (Profinite.of G)

@[simp]

theorem ProfiniteGrp.coe_of (X : ProfiniteGrp.{u_1}) : ↑(ProfiniteGrp.of ↑X.toProfinite.toTop).toProfinite.toTop = ↑X.toProfinite.toTop

@[simp]

theorem ProfiniteAddGrp.coe_of (X : ProfiniteAddGrp.{u_1}) : ↑(ProfiniteAddGrp.of ↑X.toProfinite.toTop).toProfinite.toTop = ↑X.toProfinite.toTop

@[simp]

theorem ProfiniteGrp.coe_id (X : ProfiniteGrp.{u_1}) : CategoryTheory.CategoryStruct.id ((CategoryTheory.forget ProfiniteGrp.{u_1}).obj X) = id

@[simp]

theorem ProfiniteAddGrp.coe_id (X : ProfiniteAddGrp.{u_1}) : CategoryTheory.CategoryStruct.id ((CategoryTheory.forget ProfiniteAddGrp.{u_1}).obj X) = id

@[simp]

theorem ProfiniteGrp.coe_comp {X : ProfiniteGrp.{u_1}} {Y : ProfiniteGrp.{u_1}} {Z : ProfiniteGrp.{u_1}} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget ProfiniteGrp.{u_1}).map f) ((CategoryTheory.forget ProfiniteGrp.{u_1}).map g) = ⇑g ∘ ⇑f

@[simp]

theorem ProfiniteAddGrp.coe_comp {X : ProfiniteAddGrp.{u_1}} {Y : ProfiniteAddGrp.{u_1}} {Z : ProfiniteAddGrp.{u_1}} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget ProfiniteAddGrp.{u_1}).map f) ((CategoryTheory.forget ProfiniteAddGrp.{u_1}).map g) = ⇑g ∘ ⇑f

@[reducible, inline]

abbrev ProfiniteGrp.ofProfinite (G : Profinite) [Group ↑G.toTop] [TopologicalGroup ↑G.toTop] : ProfiniteGrp.{u_1}

Construct a term of ProfiniteGrp from a type endowed with the structure of a profinite topological group.

Equations

• ProfiniteGrp.ofProfinite G = ProfiniteGrp.of ↑G.toTop

@[reducible, inline]

abbrev ProfiniteAddGrp.ofProfinite (G : Profinite) [AddGroup ↑G.toTop] [TopologicalAddGroup ↑G.toTop] : ProfiniteAddGrp.{u_1}

Construct a term of ProfiniteAddGrp from a type endowed with the structure of a profinite topological additive group.

Equations

• ProfiniteAddGrp.ofProfinite G = ProfiniteAddGrp.of ↑G.toTop

def ProfiniteGrp.pi {α : Type u} (β : α → ProfiniteGrp.{u_1}) : ProfiniteGrp.{max u u_1}

The pi-type of profinite groups is a profinite group.

Equations

• ProfiniteGrp.pi β = ProfiniteGrp.ofProfinite (Profinite.pi fun (a : α) => (β a).toProfinite)

def ProfiniteAddGrp.pi {α : Type u} (β : α → ProfiniteAddGrp.{u_1}) : ProfiniteAddGrp.{max u u_1}

The pi-type of profinite additive groups is a profinite additive group.

Equations

• ProfiniteAddGrp.pi β = ProfiniteAddGrp.ofProfinite (Profinite.pi fun (a : α) => (β a).toProfinite)

def ProfiniteGrp.ofFiniteGrp (G : FiniteGrp.{u_1}) : ProfiniteGrp.{u_1}

A FiniteGrp when given the discrete topology can be considered as a profinite group.

Equations

• ProfiniteGrp.ofFiniteGrp G = ProfiniteGrp.of ↑G.toGrp

def ProfiniteAddGrp.ofFiniteAddGrp (G : FiniteAddGrp.{u_1}) : ProfiniteAddGrp.{u_1}

A FiniteAddGrp when given the discrete topology can be considered as a profinite additive group.

Equations

• ProfiniteAddGrp.ofFiniteAddGrp G = ProfiniteAddGrp.of ↑G.toAddGrp

instance ProfiniteGrp.instHasForget₂FiniteGrp : CategoryTheory.HasForget₂ FiniteGrp.{u_1} ProfiniteGrp.{u_1}

Equations

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

instance ProfiniteAddGrp.instHasForget₂FiniteAddGrp : CategoryTheory.HasForget₂ FiniteAddGrp.{u_1} ProfiniteAddGrp.{u_1}

Equations

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

instance ProfiniteGrp.instHasForget₂Grp : CategoryTheory.HasForget₂ ProfiniteGrp.{u_1} Grp

Equations

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

instance ProfiniteAddGrp.instHasForget₂AddGrp : CategoryTheory.HasForget₂ ProfiniteAddGrp.{u_1} AddGrp

Equations

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

def ProfiniteGrp.ofClosedSubgroup {G : ProfiniteGrp.{u_1}} (H : ClosedSubgroup ↑G.toProfinite.toTop) : ProfiniteGrp.{u_1}

A closed subgroup of a profinite group is profinite.

Equations

• ProfiniteGrp.ofClosedSubgroup H = ProfiniteGrp.of ↥↑H

def ProfiniteGrp.profiniteGrpToProfinite : CategoryTheory.Functor ProfiniteGrp.{u_1} Profinite

The functor mapping a profinite group to its underlying profinite space.

Equations

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

instance ProfiniteGrp.instFaithfulProfiniteProfiniteGrpToProfinite : ProfiniteGrp.profiniteGrpToProfinite.Faithful

Equations

• ProfiniteGrp.instFaithfulProfiniteProfiniteGrpToProfinite = ⋯

Limits in the category of profinite groups

In this section, we construct limits in the category of profinite groups.

• ProfiniteGrp.limitCone : The explicit limit cone in ProfiniteGrp.

• ProfiniteGrp.limitConeIsLimit: ProfiniteGrp.limitCone is a limit cone.

def ProfiniteGrp.limitConePtAux {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u} ) : Subgroup ((j : J) → ↑(F.obj j).toProfinite.toTop)

Auxiliary construction to obtain the group structure on the limit of profinite groups.

Equations

• ProfiniteGrp.limitConePtAux F = { carrier := {x : (j : J) → ↑(F.obj j).toProfinite.toTop | ∀ ⦃i j : J⦄ (π : i ⟶ j), (F.map π) (x i) = x j}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

instance ProfiniteGrp.instGroupαTopologicalSpaceToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompProfiniteGrpToProfinite {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u} ) : Group ↑(Profinite.limitCone (F.comp ProfiniteGrp.profiniteGrpToProfinite)).pt.toTop

Equations

• ProfiniteGrp.instGroupαTopologicalSpaceToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompProfiniteGrpToProfinite F = inferInstanceAs (Group ↥(ProfiniteGrp.limitConePtAux F))

instance ProfiniteGrp.instTopologicalGroupαTopologicalSpaceToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompProfiniteGrpToProfinite {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u} ) : TopologicalGroup ↑(Profinite.limitCone (F.comp ProfiniteGrp.profiniteGrpToProfinite)).pt.toTop

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev ProfiniteGrp.limitCone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u} ) : CategoryTheory.Limits.Cone F

The explicit limit cone in ProfiniteGrp.

Equations

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

def ProfiniteGrp.limitConeIsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u} ) : CategoryTheory.Limits.IsLimit (ProfiniteGrp.limitCone F)

ProfiniteGrp.limitCone is a limit cone.

Equations

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

instance ProfiniteGrp.instHasLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u} ) : CategoryTheory.Limits.HasLimit F

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev ProfiniteGrp.limit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u} ) : ProfiniteGrp.{max v u}

The abbreviation for the limit of ProfiniteGrps.

Equations

• ProfiniteGrp.limit F = (ProfiniteGrp.limitCone F).pt

instance ProfiniteGrp.instPreservesLimitsProfiniteProfiniteGrpToProfinite : CategoryTheory.Limits.PreservesLimits ProfiniteGrp.profiniteGrpToProfinite

Equations

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