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 : IsTopologicalGroup ↑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 : IsTopologicalAddGroup ↑self.toProfinite.toTop

  The above data together form a topological additive group.

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

Equations

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

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

Equations

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

@[reducible, inline]

abbrev ProfiniteGrp.of (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup 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)

@[reducible, inline]

abbrev ProfiniteAddGrp.of (G : Type u) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup 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 ProfiniteGrp.coe_of (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : ↑(of G).toProfinite.toTop = G

theorem ProfiniteAddGrp.coe_of (G : Type u) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : ↑(of G).toProfinite.toTop = G

structure ProfiniteAddGrp.Hom (A B : ProfiniteAddGrp.{u}) : Type u

The type of morphisms in ProfiniteAddGrp.

• hom' : ContinuousAddMonoidHom ↑A.toProfinite.toTop ↑B.toProfinite.toTop

  The underlying ContinuousAddMonoidHom.

theorem ProfiniteAddGrp.Hom.ext {A B : ProfiniteAddGrp.{u}} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y

structure ProfiniteGrp.Hom (A B : ProfiniteGrp.{u}) : Type u

The type of morphisms in ProfiniteGrp.

• hom' : ContinuousMonoidHom ↑A.toProfinite.toTop ↑B.toProfinite.toTop

  The underlying ContinuousMonoidHom.

theorem ProfiniteGrp.Hom.ext {A B : ProfiniteGrp.{u}} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y

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

Equations

• instCategoryProfiniteGrp = CategoryTheory.Category.mk @instCategoryProfiniteGrp.proof_1 @instCategoryProfiniteGrp.proof_2 @instCategoryProfiniteGrp.proof_3

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

Equations

• instCategoryProfiniteAddGrp = CategoryTheory.Category.mk @instCategoryProfiniteAddGrp.proof_1 @instCategoryProfiniteAddGrp.proof_2 @instCategoryProfiniteAddGrp.proof_3

instance instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite : CategoryTheory.ConcreteCategory ProfiniteGrp.{u_1} fun (X Y : ProfiniteGrp.{u_1}) => ContinuousMonoidHom ↑X.toProfinite.toTop ↑Y.toProfinite.toTop

Equations

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

instance instConcreteCategoryProfiniteAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite : CategoryTheory.ConcreteCategory ProfiniteAddGrp.{u_1} fun (X Y : ProfiniteAddGrp.{u_1}) => ContinuousAddMonoidHom ↑X.toProfinite.toTop ↑Y.toProfinite.toTop

Equations

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

@[reducible, inline]

abbrev ProfiniteGrp.Hom.hom {M N : ProfiniteGrp.{u}} (f : M.Hom N) : ContinuousMonoidHom ↑M.toProfinite.toTop ↑N.toProfinite.toTop

The underlying ContinuousMonoidHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev ProfiniteAddGrp.Hom.hom {M N : ProfiniteAddGrp.{u}} (f : M.Hom N) : ContinuousAddMonoidHom ↑M.toProfinite.toTop ↑N.toProfinite.toTop

The underlying ContinuousAddMonoidHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev ProfiniteGrp.ofHom {X Y : Type u} [Group X] [TopologicalSpace X] [IsTopologicalGroup X] [CompactSpace X] [TotallyDisconnectedSpace X] [Group Y] [TopologicalSpace Y] [IsTopologicalGroup Y] [CompactSpace Y] [TotallyDisconnectedSpace Y] (f : ContinuousMonoidHom X Y) : of X ⟶ of Y

Typecheck a ContinuousMonoidHom as a morphism in ProfiniteGrp.

Equations

• ProfiniteGrp.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

@[reducible, inline]

abbrev ProfiniteAddGrp.ofHom {X Y : Type u} [AddGroup X] [TopologicalSpace X] [IsTopologicalAddGroup X] [CompactSpace X] [TotallyDisconnectedSpace X] [AddGroup Y] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [CompactSpace Y] [TotallyDisconnectedSpace Y] (f : ContinuousAddMonoidHom X Y) : of X ⟶ of Y

Typecheck a ContinuousAddMonoidHom as a morphism in ProfiniteAddGrp.

Equations

• ProfiniteAddGrp.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

instance ProfiniteGrp.instCoeFunHomForallCarrierToTopTotallyDisconnectedSpaceToProfinite {M N : ProfiniteGrp.{u}} : CoeFun (M ⟶ N) fun (x : M ⟶ N) => ↑M.toProfinite.toTop → ↑N.toProfinite.toTop

Equations

• ProfiniteGrp.instCoeFunHomForallCarrierToTopTotallyDisconnectedSpaceToProfinite = { coe := fun (f : M ⟶ N) => ⇑(ProfiniteGrp.Hom.hom f) }

instance ProfiniteAddGrp.instCoeFunHomForallCarrierToTopTotallyDisconnectedSpaceToProfinite {M N : ProfiniteAddGrp.{u}} : CoeFun (M ⟶ N) fun (x : M ⟶ N) => ↑M.toProfinite.toTop → ↑N.toProfinite.toTop

Equations

• ProfiniteAddGrp.instCoeFunHomForallCarrierToTopTotallyDisconnectedSpaceToProfinite = { coe := fun (f : M ⟶ N) => ⇑(ProfiniteAddGrp.Hom.hom f) }

@[simp]

theorem ProfiniteGrp.hom_id {A : ProfiniteGrp.{u}} : Hom.hom (CategoryTheory.CategoryStruct.id A) = ContinuousMonoidHom.id ↑A.toProfinite.toTop

@[simp]

theorem ProfiniteAddGrp.hom_id {A : ProfiniteAddGrp.{u}} : Hom.hom (CategoryTheory.CategoryStruct.id A) = ContinuousAddMonoidHom.id ↑A.toProfinite.toTop

theorem ProfiniteGrp.id_apply (A : ProfiniteGrp.{u}) (a : ↑A.toProfinite.toTop) : (Hom.hom (CategoryTheory.CategoryStruct.id A)) a = a

theorem ProfiniteAddGrp.id_apply (A : ProfiniteAddGrp.{u}) (a : ↑A.toProfinite.toTop) : (Hom.hom (CategoryTheory.CategoryStruct.id A)) a = a

@[simp]

theorem ProfiniteGrp.hom_comp {A B C : ProfiniteGrp.{u}} (f : A ⟶ B) (g : B ⟶ C) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

@[simp]

theorem ProfiniteAddGrp.hom_comp {A B C : ProfiniteAddGrp.{u}} (f : A ⟶ B) (g : B ⟶ C) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

theorem ProfiniteGrp.comp_apply {A B C : ProfiniteGrp.{u}} (f : A ⟶ B) (g : B ⟶ C) (a : ↑A.toProfinite.toTop) : (Hom.hom (CategoryTheory.CategoryStruct.comp f g)) a = (Hom.hom g) ((Hom.hom f) a)

theorem ProfiniteAddGrp.comp_apply {A B C : ProfiniteAddGrp.{u}} (f : A ⟶ B) (g : B ⟶ C) (a : ↑A.toProfinite.toTop) : (Hom.hom (CategoryTheory.CategoryStruct.comp f g)) a = (Hom.hom g) ((Hom.hom f) a)

theorem ProfiniteAddGrp.hom_ext {A B : ProfiniteAddGrp.{u}} {f g : A ⟶ B} (hf : Hom.hom f = Hom.hom g) : f = g

theorem ProfiniteGrp.hom_ext {A B : ProfiniteGrp.{u}} {f g : A ⟶ B} (hf : Hom.hom f = Hom.hom g) : f = g

@[simp]

theorem ProfiniteGrp.hom_ofHom {X Y : Type u} [Group X] [TopologicalSpace X] [IsTopologicalGroup X] [CompactSpace X] [TotallyDisconnectedSpace X] [Group Y] [TopologicalSpace Y] [IsTopologicalGroup Y] [CompactSpace Y] [TotallyDisconnectedSpace Y] (f : ContinuousMonoidHom X Y) : Hom.hom (ofHom f) = f

@[simp]

theorem ProfiniteAddGrp.hom_ofHom {X Y : Type u} [AddGroup X] [TopologicalSpace X] [IsTopologicalAddGroup X] [CompactSpace X] [TotallyDisconnectedSpace X] [AddGroup Y] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [CompactSpace Y] [TotallyDisconnectedSpace Y] (f : ContinuousAddMonoidHom X Y) : Hom.hom (ofHom f) = f

@[simp]

theorem ProfiniteGrp.ofHom_hom {A B : ProfiniteGrp.{u}} (f : A ⟶ B) : ofHom (Hom.hom f) = f

@[simp]

theorem ProfiniteAddGrp.ofHom_hom {A B : ProfiniteAddGrp.{u}} (f : A ⟶ B) : ofHom (Hom.hom f) = f

@[simp]

theorem ProfiniteGrp.ofHom_id {X : Type u} [Group X] [TopologicalSpace X] [IsTopologicalGroup X] [CompactSpace X] [TotallyDisconnectedSpace X] : ofHom (ContinuousMonoidHom.id X) = CategoryTheory.CategoryStruct.id (of X)

@[simp]

theorem ProfiniteAddGrp.ofHom_id {X : Type u} [AddGroup X] [TopologicalSpace X] [IsTopologicalAddGroup X] [CompactSpace X] [TotallyDisconnectedSpace X] : ofHom (ContinuousAddMonoidHom.id X) = CategoryTheory.CategoryStruct.id (of X)

@[simp]

theorem ProfiniteGrp.ofHom_comp {X Y Z : Type u} [Group X] [TopologicalSpace X] [IsTopologicalGroup X] [CompactSpace X] [TotallyDisconnectedSpace X] [Group Y] [TopologicalSpace Y] [IsTopologicalGroup Y] [CompactSpace Y] [TotallyDisconnectedSpace Y] [Group Z] [TopologicalSpace Z] [IsTopologicalGroup Z] [CompactSpace Z] [TotallyDisconnectedSpace Z] (f : ContinuousMonoidHom X Y) (g : ContinuousMonoidHom Y Z) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

@[simp]

theorem ProfiniteAddGrp.ofHom_comp {X Y Z : Type u} [AddGroup X] [TopologicalSpace X] [IsTopologicalAddGroup X] [CompactSpace X] [TotallyDisconnectedSpace X] [AddGroup Y] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [CompactSpace Y] [TotallyDisconnectedSpace Y] [AddGroup Z] [TopologicalSpace Z] [IsTopologicalAddGroup Z] [CompactSpace Z] [TotallyDisconnectedSpace Z] (f : ContinuousAddMonoidHom X Y) (g : ContinuousAddMonoidHom Y Z) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem ProfiniteGrp.ofHom_apply {X Y : Type u} [Group X] [TopologicalSpace X] [IsTopologicalGroup X] [CompactSpace X] [TotallyDisconnectedSpace X] [Group Y] [TopologicalSpace Y] [IsTopologicalGroup Y] [CompactSpace Y] [TotallyDisconnectedSpace Y] (f : ContinuousMonoidHom X Y) (x : X) : (Hom.hom (ofHom f)) x = f x

theorem ProfiniteAddGrp.ofHom_apply {X Y : Type u} [AddGroup X] [TopologicalSpace X] [IsTopologicalAddGroup X] [CompactSpace X] [TotallyDisconnectedSpace X] [AddGroup Y] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [CompactSpace Y] [TotallyDisconnectedSpace Y] (f : ContinuousAddMonoidHom X Y) (x : X) : (Hom.hom (ofHom f)) x = f x

theorem ProfiniteGrp.inv_hom_apply {A B : ProfiniteGrp.{u}} (e : A ≅ B) (x : ↑A.toProfinite.toTop) : (Hom.hom e.inv) ((Hom.hom e.hom) x) = x

theorem ProfiniteAddGrp.neg_hom_apply {A B : ProfiniteAddGrp.{u}} (e : A ≅ B) (x : ↑A.toProfinite.toTop) : (Hom.hom e.inv) ((Hom.hom e.hom) x) = x

theorem ProfiniteGrp.hom_inv_apply {A B : ProfiniteGrp.{u}} (e : A ≅ B) (x : ↑B.toProfinite.toTop) : (Hom.hom e.hom) ((Hom.hom e.inv) x) = x

theorem ProfiniteAddGrp.hom_neg_apply {A B : ProfiniteAddGrp.{u}} (e : A ≅ B) (x : ↑B.toProfinite.toTop) : (Hom.hom e.hom) ((Hom.hom e.inv) x) = x

@[simp]

theorem ProfiniteGrp.coe_id (X : ProfiniteGrp.{u_1}) : ⇑(Hom.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

theorem ProfiniteAddGrp.coe_id (X : ProfiniteAddGrp.{u_1}) : ⇑(Hom.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

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

@[simp]

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

@[reducible, inline]

abbrev ProfiniteGrp.ofProfinite (G : Profinite) [Group ↑G.toTop] [IsTopologicalGroup ↑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] [IsTopologicalAddGroup ↑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 ProfiniteAddGrp.ofClosedAddSubgroup {G : ProfiniteAddGrp.{u_1}} (H : ClosedAddSubgroup ↑G.toProfinite.toTop) : ProfiniteAddGrp.{u_1}

A closed additive subgroup of a profinite additive group is profinite.

Equations

• ProfiniteAddGrp.ofClosedAddSubgroup H = ProfiniteAddGrp.of ↥↑H

def ProfiniteGrp.ofContinuousMulEquiv {G : ProfiniteGrp.{u}} {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H] (e : ↑G.toProfinite.toTop ≃ₜ* H) : ProfiniteGrp.{v}

A topological group that has a ContinuousMulEquiv to a profinite group is profinite.

Equations

• ProfiniteGrp.ofContinuousMulEquiv e = ProfiniteGrp.of H

def ProfiniteAddGrp.ofContinuousAddEquiv {G : ProfiniteAddGrp.{u}} {H : Type v} [TopologicalSpace H] [AddGroup H] [IsTopologicalAddGroup H] (e : ↑G.toProfinite.toTop ≃ₜ+ H) : ProfiniteAddGrp.{v}

A topological additive group that has a ContinuousAddEquiv to a profinite additive group is profinite.

Equations

• ProfiniteAddGrp.ofContinuousAddEquiv e = ProfiniteAddGrp.of H

def ProfiniteGrp.ContinuousMulEquiv.toProfiniteGrpIso {X Y : ProfiniteGrp.{u_1}} (e : ↑X.toProfinite.toTop ≃ₜ* ↑Y.toProfinite.toTop) : X ≅ Y

Build an isomorphism in the category ProfiniteGrp from a ContinuousMulEquiv between ProfiniteGrps.

Equations

• ProfiniteGrp.ContinuousMulEquiv.toProfiniteGrpIso e = { hom := ProfiniteGrp.ofHom ↑e, inv := ProfiniteGrp.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

instance ProfiniteGrp.instHasForget₂Profinite : CategoryTheory.HasForget₂ 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 ProfiniteAddGrp.instHasForget₂Profinite : CategoryTheory.HasForget₂ ProfiniteAddGrp.{u_1} Profinite

Equations

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

instance ProfiniteGrp.instFaithfulProfiniteForget₂ : (CategoryTheory.forget₂ ProfiniteGrp.{u_1} Profinite).Faithful

instance ProfiniteAddGrp.instFaithfulProfiniteForget₂ : (CategoryTheory.forget₂ ProfiniteAddGrp.{u_1} Profinite).Faithful

instance ProfiniteGrp.instReflectsIsomorphismsProfiniteForget₂ : (CategoryTheory.forget₂ ProfiniteGrp.{u_1} Profinite).ReflectsIsomorphisms

instance ProfiniteGrp.instReflectsIsomorphismsForget : (CategoryTheory.forget ProfiniteGrp.{u}).ReflectsIsomorphisms

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.

TODO

• Figure out the reason that is causing to_additive to fail in most part of this section and generate the additive version correctly.

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

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

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

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

Equations

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

instance ProfiniteGrp.instGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u}) : Group ↑(Profinite.limitCone (F.comp (CategoryTheory.forget₂ ProfiniteGrp.{max u v} Profinite))).pt.toTop

Equations

• ProfiniteGrp.instGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ F = inferInstanceAs (Group ↥(ProfiniteGrp.limitConePtAux F))

instance ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u}) : IsTopologicalGroup ↑(Profinite.limitCone (F.comp (CategoryTheory.forget₂ ProfiniteGrp.{max u v} Profinite))).pt.toTop

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

instance ProfiniteGrp.instPreservesLimitsProfiniteForget₂ : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ ProfiniteGrp.{u_1} Profinite)

instance ProfiniteGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemSubgroupLimitConePtAux {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u}) : CompactSpace ↥(limitConePtAux F)

@[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.of ↥(ProfiniteGrp.limitConePtAux F)

theorem ProfiniteGrp.limit_ext {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u}) (x y : ↑(limit F).toProfinite.toTop) (hxy : ∀ (j : J), ↑x j = ↑y j) : x = y

@[simp]

theorem ProfiniteGrp.limit_one_val {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u}) (j : J) : ↑1 j = 1

@[simp]

theorem ProfiniteGrp.limit_mul_val {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u}) (x y : ↑(limit F).toProfinite.toTop) (j : J) : ↑(x * y) j = ↑x j * ↑y j