ProCGroups/FiniteStepSolvableQuotients/Commutators/Width.lean
1import Mathlib.GroupTheory.Rank
2import ProCGroups.FiniteGeneration.CharacteristicChainsAndIndices
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/FiniteStepSolvableQuotients/Commutators/Width.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
15This file contains only formalized definitions and reductions:
17criteria for commutator subgroups of profinite groups.
19It does not assume Segal/Nikolov-Segal commutator-width theorems.
21Main API groups:
231. Algebraic bounded commutator products.
242. Uniform finite-quotient commutator-width hypotheses.
253. Profinite closure consequences.
27-/
29open scoped Topology Pointwise
31namespace ProCGroups.FiniteStepSolvableQuotients
33open ProCGroups.FiniteGeneration
35universe u
37/-- A product of commutators whose left factors lie in `A` and whose right factors are prescribed by
38`x`. -/
40 {G : Type u} [Group G] (A : Subgroup G) {n : ℕ}
41 (x : Fin n → G) (g : G) : Prop :=
42 ∃ a : Fin n → G,
43 (∀ i, a i ∈ A) ∧
44 (List.ofFn fun i : Fin n => ⁅a i, x i⁆).prod = g
46/-- A product of commutators in which the right factors come from two prescribed families and all
47left factors lie in the same subgroup. -/
49 {G : Type u} [Group G] (A : Subgroup G) {m n : ℕ}
50 (x : Fin m → G) (y : Fin n → G) (g : G) : Prop :=
51 ∃ a : Fin m → G, ∃ b : Fin n → G,
52 (∀ i, a i ∈ A) ∧ (∀ j, b j ∈ A) ∧
53 (List.ofFn fun i : Fin m => ⁅a i, x i⁆).prod *
54 (List.ofFn fun j : Fin n => ⁅b j, y j⁆).prod = g
56theorem IsProductOfCommutatorsAlongInSubgroup.mono
57 {G : Type u} [Group G] {A B : Subgroup G} {n : ℕ}
58 {x : Fin n → G} {g : G}
59 (hAB : A ≤ B)
60 (h : IsProductOfCommutatorsAlongInSubgroup A x g) :
61 IsProductOfCommutatorsAlongInSubgroup B x g := by
62 rcases h with ⟨a, ha, hprod⟩
63 exact ⟨a, fun i => hAB (ha i), hprod⟩
65theorem IsProductOfCommutatorsAlongInSubgroup.map
66 {G H : Type u} [Group G] [Group H] {A : Subgroup G} {n : ℕ}
67 {x : Fin n → G} {g : G}
68 (f : G →* H)
69 (h : IsProductOfCommutatorsAlongInSubgroup A x g) :
70 IsProductOfCommutatorsAlongInSubgroup (A.map f) (fun i => f (x i)) (f g) := by
71 rcases h with ⟨a, ha, hprod⟩
72 refine ⟨fun i => f (a i), ?_, ?_⟩
73 · intro i
74 exact ⟨a i, ha i, rfl⟩
75 · let l : List (G × G) := List.ofFn fun i : Fin n => (a i, x i)
76 have hmapList :
77 ∀ l : List (G × G),
78 f ((l.map fun p : G × G => ⁅p.1, p.2⁆).prod) =
79 (l.map fun p : G × G => ⁅f p.1, f p.2⁆).prod := by
80 intro l
81 induction l with
82 | nil =>
84 | cons p t ih =>
86 calc
87 (List.ofFn fun i : Fin n => ⁅f (a i), f (x i)⁆).prod =
88 (l.map fun p : G × G => ⁅f p.1, f p.2⁆).prod := by
89 dsimp [l]
90 rw [List.map_ofFn]
91 rfl
92 _ = f ((l.map fun p : G × G => ⁅p.1, p.2⁆).prod) := (hmapList l).symm
93 _ = f g := by
94 simpa [l, List.map_ofFn] using congrArg f hprod
96theorem IsProductOfCommutatorsAlongInSubgroup.mul
97 {G : Type u} [Group G] {A : Subgroup G} {m n : ℕ}
98 {x : Fin m → G} {y : Fin n → G} {g h : G}
99 (hg : IsProductOfCommutatorsAlongInSubgroup A x g)
100 (hh : IsProductOfCommutatorsAlongInSubgroup A y h) :
101 IsProductOfCommutatorsAlongInSubgroup A (Fin.append x y) (g * h) := by
102 rcases hg with ⟨a, ha, hprodg⟩
103 rcases hh with ⟨b, hb, hprodh⟩
104 refine ⟨Fin.append a b, ?_, ?_⟩
105 · intro i
106 cases i using Fin.addCases with
107 | left i =>
108 simpa [Fin.append_left] using ha i
109 | right i =>
110 simpa [Fin.append_right] using hb i
111 · have hlist :
112 List.ofFn (fun i : Fin (m + n) =>
113 ⁅(Fin.append a b i), (Fin.append x y i)⁆) =
114 List.ofFn (fun i : Fin m => ⁅a i, x i⁆) ++
115 List.ofFn (fun i : Fin n => ⁅b i, y i⁆) := by
116 have hfun :
117 (fun i : Fin (m + n) => ⁅(Fin.append a b i), (Fin.append x y i)⁆) =
118 Fin.append (fun i : Fin m => ⁅a i, x i⁆) (fun i : Fin n => ⁅b i, y i⁆) := by
119 funext i
120 cases i using Fin.addCases with
121 | left i =>
122 simp only [Fin.append_left]
123 | right i =>
124 simp only [Fin.append_right]
125 rw [hfun, List.ofFn_fin_append]
126 rw [hlist, List.prod_append, hprodg, hprodh]
129 {K : Type u} [Group K] [Group.FG K] {d : ℕ}
130 (hd : Group.rank K ≤ d) :
131 ∃ x : Fin d → K, Subgroup.closure (Set.range x) = (⊤ : Subgroup K) := by
132 classical
133 rcases Group.rank_spec K with ⟨S, hScard, hSgen⟩
134 have hcard : Fintype.card {a : K // a ∈ S} ≤ Fintype.card (Fin d) := by
135 simpa [hScard] using hd
136 let e : {a : K // a ∈ S} ↪ Fin d :=
137 Classical.choice (Function.Embedding.nonempty_of_card_le hcard)
138 let x : Fin d → K := fun i =>
139 if h : ∃ a : {a : K // a ∈ S}, e a = i then
140 ((Classical.choose h : {a : K // a ∈ S}) : K)
141 else 1
142 have hSsubset : (S : Set K) ⊆ Set.range x := by
143 intro a ha
144 let aS : {a : K // a ∈ S} := ⟨a, ha⟩
145 refine ⟨e aS, ?_⟩
146 dsimp [x]
147 let hEx : ∃ b : {a : K // a ∈ S}, e b = e aS := ⟨aS, rfl⟩
148 rw [dif_pos hEx]
149 have hchosen : e (Classical.choose hEx) = e aS :=
150 Classical.choose_spec hEx
151 change ((Classical.choose hEx : {a : K // a ∈ S}) : K) = (aS : K)
152 exact congrArg Subtype.val (e.injective hchosen)
153 refine ⟨x, le_antisymm le_top ?_⟩
154 rw [← hSgen]
155 exact Subgroup.closure_mono hSsubset
157/-- In a semidirect product generated by at most `d` elements, the kernel admits `d`
158normal generators. -/
160 {K : Type u} [Group K] [Group.FG K] {H L : Subgroup K} [_hH : H.Normal]
161 (hsplit : IsCompl H L) {d : ℕ} (hd : Group.rank K ≤ d) :
162 ∃ y : Fin d → K, Subgroup.normalClosure (Set.range y) = H := by
163 classical
164 rcases exists_generating_family_of_rank_le (K := K) hd with ⟨x, hx⟩
165 let qH : K →* K ⧸ H := QuotientGroup.mk' H
166 have hmapH : Subgroup.map qH H = (⊥ : Subgroup (K ⧸ H)) := by
167 ext z
168 constructor
169 · rintro ⟨h, hh, rfl⟩
170 exact (QuotientGroup.eq_one_iff (N := H) h).2 hh
171 · intro hz
172 rw [Subgroup.mem_bot] at hz
173 subst z
174 exact ⟨1, H.one_mem, by simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_one, qH]⟩
175 have hmapL : Subgroup.map qH L = (⊤ : Subgroup (K ⧸ H)) := by
176 have hmapSup :
177 Subgroup.map qH (H ⊔ L) = (⊤ : Subgroup (K ⧸ H)) := by
178 rw [hsplit.sup_eq_top]
179 exact Subgroup.map_top_of_surjective qH (QuotientGroup.mk'_surjective H)
180 rw [Subgroup.map_sup, hmapH, bot_sup_eq] at hmapSup
181 exact hmapSup
182 have hlift :
183 ∀ i : Fin d, ∃ l : K, l ∈ L ∧ qH l = qH (x i) := by
184 intro i
185 have hxmem : qH (x i) ∈ Subgroup.map qH L := by
186 rw [hmapL]
187 simp only [Subgroup.mem_top]
188 exact (Subgroup.mem_map.mp hxmem)
189 choose l hlL hlq using hlift
190 let y : Fin d → K := fun i => (l i)⁻¹ * x i
191 refine ⟨y, ?_⟩
192 let N : Subgroup K := Subgroup.normalClosure (Set.range y)
193 haveI : N.Normal := Subgroup.normalClosure_normal
194 have hyH : ∀ i, y i ∈ H := by
195 intro i
196 exact QuotientGroup.eq.mp (hlq i)
197 have hNleH : N ≤ H := by
198 refine Subgroup.normalClosure_le_normal ?_
199 rintro z ⟨i, rfl⟩
200 exact hyH i
201 have hHleN : H ≤ N := by
202 let qN : K →* K ⧸ N := QuotientGroup.mk' N
203 let M : Subgroup (K ⧸ N) := Subgroup.map qN L
204 have hxM : ∀ i : Fin d, qN (x i) ∈ M := by
205 intro i
206 refine Subgroup.mem_map.mpr ⟨l i, hlL i, ?_⟩
207 have hyN : y i ∈ N := Subgroup.subset_normalClosure ⟨i, rfl⟩
208 exact QuotientGroup.eq.mpr hyN
209 have htopLe : (⊤ : Subgroup K) ≤ Subgroup.comap qN M := by
210 rw [← hx]
211 exact (Subgroup.closure_le (Subgroup.comap qN M)).2 <| by
212 rintro z ⟨i, rfl⟩
213 exact hxM i
214 intro h hh
215 have hqmem : qN h ∈ M := htopLe (by simp only [Subgroup.mem_top])
216 rcases Subgroup.mem_map.mp hqmem with ⟨l0, hl0L, hqeq⟩
217 have hn : l0⁻¹ * h ∈ N := QuotientGroup.eq.mp hqeq
218 have hl0H : l0 ∈ H := by
219 have hnH : l0⁻¹ * h ∈ H := hNleH hn
220 have hlinvH : l0⁻¹ ∈ H := by
221 simpa [mul_assoc] using H.mul_mem hnH (H.inv_mem hh)
222 simpa using H.inv_mem hlinvH
223 have hl0bot : l0 ∈ (⊥ : Subgroup K) := by
224 rw [← hsplit.inf_eq_bot]
225 exact ⟨hl0H, hl0L⟩
226 have hl0one : l0 = 1 := by
227 simpa using hl0bot
228 have hqone : qN h = 1 := by
229 simpa [hl0one] using hqeq.symm
230 exact (QuotientGroup.eq_one_iff (N := N) h).mp hqone
231 exact le_antisymm hNleH hHleN
233end ProCGroups.FiniteStepSolvableQuotients