Documentation

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

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 #

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.

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.

@[reducible, inline]

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
@[reducible, inline]

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
theorem ProfiniteAddGrp.Hom.ext {A B : ProfiniteAddGrp.{u}} {x y : A.Hom B} (hom' : x.hom' = y.hom') :
x = y

The type of morphisms in ProfiniteGrp.

theorem ProfiniteGrp.Hom.ext {A B : ProfiniteGrp.{u}} {x y : A.Hom B} (hom' : x.hom' = y.hom') :
x = y
theorem ProfiniteGrp.hom_ext {A B : ProfiniteGrp.{u}} {f g : A B} (hf : Hom.hom f = Hom.hom g) :
f = g
@[simp]
@[simp]
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
@[simp]
@[simp]
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
@[simp]
@[reducible, inline]

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

Equations
@[reducible, inline]

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

Equations

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

Equations

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

Equations

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

Equations

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

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

A closed subgroup of a profinite group is profinite.

Equations

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

Equations

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

Equations

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

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

Limits in the category of profinite groups #

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

TODO #

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.

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.
@[reducible, inline]

The explicit limit cone in ProfiniteGrp.

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

ProfiniteGrp.limitCone is a limit cone.

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