ProCGroups/FiniteStepSolvableQuotients/AbelianActions/SlimnessAndTorsion.lean
1import ProCGroups.FiniteStepSolvableQuotients.AbelianActions.Faithful
2import ProCGroups.GroupTheory.CentralizerNormalizerCommensurator
3import ProCGroups.ProC.GroupPredicates.Abelian
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/FiniteStepSolvableQuotients/AbelianActions/SlimnessAndTorsion.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
17commutator closure formulas, and abelian-action consequences.
18-/
20open scoped Topology
22namespace ProCGroups.FiniteStepSolvableQuotients
24open ProCGroups.Abelian ProCGroups.ProC
26universe u v
28/-- A group is torsion-free when every element of finite order is trivial. -/
29def IsTorsionFreeGroup
30 (G : Type u) [Group G] : Prop :=
31 ∀ g : G, IsOfFinOrder g → g = 1
33/-- A topological group is slim when every open subgroup has trivial centralizer in the ambient
34group. -/
36 (G : Type u) [TopologicalSpace G] [Group G] : Prop :=
37 ∀ H : OpenSubgroup G, Subgroup.centralizer (H : Set G) = ⊥
39/-- A topological group is slim modulo `K` when every open subgroup has centralizer contained in
40`K`. -/
41def IsSlimModulo
42 (G : Type u) [TopologicalSpace G] [Group G]
43 (K : Subgroup G) : Prop :=
44 ∀ H : OpenSubgroup G, Subgroup.centralizer (H : Set G) ≤ K
46/-- A continuous homomorphism is relatively slim when the image of every open subgroup has trivial
47centralizer in the target. -/
49 {G : Type u} [TopologicalSpace G] [Group G]
50 {H : Type v} [TopologicalSpace H] [Group H]
51 (f : G →ₜ* H) : Prop :=
52 ∀ U : OpenSubgroup G,
53 Subgroup.centralizer ((((U : Subgroup G).map f.toMonoidHom : Subgroup H) : Set H)) = ⊥
55/-- Relative slimness for the identity map is the same as slimness. -/
56theorem isSlim_iff_isRelativelySlim_id
57 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
60 ({ toMonoidHom := MonoidHom.id G
61 continuous_toFun := continuous_id } : G →ₜ* G) := by
62 simp only [IsSlim, IsRelativelySlim, Subgroup.map_id, OpenSubgroup.coe_toSubgroup]
64/-- Slim groups have trivial center. -/
65theorem center_eq_bot_of_isSlim
66 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
68 Subgroup.center G = ⊥ := by
69 simpa [Subgroup.centralizer_univ] using hSlim (⊤ : OpenSubgroup G)
71/-- Slimness modulo `K` forces the center into `K`. -/
72theorem center_le_of_isSlimModulo
73 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
74 {K : Subgroup G} (hSlim : IsSlimModulo G K) :
75 Subgroup.center G ≤ K := by
76 simpa [Subgroup.centralizer_univ] using hSlim (⊤ : OpenSubgroup G)
78/-- Slimness modulo the trivial subgroup is just slimness. -/
79theorem isSlim_of_isSlimModulo_bot
80 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
81 (hSlim : IsSlimModulo G (⊥ : Subgroup G)) :
83 intro H
84 exact le_antisymm (hSlim H) bot_le
86/-- A multiplicatively commutative group can be bundled as a commutative group. -/
88 {G : Type u} [Group G] [IsMulCommutative G] : CommGroup G :=
89 { ‹Group G› with
90 mul_comm := by
91 intro a b
92 exact mul_comm a b }
94/-- Torsion-freeness of open-subgroup abelianizations implies ordinary torsion-freeness in the
95commutative case. -/
97 {G : Type u} [TopologicalSpace G] [Group G] [IsMulCommutative G]
98 [IsTopologicalGroup G] [T1Space G]
99 (hG : IsAbTorsionFree G) :
100 IsMulTorsionFree G := by
101 letI : CommGroup G := commGroupOfIsMulCommutative (G := G)
102 exact isMulTorsionFree_of_isAbTorsionFree_commGroup (G := G) hG
104/-- Multiplicative torsion-freeness implies the usual finite-order formulation. -/
106 {G : Type u} [Group G] [IsMulTorsionFree G] :
107 IsTorsionFreeGroup G := by
108 intro g hg
109 by_contra hne
110 exact (not_isOfFinOrder_of_isMulTorsionFree hne) hg
112/-- An automorphism of a torsion-free group that is trivial on a finite-index subgroup is
113trivial everywhere. -/
115 {A : Type u} [Group A] [IsMulTorsionFree A]
116 (φ : MulAut A) (B : Subgroup A) [B.FiniteIndex]
117 (hφ : ∀ b : A, b ∈ B → φ b = b) :
118 φ = 1 := by
119 ext a
120 let C : Subgroup A := B.normalCore
121 letI : C.FiniteIndex := Subgroup.finiteIndex_normalCore (H := B)
122 have hidx : C.index ≠ 0 := by
123 simpa [C] using (Subgroup.finiteIndex_iff (H := C)).mp ‹C.FiniteIndex›
124 have haC : a ^ C.index ∈ C := C.pow_index_mem a
125 have hpow :
126 (φ a) ^ C.index = a ^ C.index := by
127 calc
128 (φ a) ^ C.index = φ (a ^ C.index) := by simp only [map_pow]
129 _ = a ^ C.index := hφ _ ((Subgroup.normalCore_le B) haC)
130 exact IsMulTorsionFree.pow_left_injective (M := A) hidx hpow
132/-- A nontrivial class in the topological abelianization of a closed subgroup remains nontrivial in
133the topological abelianization of some ambient open subgroup containing it. -/
135 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
136 [CompactSpace G] [TotallyDisconnectedSpace G]
137 (T : ClosedSubgroup G)
138 {a : TopologicalAbelianization ↥(T : Subgroup G)} (hne : a ≠ 1) :
139 ∃ H : OpenSubgroup G,
140 (T : Subgroup G) ≤ (H : Subgroup G) ∧
141 ∃ f : TopologicalAbelianization ↥(T : Subgroup G) →*
142 TopologicalAbelianization ↥(H : Subgroup G),
143 f a ≠ 1 := by
144 classical
145 let hGprof : ProCGroups.IsProfiniteGroup G := by
146 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
147 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective
148 (Subgroup.closedCommutator (T : Subgroup G)) a
149 let A := TopologicalAbelianization ↥(T : Subgroup G)
150 have hxne : TopologicalAbelianization.mk ↥(T : Subgroup G) x ≠ 1 := hne
151 let hTprof : IsProfiniteGroup ↥(T : Subgroup G) :=
152 IsProfiniteGroup.of_closedSubgroup (G := G) hGprof T
153 have hAprof : IsProfiniteGroup A := by
154 letI : T2Space ↥(T : Subgroup G) := IsProfiniteGroup.t2Space hTprof
155 simpa [A] using
157 (G := ↥(T : Subgroup G)) hTprof
158 (Subgroup.isClosed_closedCommutator (T : Subgroup G)))
159 obtain ⟨Uab, hxUab⟩ :=
160 ProCGroups.ProC.exists_openNormalSubgroup_not_mem (G := A) hAprof hxne
161 let qA : A →* A ⧸ (Uab : Subgroup A) := QuotientGroup.mk' (Uab : Subgroup A)
162 have hqAx_ne : qA (TopologicalAbelianization.mk ↥(T : Subgroup G) x) ≠ 1 := by
163 intro hq
164 exact hxUab ((QuotientGroup.eq_one_iff (N := (Uab : Subgroup A))
165 (TopologicalAbelianization.mk ↥(T : Subgroup G) x)).1 hq)
166 let N0 : OpenNormalSubgroup ↥(T : Subgroup G) :=
167 OpenNormalSubgroup.comap
168 (TopologicalAbelianization.mk ↥(T : Subgroup G))
169 (by
170 simpa [TopologicalAbelianization.mk] using
171 (continuous_quotient_mk' :
172 Continuous
173 (QuotientGroup.mk'
174 (Subgroup.closedCommutator (T : Subgroup G))))) Uab
175 have hN0ker :
176 (N0 : Subgroup ↥(T : Subgroup G)) ≤
178 intro y hy
179 change qA (TopologicalAbelianization.mk ↥(T : Subgroup G) y) = 1
180 exact (QuotientGroup.eq_one_iff (N := (Uab : Subgroup A))
181 (TopologicalAbelianization.mk ↥(T : Subgroup G) y)).2 hy
182 obtain ⟨V, hVT⟩ :=
184 (G := G) hGprof T N0.toOpenSubgroup
185 let Hsub : Subgroup G := (T : Subgroup G) ⊔ (V : Subgroup G)
186 have hHOpen : IsOpen (Hsub : Set G) := by
187 exact Subgroup.isOpen_of_openSubgroup Hsub
188 (show (V : Subgroup G) ≤ Hsub from le_sup_right)
189 let H : OpenSubgroup G := ⟨Hsub, hHOpen⟩
190 let ι : ↥(T : Subgroup G) →* ↥(H : Subgroup G) :=
191 { toFun := fun y => ⟨y.1, (show (T : Subgroup G) ≤ (H : Subgroup G) from le_sup_left) y.2⟩
192 map_one' := by ext; simp only [OneMemClass.coe_one, H, Hsub]
193 map_mul' := by intro y z; ext; rfl }
194 let qT : ↥(T : Subgroup G) →* A ⧸ (Uab : Subgroup A) :=
195 qA.comp (TopologicalAbelianization.mk ↥(T : Subgroup G))
196 let VT : OpenNormalSubgroup ↥(T : Subgroup G) :=
198 have hVTker : (VT : Subgroup ↥(T : Subgroup G)) ≤ qT.ker := by
199 exact
200 (show (VT : Subgroup ↥(T : Subgroup G)) ≤ (N0 : Subgroup ↥(T : Subgroup G)) from hVT).trans
201 hN0ker
202 let L : Subgroup (G ⧸ (V : Subgroup G)) :=
203 Subgroup.map (QuotientGroup.mk' (V : Subgroup G)) (T : Subgroup G)
204 let ψ : ↥(T : Subgroup G) →* L :=
205 { toFun := fun y => ⟨QuotientGroup.mk' (V : Subgroup G) y.1, ⟨y.1, y.2, rfl⟩⟩
206 map_one' := by ext; rfl
207 map_mul' := by intro y z; ext; rfl }
208 have hψSurj : Function.Surjective ψ := by
209 intro z
210 rcases z with ⟨z, hz⟩
211 rcases hz with ⟨y, hy, hyz⟩
212 exact ⟨⟨y, hy⟩, Subtype.ext hyz⟩
213 have hψKer : (VT : Subgroup ↥(T : Subgroup G)) = ψ.ker := by
214 ext y
215 constructor
216 · intro hy
217 apply Subtype.ext
218 exact (QuotientGroup.eq_one_iff (N := (V : Subgroup G)) y.1).2 hy
219 · intro hy
220 exact (QuotientGroup.eq_one_iff (N := (V : Subgroup G)) y.1).1 <| congrArg Subtype.val hy
221 let qTquot : ↥(T : Subgroup G) ⧸ ψ.ker →* A ⧸ (Uab : Subgroup A) :=
222 QuotientGroup.lift ψ.ker qT (by simpa [hψKer] using hVTker)
223 let qL : L →* A ⧸ (Uab : Subgroup A) :=
224 qTquot.comp (QuotientGroup.quotientKerEquivOfSurjective ψ hψSurj).symm.toMonoidHom
225 let qLcont : L →ₜ* A ⧸ (Uab : Subgroup A) :=
226 { toMonoidHom := qL
227 continuous_toFun := by
228 letI : DiscreteTopology L := inferInstance
229 exact continuous_of_discreteTopology }
230 let qHaux : ↥(H : Subgroup G) →* L :=
231 { toFun := fun y =>
232 ⟨QuotientGroup.mk' (V : Subgroup G) y.1, by
233 rcases
234 (Subgroup.mem_sup_of_normal_right
235 (s := (T : Subgroup G)) (t := (V : Subgroup G)) (x := y.1)).1 y.2 with
236 ⟨t, htT, v, hvV, htv⟩
237 refine ⟨t, htT, ?_⟩
238 have hv1 : QuotientGroup.mk' (V : Subgroup G) v = 1 := by
239 exact (QuotientGroup.eq_one_iff (N := (V : Subgroup G)) v).2 hvV
240 calc
241 QuotientGroup.mk' (V : Subgroup G) t =
242 QuotientGroup.mk' (V : Subgroup G) t * 1 := by simp only [QuotientGroup.mk'_apply, mul_one]
243 _ = QuotientGroup.mk' (V : Subgroup G) t *
244 QuotientGroup.mk' (V : Subgroup G) v := by rw [hv1]
246 _ = QuotientGroup.mk' (V : Subgroup G) y.1 := by rw [htv]⟩
247 map_one' := by ext; rfl
248 map_mul' := by intro y z; ext; rfl }
249 let qH : ↥(H : Subgroup G) →ₜ* A ⧸ (Uab : Subgroup A) :=
250 { toMonoidHom := qL.comp qHaux
251 continuous_toFun := by
252 have hqHaux : Continuous qHaux := by
253 exact Continuous.subtype_mk
254 (by simpa [qHaux] using (continuous_quotient_mk'.comp continuous_subtype_val))
255 (fun y => (qHaux y).2)
256 exact qLcont.continuous_toFun.comp hqHaux }
257 have hqH_on_T : ∀ y : ↥(T : Subgroup G), qH (ι y) = qT y := by
258 intro y
259 have hqHaux : qHaux (ι y) = ψ y := by
260 apply Subtype.ext
261 rfl
262 change qL (qHaux (ι y)) = qT y
263 rw [hqHaux]
264 have hmk :
265 (QuotientGroup.quotientKerEquivOfSurjective ψ hψSurj).symm (ψ y) =
266 QuotientGroup.mk' ψ.ker y := by
267 rw [QuotientGroup.quotientKerEquivOfSurjective,
268 QuotientGroup.quotientKerEquivOfRightInverse_symm_apply]
269 apply QuotientGroup.eq.2
270 change ψ ((Exists.choose (Function.Surjective.hasRightInverse hψSurj) (ψ y))⁻¹ * y) = 1
271 simp only [map_mul, map_inv, Exists.choose_spec (Function.Surjective.hasRightInverse hψSurj) (ψ y),
272 inv_mul_cancel]
273 simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply, hmk,
274 QuotientGroup.mk'_apply, QuotientGroup.lift_mk, qL, qTquot]
275 let ιcont : ↥(T : Subgroup G) →ₜ* ↥(H : Subgroup G) :=
276 { toMonoidHom := ι
277 continuous_toFun := by
278 exact Continuous.subtype_mk continuous_subtype_val
279 (fun y => (show (T : Subgroup G) ≤ (H : Subgroup G) from le_sup_left) y.2) }
280 have hclosedBot :
281 IsClosed (((⊥ : Subgroup (A ⧸ (Uab : Subgroup A))) : Set (A ⧸ (Uab : Subgroup A)))) := by
282 change IsClosed ({(1 : A ⧸ (Uab : Subgroup A))} : Set (A ⧸ (Uab : Subgroup A)))
283 exact isClosed_singleton
284 have hcommMapBot :
285 (commutator ↥(H : Subgroup G)).map (qH : ↥(H : Subgroup G) →* A ⧸ (Uab : Subgroup A)) ≤
286 (⊥ : Subgroup (A ⧸ (Uab : Subgroup A))) := by
287 rw [_root_.map_commutator_eq]
288 refine Subgroup.commutator_le.mpr ?_
289 intro a ha b hb
290 exact commutatorElement_eq_one_iff_mul_comm.2 (mul_comm a b)
291 have hcommClosureBot :
292 (Subgroup.closedCommutator (H : Subgroup G)).map
293 (qH : ↥(H : Subgroup G) →* A ⧸ (Uab : Subgroup A)) ≤
294 (⊥ : Subgroup (A ⧸ (Uab : Subgroup A))) := by
296 (f := qH)
297 (G₁ := commutator ↥(H : Subgroup G))
298 (Q₁ := (⊥ : Subgroup (A ⧸ (Uab : Subgroup A))))
299 hcommMapBot
300 hclosedBot
301 let fAb : TopologicalAbelianization ↥(T : Subgroup G) →*
302 TopologicalAbelianization ↥(H : Subgroup G) :=
303 TopologicalAbelianization.map ιcont
304 have hbne : fAb (TopologicalAbelianization.mk ↥(T : Subgroup G) x) ≠ 1 := by
305 intro hb
306 have hxcomm :
307 ι x ∈ Subgroup.closedCommutator (H : Subgroup G) := by
308 have hb' :
309 TopologicalAbelianization.mk ↥(H : Subgroup G) (ι x) = 1 := by
310 change TopologicalAbelianization.mk ↥(H : Subgroup G) (ι x) = 1 at hb
311 exact hb
312 exact
313 (QuotientGroup.eq_one_iff
314 (N := Subgroup.closedCommutator (H : Subgroup G))
315 (ι x)).1 hb'
316 have hxmap :
317 qH (ι x) ∈
318 (Subgroup.closedCommutator (H : Subgroup G)).map
319 (qH : ↥(H : Subgroup G) →* A ⧸ (Uab : Subgroup A)) := ⟨ι x, hxcomm, rfl⟩
320 have hxbot : qH (ι x) ∈ (⊥ : Subgroup (A ⧸ (Uab : Subgroup A))) := hcommClosureBot hxmap
321 have hqHx : qH (ι x) = 1 := by simpa using hxbot
322 have hqTx : qT x = 1 := by simpa [hqH_on_T x] using hqHx
323 exact hqAx_ne (by simpa [qT] using hqTx)
324 exact ⟨H, le_sup_left, ⟨fAb, hbne⟩⟩
326/-- The topological abelianization of a closed subgroup is torsion-free under the local
327abelianization torsion-free hypothesis. -/
329 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
330 [CompactSpace G] [TotallyDisconnectedSpace G]
331 (hG : IsAbTorsionFree G)
332 (T : ClosedSubgroup G) :
333 IsMulTorsionFree (TopologicalAbelianization ↥(T : Subgroup G)) := by
334 classical
335 rw [isMulTorsionFree_iff_not_isOfFinOrder]
336 intro a hne hfin
337 obtain ⟨H, -, fAb, hbne⟩ :=
338 exists_openSubgroup_nontrivial_topologicalAbelianizationImage (G := G) T (a := a) hne
339 have hbfin : IsOfFinOrder (fAb a) := MonoidHom.isOfFinOrder fAb hfin
340 have hHtf :
341 IsMulTorsionFree (TopologicalAbelianization ↥(H : Subgroup G)) := hG H
342 exact
343 (isMulTorsionFree_iff_not_isOfFinOrder
344 (G := TopologicalAbelianization ↥(H : Subgroup G))).mp hHtf hbne hbfin
346/-- The local abelianization torsion-free condition passes to closed subgroups. -/
348 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
349 [CompactSpace G] [TotallyDisconnectedSpace G]
350 (hG : IsAbTorsionFree G)
351 {K : Subgroup G} (hKClosed : IsClosed (K : Set G)) :
352 IsAbTorsionFree ↥K := by
353 let T : ClosedSubgroup G := ⟨K, hKClosed⟩
354 let hGprof : ProCGroups.IsProfiniteGroup G := by
355 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
356 letI : IsTopologicalGroup T := by
357 change IsTopologicalGroup ↥(T : Subgroup G)
358 infer_instance
359 intro N
360 let N0 : OpenSubgroup T := N
361 letI : IsTopologicalGroup ↥(N0 : Subgroup T) := by
362 infer_instance
363 let N' : ClosedSubgroup G := ProCGroups.ProC.closedSubgroupOfOpenSubgroup (G := G) hGprof T N0
364 have hN'tf :
365 IsMulTorsionFree (TopologicalAbelianization ↥(N' : Subgroup G)) :=
366 isMulTorsionFree_topologicalAbelianization_of_closedSubgroup (G := G) hG N'
367 have hle :
368 (N' : Subgroup G) ≤ (T : Subgroup G) :=
369 ProCGroups.ProC.closedSubgroupOfOpenSubgroup_le (G := G) hGprof T N0
370 let eEq : ↥(N0 : Subgroup T) ≃ₜ*
371 ↥(((N' : Subgroup G).subgroupOf (T : Subgroup G))) :=
372 { toMulEquiv :=
373 { toFun := fun x => ⟨x.1, by
374 exact
376 (G := G) hGprof T N0).symm ▸ x.2⟩
377 invFun := fun x => ⟨x.1, by
378 exact
380 (G := G) hGprof T N0) ▸ x.2⟩
381 left_inv := by intro x; ext; rfl
382 right_inv := by intro x; ext; rfl
383 map_mul' := by intro x y; rfl }
384 continuous_toFun := by
385 exact Continuous.subtype_mk continuous_subtype_val
386 (fun x =>
388 (G := G) hGprof T N0).symm ▸ x.2)
389 continuous_invFun := by
390 exact Continuous.subtype_mk continuous_subtype_val
391 (fun x =>
393 (G := G) hGprof T N0) ▸ x.2) }
394 let eN : ↥(N0 : Subgroup T) ≃ₜ* ↥(N' : Subgroup G) :=
395 eEq.trans (Subgroup.subgroupOfContinuousMulEquivOfLe hle)
396 let eAb :
397 TopologicalAbelianization ↥(N0 : Subgroup T) ≃ₜ*
398 TopologicalAbelianization ↥(N' : Subgroup G) :=
399 TopologicalAbelianization.congr (G := ↥(N0 : Subgroup T))
400 (H := ↥(N' : Subgroup G)) eN
401 letI : IsMulTorsionFree (TopologicalAbelianization ↥(N' : Subgroup G)) := hN'tf
402 exact eAb.symm.isMulTorsionFree
404/-- A commutative closed subgroup of an `ab`-torsion-free profinite group is torsion-free. -/
406 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
407 [CompactSpace G] [TotallyDisconnectedSpace G]
408 {K : Subgroup G} (hKClosed : IsClosed (K : Set G))
409 [IsMulCommutative ↥K]
410 (hG : IsAbTorsionFree G) :
411 IsTorsionFreeGroup ↥K := by
412 have hKab : IsAbTorsionFree ↥K := isAbTorsionFree_closedSubgroup (G := G) hG hKClosed
413 let T : ClosedSubgroup G := ⟨K, hKClosed⟩
414 haveI : CompactSpace ↥K := by
415 simpa using (inferInstance : CompactSpace T)
416 letI : T2Space ↥K := inferInstance
417 letI : T1Space ↥K := inferInstance
418 letI : IsMulTorsionFree ↥K :=
419 isMulTorsionFree_of_isAbTorsionFree_isMulCommutative (G := ↥K) hKab
420 exact isTorsionFreeGroup_of_isMulTorsionFree (G := ↥K)
422/-- An `ab`-torsion-free profinite group is torsion-free. -/
424 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
425 [CompactSpace G] [TotallyDisconnectedSpace G]
426 (hG : IsAbTorsionFree G) :
427 IsTorsionFreeGroup G := by
428 intro g hg
429 have hKClosed : IsClosed (((Subgroup.zpowers g : Subgroup G) : Set G)) := by
430 simpa using
431 (show (((Subgroup.zpowers g : Subgroup G) : Set G)).Finite from by
432 simpa using (finite_zpowers (a := g)).2 hg).isClosed
433 have hKtf : IsTorsionFreeGroup ↥(Subgroup.zpowers g) :=
435 (G := G) (K := Subgroup.zpowers g) hKClosed hG
436 let x : Subgroup.zpowers g := ⟨g, Subgroup.mem_zpowers g⟩
437 have hxfin : IsOfFinOrder x := by
438 rw [← Submonoid.isOfFinOrder_coe]
439 simpa [x] using hg
440 have hx : x = 1 := hKtf x hxfin
441 simpa [x] using congrArg Subtype.val hx
443/-- Maximal finite-step solvable quotients of an `ab`-torsion-free profinite group are
444torsion-free. -/
446 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
447 [CompactSpace G] [TotallyDisconnectedSpace G]
448 (hG : IsAbTorsionFree G)
449 {m : ℕ} (hm : 1 ≤ m) :
450 IsTorsionFreeGroup (MaxSolvQuot G m) := by
451 refine Nat.strong_induction_on m ?_ hm
452 intro m ih hm
453 cases m with
455 cases hm
456 | succ m =>
457 cases m with
459 letI : IsMulTorsionFree (MaxSolvQuot G 1) :=
461 G (isMulTorsionFree_topologicalAbelianization_of_isAbTorsionFree (G := G) hG)
462 exact isTorsionFreeGroup_of_isMulTorsionFree (G := MaxSolvQuot G 1)
463 | succ m =>
464 let D1 : Subgroup G := topDerivedTop G (m + 1)
465 let D2 : Subgroup G := topDerivedTop G (m + 2)
466 have hD2_le_D1 : D2 ≤ D1 := by
467 dsimp [D1, D2, topDerivedTop]
468 exact topDerivedTop_antitone (G := G) (Nat.le_succ (m + 1))
469 have hprev : IsTorsionFreeGroup (MaxSolvQuot G (m + 1)) := by
470 apply ih (m + 1)
471 · exact Nat.lt_succ_self (m + 1)
472 · exact Nat.succ_le_succ (Nat.zero_le m)
473 let π : MaxSolvQuot G (m + 2) →* MaxSolvQuot G (m + 1) :=
474 QuotientGroup.map D2 D1 (MonoidHom.id G) (by exact hD2_le_D1)
475 have hD1Closed : IsClosed (D1 : Set G) := by
476 infer_instance
477 have hD1ab : IsAbTorsionFree ↥D1 :=
478 isAbTorsionFree_closedSubgroup (G := G) hG hD1Closed
479 have hbaseTF : IsMulTorsionFree (MaxSolvQuot D1 1) := by
480 exact
482 D1
484 (G := D1) hD1ab)
485 have hsub :
486 D2.subgroupOf D1 = topDerivedTop D1 1 := by
487 have hmap : (topDerivedTop D1 1).map D1.subtype = D2 := by
488 have hmapTop : ((⊤ : Subgroup D1).map D1.subtype) = D1 := by
489 ext x
490 constructor
491 · rintro ⟨y, -, rfl⟩
492 exact y.2
493 · intro hx
494 exact ⟨⟨x, hx⟩, by simp only [Subgroup.coe_top, Set.mem_univ], rfl⟩
495 calc
496 (topDerivedTop D1 1).map D1.subtype =
497 closedDerivedSeries (G := G) (((⊤ : Subgroup D1).map D1.subtype)) 1 := by
498 simpa [topDerivedTop] using
500 (G := G) (H := D1) (K := (⊤ : Subgroup D1)) hD1Closed)
501 _ = closedDerivedSeries (G := G) D1 1 := by simp only [hmapTop, closedDerivedSeries_succ, closedDerivedSeries_zero]
502 _ = D2 := by
503 simp only [closedDerivedSeries, closedDerivedSeries_succ, D1, D2]
504 apply (Subgroup.map_injective D1.subtype_injective)
505 calc
506 (D2.subgroupOf D1).map D1.subtype = D2 := Subgroup.map_subgroupOf_eq_of_le hD2_le_D1
507 _ = (topDerivedTop D1 1).map D1.subtype := hmap.symm
508 have hquotTF : IsMulTorsionFree (D1 ⧸ D2.subgroupOf D1) := by
509 let e : D1 ⧸ D2.subgroupOf D1 ≃* MaxSolvQuot D1 1 :=
510 QuotientGroup.quotientMulEquivOfEq hsub
511 letI : IsMulTorsionFree (MaxSolvQuot D1 1) := hbaseTF
512 exact e.symm.isMulTorsionFree
513 have hmapTF' : IsMulTorsionFree ↥(Subgroup.map (QuotientGroup.mk' D2) D1) := by
514 let φ : D1 →* Subgroup.map (QuotientGroup.mk' D2) D1 :=
515 { toFun := fun x => ⟨QuotientGroup.mk' D2 x, ⟨x, x.2, rfl⟩⟩
516 map_one' := by ext; rfl
517 map_mul' := by intro x y; ext; rfl }
518 have hφSurj : Function.Surjective φ := by
519 rintro ⟨y, x, hx, rfl⟩
520 refine ⟨⟨x, hx⟩, ?_⟩
521 ext
522 rfl
523 have hφKer : φ.ker = D2.subgroupOf D1 := by
524 ext x
525 constructor
526 · intro hx
527 have hx' : φ x = 1 := hx
528 have hx'' : QuotientGroup.mk' D2 (x : G) = 1 := congrArg Subtype.val hx'
529 exact (QuotientGroup.eq_one_iff (N := D2) (x : G)).1 hx''
530 · intro hx
531 change φ x = 1
532 apply Subtype.ext
533 exact (QuotientGroup.eq_one_iff (N := D2) (x : G)).2 hx
534 let e : D1 ⧸ D2.subgroupOf D1 ≃* Subgroup.map (QuotientGroup.mk' D2) D1 :=
535 (QuotientGroup.quotientMulEquivOfEq hφKer.symm).trans
536 (QuotientGroup.quotientKerEquivOfSurjective φ hφSurj)
537 letI : IsMulTorsionFree (D1 ⧸ D2.subgroupOf D1) := hquotTF
538 exact e.isMulTorsionFree
539 have hkerTF : IsTorsionFreeGroup ↥(π.ker) := by
540 have hker : π.ker = Subgroup.map (QuotientGroup.mk' D2) D1 := by
542 (QuotientGroup.ker_map (N := D2) (M := D1) (f := MonoidHom.id G) (by
543 exact hD2_le_D1))
544 let eKer : π.ker ≃* Subgroup.map (QuotientGroup.mk' D2) D1 :=
545 { toFun := fun x => ⟨x.1, by simpa [hker] using x.2⟩
546 invFun := fun x => ⟨x.1, by rw [hker]; exact x.2⟩
547 left_inv := by intro x; ext; rfl
548 right_inv := by intro x; ext; rfl
549 map_mul' := by intro x y; ext; rfl }
550 letI : IsMulTorsionFree ↥(Subgroup.map (QuotientGroup.mk' D2) D1) := hmapTF'
551 letI : IsMulTorsionFree ↥(π.ker) := eKer.symm.isMulTorsionFree
552 exact isTorsionFreeGroup_of_isMulTorsionFree (G := ↥(π.ker))
553 intro z hz
556 have hzk : z ∈ π.ker := hzπ1
557 let zk : π.ker := ⟨z, hzk⟩
558 have hzkFin : IsOfFinOrder zk := by
559 rw [← Submonoid.isOfFinOrder_coe]
560 simpa [zk] using hz
561 have hzk1 : zk = 1 := hkerTF zk hzkFin
562 simpa [zk] using congrArg Subtype.val hzk1
564/-- Closed subgroups of an `ab`-torsion-free profinite group are torsion-free. -/
566 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
567 [CompactSpace G] [TotallyDisconnectedSpace G]
568 {K : Subgroup G} (hKClosed : IsClosed (K : Set G))
569 (hG : IsAbTorsionFree G) :
570 IsTorsionFreeGroup ↥K := by
571 haveI : CompactSpace ↥K := hKClosed.isClosedEmbedding_subtypeVal.compactSpace
572 haveI : TotallyDisconnectedSpace ↥K := by infer_instance
573 have hKab : IsAbTorsionFree ↥K :=
574 isAbTorsionFree_closedSubgroup (G := G) (K := K) hG hKClosed
575 exact isTorsionFreeGroup_of_isAbTorsionFree (G := ↥K) hKab
577/-- Slimness is equivalent to every open subgroup being center-free. -/
579 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
581 constructor
582 · intro hslim H
583 rw [Subgroup.eq_bot_iff_forall]
584 intro z hz
585 have hzcent :
586 ((z : ↥((H : Subgroup G))) : G) ∈
587 Subgroup.centralizer ((H : Subgroup G) : Set G) := by
588 rw [Subgroup.mem_centralizer_iff]
589 intro y hy
590 exact congrArg Subtype.val ((Subgroup.mem_center_iff.mp hz) ⟨y, hy⟩)
591 have hzbot : ((z : ↥((H : Subgroup G))) : G) ∈ (⊥ : Subgroup G) := by
592 simpa [hslim H] using hzcent
593 exact Subtype.ext (by simpa using hzbot)
594 · intro hcenter H
595 rw [Subgroup.eq_bot_iff_forall]
596 intro z hz
597 let a : G := (z : G)
598 let V : Subgroup G := (H : Subgroup G) ⊔ Subgroup.zpowers a
599 have hVopen : IsOpen (V : Set G) := by
600 exact Subgroup.isOpen_of_openSubgroup V (show (H : Subgroup G) ≤ V from le_sup_left)
601 let Vopen : OpenSubgroup G := { toSubgroup := V, isOpen' := hVopen }
602 have haV : a ∈ V := by
603 exact
604 (le_sup_right : Subgroup.zpowers a ≤ V)
605 (Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one]⟩)
606 have hHc : (H : Subgroup G) ≤ Subgroup.centralizer ({a} : Set G) := by
607 intro h hh
608 rw [Subgroup.mem_centralizer_iff]
609 intro x hx
610 rcases Set.mem_singleton_iff.mp hx with rfl
611 exact (Subgroup.mem_centralizer_iff.mp hz (h : G) hh).symm
612 have hza : Subgroup.zpowers a ≤ Subgroup.centralizer ({a} : Set G) := by
613 intro x hx
614 rw [Subgroup.mem_centralizer_iff]
615 intro y hy
616 rcases Set.mem_singleton_iff.mp hy with rfl
617 rcases Subgroup.mem_zpowers_iff.mp hx with ⟨n, rfl⟩
618 exact (Commute.refl a).zpow_right n |>.eq
619 have hVle : V ≤ Subgroup.centralizer ({a} : Set G) := sup_le hHc hza
620 have hacenter : (⟨a, haV⟩ : V) ∈ Subgroup.center ↥V := by
621 rw [Subgroup.mem_center_iff]
622 intro x
623 have hxcent : x.1 ∈ Subgroup.centralizer ({a} : Set G) := hVle x.2
624 have hxeq : x.1 * a = a * x.1 := by
625 exact (Subgroup.mem_centralizer_iff.mp hxcent a (by simp only [Set.mem_singleton_iff])).symm
626 ext
627 exact hxeq
628 have hcenV : Subgroup.center ↥((Vopen : OpenSubgroup G) : Subgroup G) = ⊥ := hcenter Vopen
629 have hgoneV : (⟨a, haV⟩ : V) = 1 := by
630 rw [show Vopen.toSubgroup = V by rfl] at hcenV
631 rw [hcenV] at hacenter
632 simpa using hacenter
633 exact congrArg Subtype.val hgoneV
635/-- Slimness forces all open subgroups to be center-free. -/
637 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
639 Subgroup.center ↥((H : Subgroup G)) = ⊥ :=
640 (isSlim_iff_openSubgroups_center_eq_bot (G := G)).1 hslim H
642/-- Center-freeness of all open subgroups implies slimness. -/
644 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
645 (hcenter : ∀ H : OpenSubgroup G, Subgroup.center ↥((H : Subgroup G)) = ⊥) :
647 (isSlim_iff_openSubgroups_center_eq_bot (G := G)).2 hcenter
649/-- An `ab`-faithful profinite group is slim. -/
650theorem isSlim_of_isAbFaithful
651 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
652 [CompactSpace G] [TotallyDisconnectedSpace G]
653 (hG : IsAbFaithful G) :
656 intro H
658 (G := G) hG H
660/-- If the quotient action on the topological abelianization is trivial on a finite-index subgroup,
661then the acting element already lies in the open normal subgroup. -/
663 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
664 (U : OpenNormalSubgroup Q)
665 (hUtf : IsMulTorsionFree (TopologicalAbelianization ↥(U : Subgroup Q)))
666 (hρinj :
667 Function.Injective
668 (quotientConjugationTopologicalAbelianizationMap (G := Q) (N := (U : Subgroup Q))))
669 {c : Q}
670 (B : Subgroup (TopologicalAbelianization ↥(U : Subgroup Q))) [B.FiniteIndex]
671 (htriv :
672 ∀ a : TopologicalAbelianization ↥(U : Subgroup Q),
673 a ∈ B →
674 quotientConjugationTopologicalAbelianizationMap (G := Q) (N := (U : Subgroup Q))
675 (QuotientGroup.mk' (U : Subgroup Q) c) a = a) :
676 c ∈ (U : Subgroup Q) := by
677 let ρ :
678 (Q ⧸ (U : Subgroup Q)) →*
679 MulAut (TopologicalAbelianization ↥(U : Subgroup Q)) :=
680 quotientConjugationTopologicalAbelianizationMap (G := Q) (N := (U : Subgroup Q))
681 letI : IsMulTorsionFree (TopologicalAbelianization ↥(U : Subgroup Q)) := hUtf
682 have hρc : ρ (QuotientGroup.mk' (U : Subgroup Q) c) = 1 := by
683 exact
685 (φ := ρ (QuotientGroup.mk' (U : Subgroup Q) c)) (B := B) htriv
686 have hρone : ρ (QuotientGroup.mk' (U : Subgroup Q) (1 : Q)) = 1 := by
687 dsimp [ρ]
688 exact
690 (G := Q) (N := (U : Subgroup Q)) (x := (1 : Q)) (by
691 rw [Subgroup.mem_center_iff]
692 intro y
693 simp only [mul_one, one_mul])
694 exact
695 (QuotientGroup.eq_one_iff (N := (U : Subgroup Q)) c).1 <|
696 hρinj (hρc.trans hρone.symm)
698/-- If the images of `S ∩ U` have finite index in `Ab(U)` for every open normal supergroup of
699`K`, then the centralizer of `S` is contained in `K`. -/
701 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
702 [CompactSpace Q] [TotallyDisconnectedSpace Q]
703 {K : Subgroup Q} (hKClosed : IsClosed (K : Set Q)) (hKNormal : K.Normal)
704 (hTF :
705 ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
706 IsMulTorsionFree (TopologicalAbelianization ↥(U : Subgroup Q)))
707 (hFaithful :
708 ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
709 Function.Injective
711 (G := Q) (N := (U : Subgroup Q))))
712 (S : Subgroup Q)
713 (hLarge :
714 ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
715 Finite
716 ((TopologicalAbelianization ↥(U : Subgroup Q)) ⧸
717 subgroupImageInTopologicalAbelianization (Q := Q) S U)) :
718 Subgroup.centralizer (S : Set Q) ≤ K := by
719 letI : K.Normal := hKNormal
720 let Kclosed : ClosedSubgroup Q := ⟨K, hKClosed⟩
721 have hK_eq :
722 K =
723 sInf {N : Subgroup Q | IsOpen (N : Set Q) ∧ K ≤ N ∧ N.Normal} := by
724 change (Kclosed : Subgroup Q) =
725 sInf {N : Subgroup Q | IsOpen (N : Set Q) ∧ K ≤ N ∧ N.Normal}
726 exact ProCGroups.ProC.closedSubgroup_eq_sInf_openNormal (G := Q) Kclosed
727 intro c hc
728 rw [hK_eq]
729 simp only [Subgroup.mem_sInf]
730 intro N hN
731 let U : OpenNormalSubgroup Q :=
732 { toSubgroup := N
733 isOpen' := hN.1
734 isNormal' := hN.2.2 }
735 let B : Subgroup (TopologicalAbelianization ↥(U : Subgroup Q)) :=
736 subgroupImageInTopologicalAbelianization (Q := Q) S U
737 letI : Finite ((TopologicalAbelianization ↥(U : Subgroup Q)) ⧸ B) := hLarge U hN.2.1
738 letI : B.FiniteIndex := Subgroup.finiteIndex_of_finite_quotient (H := B)
739 exact
741 (Q := Q) U (hTF U hN.2.1) (hFaithful U hN.2.1) (c := c) (B := B) (by
742 intro a ha
743 letI : (U : Subgroup Q).Normal := U.isNormal'
744 rcases ha with ⟨x, hx, rfl⟩
745 have hxSU : (x : Q) ∈ S ⊓ (U : Subgroup Q) := by
746 simpa [Subgroup.mem_subgroupOf] using hx
747 have hxS : (x : Q) ∈ S := hxSU.1
748 have hcomm : c * (x : Q) = (x : Q) * c := by
749 exact (Subgroup.mem_centralizer_iff.mp hc (x : Q) hxS).symm
750 exact
752 (G := Q) (N := (U : Subgroup Q)) (g := c) (x := x) hcomm)
754/-- The centralizer of an open subgroup is contained in `K` whenever every open normal supergroup
755of `K` has torsion-free abelianization and faithful quotient action. -/
757 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
758 [CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q]
759 {K : Subgroup Q} (hKClosed : IsClosed (K : Set Q)) (hKNormal : K.Normal)
760 (hTF :
761 ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
762 IsMulTorsionFree (TopologicalAbelianization ↥(U : Subgroup Q)))
763 (hFaithful :
764 ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
765 Function.Injective
767 (G := Q) (N := (U : Subgroup Q))))
768 (H : OpenSubgroup Q) :
769 Subgroup.centralizer (H : Set Q) ≤ K := by
770 refine
772 (Q := Q) (K := K) hKClosed hKNormal hTF hFaithful (S := (H : Subgroup Q)) ?_
773 intro U hKU
774 let SU : OpenSubgroup ↥(U : Subgroup Q) :=
776 let A : Type u := TopologicalAbelianization ↥(U : Subgroup Q)
777 let B : Subgroup A :=
778 subgroupImageInTopologicalAbelianization (Q := Q) (S := (H : Subgroup Q)) U
779 have hBOpen : IsOpen (B : Set A) := by
780 dsimp [B, subgroupImageInTopologicalAbelianization, SU, A, TopologicalAbelianization.mk]
781 simpa using
782 (QuotientGroup.isOpenMap_coe
783 (N := Subgroup.closedCommutator (U : Subgroup Q)))
784 _ SU.isOpen'
785 have hUClosed : IsClosed ((U : Subgroup Q) : Set Q) := U.isClosed
786 haveI : CompactSpace ↥(U : Subgroup Q) := by
787 simpa using
788 (inferInstance : CompactSpace (⟨(U : Subgroup Q), hUClosed⟩ : ClosedSubgroup Q))
789 letI : CompactSpace A := by
790 dsimp [A]
791 infer_instance
792 exact Subgroup.quotient_finite_of_isOpen B hBOpen
794/-- If the topological closure of `S` is open, then the centralizer of `S` is already contained in
795`K` under the same torsion-free and faithful hypotheses. -/
797 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
798 [CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q]
799 {K S : Subgroup Q} (hKClosed : IsClosed (K : Set Q)) (hKNormal : K.Normal)
800 (hTF :
801 ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
802 IsMulTorsionFree (TopologicalAbelianization ↥(U : Subgroup Q)))
803 (hFaithful :
804 ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
805 Function.Injective
807 (G := Q) (N := (U : Subgroup Q))))
808 (hSOpen : IsOpen (((S.topologicalClosure : Subgroup Q) : Set Q))) :
809 Subgroup.centralizer (S : Set Q) ≤ K := by
810 let H : OpenSubgroup Q := ⟨S.topologicalClosure, hSOpen⟩
811 have hH :
812 Subgroup.centralizer (((S.topologicalClosure : Subgroup Q) : Set Q)) ≤ K := by
813 simpa [H] using
815 (Q := Q) (K := K) hKClosed hKNormal hTF hFaithful H
816 intro g hg
817 have hg' : g ∈ Subgroup.centralizer (((S.topologicalClosure : Subgroup Q) : Set Q)) := by
818 have hcentralizer :
819 Subgroup.centralizer (((S.topologicalClosure : Subgroup Q) : Set Q)) =
820 Subgroup.centralizer (S : Set Q) := by
821 simpa [ProCGroups.GroupTheory.centralizer] using
823 rw [hcentralizer]
824 exact hg
825 exact hH hg'
827/-- The map induced on topological abelianizations by a subgroup inclusion. -/
828noncomputable def topologicalAbelianizationInclusion
829 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
830 {S T : Subgroup G} (hST : S ≤ T) :
831 TopologicalAbelianization ↥S →ₜ* TopologicalAbelianization ↥T :=
832 TopologicalAbelianization.map
833 { toMonoidHom := Subgroup.inclusion hST
834 continuous_toFun := by
835 exact Continuous.subtype_mk continuous_subtype_val (fun x => hST x.2) }
837/-- The individual transfer term landing in an open normal subgroup. -/
838noncomputable def openNormalTransferTerm
839 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
840 (N : OpenNormalSubgroup G)
841 (q : G ⧸ (N : Subgroup G)) (g : G) :
842 ↥(N : Subgroup G) := by
843 letI : (N : Subgroup G).Normal := N.isNormal'
844 let ρ : G ⧸ (N : Subgroup G) → G :=
845 quotientOpenSubgroupSection (N : Subgroup G)
847 QuotientGroup.mk' (N : Subgroup G)
848 refine ⟨(ρ ((QuotientGroup.mk' (N : Subgroup G) g) * q))⁻¹ * g * ρ q, ?_⟩
849 have hρ :
850 Function.RightInverse ρ (QuotientGroup.mk (s := (N : Subgroup G))) :=
851 quotientOpenSubgroupSection_rightInverse (N : Subgroup G)
852 have hρ₁ :
854 (QuotientGroup.mk' (N : Subgroup G) g) * q := by
858 have hmem :
860 calc
864 _ =
865 (((QuotientGroup.mk' (N : Subgroup G) g) * q))⁻¹ *
866 QuotientGroup.mk' (N : Subgroup G) g * q := by
867 rw [hρ₁, hρ₂]
868 _ = 1 := by
869 simp only [QuotientGroup.mk'_apply, mul_inv_rev, mul_assoc, inv_mul_cancel, mul_one]
870 exact
871 (QuotientGroup.eq_one_iff
872 (N := (N : Subgroup G))
873 ((ρ ((QuotientGroup.mk' (N : Subgroup G) g) * q))⁻¹ * g * ρ q)).1 hmem
875/-- Transfer on topological abelianization, before passing to the quotient universal property. -/
876noncomputable def openNormalTransferTopologicalAbelianizationPre
877 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
878 (N : OpenNormalSubgroup G) [Finite (G ⧸ (N : Subgroup G))] :
879 G →ₜ* TopologicalAbelianization ↥(N : Subgroup G) := by
880 classical
881 letI : (N : Subgroup G).Normal := N.isNormal'
882 letI : Fintype (G ⧸ (N : Subgroup G)) := Fintype.ofFinite _
883 refine
884 { toMonoidHom :=
885 { toFun := fun g =>
886 ∏ q : G ⧸ (N : Subgroup G),
887 TopologicalAbelianization.mk ↥(N : Subgroup G)
888 (openNormalTransferTerm (G := G) N q g)
889 map_one' := by
890 let f : G ⧸ (N : Subgroup G) → TopologicalAbelianization ↥(N : Subgroup G) :=
891 fun q =>
892 TopologicalAbelianization.mk ↥(N : Subgroup G)
893 (openNormalTransferTerm (G := G) N q 1)
894 have hf : ∀ q : G ⧸ (N : Subgroup G), f q = 1 := by
895 intro q
896 change
897 TopologicalAbelianization.mk ↥(N : Subgroup G)
898 (openNormalTransferTerm (G := G) N q 1) = 1
899 have hterm : openNormalTransferTerm (G := G) N q 1 = 1 := by
900 apply Subtype.ext
901 simp only [openNormalTransferTerm, QuotientGroup.mk'_apply, QuotientGroup.mk_one, one_mul, mul_one,
902 inv_mul_cancel, OneMemClass.coe_one]
904 simpa [f] using Fintype.prod_eq_one f hf
905 map_mul' := by
906 intro g h
907 let f : G ⧸ (N : Subgroup G) → TopologicalAbelianization ↥(N : Subgroup G) :=
908 fun q =>
909 TopologicalAbelianization.mk ↥(N : Subgroup G)
910 (openNormalTransferTerm (G := G) N q g)
911 let k : G ⧸ (N : Subgroup G) → TopologicalAbelianization ↥(N : Subgroup G) :=
912 fun q =>
913 TopologicalAbelianization.mk ↥(N : Subgroup G)
914 (openNormalTransferTerm (G := G) N q h)
915 calc
916 (∏ q : G ⧸ (N : Subgroup G),
917 TopologicalAbelianization.mk ↥(N : Subgroup G)
918 (openNormalTransferTerm (G := G) N q (g * h))) =
919 ∏ q : G ⧸ (N : Subgroup G),
920 f ((QuotientGroup.mk' (N : Subgroup G) h) * q) * k q := by
921 apply Fintype.prod_congr
922 intro q
923 have hterm :
924 openNormalTransferTerm (G := G) N q (g * h) =
925 openNormalTransferTerm (G := G) N
926 ((QuotientGroup.mk' (N : Subgroup G) h) * q) g *
927 openNormalTransferTerm (G := G) N q h := by
928 apply Subtype.ext
929 dsimp [openNormalTransferTerm]
930 simp only [mul_assoc, mul_inv_cancel_left]
931 have hterm :=
932 congrArg (TopologicalAbelianization.mk ↥(N : Subgroup G)) hterm
934 _ =
935 (∏ q : G ⧸ (N : Subgroup G), f ((QuotientGroup.mk' (N : Subgroup G) h) * q)) *
936 ∏ q : G ⧸ (N : Subgroup G), k q := by
937 rw [Finset.prod_mul_distrib]
938 _ = (∏ q : G ⧸ (N : Subgroup G), f q) * ∏ q : G ⧸ (N : Subgroup G), k q := by
939 exact congrArg
940 (fun z => z * ∏ q : G ⧸ (N : Subgroup G), k q)
941 (Equiv.prod_comp
942 (Equiv.mulLeft (QuotientGroup.mk' (N : Subgroup G) h)) f)
943 _ = _ := rfl }
944 continuous_toFun := by
945 exact continuous_finset_prod Finset.univ fun q _ => by
946 letI : (N : Subgroup G).Normal := N.isNormal'
947 let ρ : G ⧸ (N : Subgroup G) → G :=
948 quotientOpenSubgroupSection (N : Subgroup G)
950 { toMonoidHom := QuotientGroup.mk' (N : Subgroup G)
951 continuous_toFun := continuous_quotient_mk' }
952 have hρcont : Continuous ρ := by
953 letI : ContinuousMul G := (‹IsTopologicalGroup G›).toContinuousMul
954 letI : ContinuousInv G := (‹IsTopologicalGroup G›).toContinuousInv
955 letI : DiscreteTopology (G ⧸ (N : Subgroup G)) :=
956 QuotientGroup.discreteTopology N.isOpen'
957 simpa [ρ] using
958 (continuous_of_discreteTopology :
959 Continuous (quotientOpenSubgroupSection (N : Subgroup G)))
962 have hbase :
963 Continuous (fun g : G =>
964 (ρ ((QuotientGroup.mk' (N : Subgroup G) g) * q))⁻¹ * g * ρ q) := by
965 exact ((hρcont.comp hqcont).inv.mul continuous_id).mul continuous_const
966 exact
967 (continuous_quotient_mk' :
968 Continuous (TopologicalAbelianization.mk ↥(N : Subgroup G))).comp
969 (Continuous.subtype_mk hbase (fun g => (openNormalTransferTerm (G := G) N q g).2)) }
971/-- Transfer map on topological abelianizations. -/
972noncomputable def openNormalTransferTopologicalAbelianization
973 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [T1Space G]
974 (N : OpenNormalSubgroup G) [Finite (G ⧸ (N : Subgroup G))] :
975 TopologicalAbelianization G →ₜ* TopologicalAbelianization ↥(N : Subgroup G) :=
976 TopologicalAbelianization.lift
977 (openNormalTransferTopologicalAbelianizationPre (G := G) N)
979/-- Transfer sends a fixed point to the `|G/N|`-th power of that point. -/
981 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [T1Space G]
982 (N : OpenNormalSubgroup G) [Finite (G ⧸ (N : Subgroup G))]
983 {a : TopologicalAbelianization ↥(N : Subgroup G)}
984 (hfix :
985 ∀ q : G ⧸ (N : Subgroup G),
986 quotientConjugationTopologicalAbelianizationMap (G := G) (N := (N : Subgroup G)) q a = a) :
987 openNormalTransferTopologicalAbelianization (G := G) N
988 (TopologicalAbelianization.map
990 continuous_toFun := continuous_subtype_val } a) =
991 a ^ Nat.card (G ⧸ (N : Subgroup G)) := by
992 classical
993 letI : (N : Subgroup G).Normal := N.isNormal'
994 letI : Fintype (G ⧸ (N : Subgroup G)) := Fintype.ofFinite _
995 let ιN : ↥(N : Subgroup G) →ₜ* G :=
997 continuous_toFun := continuous_subtype_val }
998 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective
999 (Subgroup.closedCommutator (N : Subgroup G)) a
1000 have hmap :
1001 TopologicalAbelianization.map ιN
1002 (TopologicalAbelianization.mk ↥(N : Subgroup G) x) =
1003 TopologicalAbelianization.mk G (ιN x) := by
1004 rfl
1005 have hlift :
1006 TopologicalAbelianization.lift
1007 (openNormalTransferTopologicalAbelianizationPre (G := G) N)
1008 (TopologicalAbelianization.mk G (ιN x)) =
1009 openNormalTransferTopologicalAbelianizationPre (G := G) N (ιN x) := by
1010 rfl
1011 change
1012 openNormalTransferTopologicalAbelianization (G := G) N
1013 (TopologicalAbelianization.map ιN
1014 (TopologicalAbelianization.mk ↥(N : Subgroup G) x)) =
1015 (TopologicalAbelianization.mk ↥(N : Subgroup G) x) ^ Nat.card (G ⧸ (N : Subgroup G))
1016 rw [openNormalTransferTopologicalAbelianization, hmap, hlift]
1017 let ρ : G ⧸ (N : Subgroup G) → G :=
1018 quotientOpenSubgroupSection (N : Subgroup G)
1019 have hρ :
1020 Function.RightInverse ρ (QuotientGroup.mk (s := (N : Subgroup G))) :=
1021 quotientOpenSubgroupSection_rightInverse (N : Subgroup G)
1022 have hterm :
1023 ∀ q : G ⧸ (N : Subgroup G),
1024 TopologicalAbelianization.mk ↥(N : Subgroup G)
1025 (openNormalTransferTerm (G := G) N q x) =
1026 TopologicalAbelianization.mk ↥(N : Subgroup G) x := by
1027 intro q
1028 have hxq : (QuotientGroup.mk' (N : Subgroup G) (x : G)) * q = q := by
1029 simp only [QuotientGroup.mk'_apply, mul_eq_right, QuotientGroup.eq_one_iff, SetLike.coe_mem]
1030 have htransfer :
1031 openNormalTransferTerm (G := G) N q x =
1032 (MulAut.conjNormal ((ρ q)⁻¹)) x := by
1033 apply Subtype.ext
1034 have hρxq' :
1035 quotientOpenSubgroupSection (N : Subgroup G)
1036 (((x : G) : G ⧸ (N : Subgroup G)) * q) =
1037 quotientOpenSubgroupSection (N : Subgroup G) q := by
1038 simpa using congrArg (quotientOpenSubgroupSection (N : Subgroup G)) hxq
1039 dsimp [openNormalTransferTerm]
1040 rw [hρxq']
1042 have hqinv : QuotientGroup.mk' (N : Subgroup G) ((ρ q)⁻¹ : G) = q⁻¹ := by
1043 simpa [map_inv] using
1044 congrArg Inv.inv
1045 (show QuotientGroup.mk' (N : Subgroup G) (ρ q) = q from by
1046 simpa using hρ q)
1047 have hfix' := hfix q⁻¹
1048 have haction :
1049 quotientConjugationTopologicalAbelianizationMap (G := G) (N := (N : Subgroup G))
1050 (QuotientGroup.mk' (N : Subgroup G) ((ρ q)⁻¹ : G))
1051 (TopologicalAbelianization.mk ↥(N : Subgroup G) x) =
1052 TopologicalAbelianization.mk ↥(N : Subgroup G)
1053 (openNormalTransferTerm (G := G) N q x) := by
1054 calc
1055 quotientConjugationTopologicalAbelianizationMap (G := G) (N := (N : Subgroup G))
1056 (QuotientGroup.mk' (N : Subgroup G) ((ρ q)⁻¹ : G))
1057 (TopologicalAbelianization.mk ↥(N : Subgroup G) x) =
1058 TopologicalAbelianization.mk ↥(N : Subgroup G)
1059 ((MulAut.conjNormal ((ρ q)⁻¹)) x) := by
1060 simpa using
1062 (N := (N : Subgroup G)) (g := ((ρ q)⁻¹ : G)) (n := x))
1063 _ =
1064 TopologicalAbelianization.mk ↥(N : Subgroup G)
1065 (openNormalTransferTerm (G := G) N q x) := by
1066 rw [htransfer]
1067 calc
1068 TopologicalAbelianization.mk ↥(N : Subgroup G)
1069 (openNormalTransferTerm (G := G) N q x) =
1070 quotientConjugationTopologicalAbelianizationMap (G := G) (N := (N : Subgroup G))
1071 (QuotientGroup.mk' (N : Subgroup G) ((ρ q)⁻¹ : G))
1072 (TopologicalAbelianization.mk ↥(N : Subgroup G) x) := by
1073 symm
1074 exact haction
1075 _ =
1076 quotientConjugationTopologicalAbelianizationMap (G := G) (N := (N : Subgroup G))
1077 (q⁻¹) (TopologicalAbelianization.mk ↥(N : Subgroup G) x) := by
1078 rw [hqinv]
1079 _ = TopologicalAbelianization.mk ↥(N : Subgroup G) x := hfix'
1080 calc
1081 (∏ q : G ⧸ (N : Subgroup G),
1082 TopologicalAbelianization.mk ↥(N : Subgroup G)
1083 (openNormalTransferTerm (G := G) N q x)) =
1084 ∏ _q : G ⧸ (N : Subgroup G), TopologicalAbelianization.mk ↥(N : Subgroup G) x := by
1085 apply Fintype.prod_congr
1086 intro q
1087 exact hterm q
1088 _ =
1089 (TopologicalAbelianization.mk ↥(N : Subgroup G) x) ^
1090 Fintype.card (G ⧸ (N : Subgroup G)) := by
1091 simp only [ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.coe_coe, Finset.prod_const, Finset.card_univ]
1092 _ =
1093 (TopologicalAbelianization.mk ↥(N : Subgroup G) x) ^
1094 Nat.card (G ⧸ (N : Subgroup G)) := by
1095 rw [Nat.card_eq_fintype_card]
1097/-- If the ambient inclusion into topological abelianization is trivial on a fixed point, then the
1098fixed point itself is trivial under torsion-freeness. -/
1100 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [T1Space G]
1101 (N : OpenNormalSubgroup G) [Finite (G ⧸ (N : Subgroup G))]
1102 (hNtf : IsMulTorsionFree (TopologicalAbelianization ↥(N : Subgroup G)))
1103 {a : TopologicalAbelianization ↥(N : Subgroup G)}
1104 (hfix :
1105 ∀ q : G ⧸ (N : Subgroup G),
1106 quotientConjugationTopologicalAbelianizationMap (G := G) (N := (N : Subgroup G)) q a = a)
1107 (ha :
1108 TopologicalAbelianization.map
1110 continuous_toFun := continuous_subtype_val } a = 1) :
1111 a = 1 := by
1112 classical
1113 letI : (N : Subgroup G).Normal := N.isNormal'
1114 letI : Fintype (G ⧸ (N : Subgroup G)) := Fintype.ofFinite _
1115 have hpow :=
1116 openNormalTransferTopologicalAbelianization_eq_pow_of_fixed (G := G) N hfix
1117 have hpow' :
1118 openNormalTransferTopologicalAbelianization (G := G) N
1119 (TopologicalAbelianization.map
1121 continuous_toFun := continuous_subtype_val } a) =
1122 a ^ Nat.card (G ⧸ (N : Subgroup G)) := by
1123 simpa [Nat.card_eq_fintype_card] using hpow
1124 have hpow1 : a ^ Nat.card (G ⧸ (N : Subgroup G)) = 1 := by
1125 calc
1126 a ^ Nat.card (G ⧸ (N : Subgroup G)) =
1127 openNormalTransferTopologicalAbelianization (G := G) N
1128 (TopologicalAbelianization.map
1130 continuous_toFun := continuous_subtype_val } a) := by
1131 rw [hpow']
1132 _ = openNormalTransferTopologicalAbelianization (G := G) N 1 := by
1133 rw [ha]
1134 _ = 1 := by
1135 simp only [openNormalTransferTopologicalAbelianization, map_one]
1136 have hcard : Nat.card (G ⧸ (N : Subgroup G)) ≠ 0 := by
1137 rw [Nat.card_eq_fintype_card]
1138 exact Fintype.card_ne_zero
1139 letI : IsMulTorsionFree (TopologicalAbelianization ↥(N : Subgroup G)) := hNtf
1140 have hpowEq :
1141 a ^ Nat.card (G ⧸ (N : Subgroup G)) =
1142 (1 : TopologicalAbelianization ↥(N : Subgroup G)) ^ Nat.card (G ⧸ (N : Subgroup G)) := by
1143 simpa using hpow1
1144 exact
1145 (IsMulTorsionFree.pow_left_injective
1146 (M := TopologicalAbelianization ↥(N : Subgroup G)) hcard) hpowEq
1148/-- A nontrivial class in `Ab(K)` survives in some open normal supergroup of `K`. -/
1150 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
1151 [CompactSpace G] [TotallyDisconnectedSpace G]
1152 {K : Subgroup G} (hKClosed : IsClosed (K : Set G)) (hKNormal : K.Normal)
1153 {a : TopologicalAbelianization ↥K} (hne : a ≠ 1) :
1154 ∃ H : OpenNormalSubgroup G, ∃ hKH : K ≤ (H : Subgroup G),
1155 topologicalAbelianizationInclusion hKH a ≠ 1 := by
1156 classical
1157 let hGprof : ProCGroups.IsProfiniteGroup G := by
1158 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
1159 let T : ClosedSubgroup G := ⟨K, hKClosed⟩
1160 letI : K.Normal := hKNormal
1161 let hKprof : IsProfiniteGroup ↥K :=
1162 IsProfiniteGroup.of_closedSubgroup (G := G) hGprof T
1163 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective
1165 let A := TopologicalAbelianization ↥K
1166 have hxne : TopologicalAbelianization.mk ↥K x ≠ 1 := hne
1167 have hAprof : IsProfiniteGroup A := by
1168 letI : T2Space ↥K := IsProfiniteGroup.t2Space hKprof
1169 simpa [A] using
1171 (G := ↥K) hKprof
1173 letI : CompactSpace A := IsProfiniteGroup.compactSpace hAprof
1174 letI : T2Space A := IsProfiniteGroup.t2Space hAprof
1175 letI : TotallyDisconnectedSpace A := IsProfiniteGroup.totallyDisconnectedSpace hAprof
1176 obtain ⟨Uab, hxUab⟩ :=
1177 ProCGroups.ProC.exists_openNormalSubgroup_not_mem (G := A) hAprof hxne
1178 let qA : A →* A ⧸ (Uab : Subgroup A) := QuotientGroup.mk' (Uab : Subgroup A)
1179 have hqAx_ne : qA (TopologicalAbelianization.mk ↥K x) ≠ 1 := by
1180 intro hq
1181 exact hxUab ((QuotientGroup.eq_one_iff (N := (Uab : Subgroup A))
1182 (TopologicalAbelianization.mk ↥K x)).1 hq)
1183 let N0 : OpenNormalSubgroup ↥K :=
1184 OpenNormalSubgroup.comap
1185 (TopologicalAbelianization.mk ↥K)
1186 (by
1187 simpa [TopologicalAbelianization.mk] using
1188 (continuous_quotient_mk' :
1189 Continuous (QuotientGroup.mk' (Subgroup.closedCommutator K)))) Uab
1190 have hN0ker :
1192 intro y hy
1193 change qA (TopologicalAbelianization.mk ↥K y) = 1
1194 exact (QuotientGroup.eq_one_iff (N := (Uab : Subgroup A))
1195 (TopologicalAbelianization.mk ↥K y)).2 hy
1196 letI : T2Space G := inferInstance
1197 obtain ⟨V, hVK⟩ :=
1198 exists_openNormalSubgroup_inter_closedSubgroup_le (G := G) hGprof T N0.toOpenSubgroup
1199 let Hsub : Subgroup G := K ⊔ (V : Subgroup G)
1200 have hHopen : IsOpen (Hsub : Set G) := by
1201 exact Subgroup.isOpen_of_openSubgroup Hsub
1202 (show (V : Subgroup G) ≤ Hsub from le_sup_right)
1203 let H : OpenNormalSubgroup G :=
1204 { toOpenSubgroup := ⟨Hsub, hHopen⟩
1205 isNormal' := by
1206 change (K ⊔ (V : Subgroup G)).Normal
1207 infer_instance }
1208 have hKH : K ≤ (H : Subgroup G) := le_sup_left
1209 let ι : ↥K →* ↥(H : Subgroup G) := Subgroup.inclusion hKH
1210 let qT : ↥K →* A ⧸ (Uab : Subgroup A) :=
1211 qA.comp (TopologicalAbelianization.mk ↥K)
1212 let VK : OpenNormalSubgroup ↥K :=
1213 OpenNormalSubgroup.comap (K.subtype) continuous_subtype_val V
1214 have hVKker : (VK : Subgroup ↥K) ≤ qT.ker := by
1215 exact (show (VK : Subgroup ↥K) ≤ (N0 : Subgroup ↥K) from hVK).trans hN0ker
1216 let L : Subgroup (G ⧸ (V : Subgroup G)) :=
1217 Subgroup.map (QuotientGroup.mk' (V : Subgroup G)) K
1218 let ψ : ↥K →* L :=
1219 { toFun := fun y => ⟨QuotientGroup.mk' (V : Subgroup G) y.1, ⟨y.1, y.2, rfl⟩⟩
1220 map_one' := by ext; rfl
1221 map_mul' := by intro y z; ext; rfl }
1222 have hψsurj : Function.Surjective ψ := by
1223 intro z
1224 rcases z with ⟨z, hz⟩
1225 rcases hz with ⟨y, hy, hyz⟩
1226 refine ⟨⟨y, hy⟩, ?_⟩
1227 apply Subtype.ext
1228 exact hyz
1229 have hψker : (VK : Subgroup ↥K) = ψ.ker := by
1230 ext y
1231 constructor
1232 · intro hy
1233 change ψ y = 1
1234 apply Subtype.ext
1235 exact (QuotientGroup.eq_one_iff (N := (V : Subgroup G)) y.1).2 hy
1236 · intro hy
1237 exact (QuotientGroup.eq_one_iff (N := (V : Subgroup G)) y.1).1 <| congrArg Subtype.val hy
1238 let qTquot : ↥K ⧸ ψ.ker →* A ⧸ (Uab : Subgroup A) :=
1239 QuotientGroup.lift ψ.ker qT (by simpa [hψker] using hVKker)
1240 let qL : L →* A ⧸ (Uab : Subgroup A) :=
1241 qTquot.comp (QuotientGroup.quotientKerEquivOfSurjective ψ hψsurj).symm.toMonoidHom
1242 have hLdisc : DiscreteTopology L := by infer_instance
1243 let qLcont : L →ₜ* A ⧸ (Uab : Subgroup A) :=
1244 { toMonoidHom := qL
1245 continuous_toFun := continuous_of_discreteTopology }
1246 let qHaux : ↥(H : Subgroup G) →* L :=
1247 { toFun := fun y =>
1248 ⟨QuotientGroup.mk' (V : Subgroup G) y.1, by
1249 have hyHsub : y.1 ∈ Hsub := y.2
1250 have hydecomp : ∃ t ∈ K, ∃ v ∈ (V : Subgroup G), t * v = y.1 := by
1251 exact (Subgroup.mem_sup_of_normal_right
1252 (s := K) (t := (V : Subgroup G)) (x := y.1)).1 hyHsub
1253 change QuotientGroup.mk' (V : Subgroup G) y.1 ∈
1254 Subgroup.map (QuotientGroup.mk' (V : Subgroup G)) K
1255 rcases hydecomp with ⟨t, htK, v, hvV, htv⟩
1256 have hv1 : QuotientGroup.mk' (V : Subgroup G) v = 1 := by
1257 exact (QuotientGroup.eq_one_iff (N := (V : Subgroup G)) v).2 hvV
1258 refine ⟨t, htK, ?_⟩
1259 calc
1260 QuotientGroup.mk' (V : Subgroup G) t =
1261 QuotientGroup.mk' (V : Subgroup G) t * 1 := by simp only [QuotientGroup.mk'_apply, mul_one]
1262 _ =
1263 QuotientGroup.mk' (V : Subgroup G) t *
1264 QuotientGroup.mk' (V : Subgroup G) v := by rw [hv1]
1266 _ = QuotientGroup.mk' (V : Subgroup G) y.1 := by rw [htv]⟩
1267 map_one' := by ext; rfl
1268 map_mul' := by intro y z; ext; rfl }
1269 let qH : ↥(H : Subgroup G) →ₜ* A ⧸ (Uab : Subgroup A) :=
1270 { toMonoidHom := qL.comp qHaux
1271 continuous_toFun := by
1272 have hqHaux : Continuous qHaux := by
1273 exact Continuous.subtype_mk
1274 (by simpa [qHaux] using (continuous_quotient_mk'.comp continuous_subtype_val))
1275 (fun y => (qHaux y).2)
1276 exact qLcont.continuous_toFun.comp hqHaux }
1277 have hqH_on_K : ∀ y : ↥K, qH (ι y) = qT y := by
1278 intro y
1279 change qL (qHaux (ι y)) = qT y
1280 have hqHaux : qHaux (ι y) = ψ y := by
1281 apply Subtype.ext
1282 rfl
1283 rw [hqHaux]
1284 change qTquot ((QuotientGroup.quotientKerEquivOfSurjective ψ hψsurj).symm (ψ y)) = qT y
1285 have hmk :
1286 (QuotientGroup.quotientKerEquivOfSurjective ψ hψsurj).symm (ψ y) =
1287 QuotientGroup.mk' ψ.ker y := by
1288 apply (QuotientGroup.quotientKerEquivOfSurjective ψ hψsurj).injective
1289 simpa using
1290 (show
1291 (QuotientGroup.quotientKerEquivOfSurjective ψ hψsurj)
1292 ((QuotientGroup.mk' ψ.ker) y) = ψ y by
1293 rfl)
1294 rw [hmk]
1295 rfl
1296 let fAb : TopologicalAbelianization ↥K →ₜ*
1297 TopologicalAbelianization ↥(H : Subgroup G) :=
1299 have hclosedBot :
1300 IsClosed (((⊥ : Subgroup (A ⧸ (Uab : Subgroup A))) : Set (A ⧸ (Uab : Subgroup A)))) := by
1301 change IsClosed ({(1 : A ⧸ (Uab : Subgroup A))} : Set (A ⧸ (Uab : Subgroup A)))
1302 exact isClosed_singleton
1303 have hcommMapBot :
1304 (commutator ↥(H : Subgroup G)).map (qH : ↥(H : Subgroup G) →* A ⧸ (Uab : Subgroup A)) ≤
1305 (⊥ : Subgroup (A ⧸ (Uab : Subgroup A))) := by
1306 rw [_root_.map_commutator_eq]
1307 refine Subgroup.commutator_le.mpr ?_
1308 intro a ha b hb
1309 change ⁅a, b⁆ = (1 : A ⧸ (Uab : Subgroup A))
1310 exact commutatorElement_eq_one_iff_mul_comm.2 (mul_comm a b)
1311 have hcommClosureBot :
1312 (Subgroup.closedCommutator (H : Subgroup G)).map
1313 (qH : ↥(H : Subgroup G) →* A ⧸ (Uab : Subgroup A)) ≤
1314 (⊥ : Subgroup (A ⧸ (Uab : Subgroup A))) := by
1316 (f := qH)
1317 (G₁ := commutator ↥(H : Subgroup G))
1318 (Q₁ := (⊥ : Subgroup (A ⧸ (Uab : Subgroup A))))
1319 hcommMapBot
1320 hclosedBot
1321 have hbne : fAb (TopologicalAbelianization.mk ↥K x) ≠ 1 := by
1322 intro hb
1323 have hxcomm : ι x ∈ Subgroup.closedCommutator (H : Subgroup G) := by
1324 have hb' : TopologicalAbelianization.mk ↥(H : Subgroup G) (ι x) = 1 := by
1325 change topologicalAbelianizationInclusion hKH (TopologicalAbelianization.mk ↥K x) = 1 at hb
1326 simpa only [fAb, topologicalAbelianizationInclusion, TopologicalAbelianization.map_apply_mk]
1327 using hb
1328 exact
1329 (QuotientGroup.eq_one_iff
1330 (N := Subgroup.closedCommutator (H : Subgroup G))
1331 (ι x)).1 hb'
1332 have hxmap :
1333 qH (ι x) ∈
1334 (Subgroup.closedCommutator (H : Subgroup G)).map
1335 (qH : ↥(H : Subgroup G) →* A ⧸ (Uab : Subgroup A)) := ⟨ι x, hxcomm, rfl⟩
1336 have hxbot : qH (ι x) ∈ (⊥ : Subgroup (A ⧸ (Uab : Subgroup A))) := hcommClosureBot hxmap
1337 have hqHx : qH (ι x) = 1 := by
1338 simpa using hxbot
1339 have hqTx : qT x = 1 := by
1340 simpa [hqH_on_K x] using hqHx
1341 exact hqAx_ne (by simpa [qT] using hqTx)
1342 exact ⟨H, hKH, by simpa [fAb, topologicalAbelianizationInclusion] using hbne⟩
1344/-- If every open normal supergroup of `K` has torsion-free abelianization, then `Ab(K)` has no
1345nontrivial fixed points under the quotient conjugation action. -/
1347 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
1348 [CompactSpace G] [TotallyDisconnectedSpace G]
1349 {K : Subgroup G} (hKClosed : IsClosed (K : Set G))
1350 (hKNormal : K.Normal) (hK : K ≤ topDerivedTop G 1)
1351 (hTF :
1352 ∀ H : OpenNormalSubgroup G, K ≤ (H : Subgroup G) →
1353 IsMulTorsionFree (TopologicalAbelianization ↥(H : Subgroup G))) :
1354 let _ : K.Normal := hKNormal
1356 (quotientConjugationTopologicalAbelianizationMap (G := G) (N := K)) := by
1357 letI : K.Normal := hKNormal
1358 letI : T1Space G := inferInstance
1359 change HasNoNontrivialFixedPoints
1360 (quotientConjugationTopologicalAbelianizationMap (G := G) (N := K))
1361 intro a hfix
1362 by_contra hne
1363 obtain ⟨H, hKH, hHne⟩ :=
1365 (G := G) (K := K) hKClosed hKNormal hne
1366 have hfixH :
1367 ∀ q : G ⧸ (H : Subgroup G),
1368 quotientConjugationTopologicalAbelianizationMap (G := G) (N := (H : Subgroup G)) q
1369 (topologicalAbelianizationInclusion hKH a) =
1370 topologicalAbelianizationInclusion hKH a := by
1371 letI : K.Normal := hKNormal
1372 intro q
1373 obtain ⟨g, rfl⟩ := QuotientGroup.mk'_surjective (H : Subgroup G) q
1374 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective
1376 have hconj :
1378 (quotientConjugationTopologicalAbelianizationMap (G := G) (N := K)
1379 (QuotientGroup.mk' K g) (TopologicalAbelianization.mk ↥K x)) =
1380 quotientConjugationTopologicalAbelianizationMap (G := G) (N := (H : Subgroup G))
1381 (QuotientGroup.mk' (H : Subgroup G) g)
1382 (topologicalAbelianizationInclusion hKH (TopologicalAbelianization.mk ↥K x)) := by
1383 simp only [QuotientGroup.mk'_apply]
1384 change
1386 (TopologicalAbelianization.mk ↥K ((MulAut.conjNormal g) x)) =
1387 TopologicalAbelianization.mk ↥(H : Subgroup G)
1388 ((MulAut.conjNormal g) ((Subgroup.inclusion hKH) x))
1389 simp only [topologicalAbelianizationInclusion, ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.coe_coe]
1390 rfl
1391 exact hconj.trans
1392 (congrArg (topologicalAbelianizationInclusion hKH) (hfix (QuotientGroup.mk' K g)))
1393 have haH :
1394 TopologicalAbelianization.map
1396 continuous_toFun := continuous_subtype_val }
1397 (topologicalAbelianizationInclusion hKH a) = 1 := by
1398 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective
1400 have hx1 : TopologicalAbelianization.mk G x.1 = 1 := by
1401 exact
1402 (QuotientGroup.eq_one_iff
1403 (N := Subgroup.closedCommutator G) x.1).2
1404 (by simpa [topDerivedTop] using hK x.2)
1405 change
1406 TopologicalAbelianization.map
1408 continuous_toFun := continuous_subtype_val }
1409 (topologicalAbelianizationInclusion hKH (TopologicalAbelianization.mk ↥K x)) = 1
1410 simpa only [topologicalAbelianizationInclusion, TopologicalAbelianization.map_apply_mk] using hx1
1411 have hHtf : IsMulTorsionFree (TopologicalAbelianization ↥(H : Subgroup G)) := hTF H hKH
1412 exact hHne <|
1414 (G := G) H hHtf hfixH haH
1416/-- The local torsion-free abelianization hypothesis rules out nontrivial fixed points on every
1417closed normal subgroup contained in the first closed derived subgroup. -/
1419 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
1420 [CompactSpace G] [TotallyDisconnectedSpace G]
1421 {K : Subgroup G} (hKClosed : IsClosed (K : Set G))
1422 (hKNormal : K.Normal) (hK : K ≤ topDerivedTop G 1)
1423 (hG : IsAbTorsionFree G) :
1424 let _ : K.Normal := hKNormal
1426 (quotientConjugationTopologicalAbelianizationMap (G := G) (N := K)) := by
1427 exact
1429 (G := G) hKClosed hKNormal hK (fun H _ => hG H.toOpenSubgroup)
1431/-- Open subgroups above the last derived subgroup in a maximal finite-step solvable
1432quotient have torsion-free topological abelianization under the ambient `ab`-torsion-free
1433hypothesis. -/
1435 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
1436 [CompactSpace G]
1437 (hG : IsAbTorsionFree G)
1438 {m : ℕ} (hm : 2 ≤ m)
1439 (H : OpenSubgroup (MaxSolvQuot G m))
1440 (hH : aboveLastDerived (G := G) m H) :
1441 IsMulTorsionFree
1442 (TopologicalAbelianization ↥(H : Subgroup (MaxSolvQuot G m))) := by
1443 let Q : Type u := MaxSolvQuot G m
1444 let π : G →ₜ* Q := continuousToMaxSolvQuot G m
1445 let Hpre : OpenSubgroup G := preimageOpenSubgroup π H
1447 simpa [π, Q] using continuousToMaxSolvQuot_surjective (G := G) m
1448 have hder_pre : topDerivedTop G (m - 1) ≤ ((H : Subgroup Q).comap (π : G →* Q)) := by
1449 intro x hx
1450 exact hH ((topDerivedTop_le_comap (f := π) (m := m - 1)) hx)
1451 have hm1 : 1 ≤ m := le_trans (by decide) hm
1452 have hker :
1454 (topDerivedTop ↥((Hpre : Subgroup G)) 1).map ((Hpre : Subgroup G).subtype) := by
1458 have hclosed :
1459 IsClosedMap (π.restrictPreimage (H : Subgroup Q)) := by
1460 exact
1463 ((continuousToMaxSolvQuot G m).continuous_toFun.isClosedMap)
1464 (Subgroup.isClosed_of_isOpen (H : Subgroup Q) H.isOpen')
1465 let e :
1466 MaxSolvQuot ↥((Hpre : Subgroup G)) 1 ≃*
1467 MaxSolvQuot ↥(H : Subgroup Q) 1 :=
1468 Classical.choice <|
1469 preimageOpenSubgroup_maxSolvQuot_mulEquiv_of_ker_le π hπsurj H hclosed 1 hker
1470 have hpreTF : IsMulTorsionFree (TopologicalAbelianization ↥((Hpre : Subgroup G))) := hG Hpre
1471 have hpreTF' : IsMulTorsionFree (MaxSolvQuot ↥((Hpre : Subgroup G)) 1) := by
1472 exact
1474 ↥((Hpre : Subgroup G)) hpreTF
1475 letI : IsMulTorsionFree (MaxSolvQuot ↥((Hpre : Subgroup G)) 1) := hpreTF'
1476 change IsMulTorsionFree (MaxSolvQuot ↥(H : Subgroup Q) 1)
1477 exact e.isMulTorsionFree
1479/-- Open normal supergroups above the last derived subgroup in a maximal finite-step solvable
1480quotient have torsion-free topological abelianization under the ambient `ab`-torsion-free
1481hypothesis. -/
1483 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
1484 [CompactSpace G]
1485 (hG : IsAbTorsionFree G)
1486 {m : ℕ} (hm : 2 ≤ m)
1487 (U : OpenNormalSubgroup (MaxSolvQuot G m))
1488 (hU : lastDerivedSubgroup (G := G) m ≤ (U : Subgroup (MaxSolvQuot G m))) :
1489 IsMulTorsionFree
1490 (TopologicalAbelianization ↥(U : Subgroup (MaxSolvQuot G m))) := by
1491 simpa using
1493 (G := G) hG hm U.toOpenSubgroup hU
1495/-- The `m`-th closed derived subgroup vanishes in the maximal `m`-step solvable quotient. -/
1497 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
1498 [CompactSpace G] [TotallyDisconnectedSpace G]
1499 (m : ℕ) :
1500 topDerivedTop (MaxSolvQuot G m) m = ⊥ := by
1501 let Q : Type u := MaxSolvQuot G m
1502 let π : G →ₜ* Q := continuousToMaxSolvQuot G m
1503 letI : T2Space Q := by
1504 dsimp [Q, MaxSolvQuot]
1505 infer_instance
1507 simpa [Q, π] using continuousToMaxSolvQuot_surjective (G := G) m
1508 have hclosed :
1509 ∀ n : ℕ,
1510 IsClosed (((closedCommutator (topDerivedTop G n) (topDerivedTop G n)).map
1512 intro n
1513 refine
1515 (f := π) ((continuousToMaxSolvQuot G m).continuous_toFun.isClosedMap)
1516 (K := closedCommutator (topDerivedTop G n) (topDerivedTop G n)) ?_
1517 exact Subgroup.isClosed_topologicalClosure (s := ⁅topDerivedTop G n, topDerivedTop G n⁆)
1518 have hmap := topDerived_map_eq_of_surj (f := π) hπsurj hclosed m
1519 calc
1520 topDerivedTop Q m = (topDerivedTop G m).map (π : G →* Q) := by
1521 symm
1523 _ = ⊥ := by
1524 refine (Subgroup.map_eq_bot_iff (f := (π : G →* Q)) (H := topDerivedTop G m)).2 ?_
1525 intro x hx
1526 exact (MonoidHom.mem_ker).2
1527 ((continuousToMaxSolvQuot_eq_one_iff (G := G) (m := m) (x := x)).2 hx)
1529/-- Maximal finite-step solvable quotients are center-free under the local torsion-free and
1530faithful abelianization hypotheses. -/
1532 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
1533 [CompactSpace G] [TotallyDisconnectedSpace G]
1534 (hTorsion : IsAbTorsionFree G) (hFaithful : IsAbFaithful G)
1535 {m : ℕ} (hm : 2 ≤ m) :
1536 Subgroup.center (MaxSolvQuot G m) = ⊥ := by
1537 let Q : Type u := MaxSolvQuot G m
1538 let hGprof : IsProfiniteGroup G := by
1539 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
1540 have hQprof : IsProfiniteGroup Q := by
1541 simpa [Q, MaxSolvQuot] using
1543 (G := G) hGprof
1544 (show IsClosed ((topDerivedTop G m : Subgroup G) : Set G) by infer_instance))
1545 letI : CompactSpace Q := IsProfiniteGroup.compactSpace hQprof
1546 letI : TotallyDisconnectedSpace Q := IsProfiniteGroup.totallyDisconnectedSpace hQprof
1547 let K : Subgroup Q := lastDerivedSubgroup (G := G) m
1548 letI : K.Normal := by
1549 dsimp [K, lastDerivedSubgroup]
1550 infer_instance
1551 have hm1 : 1 ≤ m := by
1552 exact le_trans (by decide) hm
1553 have hmK : 1 ≤ m - 1 := Nat.le_sub_of_add_le hm
1554 have hcenter_le : Subgroup.center Q ≤ K := by
1555 simpa [Q, K] using
1556 center_le_lastDerivedSubgroup_of_isAbFaithful (G := G) (m := m) hFaithful hm1
1557 have hKClosed : IsClosed ((K : Subgroup Q) : Set Q) := by
1558 simpa [K, lastDerivedSubgroup] using
1559 (show IsClosed ((topDerivedTop Q (m - 1) : Subgroup Q) : Set Q) by infer_instance)
1560 have hKle1 : K ≤ topDerivedTop Q 1 := by
1561 have hanti : Antitone (topDerivedTop (MaxSolvQuot G m)) := by
1562 apply antitone_nat_of_succ_le
1563 intro n
1564 dsimp [topDerivedTop, closedDerivedSeries, closedCommutator]
1565 exact
1566 Subgroup.topologicalClosure_minimal
1567 (s := ⁅topDerivedTop (MaxSolvQuot G m) n, topDerivedTop (MaxSolvQuot G m) n⁆)
1568 (t := topDerivedTop (MaxSolvQuot G m) n)
1569 (Subgroup.commutator_le_self (topDerivedTop (MaxSolvQuot G m) n))
1570 (by infer_instance)
1571 change topDerivedTop (MaxSolvQuot G m) (m - 1) ≤ topDerivedTop (MaxSolvQuot G m) 1
1572 exact hanti hmK
1573 have hstepK : closedDerivedSeries (G := Q) K 1 = ⊥ := by
1574 calc
1575 closedDerivedSeries (G := Q) K 1 = topDerivedTop Q m := by
1576 simpa [K, lastDerivedSubgroup, tsub_add_cancel_of_le hm1] using
1577 (topDerived_add (G := Q) (m := m - 1) (n := 1))
1578 _ = ⊥ := topDerivedTop_eq_bot_maxSolvQuot (G := G) m
1579 have hKder1bot : topDerivedTop K 1 = ⊥ := by
1580 exact
1582 (Q := Q) (K := K) hKClosed hstepK
1583 have hinj : Function.Injective (TopologicalAbelianization.mk ↥K) := by
1584 exact injective_topologicalAbelianizationMk_of_topDerivedTop_one_eq_bot (G := K) hKder1bot
1585 have hfixed :
1587 (quotientConjugationTopologicalAbelianizationMap (G := Q) (N := K)) := by
1588 exact
1590 (G := Q) hKClosed (show K.Normal by infer_instance) hKle1
1591 (fun U hKU =>
1593 (G := G) hTorsion hm U hKU)
1594 exact
1596 (Q := Q) (K := K) hcenter_le hfixed hinj
1598/-- If the topological closure of a subgroup is open in a maximal finite-step solvable quotient,
1599its centralizer is contained in the last derived subgroup under the local torsion-free and
1600faithful abelianization hypotheses. -/
1602 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
1603 [CompactSpace G] [TotallyDisconnectedSpace G]
1604 (hTorsion : IsAbTorsionFree G) (hFaithful : IsAbFaithful G)
1605 {m : ℕ} (hm : 1 ≤ m)
1606 (S : Subgroup (MaxSolvQuot G m))
1607 (hSOpen :
1608 IsOpen (((S.topologicalClosure : Subgroup (MaxSolvQuot G m)) :
1609 Set (MaxSolvQuot G m)))) :
1610 Subgroup.centralizer (S : Set (MaxSolvQuot G m))
1611 ≤ lastDerivedSubgroup (G := G) m := by
1612 by_cases hm1 : m = 1
1613 · subst hm1
1614 simp only [closedDerivedSeries_succ, closedDerivedSeries_zero, lastDerivedSubgroup, topDerivedTop, tsub_self,
1615 le_top]
1616 have hm2 : 2 ≤ m := Nat.succ_le_of_lt (lt_of_le_of_ne hm (Ne.symm hm1))
1617 let Q : Type u := MaxSolvQuot G m
1618 let hGprof : IsProfiniteGroup G := by
1619 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
1620 have hQprof : IsProfiniteGroup Q := by
1621 simpa [Q, MaxSolvQuot] using
1623 (G := G) hGprof
1624 (show IsClosed ((topDerivedTop G m : Subgroup G) : Set G) by infer_instance))
1625 letI : CompactSpace Q := IsProfiniteGroup.compactSpace hQprof
1626 letI : T2Space Q := IsProfiniteGroup.t2Space hQprof
1627 letI : TotallyDisconnectedSpace Q := IsProfiniteGroup.totallyDisconnectedSpace hQprof
1628 let K : Subgroup Q := lastDerivedSubgroup (G := G) m
1629 have hKClosed : IsClosed ((K : Subgroup Q) : Set Q) := by
1630 simpa [Q, K, lastDerivedSubgroup] using
1631 (show IsClosed ((topDerivedTop Q (m - 1) : Subgroup Q) : Set Q) by infer_instance)
1632 have hKNormal : K.Normal := by
1633 dsimp [Q, K, lastDerivedSubgroup]
1634 infer_instance
1635 exact
1637 (Q := Q) (K := K) hKClosed hKNormal
1638 (hTF := by
1639 intro U hKU
1640 exact
1642 (G := G) hTorsion hm2 U hKU)
1643 (hFaithful := by
1644 intro U hKU
1645 exact
1647 (G := G) hFaithful hm2 U hKU)
1648 hSOpen
1650/-- Open subgroups of a maximal finite-step solvable quotient have centralizer contained in the
1651last derived subgroup under the local torsion-free and faithful abelianization hypotheses. -/
1652theorem
1653 centralizer_openSubgroup_le_lastDerived_of_abTorsionFree_faithful
1654 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
1655 [CompactSpace G] [TotallyDisconnectedSpace G]
1656 (hTorsion : IsAbTorsionFree G) (hFaithful : IsAbFaithful G)
1657 {m : ℕ} (hm : 1 ≤ m)
1658 (H : OpenSubgroup (MaxSolvQuot G m)) :
1659 Subgroup.centralizer (H : Set (MaxSolvQuot G m))
1660 ≤ lastDerivedSubgroup (G := G) m := by
1661 by_cases hm1 : m = 1
1662 · subst hm1
1663 simp only [closedDerivedSeries_succ, closedDerivedSeries_zero, lastDerivedSubgroup, topDerivedTop, tsub_self,
1664 le_top]
1665 have hm2 : 2 ≤ m := Nat.succ_le_of_lt (lt_of_le_of_ne hm (Ne.symm hm1))
1666 let Q : Type u := MaxSolvQuot G m
1667 let hGprof : IsProfiniteGroup G := by
1668 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
1669 have hQprof : IsProfiniteGroup Q := by
1670 simpa [Q, MaxSolvQuot] using
1672 (G := G) hGprof
1673 (show IsClosed ((topDerivedTop G m : Subgroup G) : Set G) by infer_instance))
1674 letI : CompactSpace Q := IsProfiniteGroup.compactSpace hQprof
1675 letI : T2Space Q := IsProfiniteGroup.t2Space hQprof
1676 letI : TotallyDisconnectedSpace Q := IsProfiniteGroup.totallyDisconnectedSpace hQprof
1677 let K : Subgroup Q := lastDerivedSubgroup (G := G) m
1678 have hKClosed : IsClosed ((K : Subgroup Q) : Set Q) := by
1679 simpa [Q, K, lastDerivedSubgroup] using
1680 (show IsClosed ((topDerivedTop Q (m - 1) : Subgroup Q) : Set Q) by infer_instance)
1681 have hKNormal : K.Normal := by
1682 dsimp [Q, K, lastDerivedSubgroup]
1683 infer_instance
1684 exact
1686 (Q := Q) (K := K) hKClosed hKNormal
1687 (hTF := by
1688 intro U hKU
1689 exact
1691 (G := G) hTorsion hm2 U hKU)
1692 (hFaithful := by
1693 intro U hKU
1694 exact
1696 (G := G) hFaithful hm2 U hKU)
1697 H
1699/-- Maximal finite-step solvable quotients are slim modulo their last derived subgroup under the
1700local torsion-free and faithful abelianization hypotheses. -/
1702 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
1703 [CompactSpace G] [TotallyDisconnectedSpace G]
1704 (hTorsion : IsAbTorsionFree G) (hFaithful : IsAbFaithful G)
1705 {m : ℕ} (hm : 1 ≤ m) :
1706 IsSlimModulo (MaxSolvQuot G m)
1707 (lastDerivedSubgroup (G := G) m) := by
1708 intro H
1709 exact
1710 centralizer_openSubgroup_le_lastDerived_of_abTorsionFree_faithful
1711 (G := G) hTorsion hFaithful hm H
1713/-- The center of a maximal finite-step solvable quotient is contained in the last derived subgroup
1714under the local torsion-free and faithful abelianization hypotheses. -/
1716 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
1717 [CompactSpace G] [TotallyDisconnectedSpace G]
1718 (hTorsion : IsAbTorsionFree G) (hFaithful : IsAbFaithful G)
1719 {m : ℕ} (hm : 1 ≤ m) :
1720 Subgroup.center (MaxSolvQuot G m) ≤
1721 lastDerivedSubgroup (G := G) m := by
1722 exact
1724 (G := MaxSolvQuot G m)
1725 (K := lastDerivedSubgroup (G := G) m)
1727 (G := G) hTorsion hFaithful hm)
1729/-- If the last derived subgroup already vanishes, then the maximal finite-step solvable quotient
1730is slim under the local torsion-free and faithful abelianization hypotheses. -/
1732 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
1733 [CompactSpace G] [TotallyDisconnectedSpace G]
1734 (hTorsion : IsAbTorsionFree G) (hFaithful : IsAbFaithful G)
1735 {m : ℕ} (hm : 1 ≤ m)
1736 (hder : lastDerivedSubgroup (G := G) m = ⊥) :
1737 IsSlim (MaxSolvQuot G m) := by
1738 exact
1740 (G := MaxSolvQuot G m)
1741 (by
1742 simpa [hder] using
1744 (G := G) hTorsion hFaithful hm))
1746end ProCGroups.FiniteStepSolvableQuotients