Source: ProCGroups.FiniteStepSolvableQuotients.Commutators.Width
1import Mathlib.GroupTheory.Rank
2import ProCGroups.FiniteGeneration.CharacteristicChainsAndIndices
4/-!
5# Uniform commutator-width estimates
7This module encodes products of commutators with prescribed factors and proves the functorial and
8rank-theoretic estimates used to obtain uniform width bounds.
9-/
11open scoped Topology Pointwise commutatorElement
13namespace ProCGroups.FiniteStepSolvableQuotients
15open ProCGroups.FiniteGeneration
17universe u
19/--
20A product of commutators whose left factors lie in \(A\) and whose right factors are prescribed
21by \(x\).
22-/
23def IsProductOfCommutatorsAlongInSubgroup
24 {G : Type u} [Group G] (A : Subgroup G) {n : ℕ}
25 (x : Fin n → G) (g : G) : Prop :=
26 ∃ a : Fin n → G,
27 (∀ i, a i ∈ A) ∧
28 (List.ofFn fun i : Fin n => ⁅a i, x i⁆).prod = g
30/--
31A product of commutators in which the right factors come from two prescribed families and all
32left factors lie in the same subgroup.
33-/
34def IsProductOfCommutatorsAlongPairInSubgroup
35 {G : Type u} [Group G] (A : Subgroup G) {m n : ℕ}
36 (x : Fin m → G) (y : Fin n → G) (g : G) : Prop :=
37 ∃ a : Fin m → G, ∃ b : Fin n → G,
38 (∀ i, a i ∈ A) ∧ (∀ j, b j ∈ A) ∧
39 (List.ofFn fun i : Fin m => ⁅a i, x i⁆).prod *
40 (List.ofFn fun j : Fin n => ⁅b j, y j⁆).prod = g
42/--
43A product-of-commutators witness remains valid after enlarging the allowed number of commutator
44factors.
45-/
46theorem IsProductOfCommutatorsAlongInSubgroup.mono
47 {G : Type u} [Group G] {A B : Subgroup G} {n : ℕ}
48 {x : Fin n → G} {g : G}
49 (hAB : A ≤ B)
50 (h : IsProductOfCommutatorsAlongInSubgroup A x g) :
51 IsProductOfCommutatorsAlongInSubgroup B x g := by
52 rcases h with ⟨a, ha, hprod⟩
53 exact ⟨a, fun i => hAB (ha i), hprod⟩
55/-- Being a product of commutators along a subgroup is preserved by the induced map. -/
56theorem IsProductOfCommutatorsAlongInSubgroup.map
57 {G H : Type u} [Group G] [Group H] {A : Subgroup G} {n : ℕ}
58 {x : Fin n → G} {g : G}
59 (f : G →* H)
60 (h : IsProductOfCommutatorsAlongInSubgroup A x g) :
61 IsProductOfCommutatorsAlongInSubgroup (A.map f) (fun i => f (x i)) (f g) := by
62 rcases h with ⟨a, ha, hprod⟩
63 refine ⟨fun i => f (a i), ?_, ?_⟩
64 · intro i
65 exact ⟨a i, ha i, rfl⟩
66 · let l : List (G × G) := List.ofFn fun i : Fin n => (a i, x i)
67 have hmapList :
68 ∀ l : List (G × G),
69 f ((l.map fun p : G × G => ⁅p.1, p.2⁆).prod) =
70 (l.map fun p : G × G => ⁅f p.1, f p.2⁆).prod := by
71 intro l
72 induction l with
73 | nil =>
74 simp only [List.map_nil, List.prod_nil, map_one]
75 | cons p t ih =>
76 simp only [List.map_cons, List.prod_cons, map_mul, map_commutatorElement, ih]
77 calc
78 (List.ofFn fun i : Fin n => ⁅f (a i), f (x i)⁆).prod =
79 (l.map fun p : G × G => ⁅f p.1, f p.2⁆).prod := by
80 dsimp [l]
81 rw [List.map_ofFn]
82 rfl
83 _ = f ((l.map fun p : G × G => ⁅p.1, p.2⁆).prod) := (hmapList l).symm
84 _ = f g := by
85 have hcommList :
86 (l.map fun p : G × G => ⁅p.1, p.2⁆) =
87 List.ofFn (fun i : Fin n => ⁅a i, x i⁆) := by
88 dsimp [l]
89 rw [List.map_ofFn]
90 rfl
91 rw [hcommList, hprod]
93/--
94Multiplying two subgroup-bounded commutator-product witnesses gives a witness with the sum of
95the allowed widths.
96-/
97theorem IsProductOfCommutatorsAlongInSubgroup.mul
98 {G : Type u} [Group G] {A : Subgroup G} {m n : ℕ}
99 {x : Fin m → G} {y : Fin n → G} {g h : G}
100 (hg : IsProductOfCommutatorsAlongInSubgroup A x g)
101 (hh : IsProductOfCommutatorsAlongInSubgroup A y h) :
102 IsProductOfCommutatorsAlongInSubgroup A (Fin.append x y) (g * h) := by
103 rcases hg with ⟨a, ha, hprodg⟩
104 rcases hh with ⟨b, hb, hprodh⟩
105 refine ⟨Fin.append a b, ?_, ?_⟩
106 · intro i
107 cases i using Fin.addCases with
108 | left i =>
109 simpa [Fin.append_left] using ha i
110 | right i =>
111 simpa [Fin.append_right] using hb i
112 · have hlist :
113 List.ofFn (fun i : Fin (m + n) =>
114 ⁅(Fin.append a b i), (Fin.append x y i)⁆) =
115 List.ofFn (fun i : Fin m => ⁅a i, x i⁆) ++
116 List.ofFn (fun i : Fin n => ⁅b i, y i⁆) := by
117 have hfun :
118 (fun i : Fin (m + n) => ⁅(Fin.append a b i), (Fin.append x y i)⁆) =
119 Fin.append (fun i : Fin m => ⁅a i, x i⁆) (fun i : Fin n => ⁅b i, y i⁆) := by
120 funext i
121 cases i using Fin.addCases with
122 | left i =>
123 simp only [Fin.append_left]
124 | right i =>
125 simp only [Fin.append_right]
126 rw [hfun, List.ofFn_fin_append]
127 rw [hlist, List.prod_append, hprodg, hprodh]
129/-- A rank bound supplies a generating family of the corresponding bounded cardinality. -/
130theorem exists_generating_family_of_rank_le
131 {K : Type u} [Group K] [Group.FG K] {d : ℕ}
132 (hd : Group.rank K ≤ d) :
133 ∃ x : Fin d → K, Subgroup.closure (Set.range x) = (⊤ : Subgroup K) := by
134 classical
135 rcases Group.rank_spec K with ⟨S, hScard, hSgen⟩
136 have hcard : Fintype.card {a : K // a ∈ S} ≤ Fintype.card (Fin d) := by
137 simpa [hScard] using hd
138 let e : {a : K // a ∈ S} ↪ Fin d :=
139 Classical.choice (Function.Embedding.nonempty_of_card_le hcard)
140 let x : Fin d → K := fun i =>
141 if h : ∃ a : {a : K // a ∈ S}, e a = i then
142 ((Classical.choose h : {a : K // a ∈ S}) : K)
143 else 1
144 have hSsubset : (S : Set K) ⊆ Set.range x := by
145 intro a ha
146 let aS : {a : K // a ∈ S} := ⟨a, ha⟩
147 refine ⟨e aS, ?_⟩
148 dsimp [x]
149 let hEx : ∃ b : {a : K // a ∈ S}, e b = e aS := ⟨aS, rfl⟩
150 rw [dif_pos hEx]
151 change ((Classical.choose hEx : {a : K // a ∈ S}) : K) = (aS : K)
152 exact congrArg Subtype.val (e.injective (Classical.choose_spec hEx))
153 refine ⟨x, le_antisymm le_top ?_⟩
154 rw [← hSgen]
155 exact Subgroup.closure_mono hSsubset
157/--
158In a semidirect product generated by at most d elements, the kernel admits d normal generators.
159-/
160theorem exists_normalGenerators_of_split_group_of_rank_le
161 {K : Type u} [Group K] [Group.FG K] {H L : Subgroup K} [_hH : H.Normal]
162 (hsplit : IsCompl H L) {d : ℕ} (hd : Group.rank K ≤ d) :
163 ∃ y : Fin d → K, Subgroup.normalClosure (Set.range y) = H := by
164 classical
165 rcases exists_generating_family_of_rank_le (K := K) hd with ⟨x, hx⟩
166 let qH : K →* K ⧸ H := QuotientGroup.mk' H
167 have hmapH : Subgroup.map qH H = (⊥ : Subgroup (K ⧸ H)) := by
168 ext z
169 constructor
170 · rintro ⟨h, hh, rfl⟩
171 exact (QuotientGroup.eq_one_iff (N := H) h).2 hh
172 · intro hz
173 rw [Subgroup.mem_bot] at hz
174 subst z
175 exact ⟨1, H.one_mem, by simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_one, qH]⟩
176 have hmapL : Subgroup.map qH L = (⊤ : Subgroup (K ⧸ H)) := by
177 have hmapSup :
178 Subgroup.map qH (H ⊔ L) = (⊤ : Subgroup (K ⧸ H)) := by
179 rw [hsplit.sup_eq_top]
180 exact Subgroup.map_top_of_surjective qH (QuotientGroup.mk'_surjective H)
181 rw [Subgroup.map_sup, hmapH, bot_sup_eq] at hmapSup
182 exact hmapSup
183 have hlift :
184 ∀ i : Fin d, ∃ l : K, l ∈ L ∧ qH l = qH (x i) := by
185 intro i
186 have hxmem : qH (x i) ∈ Subgroup.map qH L := by
187 rw [hmapL]
188 simp only [Subgroup.mem_top]
189 exact (Subgroup.mem_map.mp hxmem)
190 choose l hlL hlq using hlift
191 let y : Fin d → K := fun i => (l i)⁻¹ * x i
192 refine ⟨y, ?_⟩
193 let N : Subgroup K := Subgroup.normalClosure (Set.range y)
194 haveI : N.Normal := Subgroup.normalClosure_normal
195 have hyH : ∀ i, y i ∈ H := by
196 intro i
197 exact QuotientGroup.eq.mp (hlq i)
198 have hNleH : N ≤ H := by
199 refine Subgroup.normalClosure_le_normal ?_
200 rintro z ⟨i, rfl⟩
201 exact hyH i
202 have hHleN : H ≤ N := by
203 let qN : K →* K ⧸ N := QuotientGroup.mk' N
204 let M : Subgroup (K ⧸ N) := Subgroup.map qN L
205 have hxM : ∀ i : Fin d, qN (x i) ∈ M := by
206 intro i
207 refine Subgroup.mem_map.mpr ⟨l i, hlL i, ?_⟩
208 have hyN : y i ∈ N := Subgroup.subset_normalClosure ⟨i, rfl⟩
209 exact QuotientGroup.eq.mpr hyN
210 have htopLe : (⊤ : Subgroup K) ≤ Subgroup.comap qN M := by
211 rw [← hx]
212 exact (Subgroup.closure_le (Subgroup.comap qN M)).2 <| by
213 rintro z ⟨i, rfl⟩
214 exact hxM i
215 intro h hh
216 have hqmem : qN h ∈ M := htopLe (by simp only [Subgroup.mem_top])
217 rcases Subgroup.mem_map.mp hqmem with ⟨l0, hl0L, hqeq⟩
218 have hn : l0⁻¹ * h ∈ N := QuotientGroup.eq.mp hqeq
219 have hl0H : l0 ∈ H := by
220 have hnH : l0⁻¹ * h ∈ H := hNleH hn
221 have hlinvH : l0⁻¹ ∈ H := by
222 simpa [mul_assoc] using H.mul_mem hnH (H.inv_mem hh)
223 simpa using H.inv_mem hlinvH
224 have hl0bot : l0 ∈ (⊥ : Subgroup K) := by
225 rw [← hsplit.inf_eq_bot]
226 exact ⟨hl0H, hl0L⟩
227 have hl0one : l0 = 1 := by
228 simpa using hl0bot
229 have hqone : qN h = 1 := by
230 simpa [hl0one] using hqeq.symm
231 exact (QuotientGroup.eq_one_iff (N := N) h).mp hqone
232 exact le_antisymm hNleH hHleN
234end ProCGroups.FiniteStepSolvableQuotients