Yamaguchi Lean 4 Library
ProCGroups/FiniteStepSolvableQuotients/Commutators/DerivedSeriesAndQuotients.lean
ProCGroups/FiniteStepSolvableQuotients/Commutators/DerivedSeriesAndQuotients/Source

ProCGroups/FiniteStepSolvableQuotients/Commutators/DerivedSeriesAndQuotients.lean

1import Mathlib.Topology.Algebra.Group.TopologicalAbelianization
2import Mathlib.Topology.Algebra.OpenSubgroup
3import ProCGroups.GroupTheory.CentralizerNormalizerCommensurator
4import ProCGroups.Order.Basic
5import ProCGroups.ProC.OpenNormalSubgroups.Separation
6import ProCGroups.Topologies.TopologicallyCharacteristicSubgroups
8/-
9PUBLIC_PAGE_SNAPSHOT
10generated_at: 2026-05-27T09:47:29+09:00
11lean_source: lean4/ProCGroups/FiniteStepSolvableQuotients/Commutators/DerivedSeriesAndQuotients.lean
12translation_root: data/translation
13purpose: identifies the local data snapshot used to build pages/
14placement: after imports, never before imports
15-/
16/-!
17# Finite-step solvable quotients
19Develops topological derived series, maximal solvable quotients of bounded derived length, commutator closure formulas, and abelian-action consequences.
20-/
22universe u v
24namespace TopologicalGroup
29/-- Closed-map properties descend to the restriction to a subgroup preimage. -/
31 {G : Type u} [TopologicalSpace G] [Group G]
32 {Q : Type v} [TopologicalSpace Q] [Group Q]
33 (π : G →ₜ* Q) (Q₁ : Subgroup Q)
34 (hπ : IsClosedMap π)
35 (hQ₁ : IsClosed (Q₁ : Set Q)) :
36 IsClosedMap (π.restrictPreimage Q₁) := by
37 let G₁ : Subgroup G := Q₁.comap (π : G →* Q)
38 have hG₁ : IsClosed (G₁ : Set G) := hQ₁.preimage π.continuous
39 intro s hs
40 have hsG : IsClosed (((G₁ : Subgroup G).subtype : G₁ → G) '' s) :=
41 hG₁.isClosedMap_subtype_val _ hs
42 have himg :
43 IsClosed ((fun x : G => π x) '' (((G₁ : Subgroup G).subtype : G₁ → G) '' s)) :=
44 hπ _ hsG
45 refine
46 (hQ₁.isClosedEmbedding_subtypeVal.isClosed_iff_image_isClosed).2 ?_
47 simpa [G₁, ContinuousMonoidHom.restrictPreimage, Set.image_image] using himg
49/-- If the image of a subgroup is contained in a closed subgroup, then the image of its closure is
50contained there as well. -/
52 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
53 {Q : Type v} [TopologicalSpace Q] [Group Q]
54 {G₁ : Subgroup G} {Q₁ : Subgroup Q} {f : G →ₜ* Q}
55 (h₁ : G₁.map (f : G →* Q) ≤ Q₁)
56 (hclosed : IsClosed (Q₁ : Set Q)) :
57 (G₁.topologicalClosure).map (f : G →* Q) ≤ Q₁ := by
58 have hMapsTo : Set.MapsTo (fun x : G => f x) (G₁ : Set G) (Q₁ : Set Q) := by
59 intro x hx
60 exact h₁ ⟨x, hx, rfl⟩
61 have hMapsTo_cl :
62 Set.MapsTo (fun x : G => f x) (_root_.closure (G₁ : Set G)) (Q₁ : Set Q) :=
63 Set.MapsTo.closure_left hMapsTo f.continuous hclosed
64 rintro y ⟨x, hx, rfl⟩
65 exact hMapsTo_cl hx
67/-- The image of a closure is contained in the closure of the image. -/
69 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
70 {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
71 {G₁ : Subgroup G} {Q₁ : Subgroup Q} (f : G →ₜ* Q)
72 (h₁ : G₁.map (f : G →* Q) ≤ Q₁) :
73 (G₁.topologicalClosure).map (f : G →* Q) ≤ Q₁.topologicalClosure := by
74 refine
75 map_closure_le_of_map_le (f := f) (G₁ := G₁) (Q₁ := Q₁.topologicalClosure) ?_ ?_
76 · exact le_trans h₁ (Subgroup.le_topologicalClosure (s := Q₁))
77 · exact Subgroup.isClosed_topologicalClosure (s := Q₁)
79/-- Closed maps send closed subgroups to closed images. -/
81 {G : Type u} [TopologicalSpace G] [Group G]
82 {H : Type v} [TopologicalSpace H] [Group H]
83 (f : G →ₜ* H) (hclosed : IsClosedMap f)
84 (K : Subgroup G) (hK : IsClosed (K : Set G)) :
85 IsClosed (((K.map (f : G →* H) : Subgroup H) : Set H)) := by
86 have him : IsClosed ((fun x : G => f x) '' (K : Set G)) := hclosed _ hK
87 have hEq :
88 (fun x : G => f x) '' (K : Set G)
89 = (((K.map (f : G →* H) : Subgroup H) : Set H)) := by
90 exact image_subtype_eq_map (f := (f : G →* H)) (K := K)
91 exact hEq ▸ him
93/-- If the comap along the quotient-induced map is exactly the source kernel, then the induced map
94has trivial kernel. -/
96 {G : Type u} [Group G]
97 {H : Type v} [Group H]
98 {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
99 (f : G →* H) (h : N ≤ M.comap f) (hcomap : M.comap f = N) :
100 (QuotientGroup.map (N := N) (M := M) (f := f) h).ker = ⊥ := by
101 calc
102 (QuotientGroup.map (N := N) (M := M) (f := f) h).ker =
103 Subgroup.map (QuotientGroup.mk' N) (Subgroup.comap f M) := by
104 simpa using QuotientGroup.ker_map (N := N) (M := M) (f := f) h
105 _ = Subgroup.map (QuotientGroup.mk' N) N := by simp only [hcomap, QuotientGroup.map_mk'_self]
106 _ = ⊥ := by
107 refine (Subgroup.map_eq_bot_iff (f := QuotientGroup.mk' N) (H := N)).2 ?_
108 intro x hx
109 simpa using hx
111end TopologicalGroup
113namespace MulEquiv
115/-- Multiplicative equivalences transport torsion-freeness. -/
117 {M : Type u} [Monoid M]
118 {N : Type v} [Monoid N]
119 (e : M ≃* N) [IsMulTorsionFree M] :
120 IsMulTorsionFree N := by
121 exact Function.Injective.isMulTorsionFree (e.symm : N →* M) e.symm.injective
123end MulEquiv
125namespace ProCGroups.FiniteStepSolvableQuotients
127/-- The closed commutator subgroup generated by two subgroups. -/
128abbrev closedCommutator
129 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
130 (H K : Subgroup G) : Subgroup G :=
131 (⁅H, K⁆).topologicalClosure
133/-- The closed derived series starting from a subgroup. -/
135 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
136 (K : Subgroup G) : ℕ → Subgroup G
137 | 0 => K
138 | n + 1 => closedCommutator (closedDerivedSeries K n) (closedDerivedSeries K n)
140/-- The ambient closed derived series. -/
142 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
143 (m : ℕ) : Subgroup G :=
144 closedDerivedSeries (G := G) (⊤ : Subgroup G) m
147 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
148 {m : ℕ} :
149 IsClosed (topDerivedTop G m : Set G) := by
150 cases m with
151 | zero =>
152 change IsClosed ((⊤ : Subgroup G) : Set G)
153 exact isClosed_univ
154 | succ m =>
155 simp only [topDerivedTop, closedDerivedSeries, closedCommutator]
156 exact isClosed_closure
159 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
160 {m : ℕ} :
161 (topDerivedTop G m).Normal := by
162 induction m with
163 | zero =>
164 simpa [topDerivedTop] using (inferInstance : (⊤ : Subgroup G).Normal)
165 | succ m ihm =>
166 dsimp [topDerivedTop, closedDerivedSeries, closedCommutator]
167 letI : (topDerivedTop G m).Normal := ihm
168 exact Subgroup.is_normal_topologicalClosure ⁅topDerivedTop G m, topDerivedTop G m⁆
170/-- The quotient by the `m`th closed derived subgroup. -/
172 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
173 (m : ℕ) : Type u :=
174 G ⧸ topDerivedTop G m
176/-- The natural quotient map to the maximal `m`-step solvable quotient. -/
178 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
179 (m : ℕ) :
180 G →* MaxSolvQuot G m :=
181 QuotientGroup.mk' (topDerivedTop G m)
183/-- The natural quotient map as a continuous homomorphism. -/
185 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
186 (m : ℕ) :
187 G →ₜ* MaxSolvQuot G m :=
188 { toMonoidHom := toMaxSolvQuot G m
189 continuous_toFun := continuous_quotient_mk' }
191/-- The preimage open subgroup induced by a continuous homomorphism. -/
193 {G : Type u} [TopologicalSpace G] [Group G]
194 {Q : Type v} [TopologicalSpace Q] [Group Q]
195 (f : G →ₜ* Q) (H : OpenSubgroup Q) : OpenSubgroup G :=
196 OpenSubgroup.comap (f := (f : G →* Q)) f.continuous H
198scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
200scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
202scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
205open scoped ProCGroupsSolvableQuotients
208 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
209 (K : Subgroup G) :
210 closedDerivedSeries (G := G) K 0 = K := rfl
213 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
214 (K : Subgroup G) (n : ℕ) :
215 closedDerivedSeries (G := G) K (n + 1) =
216 ⁅closedDerivedSeries (G := G) K n, closedDerivedSeries (G := G) K n⁆ₜ := rfl
218@[simp] lemma topDerivedTop_zero
219 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
220 G⟦0⟧ₜ = (⊤ : Subgroup G) := rfl
222@[simp] lemma topDerivedTop_succ
223 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
224 (n : ℕ) :
225 G⟦n + 1⟧ₜ = ⁅G⟦n⟧ₜ, G⟦n⟧ₜ⁆ₜ := rfl
227/-- Closed commutators map monotonically under continuous homomorphisms. -/
229 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
230 {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
231 {G₁ G₂ : Subgroup G} {Q₁ Q₂ : Subgroup Q} {f : G →ₜ* Q}
232 (h₁ : G₁.map (f : G →* Q) ≤ Q₁)
233 (h₂ : G₂.map (f : G →* Q) ≤ Q₂) :
234 (⁅G₁, G₂⁆ₜ).map (f : G →* Q) ≤ ⁅Q₁, Q₂⁆ₜ := by
235 dsimp [closedCommutator]
236 have hcomm :
237 (⁅G₁, G₂⁆).map (f : G →* Q) ≤ ⁅Q₁, Q₂⁆ := by
238 calc
239 (⁅G₁, G₂⁆).map (f : G →* Q) = ⁅G₁.map (f : G →* Q), G₂.map (f : G →* Q)⁆ := by
240 simpa using Subgroup.map_commutator G₁ G₂ (f : G →* Q)
241 _ ≤ ⁅Q₁, Q₂⁆ := Subgroup.commutator_mono h₁ h₂
242 exact TopologicalGroup.map_closure_le_closure (f := f) (G₁ := ⁅G₁, G₂⁆) (Q₁ := ⁅Q₁, Q₂⁆) hcomm
244/-- If target subgroups lie in the corresponding images, then their commutator lies in the image of
245the source closed commutator. -/
247 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
248 {Q : Type v} [Group Q]
249 (φ : G →* Q)
250 {G₁ G₂ : Subgroup G} {Q₁ Q₂ : Subgroup Q}
251 (h₁ : Q₁ ≤ G₁.map φ) (h₂ : Q₂ ≤ G₂.map φ) :
252 ⁅Q₁, Q₂⁆ ≤ (⁅G₁, G₂⁆ₜ).map φ := by
253 have h0 :
254 ⁅Q₁, Q₂⁆ ≤ (⁅G₁, G₂⁆).map φ :=
255 Subgroup.commutator_le_map_commutator
256 (f := φ) (H₁ := G₁) (H₂ := G₂) (K₁ := Q₁) (K₂ := Q₂) h₁ h₂
257 have hmono :
258 (⁅G₁, G₂⁆).map φ ≤ (⁅G₁, G₂⁆ₜ).map φ := by
259 simpa [closedCommutator] using
260 Subgroup.map_mono (f := φ) (Subgroup.le_topologicalClosure (s := ⁅G₁, G₂⁆))
261 exact le_trans h0 hmono
263/-- If the stagewise images match and the closed commutator image is closed, then the closed
264commutator maps exactly onto the target closed commutator. -/
266 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
267 {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
268 {G₁ G₂ : Subgroup G} {Q₁ Q₂ : Subgroup Q} {f : G →ₜ* Q}
269 (h₁ : G₁.map (f : G →* Q) = Q₁)
270 (h₂ : G₂.map (f : G →* Q) = Q₂)
271 (hclosed : IsClosed (((⁅G₁, G₂⁆ₜ).map (f : G →* Q) : Subgroup Q) : Set Q)) :
272 (⁅G₁, G₂⁆ₜ).map (f : G →* Q) = ⁅Q₁, Q₂⁆ₜ := by
273 let φ : G →* Q := (f : G →* Q)
274 have hle : (⁅G₁, G₂⁆ₜ).map φ ≤ ⁅Q₁, Q₂⁆ₜ := by
275 simpa [φ] using
277 (h₁ := by simpa using le_of_eq h₁)
278 (h₂ := by simpa using le_of_eq h₂)
279 have hge : ⁅Q₁, Q₂⁆ₜ ≤ (⁅G₁, G₂⁆ₜ).map φ := by
280 dsimp [closedCommutator]
281 refine
282 Subgroup.topologicalClosure_minimal
283 (s := ⁅Q₁, Q₂⁆) (t := (⁅G₁, G₂⁆ₜ).map φ) ?_ hclosed
284 refine commutator_le_map_closedCommutator (φ := φ) (G₁ := G₁) (G₂ := G₂) ?_ ?_
285 · simpa [φ] using ge_of_eq h₁
286 · simpa [φ] using ge_of_eq h₂
287 exact le_antisymm hle (by simpa [closedCommutator] using hge)
289/-- Closed commutators of topologically characteristic subgroups are again topologically
290characteristic. -/
291theorem closedCommutator_topologicallyCharacteristic
292 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
293 (G₁ G₂ : Subgroup G)
294 (h₁ : G₁.TopologicallyCharacteristic)
295 (h₂ : G₂.TopologicallyCharacteristic) :
296 (⁅G₁, G₂⁆ₜ).TopologicallyCharacteristic := by
297 letI : G₁.TopologicallyCharacteristic := h₁
298 letI : G₂.TopologicallyCharacteristic := h₂
299 have hcomm : (⁅G₁, G₂⁆).TopologicallyCharacteristic := by
300 infer_instance
301 simpa [closedCommutator] using
303 (H := ⁅G₁, G₂⁆) (hH := hcomm))
305/-- Restarting the ambient closed derived series adds indices. -/
306@[simp] lemma topDerived_add
307 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
308 (m n : ℕ) :
309 closedDerivedSeries (G := G) (G⟦m⟧ₜ) n = G⟦m + n⟧ₜ := by
310 induction n with
311 | zero =>
312 simp only [closedDerivedSeries_zero, add_zero]
313 | succ n ihn =>
314 rw [show m + (n + 1) = m + n + 1 by rw [Nat.add_assoc]]
316 simp only [closedDerivedSeries_succ, ihn]
318/-- The ambient closed derived series is antitone. -/
320 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
321 Antitone (topDerivedTop G) := by
322 apply antitone_nat_of_succ_le
323 intro m
324 dsimp [topDerivedTop, closedDerivedSeries, closedCommutator]
325 exact
326 Subgroup.topologicalClosure_minimal
327 (s := ⁅G⟦m⟧ₜ, G⟦m⟧ₜ⁆)
328 (t := G⟦m⟧ₜ)
329 (Subgroup.commutator_le_self (G⟦m⟧ₜ))
330 (by infer_instance)
332/-- Every stage of the ambient closed derived series is topologically characteristic. -/
334 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
335 {m : ℕ} :
337 induction m with
338 | zero =>
339 refine ⟨?_⟩
340 intro e
341 simp only [ContinuousMulEquiv.toMulEquiv_eq_coe, MulEquiv.toMonoidHom_eq_coe, topDerivedTop,
342 closedDerivedSeries_zero, Subgroup.comap_top]
343 | succ m ihm =>
345 closedCommutator_topologicallyCharacteristic
346 (G₁ := G⟦m⟧ₜ) (G₂ := G⟦m⟧ₜ) ihm ihm
348/-- The closed derived series is monotone under continuous homomorphisms. -/
350 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
351 {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
352 (f : G →ₜ* Q) (m : ℕ) :
353 (G⟦m⟧ₜ).map (f : G →* Q) ≤ Q⟦m⟧ₜ := by
354 induction m with
355 | zero =>
357 | succ m ih =>
358 dsimp [topDerivedTop, closedDerivedSeries, closedCommutator]
359 exact
361 (G₁ := ⁅G⟦m⟧ₜ, G⟦m⟧ₜ⁆)
362 (Q₁ := ⁅Q⟦m⟧ₜ, Q⟦m⟧ₜ⁆) <|
363 by
364 calc
365 (⁅G⟦m⟧ₜ, G⟦m⟧ₜ⁆).map (f : G →* Q)
366 = ⁅(G⟦m⟧ₜ).map (f : G →* Q), (G⟦m⟧ₜ).map (f : G →* Q)⁆ := by
367 simpa using
368 (Subgroup.map_commutator (G⟦m⟧ₜ) (G⟦m⟧ₜ) (f : G →* Q))
369 _ ≤ ⁅Q⟦m⟧ₜ, Q⟦m⟧ₜ⁆ := by
370 exact Subgroup.commutator_mono ih ih)
372/-- The ambient closed derived series pulls back along continuous homomorphisms. -/
374 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
375 {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
376 (f : G →ₜ* Q) (m : ℕ) :
377 G⟦m⟧ₜ ≤ (Q⟦m⟧ₜ).comap (f : G →* Q) := by
378 exact (Subgroup.map_le_iff_le_comap).1 (topDerived_map_le (f := f) m)
380/-- A point in the ambient `m`th derived subgroup lies in the first derived subgroup of any larger
381subgroup containing the `(m - 1)`st derived term. -/
383 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
384 {K : Subgroup G} {m : ℕ} (hm : 1 ≤ m)
385 (hK : G⟦m - 1⟧ₜ ≤ K)
386 {x : G} (hx : x ∈ G⟦m⟧ₜ) :
387 x ∈ closedDerivedSeries (G := G) K 1 := by
388 have hmEq : m = (m - 1) + 1 := (tsub_add_cancel_of_le hm).symm
389 have hx0 : x ∈ G⟦(m - 1) + 1⟧ₜ := hmEq ▸ hx
390 rw [← topDerived_add (G := G) (m := m - 1) (n := 1)] at hx0
391 have hmono :
392 closedDerivedSeries (G := G) (G⟦m - 1⟧ₜ) 1 ≤ closedDerivedSeries (G := G) K 1 := by
393 dsimp [closedDerivedSeries, closedCommutator]
394 refine
395 Subgroup.topologicalClosure_minimal
396 (s := ⁅G⟦m - 1⟧ₜ, G⟦m - 1⟧ₜ⁆)
397 (t := ⁅K, K⁆ₜ) ?_
398 (Subgroup.isClosed_topologicalClosure (s := ⁅K, K⁆))
399 exact (Subgroup.commutator_mono hK hK).trans (Subgroup.le_topologicalClosure _)
400 exact hmono hx0
402/-- Push the first derived subgroup of a closed subgroup back to the ambient group. -/
404 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
405 {H : Subgroup G} {K : Subgroup H} (hH : IsClosed (H : Set G)) :
406 (closedDerivedSeries (G := H) K 1).map H.subtype =
407 closedDerivedSeries (G := G) (K.map H.subtype) 1 := by
408 have hclosedSubtype : IsClosedMap (H.subtype : H → G) := hH.isClosedMap_subtype_val
409 have hclosure :
410 closure ((fun y : H => (y : G)) '' (((⁅K, K⁆ : Subgroup H) : Set H))) =
411 (fun y : H => (y : G)) '' closure (((⁅K, K⁆ : Subgroup H) : Set H)) :=
412 hclosedSubtype.closure_image_eq_of_continuous continuous_subtype_val _
413 have himg :
414 ((fun y : H => (y : G)) '' (((⁅K, K⁆ : Subgroup H) : Set H))) =
415 (((⁅K.map H.subtype, K.map H.subtype⁆ : Subgroup G) : Set G)) := by
417 congrArg (fun L : Subgroup G => (L : Set G))
418 (Subgroup.map_commutator K K H.subtype)
419 ext x
420 change
421 x ∈ ((fun y : H => (y : G)) '' ((((⁅K, K⁆).topologicalClosure : Subgroup H) : Set H))) ↔
422 x ∈ (((⁅K.map H.subtype, K.map H.subtype⁆).topologicalClosure : Subgroup G) : Set G)
423 change
424 x ∈ ((fun y : H => (y : G)) '' closure (((⁅K, K⁆ : Subgroup H) : Set H))) ↔
425 x ∈ closure (((⁅K.map H.subtype, K.map H.subtype⁆ : Subgroup G) : Set G))
426 rw [← hclosure, himg]
428/-- Surjective maps identify the stagewise closed derived subgroups once the commutator images are
429closed. -/
431 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
432 {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
433 (f : G →ₜ* H) (hf : Function.Surjective f)
434 (hclosed_comm :
435 ∀ n : ℕ,
436 IsClosed (((⁅G⟦n⟧ₜ, G⟦n⟧ₜ⁆ₜ).map (f : G →* H) : Subgroup H) : Set H))
437 (n : ℕ) :
438 (G⟦n⟧ₜ).map (f : G →* H) = H⟦n⟧ₜ := by
439 induction n with
440 | zero =>
441 ext y
442 constructor
443 · rintro ⟨x, -, rfl⟩
444 simp only [topDerivedTop, closedDerivedSeries_zero, MonoidHom.coe_coe, Subgroup.mem_top]
445 · intro hy
446 rcases hf y with ⟨x, rfl⟩
447 exact ⟨x, by simp only [topDerivedTop, closedDerivedSeries_zero, Subgroup.coe_top, Set.mem_univ], rfl⟩
448 | succ n ihn =>
449 apply le_antisymm
450 · exact topDerived_map_le (f := f) (m := n + 1)
451 · dsimp [topDerivedTop, closedDerivedSeries, closedCommutator]
452 refine
453 Subgroup.topologicalClosure_minimal
454 (s := ⁅H⟦n⟧ₜ, H⟦n⟧ₜ⁆)
455 (t := (⁅G⟦n⟧ₜ, G⟦n⟧ₜ⁆ₜ).map (f : G →* H)) ?_
456 (hclosed_comm n)
457 calc
458 ⁅H⟦n⟧ₜ, H⟦n⟧ₜ⁆
459 = ⁅(G⟦n⟧ₜ).map (f : G →* H), (G⟦n⟧ₜ).map (f : G →* H)⁆ := by
460 simp only [ihn]
461 _ = (⁅G⟦n⟧ₜ, G⟦n⟧ₜ⁆).map (f : G →* H) := by
462 symm
463 simpa using
464 (Subgroup.map_commutator (G⟦n⟧ₜ) (G⟦n⟧ₜ) (f : G →* H))
465 _ ≤ (⁅G⟦n⟧ₜ, G⟦n⟧ₜ⁆ₜ).map (f : G →* H) := by
466 exact Subgroup.map_mono (Subgroup.le_topologicalClosure _)
468/-- Images of closed commutators of derived terms are closed when the source is compact and the
469target is Hausdorff. -/
471 {G H : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
472 [CompactSpace G] [TopologicalSpace H] [Group H] [T2Space H]
473 (f : G →ₜ* H) (n : ℕ) :
474 IsClosed
475 (((closedCommutator (topDerivedTop G n) (topDerivedTop G n)).map
476 (f : G →* H) : Subgroup H) : Set H) := by
477 let K : ClosedSubgroup G :=
478 ⟨closedCommutator (topDerivedTop G n) (topDerivedTop G n), by
479 dsimp [closedCommutator]
480 exact isClosed_closure⟩
481 simpa [K] using
482 (ProCGroups.Order.ClosedSubgroup.map K (f : G →* H) f.continuous_toFun).isClosed'
484/-- The closed derived series is monotone in the initial subgroup. -/
486 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
487 {K L : Subgroup G} (hKL : K ≤ L) (n : ℕ) :
488 closedDerivedSeries (G := G) K n ≤ closedDerivedSeries (G := G) L n := by
489 induction n with
490 | zero =>
491 simpa using hKL
492 | succ n ih =>
493 dsimp [closedDerivedSeries, closedCommutator]
494 refine
495 Subgroup.topologicalClosure_minimal
496 (s := ⁅closedDerivedSeries (G := G) K n,
497 closedDerivedSeries (G := G) K n⁆)
498 (t := ⁅closedDerivedSeries (G := G) L n,
499 closedDerivedSeries (G := G) L n⁆ₜ) ?_
500 (Subgroup.isClosed_topologicalClosure
501 (s := ⁅closedDerivedSeries (G := G) L n,
502 closedDerivedSeries (G := G) L n⁆))
503 exact
504 (Subgroup.commutator_mono ih ih).trans
505 (Subgroup.le_topologicalClosure
506 (s := ⁅closedDerivedSeries (G := G) L n,
507 closedDerivedSeries (G := G) L n⁆))
509/-- The internal derived series of a closed subgroup maps to the corresponding ambient derived
510series. -/
512 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
513 {H : Subgroup G} (hH : IsClosed (H : Set G)) (n : ℕ) :
514 (topDerivedTop H n).map H.subtype =
515 closedDerivedSeries (G := G) H n := by
516 let incl : H →ₜ* G :=
517 { toMonoidHom := H.subtype
518 continuous_toFun := continuous_subtype_val }
519 induction n with
520 | zero =>
521 ext x
522 constructor
523 · rintro ⟨y, -, rfl⟩
524 exact y.2
525 · intro hx
526 exact ⟨⟨x, hx⟩, by simp only [topDerivedTop, closedDerivedSeries_zero, Subgroup.coe_top, Set.mem_univ], rfl⟩
527 | succ n ih =>
528 have hclosed :
529 IsClosed
530 (((closedCommutator (topDerivedTop H n) (topDerivedTop H n)).map
531 (incl : H →* G) : Subgroup G) : Set G) := by
532 exact
534 (f := incl) hH.isClosedMap_subtype_val
535 (K := closedCommutator (topDerivedTop H n) (topDerivedTop H n))
536 (Subgroup.isClosed_topologicalClosure
537 (s := ⁅topDerivedTop H n, topDerivedTop H n⁆))
538 have hmap :=
540 (f := incl) (h₁ := ih) (h₂ := ih) hclosed
541 simpa [incl, topDerivedTop, closedDerivedSeries] using hmap
543/-- Higher ambient derived terms lie in the corresponding derived term of any open subgroup
544containing the first derived term. -/
546 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
547 (H : OpenSubgroup G) {m : ℕ} (hm : 1 ≤ m)
548 (hfirst : topDerivedTop G 1 ≤ (H : Subgroup G)) :
550 (topDerivedTop ↥(H : Subgroup G) (m - 1)).map
551 (Subgroup.subtype (H : Subgroup G)) := by
552 have hpred : 1 + (m - 1) = m := by
553 simpa [Nat.add_comm] using
554 Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero (Nat.ne_of_gt hm))
555 intro x hx
556 have htop :
557 closedDerivedSeries (G := G) (topDerivedTop G 1) (m - 1) =
558 topDerivedTop G m := by
559 simpa [hpred] using
560 (topDerived_add (G := G) (m := 1) (n := m - 1))
561 have hxseries :
562 x ∈ closedDerivedSeries (G := G) (topDerivedTop G 1) (m - 1) := by
563 rw [htop]
564 exact hx
565 have hxH :
566 x ∈ closedDerivedSeries (G := G) (H : Subgroup G) (m - 1) :=
567 closedDerivedSeries_mono hfirst (m - 1) hxseries
568 have hHclosed : IsClosed (((H : Subgroup G) : Set G)) :=
571 (G := G) (H := (H : Subgroup G)) hHclosed (m - 1)]
572 exact hxH
574/-- If a profinite element projects into all open-normal derived lifts and the corresponding
575ambient derived term is trivial, then the element is trivial. -/
577 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
578 [CompactSpace Q] [TotallyDisconnectedSpace Q]
579 {m : ℕ} (hm : 3 ≤ m)
580 (hQm : topDerivedTop Q m = ⊥)
581 {d : Q}
582 (hproj :
583 ∀ H : OpenNormalSubgroup Q,
584 topDerivedTop Q 1 ≤ (H : Subgroup Q) →
585 d ∈ (topDerivedTop ↥(H : Subgroup Q) (m - 1)).map
586 (Subgroup.subtype (H : Subgroup Q))) :
587 d = 1 := by
588 classical
589 have hmpos : 0 < m := lt_of_lt_of_le (by decide : 0 < 3) hm
590 have hpred : 1 + (m - 1) = m := by
591 simpa [Nat.add_comm] using Nat.succ_pred_eq_of_pos hmpos
592 have hd_all : ∀ U : OpenNormalSubgroup Q, d ∈ (U : Subgroup Q) := by
593 intro U
594 let qU : Q →ₜ* Q ⧸ (U : Subgroup Q) :=
596 let K : Subgroup Q := topDerivedTop Q 1
597 have hKnormal : K.Normal := by
598 change (topDerivedTop Q 1).Normal
599 infer_instance
600 letI : K.Normal := hKnormal
601 let Hsub : Subgroup Q := K ⊔ (U : Subgroup Q)
602 have hHopen : IsOpen (Hsub : Set Q) := by
603 exact
604 Subgroup.isOpen_of_openSubgroup Hsub
605 (show (U : Subgroup Q) ≤ Hsub from le_sup_right)
606 let H : OpenNormalSubgroup Q :=
607 { toOpenSubgroup :=
608 { toSubgroup := Hsub
609 isOpen' := hHopen }
610 isNormal' := by
611 dsimp [Hsub]
612 infer_instance }
613 have hKleH : topDerivedTop Q 1 ≤ (H : Subgroup Q) := by
614 change K ≤ Hsub
615 exact le_sup_left
616 rcases hproj H hKleH with ⟨y, hy, hyd⟩
617 let inclK : K →ₜ* Q :=
618 { toMonoidHom := K.subtype
619 continuous_toFun := continuous_subtype_val }
620 let qK0 : K →ₜ* Q ⧸ (U : Subgroup Q) := qU.comp inclK
621 let qKr : K →ₜ* qK0.toMonoidHom.range := qK0.rangeRestrict
622 letI : DiscreteTopology (Q ⧸ (U : Subgroup Q)) :=
623 QuotientGroup.discreteTopology
625 letI : DiscreteTopology qK0.toMonoidHom.range := inferInstance
626 have hKclosed : IsClosed (K : Set Q) := by
627 change IsClosed ((topDerivedTop Q 1 : Subgroup Q) : Set Q)
628 infer_instance
629 have hKmap :
630 (topDerivedTop K (m - 1)).map K.subtype =
631 closedDerivedSeries (G := Q) K (m - 1) :=
633 (G := Q) (H := K) hKclosed (m - 1)
634 have hKmap_bot : (topDerivedTop K (m - 1)).map K.subtype = ⊥ := by
635 calc
636 (topDerivedTop K (m - 1)).map K.subtype =
637 closedDerivedSeries (G := Q) K (m - 1) := hKmap
638 _ = topDerivedTop Q (1 + (m - 1)) := by
639 simpa [K] using
640 (topDerived_add (G := Q) (m := 1) (n := m - 1))
641 _ = topDerivedTop Q m := by rw [hpred]
642 _ = ⊥ := hQm
643 have hKder_bot : topDerivedTop K (m - 1) = ⊥ := by
644 apply le_antisymm
645 · intro z hz
646 have hzker :
647 z ∈ (K.subtype : K →* Q).ker := by
648 exact
649 (Subgroup.map_eq_bot_iff
650 (f := (K.subtype : K →* Q))
651 (H := topDerivedTop K (m - 1))).1 hKmap_bot hz
652 have hzval : (z : Q) = 1 := by
653 exact (MonoidHom.mem_ker.mp hzker)
654 exact Subgroup.mem_bot.mpr (Subtype.ext hzval)
655 · exact bot_le
656 have hclosed_comm :
657 ∀ n : ℕ,
658 IsClosed
659 (((closedCommutator (topDerivedTop K n) (topDerivedTop K n)).map
660 (qKr : K →* qK0.toMonoidHom.range) :
661 Subgroup qK0.toMonoidHom.range) : Set qK0.toMonoidHom.range) := by
662 intro n
663 exact isClosed_discrete _
664 have hKrange_eq :
665 (topDerivedTop K (m - 1)).map
666 (qKr : K →* qK0.toMonoidHom.range) =
667 topDerivedTop qK0.toMonoidHom.range (m - 1) := by
668 exact
670 (f := qKr)
671 (MonoidHom.rangeRestrict_surjective qK0.toMonoidHom)
672 hclosed_comm (m - 1)
673 have hKrange_bot : topDerivedTop qK0.toMonoidHom.range (m - 1) = ⊥ := by
674 rw [← hKrange_eq, hKder_bot]
675 ext z
676 simp only [ContinuousMonoidHom.coe_toMonoidHom, Subgroup.map_bot, Subgroup.mem_bot]
677 have hqH_mem_Krange :
678 ∀ z : H, qU z.1 ∈ qK0.toMonoidHom.range := by
679 intro z
680 have hzH : z.1 ∈ Hsub := z.2
681 rcases
682 (Subgroup.mem_sup_of_normal_right (s := K) (t := (U : Subgroup Q))).1
683 hzH with
684 ⟨k, hk, u, hu, hku⟩
685 refine ⟨⟨k, hk⟩, ?_⟩
686 change qU k = qU z.1
687 rw [← hku]
689 have hqu : qU u = 1 :=
691 (U := U) (x := u)).2 hu
692 rw [hqu, mul_one]
693 let qHK : ↥(H : Subgroup Q) →ₜ* qK0.toMonoidHom.range :=
694 { toMonoidHom := qU.toMonoidHom.comp H.subtype |>.codRestrict
695 qK0.toMonoidHom.range hqH_mem_Krange
696 continuous_toFun :=
697 (qU.continuous.comp continuous_subtype_val).subtype_mk hqH_mem_Krange }
698 have hyK :
699 qHK y ∈ topDerivedTop qK0.toMonoidHom.range (m - 1) := by
700 exact topDerived_map_le (f := qHK) (m := m - 1) ⟨y, hy, rfl⟩
701 have hqy_one : (qU y.1) = 1 := by
702 have hybot : qHK y ∈ (⊥ : Subgroup qK0.toMonoidHom.range) := by
703 simpa [hKrange_bot] using hyK
704 have hsub : qHK y = 1 := by
705 simpa using hybot
706 exact congrArg Subtype.val hsub
707 have hqd_one : qU d = 1 := by
708 rw [← hyd]
709 exact hqy_one
710 exact
712 (U := U) (x := d)).mp hqd_one
713 let Bot : ClosedSubgroup Q := ⊥
714 letI : ((Bot : Subgroup Q).Normal) := by
715 change (⊥ : Subgroup Q).Normal
716 infer_instance
717 have hdbot : d ∈ (Bot : Subgroup Q) := by
719 simp only [Subgroup.mem_sInf, Set.mem_setOf_eq]
720 intro N hN
721 let U : OpenNormalSubgroup Q :=
722 { toOpenSubgroup :=
723 { toSubgroup := N
724 isOpen' := hN.1 }
725 isNormal' := hN.2.2 }
726 exact hd_all U
727 exact Subgroup.mem_bot.mp (by simpa [Bot] using hdbot)
729/-- Topological cyclic generation forces the first derived term to be trivial. -/
731 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
732 [T2Space Q] (x : Q)
733 (hgen : ProCGroups.Generation.TopologicallyGenerates (G := Q) ({x} : Set Q)) :
734 topDerivedTop Q 1 = ⊥ := by
735 have hcyc :
736 (ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) : Subgroup Q) =
737 ⊤ := by
740 have hxcent_top : ProCGroups.GroupTheory.centralizerOf x = ⊤ := by
741 simpa [hcyc] using
743 (G := Q) x (1 : ℤ) hgen
744 have hcomm : ∀ a b : Q, a * b = b * a := by
745 intro a b
746 have hbcx : b ∈ ProCGroups.GroupTheory.centralizerOf x := by
747 simp only [hxcent_top, Subgroup.mem_top]
748 have hx_cb : x ∈ ProCGroups.GroupTheory.centralizerOf b := by
750 exact (ProCGroups.GroupTheory.mem_centralizerOf_iff.mp hbcx).symm
751 have hcyc_le_cb :
752 (ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) : Subgroup Q) ≤
754 exact
756 (G := Q) (S := ({x} : Set Q)) (T := ({b} : Set Q)) (by
757 intro y hy
758 rw [Set.mem_singleton_iff] at hy
759 subst y
761 have ha_cb : a ∈ ProCGroups.GroupTheory.centralizerOf b := by
762 have : a ∈ (ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) :
763 Subgroup Q) := by
764 rw [hcyc]
765 simp only [Subgroup.mem_top]
766 exact hcyc_le_cb this
767 exact ProCGroups.GroupTheory.mem_centralizerOf_iff.mp ha_cb
768 letI : CommGroup Q := { (inferInstance : Group Q) with
769 mul_comm := hcomm }
770 have hcommutator_bot : ⁅(⊤ : Subgroup Q), (⊤ : Subgroup Q)⁆ = ⊥ := by
771 rw [Subgroup.commutator_eq_bot_iff_le_centralizer]
772 intro a _
773 rw [Subgroup.mem_centralizer_iff]
774 intro b _
775 exact hcomm b a
776 change closedCommutator (⊤ : Subgroup Q) (⊤ : Subgroup Q) = ⊥
777 dsimp [closedCommutator]
778 rw [hcommutator_bot]
779 apply le_antisymm
780 · exact
781 Subgroup.topologicalClosure_minimal
782 (s := (⊥ : Subgroup Q)) (t := (⊥ : Subgroup Q)) le_rfl
783 (isClosed_singleton (x := (1 : Q)))
784 · exact Subgroup.le_topologicalClosure (s := (⊥ : Subgroup Q))
786/-- The induced map on maximal finite-step solvable quotients. -/
788 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
789 {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
790 (f : G →ₜ* Q) (m : ℕ) :
791 (G^ₘ m) →ₜ* (Q^ₘ m) := by
792 exact QuotientGroup.mapₜ (G⟦m⟧ₜ) (Q⟦m⟧ₜ) f (topDerivedTop_le_comap (f := f) m)
794scoped[ProCGroupsSolvableQuotients] notation f "⟪" m "⟫" =>
797open scoped ProCGroupsSolvableQuotients
799/-- The induced map on finite-step solvable quotients is an equivalence under surjectivity and the
800expected kernel condition on a subgroup preimage. -/
801noncomputable def TopologicalGroup.restrictPreimage_topMaxSolvQuot_mulEquiv
802 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
803 {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
804 {π : G →ₜ* Q} {Q₁ : Subgroup Q} {m : ℕ}
805 (hπ : Function.Surjective π)
806 (hclosed : IsClosedMap (π.restrictPreimage Q₁))
807 (hker :
808 (π.restrictPreimage Q₁).ker ≤
809 topDerivedTop ↥(Q₁.comap (π : G →* Q)) m) :
810 MaxSolvQuot (Q₁.comap (π : G →* Q)) m ≃* MaxSolvQuot Q₁ m := by
811 classical
812 let G0 : Type u := Q₁.comap (π : G →* Q)
813 let f : G0 →ₜ* Q₁ := π.restrictPreimage Q₁
814 have hf : Function.Surjective f := by
815 simpa [f, G0] using π.restrictPreimage_surjective hπ Q₁
816 have hclosed' : IsClosedMap f := by
817 simpa [f, G0] using hclosed
818 have hker' : f.toMonoidHom.ker ≤ topDerivedTop G0 m := by
819 simpa [f, G0] using hker
820 have hclosed_comm :
821 ∀ n : ℕ,
822 IsClosed (((⁅G0⟦n⟧ₜ, G0⟦n⟧ₜ⁆ₜ).map (f : G0 →* Q₁) : Subgroup Q₁) : Set Q₁) := by
823 intro n
824 refine
826 (K := ⁅G0⟦n⟧ₜ, G0⟦n⟧ₜ⁆ₜ) ?_
827 exact Subgroup.isClosed_topologicalClosure (s := ⁅G0⟦n⟧ₜ, G0⟦n⟧ₜ⁆)
828 have hmap : (G0⟦m⟧ₜ).map (f : G0 →* Q₁) = Q₁⟦m⟧ₜ :=
829 topDerived_map_eq_of_surj (f := f) hf hclosed_comm m
830 have hcomap_eq :
831 Subgroup.comap (f : G0 →* Q₁) (Q₁⟦m⟧ₜ) = G0⟦m⟧ₜ := by
832 exact
834 (f := (f : G0 →* Q₁)) (N := G0⟦m⟧ₜ) (M := Q₁⟦m⟧ₜ) hmap hker'
835 have hsurj :
836 Function.Surjective ((f⟪m⟫) : MaxSolvQuot G0 m → MaxSolvQuot Q₁ m) := by
837 have hcomp :
838 Function.Surjective
839 (fun x : G0 =>
840 (QuotientGroup.mk : Q₁ → (Q₁ ⧸ Q₁⟦m⟧ₜ)) (f x)) :=
841 (QuotientGroup.mk_surjective (s := Q₁⟦m⟧ₜ)).comp hf
843 exact
844 QuotientGroup.map_surjective_of_surjective
845 (N := G0⟦m⟧ₜ)
846 (M := Q₁⟦m⟧ₜ)
847 (f := (f : G0 →* Q₁))
848 (h := topDerivedTop_le_comap (f := f) m)
849 hcomp
850 have hker_eq_bot : (f⟪m⟫).toMonoidHom.ker = ⊥ := by
851 have hker0 :
852 (QuotientGroup.map
853 (N := G0⟦m⟧ₜ)
854 (M := Q₁⟦m⟧ₜ)
855 (f := (f : G0 →* Q₁))
856 (topDerivedTop_le_comap (f := f) m)).ker = ⊥ := by
857 exact
859 (f := (f : G0 →* Q₁))
860 (N := G0⟦m⟧ₜ) (M := Q₁⟦m⟧ₜ)
861 (h := topDerivedTop_le_comap (f := f) m)
862 hcomap_eq
864 exact hker0
865 have hinj :
866 Function.Injective ((f⟪m⟫) : MaxSolvQuot G0 m → MaxSolvQuot Q₁ m) := by
867 have hinj0 : Function.Injective (f⟪m⟫).toMonoidHom :=
868 (MonoidHom.ker_eq_bot_iff (f := (f⟪m⟫).toMonoidHom)).1 hker_eq_bot
869 exact hinj0
870 exact MulEquiv.ofBijective (((π.restrictPreimage Q₁)⟪m⟫).toMonoidHom)
871 ⟨hinj, hsurj⟩
873/-- The quotient map to the maximal `m`-step solvable quotient is surjective. -/
875 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
876 (m : ℕ) :
877 Function.Surjective (continuousToMaxSolvQuot G m) := by
878 change Function.Surjective (toMaxSolvQuot G m)
879 exact QuotientGroup.mk_surjective (s := topDerivedTop G m)
881/-- The quotient map kills exactly the `m`th closed derived subgroup. -/
883 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
884 {m : ℕ} {x : G} :
885 continuousToMaxSolvQuot G m x = 1 ↔ x ∈ topDerivedTop G m := by
886 change toMaxSolvQuot G m x = 1 ↔ x ∈ topDerivedTop G m
887 exact QuotientGroup.eq_one_iff (N := topDerivedTop G m) x
889/-- The kernel of the ambient quotient map lands in the first closed derived subgroup of any
890preimage open subgroup containing the previous derived term. -/
892 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
893 {m : ℕ} (hm : 1 ≤ m)
894 (H : OpenSubgroup (MaxSolvQuot G m))
895 (hH :
896 topDerivedTop G (m - 1) ≤
897 ((H : Subgroup (MaxSolvQuot G m)).comap
898 (continuousToMaxSolvQuot G m : G →* MaxSolvQuot G m))) :
901 ↥((preimageOpenSubgroup (continuousToMaxSolvQuot G m) H : OpenSubgroup G) :
902 Subgroup G) 1).map
903 (Subgroup.subtype
904 ((preimageOpenSubgroup (continuousToMaxSolvQuot G m) H : OpenSubgroup G) :
905 Subgroup G)) := by
906 let Q : Type u := MaxSolvQuot G m
907 let π : G →ₜ* Q := continuousToMaxSolvQuot G m
908 let Hpre : OpenSubgroup G := preimageOpenSubgroup π H
909 have hHpreOpen : IsOpen ((Hpre : Subgroup G) : Set G) := Hpre.isOpen'
910 intro x hx
911 have hxder : x ∈ topDerivedTop G m := by
912 exact
913 (continuousToMaxSolvQuot_eq_one_iff (G := G) (m := m) (x := x)).1
914 ((MonoidHom.mem_ker).1 hx)
915 have hxder' :
916 x ∈ closedDerivedSeries (G := G)
917 ((H : Subgroup Q).comap (π : G →* Q)) 1 := by
918 simpa [π, Q] using
920 (by simpa [π, Q] using hH) hxder)
921 have htopMap :
922 ((⊤ : Subgroup ↥((H : Subgroup Q).comap (π : G →* Q))).map
923 ((Subgroup.comap (π : G →* Q) H).subtype)) =
924 (H : Subgroup Q).comap (π : G →* Q) := by
925 ext x
926 constructor
927 · rintro ⟨y, -, rfl⟩
928 exact y.2
929 · intro hx'
930 exact ⟨⟨x, hx'⟩, by simp only [Subgroup.coe_top, Set.mem_univ], rfl⟩
931 have hmap :
932 (topDerivedTop ↥((Hpre : Subgroup G)) 1).map ((Hpre : Subgroup G).subtype) =
933 closedDerivedSeries (G := G) ((H : Subgroup Q).comap (π : G →* Q)) 1 := by
934 have hmap0 :=
936 (G := G)
937 (H := ((H : Subgroup Q).comap (π : G →* Q)))
938 (K := (⊤ : Subgroup ↥((H : Subgroup Q).comap (π : G →* Q))))
939 (Subgroup.isClosed_of_isOpen _ hHpreOpen)
940 rw [htopMap] at hmap0
941 simpa [Hpre, π] using hmap0
942 change x ∈ (topDerivedTop ↥((Hpre : Subgroup G)) 1).map ((Hpre : Subgroup G).subtype)
943 rw [hmap]
944 exact hxder'
946/-- The first maximal solvable quotient is the topological abelianization. -/
948 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
949 (hG : IsMulTorsionFree (TopologicalAbelianization G)) :
950 IsMulTorsionFree (MaxSolvQuot G 1) := by
951 simpa [MaxSolvQuot, TopologicalAbelianization, topDerivedTop, closedDerivedSeries,
952 closedCommutator] using hG
954/-- The induced map between maximal finite-step solvable quotients of a subgroup preimage and the
955target subgroup is an isomorphism under the expected kernel bound. -/
957 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
958 {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
959 (f : G →ₜ* Q) (hf : Function.Surjective f) (H : OpenSubgroup Q)
960 (hclosed : IsClosedMap (f.restrictPreimage (H : Subgroup Q)))
961 (n : ℕ)
962 (hker :
963 f.ker ≤
965 ↥((preimageOpenSubgroup f H : OpenSubgroup G) : Subgroup G) n).map
966 (Subgroup.subtype
967 ((preimageOpenSubgroup f H : OpenSubgroup G) : Subgroup G))) :
968 Nonempty
969 (MaxSolvQuot ↥((preimageOpenSubgroup f H : OpenSubgroup G) : Subgroup G) n ≃*
970 MaxSolvQuot ↥(H : Subgroup Q) n) := by
971 let Hpre : OpenSubgroup G := preimageOpenSubgroup f H
972 have hker' :
973 (f.restrictPreimage (H : Subgroup Q)).ker ≤
974 topDerivedTop ↥((Hpre : Subgroup G)) n := by
975 intro x hx
976 have hxker : x.1 ∈ f.ker := by
977 change f.restrictPreimage (H : Subgroup Q) x = 1 at hx
978 change f x.1 = 1
979 exact congrArg Subtype.val hx
980 have hxder :
981 x.1 ∈
982 (topDerivedTop ↥((Hpre : Subgroup G)) n).map
983 ((Hpre : Subgroup G).subtype) :=
984 hker hxker
985 rcases hxder with ⟨y, hy, hyx⟩
986 exact Subtype.ext hyx ▸ hy
987 exact
988 ⟨TopologicalGroup.restrictPreimage_topMaxSolvQuot_mulEquiv
989 (π := f) (Q₁ := (H : Subgroup Q)) (m := n) hf hclosed hker'⟩
991end ProCGroups.FiniteStepSolvableQuotients