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
: AFiniteGrp
when given the discrete topology can be considered as a profinite group.ofClosedSubgroup
: A closed subgroup of a profinite group is profinite.
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.
Instances For
The above data together form a topological group.
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.
Instances For
The above data together form a topological additive group.
Equations
- ProfiniteAddGrp.instCoeSortType = { coe := fun (G : ProfiniteAddGrp.{?u.1}) => ↑G.toProfinite.toTop }
Equations
- ProfiniteGrp.instCoeSortType = { coe := fun (G : ProfiniteGrp.{?u.1}) => ↑G.toProfinite.toTop }
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
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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.
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
Instances For
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
Instances For
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
Instances For
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
Instances For
The pi-type of profinite additive groups is a profinite additive group.
Equations
- ProfiniteAddGrp.pi β = ProfiniteAddGrp.ofProfinite (Profinite.pi fun (a : α) => (β a).toProfinite)
Instances For
The pi-type of profinite groups is a profinite group.
Equations
- ProfiniteGrp.pi β = ProfiniteGrp.ofProfinite (Profinite.pi fun (a : α) => (β a).toProfinite)
Instances For
A FiniteAddGrp
when given the discrete topology can be considered as a
profinite additive group.
Equations
- ProfiniteAddGrp.ofFiniteAddGrp G = ProfiniteAddGrp.of ↑G.toAddGrp
Instances For
A FiniteGrp
when given the discrete topology can be considered as a profinite group.
Equations
- ProfiniteGrp.ofFiniteGrp G = ProfiniteGrp.of ↑G.toGrp
Instances For
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
Instances For
The functor mapping a profinite group to its underlying profinite space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 inProfiniteGrp
.ProfiniteGrp.limitConeIsLimit
:ProfiniteGrp.limitCone
is a limit cone.
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' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
The explicit limit cone in ProfiniteGrp
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
ProfiniteGrp.limitCone
is a limit cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
The abbreviation for the limit of ProfiniteGrp
s.
Equations
- ProfiniteGrp.limit F = (ProfiniteGrp.limitCone F).pt
Instances For
Equations
- One or more equations did not get rendered due to their size.