Yamaguchi Lean 4 Library
ProCGroups/FreeProC/Abelianization.lean
ProCGroups/FreeProC/Abelianization/Source

ProCGroups/FreeProC/Abelianization.lean

1import Mathlib.Topology.Constructions
2import Mathlib.Topology.Instances.ZMod
3import ProCGroups.Abelian.TopologicalAbelianization
4import ProCGroups.FreeProC.Basic
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/ProCGroups/FreeProC/Abelianization.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Abelianization coordinates of free pro-C groups
17This module records finite cyclic coordinate maps out of the topological abelianization of a
18finite-rank free pro-`Σ` group.
19-/
21open scoped Topology
23namespace ProCGroups.FreeProC
25universe u v
27/-- A finite cyclic coordinate on the topological abelianization of a finite-rank free
28pro-`Σ` group, sending one chosen basis element to the standard generator. -/
30 {sigma : Set ℕ}
31 {F : Type u} [TopologicalSpace F] [Group F] [IsTopologicalGroup F]
32 {r L : ℕ} (hLpos : 0 < L)
34 (X : Fin r → F)
35 (hFree :
39 (i : Fin r) :
40 ∃ χ : TopologicalAbelianization F →ₜ* Multiplicative (ZMod L),
42 Multiplicative.ofAdd (1 : ZMod L) := by
43 classical
44 let C : ProCGroups.FiniteGroupClass.{u} := ProCGroups.FiniteGroupClass.sigmaGroup sigma
45 letI : NeZero L := ⟨Nat.ne_of_gt hLpos⟩
46 let T : Type u := ULift.{u} (Multiplicative (ZMod L))
47 letI : Group T := inferInstance
48 letI : CommGroup T := inferInstance
49 letI : TopologicalSpace T := ⊥
50 letI : DiscreteTopology T := ⟨rfl⟩
51 letI : IsTopologicalGroup T := by infer_instance
52 let φ : Fin r → T :=
53 fun j => if j = i then ULift.up (Multiplicative.ofAdd (1 : ZMod L)) else 1
54 have hφ : FamilyConvergesToOne (G := T) φ :=
55 FamilyConvergesToOne.of_finite_domain φ
56 have htarget :
58 (G := T) := by
59 letI : Finite T := by
60 exact Finite.of_equiv (Multiplicative (ZMod L)) Equiv.ulift.symm
61 exact
63 (C := C) (G := T)
64 (ProCGroups.FiniteGroupClass.sigmaGroup_quotientClosed sigma)
65 (ProCGroups.FiniteGroupClass.sigmaGroup_cyclicZMod (sigma := sigma) hLpos hLsigma)
66 rcases
67 hFree.existsUnique_liftHom_of_convergesToOne_of_finiteGroupClass
68 C
69 (ProCGroups.FiniteGroupClass.sigmaGroup_isomClosed sigma)
70 (ProCGroups.FiniteGroupClass.sigmaGroup_subgroupClosed sigma)
71 (ProCGroups.FiniteGroupClass.sigmaGroup_quotientClosed sigma)
72 htarget φ hφ with
73 ⟨χF, hχF, _⟩
74 letI : TopologicalSpace (Multiplicative (ZMod L)) := ⊥
75 letI : DiscreteTopology (Multiplicative (ZMod L)) := ⟨rfl⟩
76 letI : IsTopologicalGroup (Multiplicative (ZMod L)) := by infer_instance
77 let down : T →ₜ* Multiplicative (ZMod L) :=
78 { toMonoidHom := (MulEquiv.ulift : T ≃* Multiplicative (ZMod L)).toMonoidHom
79 continuous_toFun := continuous_of_discreteTopology }
80 refine ⟨down.comp (ProCGroups.Abelian.TopologicalAbelianization.lift χF), ?_⟩
83 Multiplicative.ofAdd (1 : ZMod L)
85 change (MulEquiv.ulift : T ≃* Multiplicative (ZMod L)) (φ i) =
86 Multiplicative.ofAdd (1 : ZMod L)
87 simp only [↓reduceIte, φ]
88 rfl
90end ProCGroups.FreeProC