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

Source: ProCGroups.FiniteStepSolvableQuotients.Commutators.DerivedSeriesAndQuotients

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/-!
9# Closed derived series and solvable quotients
11This module defines the closed derived series of a topological group and its maximal finite-step
12solvable quotients. It also records functoriality, closedness, and normality properties used to
13compare these quotients under continuous homomorphisms.
14-/
16universe u v
18namespace TopologicalGroup
23/-- Closed-map properties descend to the restriction to a subgroup preimage. -/
24lemma restrictPreimage_isClosedMap_of_isClosedMap
25 {G : Type u} [TopologicalSpace G] [Group G]
26 {Q : Type v} [TopologicalSpace Q] [Group Q]
27 (π : G →ₜ* Q) (Q₁ : Subgroup Q)
28 (hπ : IsClosedMap π)
29 (hQ₁ : IsClosed (Q₁ : Set Q)) :
31 let G₁ : Subgroup G := Q₁.comap (π : G →* Q)
32 have hG₁ : IsClosed (G₁ : Set G) := hQ₁.preimage π.continuous
33 intro s hs
34 have hsG : IsClosed (((G₁ : Subgroup G).subtype : G₁ → G) '' s) :=
35 hG₁.isClosedMap_subtype_val _ hs
36 have himg :
37 IsClosed ((fun x : G => π x) '' (((G₁ : Subgroup G).subtype : G₁ → G) '' s)) :=
38 hπ _ hsG
39 refine
40 (hQ₁.isClosedEmbedding_subtypeVal.isClosed_iff_image_isClosed).2 ?_
41 change IsClosed ((fun y : Q₁ => (y : Q)) '' ((ProCGroups.ContinuousMonoidHom.restrictPreimage
42 π Q₁) '' s))
43 have hEq :
44 (fun y : Q₁ => (y : Q)) '' ((ProCGroups.ContinuousMonoidHom.restrictPreimage π Q₁) '' s) =
45 (fun x : G => π x) '' ((G₁.subtype : G₁ → G) '' s) := by
46 ext y
47 constructor
48 · rintro ⟨z, ⟨x, hx, rfl⟩, rfl⟩
49 exact ⟨x, ⟨x, hx, rfl⟩, rfl⟩
50 · rintro ⟨x, ⟨z, hz, rfl⟩, rfl⟩
51 exact ⟨ProCGroups.ContinuousMonoidHom.restrictPreimage π Q₁ z, ⟨z, hz, rfl⟩, rfl⟩
52 rw [hEq]
53 exact himg
55/--
56If the image of a subgroup is contained in a closed subgroup, then the image of its closure is
57contained there as well.
58-/
59lemma map_closure_le_of_map_le
60 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
61 {Q : Type v} [TopologicalSpace Q] [Group Q]
62 {G₁ : Subgroup G} {Q₁ : Subgroup Q} {f : G →ₜ* Q}
63 (h₁ : G₁.map (f : G →* Q) ≤ Q₁)
64 (hclosed : IsClosed (Q₁ : Set Q)) :
65 (G₁.topologicalClosure).map (f : G →* Q) ≤ Q₁ := by
66 have hMapsTo : Set.MapsTo (fun x : G => f x) (G₁ : Set G) (Q₁ : Set Q) := by
67 intro x hx
68 exact h₁ ⟨x, hx, rfl⟩
69 have hMapsTo_cl :
70 Set.MapsTo (fun x : G => f x) (_root_.closure (G₁ : Set G)) (Q₁ : Set Q) :=
71 Set.MapsTo.closure_left hMapsTo f.continuous hclosed
72 rintro y ⟨x, hx, rfl⟩
73 exact hMapsTo_cl hx
75/-- The image of a closure is contained in the closure of the image. -/
76lemma map_closure_le_closure
77 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
78 {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
79 {G₁ : Subgroup G} {Q₁ : Subgroup Q} (f : G →ₜ* Q)
80 (h₁ : G₁.map (f : G →* Q) ≤ Q₁) :
81 (G₁.topologicalClosure).map (f : G →* Q) ≤ Q₁.topologicalClosure := by
82 refine
83 map_closure_le_of_map_le (f := f) (G₁ := G₁) (Q₁ := Q₁.topologicalClosure) ?_ ?_
84 · exact le_trans h₁ (Subgroup.le_topologicalClosure (s := Q₁))
85 · exact Subgroup.isClosed_topologicalClosure (s := Q₁)
87/-- Closed maps send closed subgroups to closed images. -/
88lemma isClosed_map_of_isClosedMap
89 {G : Type u} [TopologicalSpace G] [Group G]
90 {H : Type v} [TopologicalSpace H] [Group H]
91 (f : G →ₜ* H) (hclosed : IsClosedMap f)
92 (K : Subgroup G) (hK : IsClosed (K : Set G)) :
93 IsClosed (((K.map (f : G →* H) : Subgroup H) : Set H)) := by
94 have him : IsClosed ((fun x : G => f x) '' (K : Set G)) := hclosed _ hK
95 have hEq :
96 (fun x : G => f x) '' (K : Set G)
97 = (((K.map (f : G →* H) : Subgroup H) : Set H)) := by
98 exact image_subtype_eq_map (f := (f : G →* H)) (K := K)
99 exact hEq ▸ him
101/-- The kernel of the induced map is trivial under the stated comap equality hypothesis. -/
102lemma ker_map_eq_bot_of_comap_eq
103 {G : Type u} [Group G]
104 {H : Type v} [Group H]
105 {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
106 (f : G →* H) (h : N ≤ M.comap f) (hcomap : M.comap f = N) :
107 (QuotientGroup.map (N := N) (M := M) (f := f) h).ker = ⊥ := by
108 calc
109 (QuotientGroup.map (N := N) (M := M) (f := f) h).ker =
110 Subgroup.map (QuotientGroup.mk' N) (Subgroup.comap f M) := by
111 simpa using QuotientGroup.ker_map (N := N) (M := M) (f := f) h
112 _ = Subgroup.map (QuotientGroup.mk' N) N := by simp only [hcomap, QuotientGroup.map_mk'_self]
113 _ = ⊥ := by
114 refine (Subgroup.map_eq_bot_iff (f := QuotientGroup.mk' N) (H := N)).2 ?_
115 intro x hx
116 simpa using hx
118end TopologicalGroup
120namespace MulEquiv
122/-- Multiplicative equivalences transport torsion-freeness. -/
123theorem isMulTorsionFree
124 {M : Type u} [Monoid M]
125 {N : Type v} [Monoid N]
126 (e : M ≃* N) [IsMulTorsionFree M] :
127 IsMulTorsionFree N := by
128 exact Function.Injective.isMulTorsionFree (e.symm : N →* M) e.symm.injective
130end MulEquiv
132namespace ProCGroups.FiniteStepSolvableQuotients
134/-- The closed commutator subgroup of a topological group. -/
135abbrev closedCommutator
136 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
137 (H K : Subgroup G) : Subgroup G :=
138 (⁅H, K⁆).topologicalClosure
140/-- The closed derived series starting from a subgroup. -/
141def closedDerivedSeries
142 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
143 (K : Subgroup G) : ℕ → Subgroup G
144 | 0 => K
145 | n + 1 => closedCommutator (closedDerivedSeries K n) (closedDerivedSeries K n)
147/-- The `m`th closed derived subgroup of the whole topological group `G`. -/
148abbrev topDerivedTop
149 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
150 (m : ℕ) : Subgroup G :=
151 closedDerivedSeries (G := G) (⊤ : Subgroup G) m
153/-- Every term in the closed derived series of `G` is a closed subgroup. -/
154instance topDerivedTop_isClosedInst
155 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
156 {m : ℕ} :
157 IsClosed (topDerivedTop G m : Set G) := by
158 cases m with
159 | zero =>
160 change IsClosed ((⊤ : Subgroup G) : Set G)
161 exact isClosed_univ
162 | succ m =>
163 simp only [topDerivedTop, closedDerivedSeries, closedCommutator]
164 exact isClosed_closure
166/-- Every term in the closed derived series of `G` is a normal subgroup. -/
167instance topDerivedTop_normalInst
168 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
169 {m : ℕ} :
170 (topDerivedTop G m).Normal := by
171 induction m with
172 | zero =>
173 change (⊤ : Subgroup G).Normal
174 infer_instance
175 | succ m ihm =>
176 dsimp [topDerivedTop, closedDerivedSeries, closedCommutator]
177 letI : (topDerivedTop G m).Normal := ihm
178 exact Subgroup.is_normal_topologicalClosure ⁅topDerivedTop G m, topDerivedTop G m⁆
180/-- The quotient by the mth closed derived subgroup. -/
181abbrev MaxSolvQuot
182 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
183 (m : ℕ) : Type u :=
184 G ⧸ topDerivedTop G m
186/-- The natural quotient map to the maximal \(m\)-step solvable quotient. -/
187abbrev toMaxSolvQuot
188 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
189 (m : ℕ) :
190 G →* MaxSolvQuot G m :=
191 QuotientGroup.mk' (topDerivedTop G m)
193/-- The natural quotient map as a continuous homomorphism. -/
194abbrev continuousToMaxSolvQuot
195 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
196 (m : ℕ) :
197 G →ₜ* MaxSolvQuot G m :=
198 { toMonoidHom := toMaxSolvQuot G m
199 continuous_toFun := continuous_quotient_mk' }
201/-- The preimage open subgroup induced by a continuous homomorphism. -/
202abbrev preimageOpenSubgroup
203 {G : Type u} [TopologicalSpace G] [Group G]
204 {Q : Type v} [TopologicalSpace Q] [Group Q]
205 (f : G →ₜ* Q) (H : OpenSubgroup Q) : OpenSubgroup G :=
206 OpenSubgroup.comap (f := (f : G →* Q)) f.continuous H
208scoped[ProCGroupsSolvableQuotients] notation "⁅" H "," K "⁆ₜ" =>
210scoped[ProCGroupsSolvableQuotients] notation G "⟦" m "⟧ₜ" =>
212scoped[ProCGroupsSolvableQuotients] notation G "^ₘ" m =>
215open scoped ProCGroupsSolvableQuotients
217/-- The zeroth closed derived subgroup is the whole topological group. -/
218@[simp] lemma closedDerivedSeries_zero
219 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
220 (K : Subgroup G) :
221 closedDerivedSeries (G := G) K 0 = K := rfl
223/--
224The successor closed derived subgroup is the closed commutator subgroup of the previous derived
225stage.
226-/
227@[simp] lemma closedDerivedSeries_succ
228 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
229 (K : Subgroup G) (n : ℕ) :
230 closedDerivedSeries (G := G) K (n + 1) =
231 ⁅closedDerivedSeries (G := G) K n, closedDerivedSeries (G := G) K n⁆ₜ := rfl
233/-- The zeroth term of the ambient closed derived series is the whole ambient group. -/
234@[simp] lemma topDerivedTop_zero
235 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
236 G⟦0⟧ₜ = (⊤ : Subgroup G) := rfl
238/--
239The successor term of the ambient closed derived series is the closed commutator subgroup of the
240previous term.
241-/
242@[simp] lemma topDerivedTop_succ
243 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
244 (n : ℕ) :
245 G⟦n + 1⟧ₜ = ⁅G⟦n⟧ₜ, G⟦n⟧ₜ⁆ₜ := rfl
247/-- Closed commutators map monotonically under continuous homomorphisms. -/
248theorem closedCommutator_map_mono
249 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
250 {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
251 {G₁ G₂ : Subgroup G} {Q₁ Q₂ : Subgroup Q} {f : G →ₜ* Q}
252 (h₁ : G₁.map (f : G →* Q) ≤ Q₁)
253 (h₂ : G₂.map (f : G →* Q) ≤ Q₂) :
254 (⁅G₁, G₂⁆ₜ).map (f : G →* Q) ≤ ⁅Q₁, Q₂⁆ₜ := by
255 dsimp [closedCommutator]
256 have hcomm :
257 (⁅G₁, G₂⁆).map (f : G →* Q) ≤ ⁅Q₁, Q₂⁆ := by
258 calc
259 (⁅G₁, G₂⁆).map (f : G →* Q) = ⁅G₁.map (f : G →* Q), G₂.map (f : G →* Q)⁆ := by
260 simpa using Subgroup.map_commutator G₁ G₂ (f : G →* Q)
261 _ ≤ ⁅Q₁, Q₂⁆ := Subgroup.commutator_mono h₁ h₂
262 exact TopologicalGroup.map_closure_le_closure (f := f) (G₁ := ⁅G₁, G₂⁆) (Q₁ := ⁅Q₁, Q₂⁆) hcomm
264/--
265If target subgroups lie in the corresponding images, then their commutator lies in the image of
266the source closed commutator.
267-/
268lemma commutator_le_map_closedCommutator
269 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
270 {Q : Type v} [Group Q]
271 (φ : G →* Q)
272 {G₁ G₂ : Subgroup G} {Q₁ Q₂ : Subgroup Q}
273 (h₁ : Q₁ ≤ G₁.map φ) (h₂ : Q₂ ≤ G₂.map φ) :
274 ⁅Q₁, Q₂⁆ ≤ (⁅G₁, G₂⁆ₜ).map φ := by
275 have h0 :
276 ⁅Q₁, Q₂⁆ ≤ (⁅G₁, G₂⁆).map φ :=
277 Subgroup.commutator_le_map_commutator
278 (f := φ) (H₁ := G₁) (H₂ := G₂) (K₁ := Q₁) (K₂ := Q₂) h₁ h₂
279 have hmono :
280 (⁅G₁, G₂⁆).map φ ≤ (⁅G₁, G₂⁆ₜ).map φ := by
281 simpa [closedCommutator] using
282 Subgroup.map_mono (f := φ) (Subgroup.le_topologicalClosure (s := ⁅G₁, G₂⁆))
283 exact le_trans h0 hmono
285/--
286The map carries the closed commutator subgroup to the corresponding closed commutator subgroup
287under the stated equality hypothesis.
288-/
289theorem map_closedCommutator_eq_of_map_eq
290 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
291 {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
292 {G₁ G₂ : Subgroup G} {Q₁ Q₂ : Subgroup Q} {f : G →ₜ* Q}
293 (h₁ : G₁.map (f : G →* Q) = Q₁)
294 (h₂ : G₂.map (f : G →* Q) = Q₂)
295 (hclosed : IsClosed (((⁅G₁,G₂⁆ₜ).map (f : G →* Q) : Subgroup Q) : Set Q)) :
296 (⁅G₁, G₂⁆ₜ).map (f : G →* Q) = ⁅Q₁, Q₂⁆ₜ := by
297 let φ : G →* Q := (f : G →* Q)
298 have hle : (⁅G₁, G₂⁆ₜ).map φ ≤ ⁅Q₁, Q₂⁆ₜ := by
299 simpa [φ] using
300 closedCommutator_map_mono (f := f)
301 (h₁ := by simpa using le_of_eq h₁)
302 (h₂ := by simpa using le_of_eq h₂)
303 have hge : ⁅Q₁, Q₂⁆ₜ ≤ (⁅G₁, G₂⁆ₜ).map φ := by
304 dsimp [closedCommutator]
305 refine
306 Subgroup.topologicalClosure_minimal
307 (s := ⁅Q₁, Q₂⁆) (t := (⁅G₁, G₂⁆ₜ).map φ) ?_ hclosed
308 refine commutator_le_map_closedCommutator (φ := φ) (G₁ := G₁) (G₂ := G₂) ?_ ?_
309 · simpa [φ] using ge_of_eq h₁
310 · simpa [φ] using ge_of_eq h₂
311 exact le_antisymm hle (by simpa [closedCommutator] using hge)
313/--
314Closed commutators of topologically characteristic subgroups are again topologically
315characteristic.
316-/
317theorem closedCommutator_topologicallyCharacteristic
318 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
319 (G₁ G₂ : Subgroup G)
320 (h₁ : G₁.TopologicallyCharacteristic)
321 (h₂ : G₂.TopologicallyCharacteristic) :
322 (⁅G₁, G₂⁆ₜ).TopologicallyCharacteristic := by
323 letI : G₁.TopologicallyCharacteristic := h₁
324 letI : G₂.TopologicallyCharacteristic := h₂
325 have hcomm : (⁅G₁, G₂⁆).TopologicallyCharacteristic := by
326 infer_instance
327 simpa [closedCommutator] using
329 (H := ⁅G₁, G₂⁆) (hH := hcomm))
331/-- Restarting the ambient closed derived series adds indices. -/
332@[simp] lemma topDerived_add
333 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
334 (m n : ℕ) :
335 closedDerivedSeries (G := G) (G⟦m⟧ₜ) n = G⟦m + n⟧ₜ := by
336 induction n with
337 | zero =>
338 simp only [closedDerivedSeries_zero, add_zero]
339 | succ n ihn =>
340 rw [show m + (n + 1) = m + n + 1 by rw [Nat.add_assoc]]
341 rw [topDerivedTop_succ]
342 simp only [closedDerivedSeries_succ, ihn]
344/-- The ambient closed derived series is antitone. -/
345theorem topDerivedTop_antitone
346 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
347 Antitone (topDerivedTop G) := by
348 apply antitone_nat_of_succ_le
349 intro m
350 dsimp [topDerivedTop, closedDerivedSeries, closedCommutator]
351 exact
352 Subgroup.topologicalClosure_minimal
353 (s := ⁅G⟦m⟧ₜ, G⟦m⟧ₜ⁆)
354 (t := G⟦m⟧ₜ)
355 (Subgroup.commutator_le_self (G⟦m⟧ₜ))
356 (by infer_instance)
358/-- Every stage of the ambient closed derived series is topologically characteristic. -/
359instance topDerivedTop_topologicallyCharacteristicInst
360 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
361 {m : ℕ} :
362 (topDerivedTop G m).TopologicallyCharacteristic := by
363 induction m with
364 | zero =>
365 refine ⟨?_⟩
366 intro e
367 simp only [ContinuousMulEquiv.toMulEquiv_eq_coe, MulEquiv.toMonoidHom_eq_coe, topDerivedTop,
368 closedDerivedSeries_zero, Subgroup.comap_top]
369 | succ m ihm =>
370 simpa [topDerivedTop, closedDerivedSeries] using
371 closedCommutator_topologicallyCharacteristic
372 (G₁ := G⟦m⟧ₜ) (G₂ := G⟦m⟧ₜ) ihm ihm
374/-- The closed derived series is monotone under continuous homomorphisms. -/
375theorem topDerived_map_le
376 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
377 {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
378 (f : G →ₜ* Q) (m : ℕ) :
379 (G⟦m⟧ₜ).map (f : G →* Q) ≤ Q⟦m⟧ₜ := by
380 induction m with
381 | zero =>
382 simp only [topDerivedTop, closedDerivedSeries_zero, le_top]
383 | succ m ih =>
384 dsimp [topDerivedTop, closedDerivedSeries, closedCommutator]
385 exact
387 (G₁ := ⁅G⟦m⟧ₜ, G⟦m⟧ₜ⁆)
388 (Q₁ := ⁅Q⟦m⟧ₜ, Q⟦m⟧ₜ⁆) <|
389 by
390 calc
391 (⁅G⟦m⟧ₜ, G⟦m⟧ₜ⁆).map (f : G →* Q)
392 = ⁅(G⟦m⟧ₜ).map (f : G →* Q), (G⟦m⟧ₜ).map (f : G →* Q)⁆ := by
393 simpa using
394 (Subgroup.map_commutator (G⟦m⟧ₜ) (G⟦m⟧ₜ) (f : G →* Q))
395 _ ≤ ⁅Q⟦m⟧ₜ, Q⟦m⟧ₜ⁆ := by
396 exact Subgroup.commutator_mono ih ih)
398/-- The ambient closed derived series pulls back along continuous homomorphisms. -/
399lemma topDerivedTop_le_comap
400 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
401 {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
402 (f : G →ₜ* Q) (m : ℕ) :
403 G⟦m⟧ₜ ≤ (Q⟦m⟧ₜ).comap (f : G →* Q) := by
404 exact (Subgroup.map_le_iff_le_comap).1 (topDerived_map_le (f := f) m)
406/--
407A point in the ambient \(m\)-th derived subgroup lies in the first derived subgroup of any
408larger subgroup containing the \((m-1)\)-st derived term.
409-/
410theorem mem_topDerived_one_of_mem_topDerived_of_le
411 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
412 {K : Subgroup G} {m : ℕ} (hm : 1 ≤ m)
413 (hK : G⟦m - 1⟧ₜ ≤ K)
414 {x : G} (hx : x ∈ G⟦m⟧ₜ) :
415 x ∈ closedDerivedSeries (G := G) K 1 := by
416 have hmEq : m = (m - 1) + 1 := (tsub_add_cancel_of_le hm).symm
417 have hx0 : x ∈ G⟦(m - 1) + 1⟧ₜ := hmEq ▸ hx
418 rw [← topDerived_add (G := G) (m := m - 1) (n := 1)] at hx0
419 have hmono :
420 closedDerivedSeries (G := G) (G⟦m - 1⟧ₜ) 1 ≤ closedDerivedSeries (G := G) K 1 := by
421 dsimp [closedDerivedSeries, closedCommutator]
422 refine
423 Subgroup.topologicalClosure_minimal
424 (s := ⁅G⟦m - 1⟧ₜ, G⟦m - 1⟧ₜ⁆)
425 (t := ⁅K, K⁆ₜ) ?_
426 (Subgroup.isClosed_topologicalClosure (s := ⁅K, K⁆))
427 exact (Subgroup.commutator_mono hK hK).trans (Subgroup.le_topologicalClosure _)
428 exact hmono hx0
430/--
431The first derived subgroup of a closed subgroup maps back to the corresponding subgroup of the
432ambient group.
433-/
434theorem topDerived_one_map_subtype_eq_of_isClosed_subgroup
435 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
436 {H : Subgroup G} {K : Subgroup H} (hH : IsClosed (H : Set G)) :
437 (closedDerivedSeries (G := H) K 1).map H.subtype =
438 closedDerivedSeries (G := G) (K.map H.subtype) 1 := by
439 have hclosedSubtype : IsClosedMap (H.subtype : H → G) := hH.isClosedMap_subtype_val
440 have hclosure :
441 closure ((fun y : H => (y : G)) '' (((⁅K, K⁆ : Subgroup H) : Set H))) =
442 (fun y : H => (y : G)) '' closure (((⁅K, K⁆ : Subgroup H) : Set H)) :=
443 hclosedSubtype.closure_image_eq_of_continuous continuous_subtype_val _
444 have himg :
445 ((fun y : H => (y : G)) '' (((⁅K, K⁆ : Subgroup H) : Set H))) =
446 (((⁅K.map H.subtype, K.map H.subtype⁆ : Subgroup G) : Set G)) := by
448 congrArg (fun L : Subgroup G => (L : Set G))
449 (Subgroup.map_commutator K K H.subtype)
450 ext x
451 change
452 x ∈ ((fun y : H => (y : G)) '' ((((⁅K, K⁆).topologicalClosure : Subgroup H) : Set H))) ↔
453 x ∈ (((⁅K.map H.subtype, K.map H.subtype⁆).topologicalClosure : Subgroup G) : Set G)
454 change
455 x ∈ ((fun y : H => (y : G)) '' closure (((⁅K, K⁆ : Subgroup H) : Set H))) ↔
456 x ∈ closure (((⁅K.map H.subtype, K.map H.subtype⁆ : Subgroup G) : Set G))
457 rw [← hclosure, himg]
459/--
460Surjective maps identify the stagewise closed derived subgroups once the commutator images are
461closed.
462-/
463theorem topDerived_map_eq_of_surj
464 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
465 {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
466 (f : G →ₜ* H) (hf : Function.Surjective f)
467 (hclosed_comm :
468 ∀ n : ℕ,
469 IsClosed (((⁅G⟦n⟧ₜ, G⟦n⟧ₜ⁆ₜ).map (f : G →* H) : Subgroup H) : Set H))
470 (n : ℕ) :
471 (G⟦n⟧ₜ).map (f : G →* H) = H⟦n⟧ₜ := by
472 induction n with
473 | zero =>
474 ext y
475 constructor
476 · rintro ⟨x, -, rfl⟩
477 simp only [topDerivedTop, closedDerivedSeries_zero, MonoidHom.coe_coe, Subgroup.mem_top]
478 · intro hy
479 rcases hf y with ⟨x, rfl⟩
480 exact ⟨x, by simp only [topDerivedTop, closedDerivedSeries_zero, Subgroup.coe_top,
481 Set.mem_univ], rfl⟩
482 | succ n ihn =>
483 apply le_antisymm
484 · exact topDerived_map_le (f := f) (m := n + 1)
485 · dsimp [topDerivedTop, closedDerivedSeries, closedCommutator]
486 refine
487 Subgroup.topologicalClosure_minimal
488 (s := ⁅H⟦n⟧ₜ, H⟦n⟧ₜ⁆)
489 (t := (⁅G⟦n⟧ₜ, G⟦n⟧ₜ⁆ₜ).map (f : G →* H)) ?_
490 (hclosed_comm n)
491 calc
492 ⁅H⟦n⟧ₜ, H⟦n⟧ₜ⁆
493 = ⁅(G⟦n⟧ₜ).map (f : G →* H), (G⟦n⟧ₜ).map (f : G →* H)⁆ := by
494 simp only [ihn]
495 _ = (⁅G⟦n⟧ₜ, G⟦n⟧ₜ⁆).map (f : G →* H) := by
496 symm
497 simpa using
498 (Subgroup.map_commutator (G⟦n⟧ₜ) (G⟦n⟧ₜ) (f : G →* H))
499 _ ≤ (⁅G⟦n⟧ₜ, G⟦n⟧ₜ⁆ₜ).map (f : G →* H) := by
500 exact Subgroup.map_mono (Subgroup.le_topologicalClosure _)
502/--
503Images of closed commutators of derived terms are closed when the source is compact and the
504target is Hausdorff.
505-/
506theorem closedCommutator_topDerived_map_isClosed_of_compact
507 {G H : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
508 [CompactSpace G] [TopologicalSpace H] [Group H] [T2Space H]
509 (f : G →ₜ* H) (n : ℕ) :
510 IsClosed
511 (((closedCommutator (topDerivedTop G n) (topDerivedTop G n)).map
512 (f : G →* H) : Subgroup H) : Set H) := by
513 let K : ClosedSubgroup G :=
514 ⟨closedCommutator (topDerivedTop G n) (topDerivedTop G n), by
515 dsimp [closedCommutator]
516 exact isClosed_closure⟩
517 change IsClosed ((((closedCommutator (topDerivedTop G n) (topDerivedTop G n)).map
518 (f : G →* H) : Subgroup H) : Set H))
519 exact
520 (ProCGroups.Order.ClosedSubgroup.map K (f : G →* H) f.continuous_toFun).isClosed'
522/-- The closed derived series is monotone in the initial subgroup. -/
523theorem closedDerivedSeries_mono
524 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
525 {K L : Subgroup G} (hKL : K ≤ L) (n : ℕ) :
526 closedDerivedSeries (G := G) K n ≤ closedDerivedSeries (G := G) L n := by
527 induction n with
528 | zero =>
529 simpa using hKL
530 | succ n ih =>
531 dsimp [closedDerivedSeries, closedCommutator]
532 refine
533 Subgroup.topologicalClosure_minimal
534 (s := ⁅closedDerivedSeries (G := G) K n,
535 closedDerivedSeries (G := G) K n⁆)
536 (t := ⁅closedDerivedSeries (G := G) L n,
537 closedDerivedSeries (G := G) L n⁆ₜ) ?_
538 (Subgroup.isClosed_topologicalClosure
539 (s := ⁅closedDerivedSeries (G := G) L n,
540 closedDerivedSeries (G := G) L n⁆))
541 exact
542 (Subgroup.commutator_mono ih ih).trans
543 (Subgroup.le_topologicalClosure
544 (s := ⁅closedDerivedSeries (G := G) L n,
545 closedDerivedSeries (G := G) L n⁆))
547/--
548The internal derived series of a closed subgroup maps to the corresponding ambient derived
549series.
550-/
551theorem topDerived_map_subtype_eq_closedDerivedSeries_of_isClosed_subgroup
552 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
553 {H : Subgroup G} (hH : IsClosed (H : Set G)) (n : ℕ) :
554 (topDerivedTop H n).map H.subtype =
555 closedDerivedSeries (G := G) H n := by
556 let incl : H →ₜ* G :=
557 { toMonoidHom := H.subtype
558 continuous_toFun := continuous_subtype_val }
559 induction n with
560 | zero =>
561 ext x
562 constructor
563 · rintro ⟨y, -, rfl⟩
564 exact y.2
565 · intro hx
566 exact ⟨⟨x, hx⟩, by simp only [topDerivedTop, closedDerivedSeries_zero, Subgroup.coe_top,
567 Set.mem_univ], rfl⟩
568 | succ n ih =>
569 have hclosed :
570 IsClosed
571 (((closedCommutator (topDerivedTop H n) (topDerivedTop H n)).map
572 (incl : H →* G) : Subgroup G) : Set G) := by
573 exact
575 (f := incl) hH.isClosedMap_subtype_val
576 (K := closedCommutator (topDerivedTop H n) (topDerivedTop H n))
577 (Subgroup.isClosed_topologicalClosure
578 (s := ⁅topDerivedTop H n, topDerivedTop H n⁆))
579 have hmap :=
580 map_closedCommutator_eq_of_map_eq
581 (f := incl) (h₁ := ih) (h₂ := ih) hclosed
582 change
583 (topDerivedTop H (n + 1)).map H.subtype =
584 closedDerivedSeries (G := G) H (n + 1)
585 exact hmap
587/--
588Higher ambient derived terms lie in the corresponding derived term of any open subgroup
589containing the first derived term.
590-/
591theorem topDerivedTop_le_openSubgroup_pred_map_of_first_le
592 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
593 (H : OpenSubgroup G) {m : ℕ} (hm : 1 ≤ m)
594 (hfirst : topDerivedTop G 1 ≤ (H : Subgroup G)) :
595 topDerivedTop G m ≤
596 (topDerivedTop ↥(H : Subgroup G) (m - 1)).map
597 (Subgroup.subtype (H : Subgroup G)) := by
598 have hpred : 1 + (m - 1) = m := by
599 simpa [Nat.add_comm] using
600 Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero (Nat.ne_of_gt hm))
601 intro x hx
602 have htop :
603 closedDerivedSeries (G := G) (topDerivedTop G 1) (m - 1) =
604 topDerivedTop G m := by
605 simpa [hpred] using
606 (topDerived_add (G := G) (m := 1) (n := m - 1))
607 have hxseries :
608 x ∈ closedDerivedSeries (G := G) (topDerivedTop G 1) (m - 1) := by
609 rw [htop]
610 exact hx
611 have hxH :
612 x ∈ closedDerivedSeries (G := G) (H : Subgroup G) (m - 1) :=
613 closedDerivedSeries_mono hfirst (m - 1) hxseries
614 have hHclosed : IsClosed (((H : Subgroup G) : Set G)) :=
616 rw [topDerived_map_subtype_eq_closedDerivedSeries_of_isClosed_subgroup
617 (G := G) (H := (H : Subgroup G)) hHclosed (m - 1)]
618 exact hxH
620/--
621If a profinite element projects into all open-normal derived lifts and the corresponding ambient
622derived term is trivial, then the element is trivial.
623-/
624theorem eq_one_of_mem_all_openNormalSubgroup_derived
625 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
626 [CompactSpace Q] [TotallyDisconnectedSpace Q]
627 {m : ℕ} (hm : 3 ≤ m)
628 (hQm : topDerivedTop Q m = ⊥)
629 {d : Q}
630 (hproj :
631 ∀ H : OpenNormalSubgroup Q,
632 topDerivedTop Q 1 ≤ (H : Subgroup Q) →
633 d ∈ (topDerivedTop ↥(H : Subgroup Q) (m - 1)).map
634 (Subgroup.subtype (H : Subgroup Q))) :
635 d = 1 := by
636 classical
637 have hmpos : 0 < m := lt_of_lt_of_le (by decide : 0 < 3) hm
638 have hpred : 1 + (m - 1) = m := by
639 simpa [Nat.add_comm] using Nat.succ_pred_eq_of_pos hmpos
640 have hd_all : ∀ U : OpenNormalSubgroup Q, d ∈ (U : Subgroup Q) := by
641 intro U
642 let qU : Q →ₜ* Q ⧸ (U : Subgroup Q) :=
644 let K : Subgroup Q := topDerivedTop Q 1
645 have hKnormal : K.Normal := by
646 change (topDerivedTop Q 1).Normal
647 infer_instance
648 letI : K.Normal := hKnormal
649 let Hsub : Subgroup Q := K ⊔ (U : Subgroup Q)
650 have hHopen : IsOpen (Hsub : Set Q) := by
651 exact
652 Subgroup.isOpen_of_openSubgroup Hsub
653 (show (U : Subgroup Q) ≤ Hsub from le_sup_right)
654 let H : OpenNormalSubgroup Q :=
655 { toOpenSubgroup :=
656 { toSubgroup := Hsub
657 isOpen' := hHopen }
658 isNormal' := by
659 dsimp [Hsub]
660 infer_instance }
661 have hKleH : topDerivedTop Q 1 ≤ (H : Subgroup Q) := by
662 change K ≤ Hsub
663 exact le_sup_left
664 rcases hproj H hKleH with ⟨y, hy, hyd⟩
665 let inclK : K →ₜ* Q :=
666 { toMonoidHom := K.subtype
667 continuous_toFun := continuous_subtype_val }
668 let qK0 : K →ₜ* Q ⧸ (U : Subgroup Q) := qU.comp inclK
669 let qKr : K →ₜ* qK0.toMonoidHom.range := ProCGroups.ContinuousMonoidHom.rangeRestrict qK0
670 letI : DiscreteTopology (Q ⧸ (U : Subgroup Q)) :=
671 QuotientGroup.discreteTopology
673 letI : DiscreteTopology qK0.toMonoidHom.range := inferInstance
674 have hKclosed : IsClosed (K : Set Q) := by
675 change IsClosed ((topDerivedTop Q 1 : Subgroup Q) : Set Q)
676 infer_instance
677 have hKmap :
678 (topDerivedTop K (m - 1)).map K.subtype =
679 closedDerivedSeries (G := Q) K (m - 1) :=
680 topDerived_map_subtype_eq_closedDerivedSeries_of_isClosed_subgroup
681 (G := Q) (H := K) hKclosed (m - 1)
682 have hKmap_bot : (topDerivedTop K (m - 1)).map K.subtype = ⊥ := by
683 calc
684 (topDerivedTop K (m - 1)).map K.subtype =
685 closedDerivedSeries (G := Q) K (m - 1) := hKmap
686 _ = topDerivedTop Q (1 + (m - 1)) := by
687 simpa [K] using
688 (topDerived_add (G := Q) (m := 1) (n := m - 1))
689 _ = topDerivedTop Q m := by rw [hpred]
690 _ = ⊥ := hQm
691 have hKder_bot : topDerivedTop K (m - 1) = ⊥ := by
692 apply le_antisymm
693 · intro z hz
694 have hzker :
695 z ∈ (K.subtype : K →* Q).ker := by
696 exact
697 (Subgroup.map_eq_bot_iff
698 (f := (K.subtype : K →* Q))
699 (H := topDerivedTop K (m - 1))).1 hKmap_bot hz
700 have hzval : (z : Q) = 1 := by
701 exact (MonoidHom.mem_ker.mp hzker)
702 exact Subgroup.mem_bot.mpr (Subtype.ext hzval)
703 · exact bot_le
704 have hclosed_comm :
705 ∀ n : ℕ,
706 IsClosed
707 (((closedCommutator (topDerivedTop K n) (topDerivedTop K n)).map
708 (qKr : K →* qK0.toMonoidHom.range) :
709 Subgroup qK0.toMonoidHom.range) : Set qK0.toMonoidHom.range) := by
710 intro n
711 exact isClosed_discrete _
712 have hKrange_eq :
713 (topDerivedTop K (m - 1)).map
714 (qKr : K →* qK0.toMonoidHom.range) =
715 topDerivedTop qK0.toMonoidHom.range (m - 1) := by
716 exact
717 topDerived_map_eq_of_surj
718 (f := qKr)
719 (MonoidHom.rangeRestrict_surjective qK0.toMonoidHom)
720 hclosed_comm (m - 1)
721 have hKrange_bot : topDerivedTop qK0.toMonoidHom.range (m - 1) = ⊥ := by
722 rw [← hKrange_eq, hKder_bot]
723 exact Subgroup.map_bot (f := (qKr : K →* qK0.toMonoidHom.range))
724 have hqH_mem_Krange :
725 ∀ z : H, qU z.1 ∈ qK0.toMonoidHom.range := by
726 intro z
727 have hzH : z.1 ∈ Hsub := z.2
728 rcases
729 (Subgroup.mem_sup_of_normal_right (s := K) (t := (U : Subgroup Q))).1
730 hzH with
731 ⟨k, hk, u, hu, hku⟩
732 refine ⟨⟨k, hk⟩, ?_⟩
733 change qU k = qU z.1
734 rw [← hku]
735 rw [map_mul]
736 have hqu : qU u = 1 :=
738 (U := U) (x := u)).2 hu
739 rw [hqu, mul_one]
740 let qHK : ↥(H : Subgroup Q) →ₜ* qK0.toMonoidHom.range :=
741 { toMonoidHom := qU.toMonoidHom.comp H.subtype |>.codRestrict
742 qK0.toMonoidHom.range hqH_mem_Krange
743 continuous_toFun :=
744 (qU.continuous.comp continuous_subtype_val).subtype_mk hqH_mem_Krange }
745 have hyK :
746 qHK y ∈ topDerivedTop qK0.toMonoidHom.range (m - 1) := by
747 exact topDerived_map_le (f := qHK) (m := m - 1) ⟨y, hy, rfl⟩
748 have hqy_one : (qU y.1) = 1 := by
749 have hybot : qHK y ∈ (⊥ : Subgroup qK0.toMonoidHom.range) := by
750 rw [hKrange_bot] at hyK
751 exact hyK
752 have hsub : qHK y = 1 := by
753 exact Subgroup.mem_bot.mp hybot
754 exact congrArg Subtype.val hsub
755 have hqd_one : qU d = 1 := by
756 rw [← hyd]
757 exact hqy_one
758 exact
760 (U := U) (x := d)).mp hqd_one
761 let Bot : ClosedSubgroup Q := ⊥
762 letI : ((Bot : Subgroup Q).Normal) := by
763 change (⊥ : Subgroup Q).Normal
764 infer_instance
765 have hdbot : d ∈ (Bot : Subgroup Q) := by
767 simp only [Subgroup.mem_sInf, Set.mem_setOf_eq]
768 intro N hN
769 let U : OpenNormalSubgroup Q :=
770 { toOpenSubgroup :=
771 { toSubgroup := N
772 isOpen' := hN.1 }
773 isNormal' := hN.2.2 }
774 exact hd_all U
775 exact Subgroup.mem_bot.mp hdbot
777/-- Topological cyclic generation forces the first derived term to be trivial. -/
778theorem topDerivedTop_one_eq_bot_of_topologicallyGenerates_singleton
779 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
780 [T2Space Q] (x : Q)
781 (hgen : ProCGroups.Generation.TopologicallyGenerates (G := Q) ({x} : Set Q)) :
782 topDerivedTop Q 1 = ⊥ := by
783 have hcyc :
784 (ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) : Subgroup Q) =
785 ⊤ := by
788 have hxcent_top : ProCGroups.GroupTheory.centralizerOf x = ⊤ := by
789 simpa [hcyc] using
791 (G := Q) x (1 : ℤ) hgen
792 have hcomm : ∀ a b : Q, a * b = b * a := by
793 intro a b
794 have hbcx : b ∈ ProCGroups.GroupTheory.centralizerOf x := by
795 simp only [hxcent_top, Subgroup.mem_top]
796 have hx_cb : x ∈ ProCGroups.GroupTheory.centralizerOf b := by
798 exact (ProCGroups.GroupTheory.mem_centralizerOf_iff.mp hbcx).symm
799 have hcyc_le_cb :
800 (ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) : Subgroup Q) ≤
802 exact
804 (G := Q) (S := ({x} : Set Q)) (T := ({b} : Set Q)) (by
805 intro y hy
806 rw [Set.mem_singleton_iff] at hy
807 subst y
809 have ha_cb : a ∈ ProCGroups.GroupTheory.centralizerOf b := by
810 have : a ∈ (ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) :
811 Subgroup Q) := by
812 rw [hcyc]
813 simp only [Subgroup.mem_top]
814 exact hcyc_le_cb this
815 exact ProCGroups.GroupTheory.mem_centralizerOf_iff.mp ha_cb
816 letI : CommGroup Q := { (inferInstance : Group Q) with
817 mul_comm := hcomm }
818 have hcommutator_bot : ⁅(⊤ : Subgroup Q), (⊤ : Subgroup Q)⁆ = ⊥ := by
819 rw [Subgroup.commutator_eq_bot_iff_le_centralizer]
820 intro a _
821 rw [Subgroup.mem_centralizer_iff]
822 intro b _
823 exact hcomm b a
824 change closedCommutator (⊤ : Subgroup Q) (⊤ : Subgroup Q) = ⊥
825 dsimp [closedCommutator]
826 rw [hcommutator_bot]
827 apply le_antisymm
828 · exact
829 Subgroup.topologicalClosure_minimal
830 (s := (⊥ : Subgroup Q)) (t := (⊥ : Subgroup Q)) le_rfl
831 (isClosed_singleton (x := (1 : Q)))
832 · exact Subgroup.le_topologicalClosure (s := (⊥ : Subgroup Q))
834/-- The induced map on maximal finite-step solvable quotients. -/
835def topMaxSolvQuotMap
836 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
837 {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
838 (f : G →ₜ* Q) (m : ℕ) :
839 (G^ₘ m) →ₜ* (Q^ₘ m) := by
840 exact QuotientGroup.mapₜ (G⟦m⟧ₜ) (Q⟦m⟧ₜ) f (topDerivedTop_le_comap (f := f) m)
842scoped[ProCGroupsSolvableQuotients] notation f "⟪" m "⟫" =>
845open scoped ProCGroupsSolvableQuotients
847/--
848The induced map on finite-step solvable quotients is an equivalence under surjectivity and the
849required kernel containment for the subgroup preimage.
850-/
851noncomputable def TopologicalGroup.restrictPreimage_topMaxSolvQuot_mulEquiv
852 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
853 {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
854 {π : G →ₜ* Q} {Q₁ : Subgroup Q} {m : ℕ}
855 (hπ : Function.Surjective π)
856 (hclosed : IsClosedMap (ProCGroups.ContinuousMonoidHom.restrictPreimage π Q₁))
857 (hker :
859 topDerivedTop ↥(Q₁.comap (π : G →* Q)) m) :
860 MaxSolvQuot (Q₁.comap (π : G →* Q)) m ≃* MaxSolvQuot Q₁ m := by
861 classical
862 let G0 : Type u := Q₁.comap (π : G →* Q)
863 let f : G0 →ₜ* Q₁ := ProCGroups.ContinuousMonoidHom.restrictPreimage π Q₁
864 have hf : Function.Surjective f := by
865 change Function.Surjective (ProCGroups.ContinuousMonoidHom.restrictPreimage π Q₁)
867 have hclosed' : IsClosedMap f := by
869 exact hclosed
870 have hker' : f.toMonoidHom.ker ≤ topDerivedTop G0 m := by
871 change (ProCGroups.ContinuousMonoidHom.restrictPreimage π Q₁).toMonoidHom.ker ≤
872 topDerivedTop (Q₁.comap (π : G →* Q)) m
873 exact hker
874 have hclosed_comm :
875 ∀ n : ℕ,
876 IsClosed (((⁅G0⟦n⟧ₜ, G0⟦n⟧ₜ⁆ₜ).map (f : G0 →* Q₁) : Subgroup Q₁) : Set Q₁) := by
877 intro n
878 refine
880 (K := ⁅G0⟦n⟧ₜ, G0⟦n⟧ₜ⁆ₜ) ?_
881 exact Subgroup.isClosed_topologicalClosure (s := ⁅G0⟦n⟧ₜ, G0⟦n⟧ₜ⁆)
882 have hmap : (G0⟦m⟧ₜ).map (f : G0 →* Q₁) = Q₁⟦m⟧ₜ :=
883 topDerived_map_eq_of_surj (f := f) hf hclosed_comm m
884 have hcomap_eq :
885 Subgroup.comap (f : G0 →* Q₁) (Q₁⟦m⟧ₜ) = G0⟦m⟧ₜ := by
886 exact
887 QuotientGroup.comap_eq_of_map_eq_of_ker_le
888 (f := (f : G0 →* Q₁)) (N := G0⟦m⟧ₜ) (M := Q₁⟦m⟧ₜ) hmap hker'
889 have hsurj :
890 Function.Surjective ((f⟪m⟫) : MaxSolvQuot G0 m → MaxSolvQuot Q₁ m) := by
891 have hcomp :
892 Function.Surjective
893 (fun x : G0 =>
894 (QuotientGroup.mk : Q₁ → (Q₁ ⧸ Q₁⟦m⟧ₜ)) (f x)) :=
895 (QuotientGroup.mk_surjective (s := Q₁⟦m⟧ₜ)).comp hf
896 dsimp [topMaxSolvQuotMap, MaxSolvQuot]
897 exact
898 QuotientGroup.map_surjective_of_surjective
899 (N := G0⟦m⟧ₜ)
900 (M := Q₁⟦m⟧ₜ)
901 (f := (f : G0 →* Q₁))
902 (h := topDerivedTop_le_comap (f := f) m)
903 hcomp
904 have hker_eq_bot : (f⟪m⟫).toMonoidHom.ker = ⊥ := by
905 have hker0 :
906 (QuotientGroup.map
907 (N := G0⟦m⟧ₜ)
908 (M := Q₁⟦m⟧ₜ)
909 (f := (f : G0 →* Q₁))
910 (topDerivedTop_le_comap (f := f) m)).ker = ⊥ := by
911 exact
913 (f := (f : G0 →* Q₁))
914 (N := G0⟦m⟧ₜ) (M := Q₁⟦m⟧ₜ)
915 (h := topDerivedTop_le_comap (f := f) m)
916 hcomap_eq
917 dsimp [topMaxSolvQuotMap, MaxSolvQuot, G0, f]
918 exact hker0
919 have hinj :
920 Function.Injective ((f⟪m⟫) : MaxSolvQuot G0 m → MaxSolvQuot Q₁ m) := by
921 have hinj0 : Function.Injective (f⟪m⟫).toMonoidHom :=
922 (MonoidHom.ker_eq_bot_iff (f := (f⟪m⟫).toMonoidHom)).1 hker_eq_bot
923 exact hinj0
924 exact MulEquiv.ofBijective (((ProCGroups.ContinuousMonoidHom.restrictPreimage π
925 Q₁)⟪m⟫).toMonoidHom)
926 ⟨hinj, hsurj⟩
928/-- The quotient map to the maximal \(m\)-step solvable quotient is surjective. -/
929lemma continuousToMaxSolvQuot_surjective
930 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
931 (m : ℕ) :
932 Function.Surjective (continuousToMaxSolvQuot G m) := by
933 change Function.Surjective (toMaxSolvQuot G m)
934 exact QuotientGroup.mk_surjective (s := topDerivedTop G m)
936/-- The quotient map kills exactly the \(m\)-th closed derived subgroup. -/
937theorem continuousToMaxSolvQuot_eq_one_iff
938 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
939 {m : ℕ} {x : G} :
940 continuousToMaxSolvQuot G m x = 1 ↔ x ∈ topDerivedTop G m := by
941 change toMaxSolvQuot G m x = 1 ↔ x ∈ topDerivedTop G m
942 exact QuotientGroup.eq_one_iff (N := topDerivedTop G m) x
944/--
945The kernel of the ambient quotient map lands in the first closed derived subgroup of any
946preimage open subgroup containing the previous derived term.
947-/
948theorem continuousToMaxSolvQuot_ker_le_topDerived_one_map_subtype_of_le
949 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
950 {m : ℕ} (hm : 1 ≤ m)
951 (H : OpenSubgroup (MaxSolvQuot G m))
952 (hH :
953 topDerivedTop G (m - 1) ≤
954 ((H : Subgroup (MaxSolvQuot G m)).comap
955 (continuousToMaxSolvQuot G m : G →* MaxSolvQuot G m))) :
956 (continuousToMaxSolvQuot G m : G →* MaxSolvQuot G m).ker ≤
957 (topDerivedTop
958 ↥((preimageOpenSubgroup (continuousToMaxSolvQuot G m) H : OpenSubgroup G) :
959 Subgroup G) 1).map
960 (Subgroup.subtype
961 ((preimageOpenSubgroup (continuousToMaxSolvQuot G m) H : OpenSubgroup G) :
962 Subgroup G)) := by
963 let Q : Type u := MaxSolvQuot G m
964 let π : G →ₜ* Q := continuousToMaxSolvQuot G m
965 let Hpre : OpenSubgroup G := preimageOpenSubgroup π H
966 have hHpreOpen : IsOpen ((Hpre : Subgroup G) : Set G) := Hpre.isOpen'
967 intro x hx
968 have hxder : x ∈ topDerivedTop G m := by
969 exact
970 (continuousToMaxSolvQuot_eq_one_iff (G := G) (m := m) (x := x)).1
971 ((MonoidHom.mem_ker).1 hx)
972 have hxder' :
973 x ∈ closedDerivedSeries (G := G)
974 ((H : Subgroup Q).comap (π : G →* Q)) 1 := by
975 simpa [π, Q] using
976 (mem_topDerived_one_of_mem_topDerived_of_le (G := G) hm
977 (by simpa [π, Q] using hH) hxder)
978 have htopMap :
979 ((⊤ : Subgroup ↥((H : Subgroup Q).comap (π : G →* Q))).map
980 ((Subgroup.comap (π : G →* Q) H).subtype)) =
981 (H : Subgroup Q).comap (π : G →* Q) := by
982 ext x
983 constructor
984 · rintro ⟨y, -, rfl⟩
985 exact y.2
986 · intro hx'
987 exact ⟨⟨x, hx'⟩, by simp only [Subgroup.coe_top, Set.mem_univ], rfl⟩
988 have hmap :
989 (topDerivedTop ↥((Hpre : Subgroup G)) 1).map ((Hpre : Subgroup G).subtype) =
990 closedDerivedSeries (G := G) ((H : Subgroup Q).comap (π : G →* Q)) 1 := by
991 have hmap0 :=
992 topDerived_one_map_subtype_eq_of_isClosed_subgroup
993 (G := G)
994 (H := ((H : Subgroup Q).comap (π : G →* Q)))
995 (K := (⊤ : Subgroup ↥((H : Subgroup Q).comap (π : G →* Q))))
996 (Subgroup.isClosed_of_isOpen _ hHpreOpen)
997 rw [htopMap] at hmap0
998 change
999 (topDerivedTop ↥((Hpre : Subgroup G)) 1).map ((Hpre : Subgroup G).subtype) =
1000 closedDerivedSeries (G := G) ((H : Subgroup Q).comap (π : G →* Q)) 1
1001 exact hmap0
1002 change x ∈ (topDerivedTop ↥((Hpre : Subgroup G)) 1).map ((Hpre : Subgroup G).subtype)
1003 rw [hmap]
1004 exact hxder'
1006/-- The first maximal solvable quotient is the topological abelianization. -/
1007theorem isMulTorsionFree_maxSolvQuot_one_of_isMulTorsionFree_topologicalAbelianization
1008 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
1009 (hG : IsMulTorsionFree (TopologicalAbelianization G)) :
1010 IsMulTorsionFree (MaxSolvQuot G 1) := by
1011 change IsMulTorsionFree (TopologicalAbelianization G)
1012 exact hG
1014/--
1015The induced map between maximal finite-step solvable quotients of a subgroup preimage and the
1016target subgroup is an isomorphism under the expected kernel bound.
1018theorem preimageOpenSubgroup_maxSolvQuot_mulEquiv_of_ker_le
1019 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
1020 {Q : Type v} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
1021 (f : G →ₜ* Q) (hf : Function.Surjective f) (H : OpenSubgroup Q)
1022 (hclosed : IsClosedMap (ProCGroups.ContinuousMonoidHom.restrictPreimage f (H : Subgroup Q)))
1023 (n : ℕ)
1024 (hker :
1025 f.ker ≤
1026 (topDerivedTop
1027 ↥((preimageOpenSubgroup f H : OpenSubgroup G) : Subgroup G) n).map
1028 (Subgroup.subtype
1029 ((preimageOpenSubgroup f H : OpenSubgroup G) : Subgroup G))) :
1030 Nonempty
1031 (MaxSolvQuot ↥((preimageOpenSubgroup f H : OpenSubgroup G) : Subgroup G) n ≃*
1032 MaxSolvQuot ↥(H : Subgroup Q) n) := by
1033 let Hpre : OpenSubgroup G := preimageOpenSubgroup f H
1034 have hker' :
1036 topDerivedTop ↥((Hpre : Subgroup G)) n := by
1037 intro x hx
1038 have hxker : x.1 ∈ f.ker := by
1039 change ProCGroups.ContinuousMonoidHom.restrictPreimage f (H : Subgroup Q) x = 1 at hx
1040 change f x.1 = 1
1041 exact congrArg Subtype.val hx
1042 have hxder :
1043 x.1 ∈
1044 (topDerivedTop ↥((Hpre : Subgroup G)) n).map
1045 ((Hpre : Subgroup G).subtype) :=
1046 hker hxker
1047 rcases hxder with ⟨y, hy, hyx⟩
1048 exact Subtype.ext hyx ▸ hy
1049 exact
1050 ⟨TopologicalGroup.restrictPreimage_topMaxSolvQuot_mulEquiv
1051 (π := f) (Q₁ := (H : Subgroup Q)) (m := n) hf hclosed hker'⟩
1053end ProCGroups.FiniteStepSolvableQuotients