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.

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 ProfiniteAddGrp.instCoeSortType : CoeSort ProfiniteAddGrp.{u} (Type u)

Equations

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

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

Equations

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

theorem ProfiniteAddGrp.instCategory.proof_1 {X : ProfiniteAddGrp.{u_1}} {Y : ProfiniteAddGrp.{u_1}} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f = f

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

theorem ProfiniteAddGrp.instCategory.proof_3 {W : ProfiniteAddGrp.{u_1}} {X : ProfiniteAddGrp.{u_1}} {Y : ProfiniteAddGrp.{u_1}} {Z : ProfiniteAddGrp.{u_1}} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)

theorem ProfiniteAddGrp.instCategory.proof_2 {X : ProfiniteAddGrp.{u_1}} {Y : ProfiniteAddGrp.{u_1}} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = f

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.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.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.instAddMonoidHomClassHomαTopologicalSpaceToTopTotallyDisconnectedSpaceToProfinite (G : ProfiniteAddGrp.{u_1}) (H : ProfiniteAddGrp.{u_1}) : AddMonoidHomClass (G ⟶ H) ↑G.toProfinite.toTop ↑H.toProfinite.toTop

Equations

• ⋯ = ⋯

instance ProfiniteGrp.instMonoidHomClassHomαTopologicalSpaceToTopTotallyDisconnectedSpaceToProfinite (G : ProfiniteGrp.{u_1}) (H : ProfiniteGrp.{u_1}) : MonoidHomClass (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.instContinuousMapClassHomαTopologicalSpaceToTopTotallyDisconnectedSpaceToProfinite (G : ProfiniteGrp.{u_1}) (H : ProfiniteGrp.{u_1}) : ContinuousMapClass (G ⟶ H) ↑G.toProfinite.toTop ↑H.toProfinite.toTop

Equations

• ⋯ = ⋯

theorem ProfiniteAddGrp.instConcreteCategory.proof_3 : { obj := fun (G : ProfiniteAddGrp.{u_1}) => ↑G.toProfinite.toTop, map := fun {X Y : ProfiniteAddGrp.{u_1}} (f : X ⟶ Y) => ⇑f, map_id := ⋯, map_comp := ⋯ }.Faithful

theorem ProfiniteAddGrp.instConcreteCategory.proof_1 (X : ProfiniteAddGrp.{u_1}) : { obj := fun (G : ProfiniteAddGrp.{u_1}) => ↑G.toProfinite.toTop, map := fun {X Y : ProfiniteAddGrp.{u_1}} (f : X ⟶ Y) => ⇑f }.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id ({ obj := fun (G : ProfiniteAddGrp.{u_1}) => ↑G.toProfinite.toTop, map := fun {X Y : ProfiniteAddGrp.{u_1}} (f : X ⟶ Y) => ⇑f }.obj X)

theorem ProfiniteAddGrp.instConcreteCategory.proof_2 {X : ProfiniteAddGrp.{u_1}} {Y : ProfiniteAddGrp.{u_1}} {Z : ProfiniteAddGrp.{u_1}} (f : X ⟶ Y) (g : Y ⟶ Z) : { obj := fun (G : ProfiniteAddGrp.{u_1}) => ↑G.toProfinite.toTop, map := fun {X Y : ProfiniteAddGrp.{u_1}} (f : X ⟶ Y) => ⇑f }.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ({ obj := fun (G : ProfiniteAddGrp.{u_1}) => ↑G.toProfinite.toTop, map := fun {X Y : ProfiniteAddGrp.{u_1}} (f : X ⟶ Y) => ⇑f }.map f) ({ obj := fun (G : ProfiniteAddGrp.{u_1}) => ↑G.toProfinite.toTop, map := fun {X Y : ProfiniteAddGrp.{u_1}} (f : X ⟶ Y) => ⇑f }.map g)

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

Equations

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

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

Equations

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

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)

theorem ProfiniteAddGrp.of.proof_1 (G : Type u_1) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [TotallyDisconnectedSpace G] : T2Space G

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)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

theorem ProfiniteAddGrp.ofProfinite.proof_1 (G : Profinite) : CompactSpace ↑G.toTop

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

theorem ProfiniteAddGrp.pi.proof_1 {α : Type u_2} (β : α → ProfiniteAddGrp.{u_1}) : TopologicalAddGroup ((b : α) → ↑((fun (a : α) => (β a).toProfinite) b).toTop)

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

theorem ProfiniteAddGrp.ofFiniteAddGrp.proof_3 (G : FiniteAddGrp.{u_1}) : TotallyDisconnectedSpace ↑G.toAddGrp

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

theorem ProfiniteAddGrp.ofFiniteAddGrp.proof_1 (G : FiniteAddGrp.{u_1}) : TopologicalAddGroup ↑G.toAddGrp

theorem ProfiniteAddGrp.ofFiniteAddGrp.proof_2 (G : FiniteAddGrp.{u_1}) : CompactSpace ↑G.toAddGrp

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

