ProCGroups.FreeProC.exists_freeAbelianizationCyclicCoordinate
A finite cyclic coordinate on the topological abelianization of a finite-rank free pro-\(\Sigma\) group, sending one chosen basis element to the standard generator.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace ProCGroups.FreeProC
universe u vLean source · statement
theorem exists_freeAbelianizationCyclicCoordinate
{sigma : Set ℕ}
{F : Type u} [TopologicalSpace F] [Group F] [IsTopologicalGroup F]
[CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
{r L : ℕ} (hLpos : 0 < L)
(hLsigma : ProCGroups.FiniteGroupClass.IsSigmaNumber sigma L)
(X : Fin r → F)
(hFree :
IsEpimorphicallyFreeProCGroupOnConvergingSet
(C := (ProCGroups.FiniteGroupClass.sigmaGroup sigma)) (Fin r) F X)
(i : Fin r) :
∃ χ : TopologicalAbelianization F →ₜ* Multiplicative (ZMod L),
χ (ProCGroups.Abelian.TopologicalAbelianization.mk F (X i)) =
Multiplicative.ofAdd (1 : ZMod L)