Source: ProCGroups.FreeProC.Abelianization
1import Mathlib.Topology.Constructions
2import Mathlib.Topology.Instances.ZMod
3import ProCGroups.Abelian.TopologicalAbelianization
4import ProCGroups.FreeProC.Basic
6/-!
7# Pro C Groups / Free pro-C / Abelianization
9This module identifies the topological abelianization of a free pro-\(C\)
10group through its universal property and finite abelian targets.
11-/
13open scoped Topology
15namespace ProCGroups.FreeProC
17universe u v
19/--
20A finite cyclic coordinate on the topological abelianization of a finite-rank free
21pro-\(\Sigma\) group, sending one chosen basis element to the standard generator.
22-/
23theorem exists_freeAbelianizationCyclicCoordinate
24 {sigma : Set ℕ}
25 {F : Type u} [TopologicalSpace F] [Group F] [IsTopologicalGroup F]
26 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
27 {r L : ℕ} (hLpos : 0 < L)
28 (hLsigma : ProCGroups.FiniteGroupClass.IsSigmaNumber sigma L)
29 (X : Fin r → F)
30 (hFree :
31 IsEpimorphicallyFreeProCGroupOnConvergingSet
32 (C := (ProCGroups.FiniteGroupClass.sigmaGroup sigma)) (Fin r) F X)
33 (i : Fin r) :
34 ∃ χ : TopologicalAbelianization F →ₜ* Multiplicative (ZMod L),
35 χ (ProCGroups.Abelian.TopologicalAbelianization.mk F (X i)) =
36 Multiplicative.ofAdd (1 : ZMod L) := by
37 classical
38 let C : ProCGroups.FiniteGroupClass.{u} := ProCGroups.FiniteGroupClass.sigmaGroup sigma
39 letI : NeZero L := ⟨Nat.ne_of_gt hLpos⟩
40 let T : Type u := ULift.{u} (Multiplicative (ZMod L))
41 letI : Group T := inferInstance
42 letI : CommGroup T := inferInstance
43 letI : TopologicalSpace T := ⊥
44 letI : DiscreteTopology T := ⟨rfl⟩
45 letI : IsTopologicalGroup T := by infer_instance
46 letI : Finite T := by
47 exact Finite.of_equiv (Multiplicative (ZMod L)) Equiv.ulift.symm
48 let φ : Fin r → T :=
49 fun j => if j = i then ULift.up (Multiplicative.ofAdd (1 : ZMod L)) else 1
50 have hφ : FamilyConvergesToOneAlongOpenSubgroups (G := T) φ :=
51 FamilyConvergesToOneAlongOpenSubgroups.of_finite_domain φ
52 have htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C T := by
53 exact
55 (C := C) (G := T)
57 (ProCGroups.FiniteGroupClass.sigmaGroup_cyclicZMod (sigma := sigma) hLpos hLsigma)
58 rcases
59 hFree.existsUnique_liftHom_of_convergesToOneAlongOpenSubgroups_of_finiteGroupClass
60 C
63 htarget φ hφ with
64 ⟨χF, hχF, _⟩
65 letI : TopologicalSpace (Multiplicative (ZMod L)) := ⊥
66 letI : DiscreteTopology (Multiplicative (ZMod L)) := ⟨rfl⟩
67 letI : IsTopologicalGroup (Multiplicative (ZMod L)) := by infer_instance
68 let down : T →ₜ* Multiplicative (ZMod L) :=
69 { toMonoidHom := (MulEquiv.ulift : T ≃* Multiplicative (ZMod L)).toMonoidHom
70 continuous_toFun := continuous_of_discreteTopology }
71 refine ⟨down.comp (ProCGroups.Abelian.TopologicalAbelianization.lift χF), ?_⟩
72 change down (ProCGroups.Abelian.TopologicalAbelianization.lift χF
73 (ProCGroups.Abelian.TopologicalAbelianization.mk F (X i))) =
74 Multiplicative.ofAdd (1 : ZMod L)
76 change (MulEquiv.ulift : T ≃* Multiplicative (ZMod L)) (φ i) =
77 Multiplicative.ofAdd (1 : ZMod L)
78 simp only [↓reduceIte, φ]
79 rfl
81end ProCGroups.FreeProC