theorem ProfiniteAddGrp.instHasForget₂FiniteAddGrp.proof_3 {X : FiniteAddGrp.{u_1}} {Y : FiniteAddGrp.{u_1}} {Z : FiniteAddGrp.{u_1}} (f : X ⟶ Y) (g : Y ⟶ Z) : { obj := ProfiniteAddGrp.ofFiniteAddGrp, map := fun {X Y : FiniteAddGrp.{u_1}} (f : X ⟶ Y) => { toAddMonoidHom := f, continuous_toFun := ⋯ } }.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ({ obj := ProfiniteAddGrp.ofFiniteAddGrp, map := fun {X Y : FiniteAddGrp.{u_1}} (f : X ⟶ Y) => { toAddMonoidHom := f, continuous_toFun := ⋯ } }.map f) ({ obj := ProfiniteAddGrp.ofFiniteAddGrp, map := fun {X Y : FiniteAddGrp.{u_1}} (f : X ⟶ Y) => { toAddMonoidHom := f, continuous_toFun := ⋯ } }.map g)

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.

theorem ProfiniteAddGrp.instHasForget₂FiniteAddGrp.proof_1 : ∀ {X Y : FiniteAddGrp.{u_1}} (f : X ⟶ Y), Continuous (↑f).toFun

theorem ProfiniteAddGrp.instHasForget₂FiniteAddGrp.proof_4 : { obj := ProfiniteAddGrp.ofFiniteAddGrp, map := fun {X Y : FiniteAddGrp.{u_1}} (f : X ⟶ Y) => { toAddMonoidHom := f, continuous_toFun := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp (CategoryTheory.forget ProfiniteAddGrp.{u_1}) = { obj := ProfiniteAddGrp.ofFiniteAddGrp, map := fun {X Y : FiniteAddGrp.{u_1}} (f : X ⟶ Y) => { toAddMonoidHom := f, continuous_toFun := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp (CategoryTheory.forget ProfiniteAddGrp.{u_1})

theorem ProfiniteAddGrp.instHasForget₂FiniteAddGrp.proof_2 (X : FiniteAddGrp.{u_1}) : { obj := ProfiniteAddGrp.ofFiniteAddGrp, map := fun {X Y : FiniteAddGrp.{u_1}} (f : X ⟶ Y) => { toAddMonoidHom := f, continuous_toFun := ⋯ } }.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id ({ obj := ProfiniteAddGrp.ofFiniteAddGrp, map := fun {X Y : FiniteAddGrp.{u_1}} (f : X ⟶ Y) => { toAddMonoidHom := f, continuous_toFun := ⋯ } }.obj X)

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.

theorem ProfiniteAddGrp.instHasForget₂AddGrp.proof_3 : { obj := fun (P : ProfiniteAddGrp.{u_1}) => { α := ↑P.toProfinite.toTop, str := P.addGroup }, map := fun {X Y : ProfiniteAddGrp.{u_1}} (f : X ⟶ Y) => f.toAddMonoidHom, map_id := ⋯, map_comp := ⋯ }.comp (CategoryTheory.forget AddGrp) = { obj := fun (P : ProfiniteAddGrp.{u_1}) => { α := ↑P.toProfinite.toTop, str := P.addGroup }, map := fun {X Y : ProfiniteAddGrp.{u_1}} (f : X ⟶ Y) => f.toAddMonoidHom, map_id := ⋯, map_comp := ⋯ }.comp (CategoryTheory.forget AddGrp)

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

Equations

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

theorem ProfiniteAddGrp.instHasForget₂AddGrp.proof_2 {X : ProfiniteAddGrp.{u_1}} {Y : ProfiniteAddGrp.{u_1}} {Z : ProfiniteAddGrp.{u_1}} (f : X ⟶ Y) (g : Y ⟶ Z) : { obj := fun (P : ProfiniteAddGrp.{u_1}) => { α := ↑P.toProfinite.toTop, str := P.addGroup }, map := fun {X Y : ProfiniteAddGrp.{u_1}} (f : X ⟶ Y) => f.toAddMonoidHom }.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ({ obj := fun (P : ProfiniteAddGrp.{u_1}) => { α := ↑P.toProfinite.toTop, str := P.addGroup }, map := fun {X Y : ProfiniteAddGrp.{u_1}} (f : X ⟶ Y) => f.toAddMonoidHom }.map f) ({ obj := fun (P : ProfiniteAddGrp.{u_1}) => { α := ↑P.toProfinite.toTop, str := P.addGroup }, map := fun {X Y : ProfiniteAddGrp.{u_1}} (f : X ⟶ Y) => f.toAddMonoidHom }.map g)

theorem ProfiniteAddGrp.instHasForget₂AddGrp.proof_1 (X : ProfiniteAddGrp.{u_1}) : { obj := fun (P : ProfiniteAddGrp.{u_1}) => { α := ↑P.toProfinite.toTop, str := P.addGroup }, map := fun {X Y : ProfiniteAddGrp.{u_1}} (f : X ⟶ Y) => f.toAddMonoidHom }.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id ({ obj := fun (P : ProfiniteAddGrp.{u_1}) => { α := ↑P.toProfinite.toTop, str := P.addGroup }, map := fun {X Y : ProfiniteAddGrp.{u_1}} (f : X ⟶ Y) => f.toAddMonoidHom }.obj X)

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

Equations

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