Yamaguchi Lean 4 Library
Source: ProCGroups.FiniteStepSolvableQuotients.AbelianActions.SlimnessAndTorsion
ProCGroups/FiniteStepSolvableQuotients/AbelianActions/SlimnessAndTorsion/Source

Source: ProCGroups.FiniteStepSolvableQuotients.AbelianActions.SlimnessAndTorsion

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