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)

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)

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.

@[implicit_reducible]

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

@[implicit_reducible]

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

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

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

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' : ↑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

theorem ProfiniteAddGrp.Hom.ext_iff {A B : ProfiniteAddGrp.{u}} {x y : A.Hom B} : x = y ↔ x.hom' = y.hom'

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

The type of morphisms in ProfiniteGrp.

• hom' : ↑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

theorem ProfiniteGrp.Hom.ext_iff {A B : ProfiniteGrp.{u}} {x y : A.Hom B} : x = y ↔ x.hom' = y.hom'

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[reducible, inline]

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

The underlying ContinuousMonoidHom.

@[reducible, inline]

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

The underlying ContinuousAddMonoidHom.

@[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 : X →ₜ* Y) : of X ⟶ of Y

Typecheck a ContinuousMonoidHom as a morphism in ProfiniteGrp.

@[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 : X →ₜ+ Y) : of X ⟶ of Y

Typecheck a ContinuousAddMonoidHom as a morphism in ProfiniteAddGrp.

@[implicit_reducible]

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

@[implicit_reducible]

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

@[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 ProfiniteGrp.hom_ext {A B : ProfiniteGrp.{u}} {f g : A ⟶ B} (hf : Hom.hom f = Hom.hom g) : f = g

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_iff {A B : ProfiniteGrp.{u}} {f g : A ⟶ B} : f = g ↔ Hom.hom f = Hom.hom g

theorem ProfiniteAddGrp.hom_ext_iff {A B : ProfiniteAddGrp.{u}} {f g : A ⟶ B} : f = g ↔ Hom.hom f = Hom.hom 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 : 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 : 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 : X →ₜ* Y) (g : 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 : X →ₜ+ Y) (g : 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 : 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 : 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.

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

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

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

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.

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

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

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.

def ProfiniteGrp.ofFiniteGrpHom {G H : FiniteGrp.{u}} (f : G ⟶ H) : ofFiniteGrp G ⟶ ofFiniteGrp H

A morphism of FiniteGrp induces a morphism of the associated profinite groups.

def ProfiniteAddGrp.ofFiniteAddGrpHom {G H : FiniteAddGrp.{u}} (f : G ⟶ H) : ofFiniteAddGrp G ⟶ ofFiniteAddGrp H

A morphism of FiniteAddGrp induces a morphism of the associated profinite additive groups.

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance ProfiniteGrp.instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteGrpCatMonoidHomCarrier : CategoryTheory.HasForget₂ ProfiniteGrp.{u_1} GrpCat

@[implicit_reducible]

instance ProfiniteAddGrp.instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteAddGrpCatAddMonoidHomCarrier : CategoryTheory.HasForget₂ ProfiniteAddGrp.{u_1} AddGrpCat

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

A closed subgroup of a profinite group is profinite.

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.

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.

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.

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.

@[implicit_reducible]

instance ProfiniteGrp.instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap : CategoryTheory.HasForget₂ ProfiniteGrp.{u_1} Profinite

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

@[implicit_reducible]

instance ProfiniteAddGrp.instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap : CategoryTheory.HasForget₂ ProfiniteAddGrp.{u_1} Profinite

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

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

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

instance ProfiniteGrp.instReflectsIsomorphismsForgetContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite : (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.

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.

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.

@[implicit_reducible]

instance ProfiniteGrp.instGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap {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

@[implicit_reducible]

instance ProfiniteAddGrp.instAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteAddGrp.{max v u}) : AddGroup ↑(Profinite.limitCone (F.comp (CategoryTheory.forget₂ ProfiniteAddGrp.{max u v} Profinite))).pt.toTop

instance ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap {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

instance ProfiniteAddGrp.instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteAddGrp.{max v u}) : IsTopologicalAddGroup ↑(Profinite.limitCone (F.comp (CategoryTheory.forget₂ ProfiniteAddGrp.{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.

@[reducible, inline]

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

The explicit limit cone in ProfiniteAddGrp.

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.

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

ProfiniteAddGrp.limitCone is a limit cone.

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

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

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

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

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

instance ProfiniteAddGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemAddSubgroupLimitConePtAux {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteAddGrp.{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.

@[reducible, inline]

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

The abbreviation for the limit of ProfiniteAddGrps.

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

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

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

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

@[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 ProfiniteAddGrp.limit_zero_val {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteAddGrp.{max v u}) (j : J) : ↑0 j = 0

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

@[simp]

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