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

Source: ProCGroups.FiniteStepSolvableQuotients.AbelianActions.Faithful

1import Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
2import ProCGroups.FiniteStepSolvableQuotients.Abelianization
3import ProCGroups.ProC.Quotients.ClosedNormal
5/-!
6# Faithful actions on topological abelianizations
8This module defines abelianization-faithfulness for open subgroups and proves that it is preserved
9under continuous multiplicative equivalences and passage between suitable quotients.
10-/
12open scoped Topology
14namespace ProCGroups.FiniteStepSolvableQuotients
16open ProCGroups.Abelian
18universe u v
20/-- An action has no nontrivial fixed points if every globally fixed element is trivial. -/
21def HasNoNontrivialFixedPoints
22 {Q : Type u} [Group Q]
23 {A : Type v} [Group A]
24 (ρ : Q →* MulAut A) : Prop :=
25 ∀ a : A, (∀ q : Q, ρ q a = a) → a = 1
27/--
28Every open subgroup acts faithfully on the topological abelianization of each open normal
29subgroup.
30-/
31def IsAbFaithful
32 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : Prop :=
33 ∀ H : OpenSubgroup G,
34 ∀ N : OpenNormalSubgroup ↥(H : Subgroup G),
35 Function.Injective
36 (quotientConjugationTopologicalAbelianizationMap
37 (G := ↥(H : Subgroup G)) (N := (N : Subgroup ↥(H : Subgroup G))))
39/-- Faithfulness of the quotient-conjugation action pulls back across a continuous
40multiplicative equivalence, with the open normal subgroup pushed forward along
41the equivalence. -/
42theorem quotientConjAbelianization_injective_of_continuousMulEquiv_image
43 {G : Type u} {H : Type v}
44 [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
45 [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
46 (e : G ≃ₜ* H) (N : OpenNormalSubgroup G)
47 (hinjH :
48 Function.Injective
49 (quotientConjugationTopologicalAbelianizationMap
50 (G := H)
52 (ContinuousMonoidHom.toContinuousMonoidHom e) (Homeomorph.isOpenMap e.toHomeomorph)
53 e.surjective N : Subgroup H)))) :
54 Function.Injective
55 (quotientConjugationTopologicalAbelianizationMap
56 (G := G) (N := (N : Subgroup G))) := by
57 let Nmap : OpenNormalSubgroup H :=
59 (ContinuousMonoidHom.toContinuousMonoidHom e) (Homeomorph.isOpenMap e.toHomeomorph)
60 e.surjective N
61 let eN : ((N : Subgroup G) : Type u) ≃ₜ*
62 ((Nmap : Subgroup H) : Type v) :=
63 { toMulEquiv :=
64 { toFun := fun x => ⟨e x.1, by
65 change e x.1 ∈
66 (N : Subgroup G).map (ContinuousMonoidHom.toContinuousMonoidHom e).toMonoidHom
67 exact ⟨x.1, x.2, rfl⟩⟩
68 invFun := fun y => ⟨e.symm y.1, by
69 have hy : y.1 ∈
70 (N : Subgroup G).map (ContinuousMonoidHom.toContinuousMonoidHom e).toMonoidHom := by
71 simp [Nmap]
72 rcases hy with ⟨x, hxN, hxy⟩
73 have hs : e.symm y.1 = x := by
74 apply e.injective
75 simpa using hxy.symm
76 rw [hs]
77 exact hxN⟩
78 left_inv := by
79 intro x
80 ext
81 simp
82 right_inv := by
83 intro y
84 ext
85 simp
86 map_mul' := by
87 intro x y
88 ext
89 simp }
90 continuous_toFun := by
91 exact Continuous.subtype_mk
92 (e.continuous_toFun.comp continuous_subtype_val)
93 (fun x => by
94 change e x.1 ∈
95 (N : Subgroup G).map (ContinuousMonoidHom.toContinuousMonoidHom e).toMonoidHom
96 exact ⟨x.1, x.2, rfl⟩)
97 continuous_invFun := by
98 exact Continuous.subtype_mk
99 (e.symm.continuous_toFun.comp continuous_subtype_val)
100 (fun y => by
101 change e.symm y.1 ∈ (N : Subgroup G)
102 have hy : y.1 ∈
103 (N : Subgroup G).map (ContinuousMonoidHom.toContinuousMonoidHom e).toMonoidHom := by
104 simp [Nmap]
105 rcases hy with ⟨x, hxN, hxy⟩
106 have hs : e.symm y.1 = x := by
107 apply e.injective
108 simpa using hxy.symm
109 rw [hs]
110 exact hxN) }
111 let eAb :
112 TopologicalAbelianization ((N : Subgroup G) : Type u) ≃ₜ*
113 TopologicalAbelianization ((Nmap : Subgroup H) : Type v) :=
114 TopologicalAbelianization.congr eN
115 let qMap : G ⧸ (N : Subgroup G) →*
116 H ⧸ (Nmap : Subgroup H) :=
117 QuotientGroup.map (N := (N : Subgroup G)) (M := (Nmap : Subgroup H))
118 (f := (ContinuousMonoidHom.toContinuousMonoidHom e).toMonoidHom) (by
119 intro x hx
120 change e x ∈
121 (N : Subgroup G).map (ContinuousMonoidHom.toContinuousMonoidHom e).toMonoidHom
122 exact ⟨x, hx, rfl⟩)
123 have hqMapKer : qMap.ker = ⊥ := by
125 (f := (ContinuousMonoidHom.toContinuousMonoidHom e).toMonoidHom)
126 (N := (N : Subgroup G))
127 (M := (Nmap : Subgroup H))
128 (h := by
129 intro x hx
130 change e x ∈
131 (N : Subgroup G).map (ContinuousMonoidHom.toContinuousMonoidHom e).toMonoidHom
132 exact ⟨x, hx, rfl⟩)
133 (hcomap := by
134 ext x
135 constructor
136 · intro hx
137 have hx' : e x ∈
138 (N : Subgroup G).map (ContinuousMonoidHom.toContinuousMonoidHom e).toMonoidHom := by
139 simpa [Nmap] using hx
140 rcases hx' with ⟨y, hyN, hyx⟩
141 have hxy : x = y := by
142 apply e.injective
143 simpa using hyx.symm
144 simpa [hxy] using hyN
145 · intro hx
146 change e x ∈ (Nmap : Subgroup H)
147 change e x ∈
148 (N : Subgroup G).map (ContinuousMonoidHom.toContinuousMonoidHom e).toMonoidHom
149 exact ⟨x, hx, rfl⟩)
150 have hqMapInj : Function.Injective qMap := by
151 exact (MonoidHom.ker_eq_bot_iff (f := qMap)).1 hqMapKer
152 let ρG : G ⧸ (N : Subgroup G) →*
153 MulAut (TopologicalAbelianization ((N : Subgroup G) : Type u)) :=
154 quotientConjugationTopologicalAbelianizationMap
155 (G := G) (N := (N : Subgroup G))
156 let ρH : H ⧸ (Nmap : Subgroup H) →*
157 MulAut (TopologicalAbelianization ((Nmap : Subgroup H) : Type v)) :=
158 quotientConjugationTopologicalAbelianizationMap
159 (G := H) (N := (Nmap : Subgroup H))
160 have haction_mk
161 (g : G) (x : ((N : Subgroup G) : Type u)) :
162 eAb
163 (ρG (QuotientGroup.mk' (N : Subgroup G) g)
164 (TopologicalAbelianization.mk
165 ((N : Subgroup G) : Type u) x)) =
166 ρH (QuotientGroup.mk' (Nmap : Subgroup H) (e g))
167 (eAb
168 (TopologicalAbelianization.mk
169 ((N : Subgroup G) : Type u) x)) := by
170 have hconj :
171 eN ((MulAut.conjNormal g) x) =
172 (MulAut.conjNormal (e g)) (eN x) := by
173 ext
174 simp [eN]
175 rw [show
176 ρG (QuotientGroup.mk' (N : Subgroup G) g)
177 (TopologicalAbelianization.mk
178 ((N : Subgroup G) : Type u) x) =
179 TopologicalAbelianization.mk
180 ((N : Subgroup G) : Type u) ((MulAut.conjNormal g) x) by
181 simpa [ρG] using
182 (quotientConjugationTopologicalAbelianizationMap_mk_apply_mk
183 (N := (N : Subgroup G)) (g := g) (n := x))]
184 rw [show
185 eAb (TopologicalAbelianization.mk
186 ((N : Subgroup G) : Type u) ((MulAut.conjNormal g) x)) =
187 TopologicalAbelianization.mk
188 ((Nmap : Subgroup H) : Type v) (eN ((MulAut.conjNormal g) x)) by
189 rfl]
190 rw [show
191 eAb (TopologicalAbelianization.mk
192 ((N : Subgroup G) : Type u) x) =
193 TopologicalAbelianization.mk
194 ((Nmap : Subgroup H) : Type v) (eN x) by
195 rfl]
196 rw [hconj]
197 change
198 TopologicalAbelianization.mk
199 ((Nmap : Subgroup H) : Type v)
200 ((MulAut.conjNormal (e g)) (eN x)) =
201 quotientConjugationTopologicalAbelianizationMap
202 (G := H) (N := (Nmap : Subgroup H))
203 (QuotientGroup.mk' (Nmap : Subgroup H) (e g))
204 (TopologicalAbelianization.mk
205 ((Nmap : Subgroup H) : Type v) (eN x))
206 exact
207 (quotientConjugationTopologicalAbelianizationMap_mk_apply_mk
208 (N := (Nmap : Subgroup H)) (g := e g) (n := eN x)).symm
209 have hcomp :
210 ∀ q : G ⧸ (N : Subgroup G),
211 ρH (qMap q) = (MulAut.congr eAb.toMulEquiv) (ρG q) := by
212 intro q
213 obtain ⟨g, rfl⟩ := QuotientGroup.mk'_surjective (N : Subgroup G) q
214 ext a
215 obtain ⟨apre, rfl⟩ := eAb.surjective a
216 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective
217 (Subgroup.closedCommutator (N : Subgroup G)) apre
218 have hqMap_mk :
219 qMap (QuotientGroup.mk' (N : Subgroup G) g) =
220 QuotientGroup.mk' (Nmap : Subgroup H) (e g) := by
221 dsimp [qMap]
222 have hcongr_apply
223 (a₀ : TopologicalAbelianization ((N : Subgroup G) : Type u)) :
224 (MulAut.congr eAb.toMulEquiv)
225 (ρG (QuotientGroup.mk' (N : Subgroup G) g))
226 (eAb a₀) =
227 eAb
228 (ρG (QuotientGroup.mk' (N : Subgroup G) g)
229 a₀) := by
230 change
231 eAb.toMulEquiv
232 (ρG (QuotientGroup.mk' (N : Subgroup G) g)
233 (eAb.toMulEquiv.symm (eAb.toMulEquiv a₀))) =
234 eAb.toMulEquiv
235 (ρG (QuotientGroup.mk' (N : Subgroup G) g) a₀)
236 rw [eAb.toMulEquiv.symm_apply_apply]
237 rw [hqMap_mk, hcongr_apply]
238 exact (haction_mk g x).symm
239 intro q₁ q₂ hq
240 have hcongr : ρH (qMap q₁) = ρH (qMap q₂) := by
241 simpa [hcomp q₁, hcomp q₂] using
242 congrArg (MulAut.congr eAb.toMulEquiv) hq
243 exact hqMapInj (hinjH hcongr)
245/-- `IsAbFaithful` is transported by a continuous multiplicative equivalence. -/
246theorem isAbFaithful_of_continuousMulEquiv
247 {G : Type u} {H : Type v}
248 [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
249 [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
250 (e : G ≃ₜ* H) (hH : IsAbFaithful H) :
251 IsAbFaithful G := by
252 intro K N
253 let Kmap : OpenSubgroup H := by
254 refine
255 { toSubgroup := (K : Subgroup G).map (ContinuousMonoidHom.toContinuousMonoidHom e).toMonoidHom
256 isOpen' := ?_ }
257 change IsOpen (e '' ((K : Subgroup G) : Set G))
258 exact Homeomorph.isOpenMap e.toHomeomorph _ K.isOpen'
259 let eK : ((K : Subgroup G) : Type u) ≃ₜ* ((Kmap : Subgroup H) : Type v) :=
260 { toMulEquiv :=
261 { toFun := fun x => ⟨e x.1, by
262 change e x.1 ∈
263 (K : Subgroup G).map (ContinuousMonoidHom.toContinuousMonoidHom e).toMonoidHom
264 exact ⟨x.1, x.2, rfl⟩⟩
265 invFun := fun y => ⟨e.symm y.1, by
266 have hy : y.1 ∈
267 (K : Subgroup G).map (ContinuousMonoidHom.toContinuousMonoidHom e).toMonoidHom := by
268 simp [Kmap]
269 rcases hy with ⟨x, hxK, hxy⟩
270 have hs : e.symm y.1 = x := by
271 apply e.injective
272 simpa using hxy.symm
273 rw [hs]
274 exact hxK⟩
275 left_inv := by
276 intro x
277 ext
278 simp
279 right_inv := by
280 intro y
281 ext
282 simp
283 map_mul' := by
284 intro x y
285 ext
286 simp }
287 continuous_toFun := by
288 exact Continuous.subtype_mk
289 (e.continuous_toFun.comp continuous_subtype_val)
290 (fun x => by
291 change e x.1 ∈
292 (K : Subgroup G).map (ContinuousMonoidHom.toContinuousMonoidHom e).toMonoidHom
293 exact ⟨x.1, x.2, rfl⟩)
294 continuous_invFun := by
295 exact Continuous.subtype_mk
296 (e.symm.continuous_toFun.comp continuous_subtype_val)
297 (fun y => by
298 change e.symm y.1 ∈ (K : Subgroup G)
299 have hy : y.1 ∈
300 (K : Subgroup G).map (ContinuousMonoidHom.toContinuousMonoidHom e).toMonoidHom := by
301 simp [Kmap]
302 rcases hy with ⟨x, hxK, hxy⟩
303 have hs : e.symm y.1 = x := by
304 apply e.injective
305 simpa using hxy.symm
306 rw [hs]
307 exact hxK) }
308 exact quotientConjAbelianization_injective_of_continuousMulEquiv_image
309 (e := eK) (N := N)
310 (hH Kmap
311 (ProCGroups.ProC.OpenNormalSubgroup.map (ContinuousMonoidHom.toContinuousMonoidHom eK)
312 (Homeomorph.isOpenMap eK.toHomeomorph) eK.surjective N))
314/-- Continuous multiplicative equivalence invariance of `IsAbFaithful`. -/
315theorem isAbFaithful_iff_continuousMulEquiv
316 {G : Type u} {H : Type v}
317 [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
318 [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
319 (e : G ≃ₜ* H) :
320 IsAbFaithful G ↔ IsAbFaithful H :=
321 ⟨fun hG => isAbFaithful_of_continuousMulEquiv e.symm hG,
322 fun hH => isAbFaithful_of_continuousMulEquiv e hH⟩
324/-- Open subgroups of an `ab`-faithful topological group are `ab`-faithful. -/
325theorem isAbFaithful_openSubgroup
326 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
327 (hG : IsAbFaithful G) (U : OpenSubgroup G) :
328 IsAbFaithful ((U : Subgroup G) : Type u) := by
329 intro H N
330 let Hmap : OpenSubgroup G := by
331 refine
332 { toSubgroup :=
333 (H : Subgroup ((U : Subgroup G) : Type u)).map
334 ((U : Subgroup G).subtype)
335 isOpen' := ?_ }
336 change IsOpen
337 (((fun x : ((U : Subgroup G) : Type u) => (x : G)) ''
338 ((H : Subgroup ((U : Subgroup G) : Type u)) :
339 Set ((U : Subgroup G) : Type u))) : Set G)
340 exact U.isOpen'.isOpenMap_subtype_val _ H.isOpen'
341 have hHmap_le_U : (Hmap : Subgroup G) ≤ (U : Subgroup G) := by
342 intro x hx
343 rcases hx with ⟨y, _hyH, rfl⟩
344 exact y.2
345 have hsubgroupOf_eq :
346 (Hmap : Subgroup G).subgroupOf (U : Subgroup G) =
347 (H : Subgroup ((U : Subgroup G) : Type u)) := by
348 ext x
349 constructor
350 · intro hx
351 change (x : G) ∈ (Hmap : Subgroup G) at hx
352 rcases hx with ⟨y, hyH, hyx⟩
353 have hyxU : y = x := Subtype.ext hyx
354 simpa [hyxU] using hyH
355 · intro hx
356 change (x : G) ∈ (Hmap : Subgroup G)
357 exact ⟨x, hx, rfl⟩
358 let eEq : ((H : Subgroup ((U : Subgroup G) : Type u)) : Type u) ≃ₜ*
359 (((Hmap : Subgroup G).subgroupOf (U : Subgroup G)) : Type u) :=
360 { toMulEquiv :=
361 { toFun := fun x => ⟨x.1, by
362 exact hsubgroupOf_eq.symm ▸ x.2⟩
363 invFun := fun x => ⟨x.1, by
364 exact hsubgroupOf_eq ▸ x.2⟩
365 left_inv := by
366 intro x
367 ext
368 rfl
369 right_inv := by
370 intro x
371 ext
372 rfl
373 map_mul' := by
374 intro x y
375 rfl }
376 continuous_toFun := by
377 exact Continuous.subtype_mk continuous_subtype_val
378 (fun x => hsubgroupOf_eq.symm ▸ x.2)
379 continuous_invFun := by
380 exact Continuous.subtype_mk continuous_subtype_val
381 (fun x => hsubgroupOf_eq ▸ x.2) }
382 let eH : ((H : Subgroup ((U : Subgroup G) : Type u)) : Type u) ≃ₜ*
383 ((Hmap : Subgroup G) : Type u) :=
384 eEq.trans (Subgroup.subgroupOfContinuousMulEquivOfLe hHmap_le_U)
385 exact quotientConjAbelianization_injective_of_continuousMulEquiv_image
386 (e := eH) (N := N)
387 (hG Hmap
388 (ProCGroups.ProC.OpenNormalSubgroup.map (ContinuousMonoidHom.toContinuousMonoidHom eH)
389 (Homeomorph.isOpenMap eH.toHomeomorph) eH.surjective N))
391/-- The same open normal subgroup viewed inside the \(\top\) open subgroup. -/
392def openNormalSubgroupTop
393 {G : Type u} [TopologicalSpace G] [Group G]
394 (U : OpenNormalSubgroup G) :
395 OpenNormalSubgroup ↥((⊤ : OpenSubgroup G) : Subgroup G) where
396 toOpenSubgroup :=
397 OpenSubgroup.comap ((⊤ : Subgroup G).subtype) continuous_subtype_val U.toOpenSubgroup
398 isNormal' := by
399 change ((U : Subgroup G).comap ((⊤ : Subgroup G).subtype)).Normal
400 infer_instance
402/-- Injectivity on the top-open-subgroup model implies injectivity in the ambient group. -/
403theorem inj_quotientConjugationTopologicalAbelianizationMap_of_openNormalSubgroupTop
404 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
405 (U : OpenNormalSubgroup G)
406 (hTop :
407 Function.Injective
408 (quotientConjugationTopologicalAbelianizationMap
409 (G := ↥((⊤ : OpenSubgroup G) : Subgroup G))
410 (N := (openNormalSubgroupTop U : Subgroup ↥((⊤ : OpenSubgroup G) : Subgroup G))))) :
411 Function.Injective
412 (quotientConjugationTopologicalAbelianizationMap
413 (G := G) (N := (U : Subgroup G))) := by
414 let Gtop : Type u := ↥((⊤ : OpenSubgroup G) : Subgroup G)
415 let UTop : OpenNormalSubgroup Gtop := openNormalSubgroupTop U
416 let eG : Gtop ≃ₜ* G := OpenSubgroup.topContinuousMulEquiv G
417 let eU : ↥(UTop : Subgroup Gtop) ≃ₜ* ↥(U : Subgroup G) :=
418 { toMulEquiv :=
419 { toFun := fun x => ⟨x.1.1, by
420 change x.1.1 ∈ U.toOpenSubgroup
421 have hx := x.2
422 change x.1.1 ∈ U.toOpenSubgroup at hx
423 exact hx⟩
424 invFun := fun x => ⟨⟨x.1, Subgroup.mem_top x.1⟩, by
425 change x.1 ∈ U.toOpenSubgroup
426 exact x.2⟩
427 left_inv := by
428 intro x
429 apply Subtype.ext
430 rfl
431 right_inv := by
432 intro x
433 apply Subtype.ext
434 rfl
435 map_mul' := by
436 intro x y
437 apply Subtype.ext
438 rfl }
439 continuous_toFun := by
440 exact Continuous.subtype_mk
441 (continuous_subtype_val.comp continuous_subtype_val)
442 (fun x => by
443 change x.1.1 ∈ U.toOpenSubgroup
444 have hx := x.2
445 change x.1.1 ∈ U.toOpenSubgroup at hx
446 exact hx)
447 continuous_invFun := by
448 exact Continuous.subtype_mk
449 (Continuous.subtype_mk continuous_subtype_val
450 (fun x => Subgroup.mem_top x.1))
451 (fun x => by
452 change x.1 ∈ U.toOpenSubgroup
453 exact x.2) }
454 let eAb : TopologicalAbelianization ↥(UTop : Subgroup Gtop) ≃ₜ*
455 TopologicalAbelianization ↥(U : Subgroup G) :=
456 TopologicalAbelianization.congr (G := ↥(UTop : Subgroup Gtop))
457 (H := ↥(U : Subgroup G)) eU
458 let qMap : G ⧸ (U : Subgroup G) →*
459 Gtop ⧸ (UTop : Subgroup Gtop) :=
460 QuotientGroup.map (N := (U : Subgroup G)) (M := (UTop : Subgroup Gtop))
461 (f := eG.symm.toMonoidHom) (by
462 intro x hx
463 change ((eG.symm x : Gtop) : G) ∈ U.toOpenSubgroup
464 have hval : ((eG.symm x : Gtop) : G) = x := by
465 exact eG.apply_symm_apply x
466 rw [hval]
467 exact hx)
468 have hqMapKer : qMap.ker = ⊥ := by
470 (f := eG.symm.toMonoidHom)
471 (N := (U : Subgroup G))
472 (M := (UTop : Subgroup Gtop))
473 (h := by
474 intro x hx
475 change ((eG.symm x : Gtop) : G) ∈ U.toOpenSubgroup
476 have hval : ((eG.symm x : Gtop) : G) = x := by
477 exact eG.apply_symm_apply x
478 rw [hval]
479 exact hx)
480 (hcomap := by
481 ext x
482 constructor
483 · intro hx
484 change ((eG.symm x : Gtop) : G) ∈ U.toOpenSubgroup at hx
485 have hval : ((eG.symm x : Gtop) : G) = x := by
486 exact eG.apply_symm_apply x
487 rw [hval] at hx
488 exact hx
489 · intro hx
490 change ((eG.symm x : Gtop) : G) ∈ U.toOpenSubgroup
491 have hval : ((eG.symm x : Gtop) : G) = x := by
492 exact eG.apply_symm_apply x
493 rw [hval]
494 exact hx)
495 have hqMapInj : Function.Injective qMap := by
496 exact (MonoidHom.ker_eq_bot_iff (f := qMap)).1 hqMapKer
497 let ρTop : Gtop ⧸ (UTop : Subgroup Gtop) →*
498 MulAut (TopologicalAbelianization ↥(UTop : Subgroup Gtop)) :=
499 quotientConjugationTopologicalAbelianizationMap
500 (G := Gtop) (N := (UTop : Subgroup Gtop))
501 let ρU : G ⧸ (U : Subgroup G) →*
502 MulAut (TopologicalAbelianization ↥(U : Subgroup G)) :=
503 quotientConjugationTopologicalAbelianizationMap
504 (G := G) (N := (U : Subgroup G))
505 have haction_mk
506 (g : G)
507 (x : ↥(UTop : Subgroup Gtop)) :
508 eAb
509 (ρTop (QuotientGroup.mk' (UTop : Subgroup Gtop) (eG.symm g))
510 (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x)) =
511 ρU (QuotientGroup.mk' (U : Subgroup G) g)
512 (eAb (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x)) := by
513 have hconj :
514 eU ((MulAut.conjNormal (eG.symm g)) x) =
515 (MulAut.conjNormal g) (eU x) := by
516 apply Subtype.ext
517 simp only [MulAut.conjNormal_apply]
518 have hval : ((eG.symm g : Gtop) : G) = g := by
519 exact eG.apply_symm_apply g
520 change
521 ((eG.symm g : Gtop) : G) * x.1.1 * ((eG.symm g : Gtop) : G)⁻¹ =
522 g * x.1.1 * g⁻¹
523 rw [hval]
524 rw [show ρTop (QuotientGroup.mk' (UTop : Subgroup Gtop) (eG.symm g))
525 (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x) =
526 TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop)
527 ((MulAut.conjNormal (eG.symm g)) x) by
528 simpa [ρTop] using
529 (quotientConjugationTopologicalAbelianizationMap_mk_apply_mk
530 (N := (UTop : Subgroup Gtop)) (g := eG.symm g) (n := x))]
531 rw [show
532 eAb (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop)
533 ((MulAut.conjNormal (eG.symm g)) x)) =
534 TopologicalAbelianization.mk ↥(U : Subgroup G)
535 (eU ((MulAut.conjNormal (eG.symm g)) x)) by
536 rfl]
537 rw [show
538 eAb (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x) =
539 TopologicalAbelianization.mk ↥(U : Subgroup G) (eU x) by
540 rfl]
541 rw [hconj]
542 change TopologicalAbelianization.mk ↥(U : Subgroup G)
543 ((MulAut.conjNormal g) (eU x)) =
544 quotientConjugationTopologicalAbelianizationMap (G := G) (N := (U : Subgroup G))
545 (QuotientGroup.mk' (U : Subgroup G) g)
546 (TopologicalAbelianization.mk ↥(U : Subgroup G) (eU x))
547 exact (quotientConjugationTopologicalAbelianizationMap_mk_apply_mk
548 (N := (U : Subgroup G)) (g := g) (n := eU x)).symm
549 have hcomp :
550 ∀ q : G ⧸ (U : Subgroup G),
551 ρU q = (MulAut.congr eAb.toMulEquiv) (ρTop (qMap q)) := by
552 intro q
553 obtain ⟨g, rfl⟩ := QuotientGroup.mk'_surjective (U : Subgroup G) q
554 ext a
555 obtain ⟨apre, rfl⟩ := eAb.surjective a
556 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective
557 (Subgroup.closedCommutator (UTop : Subgroup Gtop)) apre
558 change
559 ρU (QuotientGroup.mk' (U : Subgroup G) g)
560 (eAb (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x)) =
561 eAb
562 (ρTop (QuotientGroup.mk' (UTop : Subgroup Gtop) (eG.symm g))
563 (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x))
564 exact (haction_mk g x).symm
565 intro q₁ q₂ hq
566 have hcongr : (MulAut.congr eAb.toMulEquiv) (ρTop (qMap q₁)) =
567 (MulAut.congr eAb.toMulEquiv) (ρTop (qMap q₂)) := by
568 simpa [ρU, hcomp q₁, hcomp q₂] using hq
569 have htopEq : ρTop (qMap q₁) = ρTop (qMap q₂) :=
570 (MulAut.congr eAb.toMulEquiv).injective hcongr
571 exact hqMapInj (hTop htopEq)
573/--
574Injectivity in the ambient group transfers to the corresponding open normal subgroup inside the
575\(\top\) open subgroup model.
576-/
577theorem inj_quotientConjugationTopologicalAbelianizationMap_on_openNormalSubgroupTop
578 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
579 (U : OpenNormalSubgroup G)
580 (hU :
581 Function.Injective
582 (quotientConjugationTopologicalAbelianizationMap
583 (G := G) (N := (U : Subgroup G)))) :
584 Function.Injective
585 (quotientConjugationTopologicalAbelianizationMap
586 (G := ↥((⊤ : OpenSubgroup G) : Subgroup G))
587 (N := (openNormalSubgroupTop U : Subgroup ↥((⊤ : OpenSubgroup G) : Subgroup G)))) := by
588 let Gtop : Type u := ↥((⊤ : OpenSubgroup G) : Subgroup G)
589 let UTop : OpenNormalSubgroup Gtop := openNormalSubgroupTop U
590 let eG : Gtop ≃ₜ* G := OpenSubgroup.topContinuousMulEquiv G
591 let eU : ↥(UTop : Subgroup Gtop) ≃ₜ* ↥(U : Subgroup G) :=
592 { toMulEquiv :=
593 { toFun := fun x => ⟨x.1.1, by
594 change x.1.1 ∈ U.toOpenSubgroup
595 have hx := x.2
596 change x.1.1 ∈ U.toOpenSubgroup at hx
597 exact hx⟩
598 invFun := fun x => ⟨⟨x.1, Subgroup.mem_top x.1⟩, by
599 change x.1 ∈ U.toOpenSubgroup
600 exact x.2⟩
601 left_inv := by
602 intro x
603 apply Subtype.ext
604 rfl
605 right_inv := by
606 intro x
607 apply Subtype.ext
608 rfl
609 map_mul' := by
610 intro x y
611 apply Subtype.ext
612 rfl }
613 continuous_toFun := by
614 exact Continuous.subtype_mk
615 (continuous_subtype_val.comp continuous_subtype_val)
616 (fun x => by
617 change x.1.1 ∈ U.toOpenSubgroup
618 have hx := x.2
619 change x.1.1 ∈ U.toOpenSubgroup at hx
620 exact hx)
621 continuous_invFun := by
622 exact Continuous.subtype_mk
623 (Continuous.subtype_mk continuous_subtype_val
624 (fun x => Subgroup.mem_top x.1))
625 (fun x => by
626 change x.1 ∈ U.toOpenSubgroup
627 exact x.2) }
628 let eAb : TopologicalAbelianization ↥(UTop : Subgroup Gtop) ≃ₜ*
629 TopologicalAbelianization ↥(U : Subgroup G) :=
630 TopologicalAbelianization.congr (G := ↥(UTop : Subgroup Gtop))
631 (H := ↥(U : Subgroup G)) eU
632 let qMap : Gtop ⧸ (UTop : Subgroup Gtop) →* G ⧸ (U : Subgroup G) :=
633 QuotientGroup.map (N := (UTop : Subgroup Gtop)) (M := (U : Subgroup G))
634 (f := eG.toMonoidHom) (by
635 intro x hx
636 change eG x ∈ U.toOpenSubgroup
637 change x.1 ∈ U.toOpenSubgroup at hx
638 have hval : eG x = x.1 := by
639 exact OpenSubgroup.topContinuousMulEquiv_apply G x
640 rw [hval]
641 exact hx)
642 have hqMapKer : qMap.ker = ⊥ := by
644 (f := eG.toMonoidHom)
645 (N := (UTop : Subgroup Gtop))
646 (M := (U : Subgroup G))
647 (h := by
648 intro x hx
649 change eG x ∈ U.toOpenSubgroup
650 change x.1 ∈ U.toOpenSubgroup at hx
651 have hval : eG x = x.1 := by
652 exact OpenSubgroup.topContinuousMulEquiv_apply G x
653 rw [hval]
654 exact hx)
655 (hcomap := by
656 ext x
657 constructor
658 · intro hx
659 change eG x ∈ U.toOpenSubgroup at hx
660 change x.1 ∈ U.toOpenSubgroup
661 have hval : eG x = x.1 := by
662 exact OpenSubgroup.topContinuousMulEquiv_apply G x
663 rw [hval] at hx
664 exact hx
665 · intro hx
666 change x.1 ∈ U.toOpenSubgroup at hx
667 change eG x ∈ U.toOpenSubgroup
668 have hval : eG x = x.1 := by
669 exact OpenSubgroup.topContinuousMulEquiv_apply G x
670 rw [hval]
671 exact hx)
672 have hqMapInj : Function.Injective qMap := by
673 exact (MonoidHom.ker_eq_bot_iff (f := qMap)).1 hqMapKer
674 let ρTop : Gtop ⧸ (UTop : Subgroup Gtop) →*
675 MulAut (TopologicalAbelianization ↥(UTop : Subgroup Gtop)) :=
676 quotientConjugationTopologicalAbelianizationMap
677 (G := Gtop) (N := (UTop : Subgroup Gtop))
678 let ρU : G ⧸ (U : Subgroup G) →*
679 MulAut (TopologicalAbelianization ↥(U : Subgroup G)) :=
680 quotientConjugationTopologicalAbelianizationMap
681 (G := G) (N := (U : Subgroup G))
682 have haction_mk
683 (g : Gtop)
684 (x : ↥(UTop : Subgroup Gtop)) :
685 eAb
686 (ρTop (QuotientGroup.mk' (UTop : Subgroup Gtop) g)
687 (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x)) =
688 ρU (QuotientGroup.mk' (U : Subgroup G) (eG g))
689 (eAb (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x)) := by
690 have hconj :
691 eU ((MulAut.conjNormal g) x) =
692 (MulAut.conjNormal (eG g)) (eU x) := by
693 apply Subtype.ext
694 simp only [MulAut.conjNormal_apply]
695 have hval : eG g = g.1 := by
696 exact OpenSubgroup.topContinuousMulEquiv_apply G g
697 change
698 g.1 * x.1.1 * g.1⁻¹ =
699 eG g * x.1.1 * (eG g)⁻¹
700 rw [hval]
701 rw [show ρTop (QuotientGroup.mk' (UTop : Subgroup Gtop) g)
702 (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x) =
703 TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop)
704 ((MulAut.conjNormal g) x) by
705 simpa [ρTop] using
706 (quotientConjugationTopologicalAbelianizationMap_mk_apply_mk
707 (N := (UTop : Subgroup Gtop)) (g := g) (n := x))]
708 rw [show eAb (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop)
709 ((MulAut.conjNormal g) x)) =
710 TopologicalAbelianization.mk ↥(U : Subgroup G) (eU ((MulAut.conjNormal g) x)) by
711 rfl]
712 rw [show eAb (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x) =
713 TopologicalAbelianization.mk ↥(U : Subgroup G) (eU x) by
714 rfl]
715 rw [hconj]
716 change TopologicalAbelianization.mk ↥(U : Subgroup G)
717 ((MulAut.conjNormal (eG g)) (eU x)) =
718 quotientConjugationTopologicalAbelianizationMap (G := G) (N := (U : Subgroup G))
719 (QuotientGroup.mk' (U : Subgroup G) (eG g))
720 (TopologicalAbelianization.mk ↥(U : Subgroup G) (eU x))
721 exact (quotientConjugationTopologicalAbelianizationMap_mk_apply_mk
722 (N := (U : Subgroup G)) (g := eG g) (n := eU x)).symm
723 have hcomp :
724 ∀ q : Gtop ⧸ (UTop : Subgroup Gtop),
725 ρU (qMap q) = (MulAut.congr eAb.toMulEquiv) (ρTop q) := by
726 intro q
727 obtain ⟨g, rfl⟩ := QuotientGroup.mk'_surjective (UTop : Subgroup Gtop) q
728 ext a
729 obtain ⟨apre, rfl⟩ := eAb.surjective a
730 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective
731 (Subgroup.closedCommutator (UTop : Subgroup Gtop)) apre
732 change
733 ρU (QuotientGroup.mk' (U : Subgroup G) (eG g))
734 (eAb (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x)) =
735 eAb
736 (ρTop (QuotientGroup.mk' (UTop : Subgroup Gtop) g)
737 (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x))
738 exact (haction_mk g x).symm
739 intro q₁ q₂ hq
740 have hcongr :
741 ρU (qMap q₁) = ρU (qMap q₂) := by
742 simpa [hcomp q₁, hcomp q₂] using congrArg (MulAut.congr eAb.toMulEquiv) hq
743 exact hqMapInj (hU hcongr)
745/-- A nontrivial element is omitted by some open normal subgroup. -/
746theorem exists_openNormalSubgroup_not_mem_of_ne_one
747 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
748 [CompactSpace G] [TotallyDisconnectedSpace G]
749 {x : G} (hx : x ≠ 1) :
750 ∃ U : OpenNormalSubgroup G, x ∉ (U : Subgroup G) := by
751 let W : Set G := ({x} : Set G)ᶜ
752 have hWOpen : IsOpen W := isClosed_singleton.isOpen_compl
753 have h1W : (1 : G) ∈ W := by
754 simpa [W, eq_comm] using hx
756 (G := G) hWOpen h1W with ⟨U, hUW⟩
757 refine ⟨U, ?_⟩
758 intro hxU
759 have hxW : x ∈ W := hUW hxU
760 simp only [Set.mem_compl_iff, Set.mem_singleton_iff, not_true_eq_false, W] at hxW
762/--
763Faithfulness of the conjugation action on every open normal subgroup of the \(\top\) open
764subgroup forces the ambient center to be trivial.
765-/
766theorem center_eq_bot_of_injective_action_on_openNormalsTop
767 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
768 [CompactSpace Q] [TotallyDisconnectedSpace Q]
769 (hfaithful :
770 ∀ U : OpenNormalSubgroup ↥((⊤ : OpenSubgroup Q) : Subgroup Q),
771 Function.Injective
772 (quotientConjugationTopologicalAbelianizationMap
773 (G := ↥((⊤ : OpenSubgroup Q) : Subgroup Q))
774 (N := (U : Subgroup ↥((⊤ : OpenSubgroup Q) : Subgroup Q))))) :
775 Subgroup.center Q = ⊥ := by
776 rw [Subgroup.eq_bot_iff_forall]
777 intro z hz
778 by_contra hzne
779 rcases exists_openNormalSubgroup_not_mem_of_ne_one (G := Q) (x := z) hzne with ⟨U, hzU⟩
780 let Gtop : Type u := ↥((⊤ : OpenSubgroup Q) : Subgroup Q)
781 let zTop : Gtop := ⟨z, by simp only [OpenSubgroup.toSubgroup_top, Subgroup.mem_top]⟩
782 let UTop : OpenNormalSubgroup Gtop := openNormalSubgroupTop U
783 let ρ : (Gtop ⧸ (UTop : Subgroup Gtop)) →*
784 MulAut (TopologicalAbelianization ↥(UTop : Subgroup Gtop)) :=
785 quotientConjugationTopologicalAbelianizationMap
786 (G := Gtop)
787 (N := (UTop : Subgroup Gtop))
788 have hzTop : zTop ∈ Subgroup.center Gtop := by
789 rw [Subgroup.mem_center_iff] at hz ⊢
790 intro y
791 ext
792 exact hz y
793 have hρz :
794 ρ (QuotientGroup.mk' (UTop : Subgroup Gtop) zTop) = 1 := by
795 dsimp [ρ]
796 exact
797 quotientConjugationTopologicalAbelianizationMap_mk_eq_one_of_mem_center
798 (G := Gtop) (N := (UTop : Subgroup Gtop)) (x := zTop) hzTop
799 have hzTop_mem :
800 zTop ∈ (UTop : Subgroup Gtop) := by
801 apply (QuotientGroup.eq_one_iff
802 (N := (UTop : Subgroup Gtop)) zTop).mp
803 apply hfaithful UTop
804 simpa using hρz
805 have hzU' : z ∈ (U : Subgroup Q) := by
806 change z ∈ U.toOpenSubgroup
807 change z ∈ U.toOpenSubgroup at hzTop_mem
808 exact hzTop_mem
809 exact hzU hzU'
811/-- An abelianization-faithful profinite group has trivial center. -/
812theorem center_eq_bot_of_isAbFaithful
813 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
814 [CompactSpace G] [TotallyDisconnectedSpace G]
815 (hG : IsAbFaithful G) :
816 Subgroup.center G = ⊥ := by
817 refine center_eq_bot_of_injective_action_on_openNormalsTop (Q := G) ?_
818 intro U
819 simpa using hG ⊤ U
821/-- Every open subgroup of an abelianization-faithful profinite group has trivial center. -/
822theorem openSubgroup_center_eq_bot_of_isAbFaithful
823 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
824 [CompactSpace G] [TotallyDisconnectedSpace G]
825 (hG : IsAbFaithful G) (H : OpenSubgroup G) :
826 Subgroup.center ↥((H : Subgroup G)) = ⊥ := by
827 have hHClosed : IsClosed (((H : OpenSubgroup G) : Set G)) := H.isClosed
828 haveI : CompactSpace ↥((H : OpenSubgroup G) : Subgroup G) := by
829 exact
830 (show IsClosed (((H : Subgroup G) : Set G)) from
831 hHClosed).isClosedEmbedding_subtypeVal.compactSpace
832 haveI : TotallyDisconnectedSpace ↥((H : OpenSubgroup G) : Subgroup G) := by
833 infer_instance
834 exact
835 center_eq_bot_of_injective_action_on_openNormalsTop
836 (Q := ↥((H : OpenSubgroup G) : Subgroup G))
837 (fun U => by
838 let Q : Type u := ↥((H : OpenSubgroup G) : Subgroup G)
839 let e : ↥((⊤ : OpenSubgroup Q) : Subgroup Q) ≃ₜ* Q :=
840 OpenSubgroup.topContinuousMulEquiv Q
841 let U' : OpenNormalSubgroup Q :=
842 OpenNormalSubgroup.comap (e.symm : Q →* ↥((⊤ : OpenSubgroup Q) : Subgroup Q))
843 e.symm.continuous_toFun U
844 have hUTopEq : openNormalSubgroupTop U' = U := by
845 ext x
846 rfl
847 have hU' :
848 Function.Injective
849 (quotientConjugationTopologicalAbelianizationMap
850 (G := Q) (N := (U' : Subgroup Q))) := hG H U'
851 have hTop :
852 Function.Injective
853 (quotientConjugationTopologicalAbelianizationMap
854 (G := ↥((⊤ : OpenSubgroup Q) : Subgroup Q))
855 (N := (openNormalSubgroupTop U' :
856 Subgroup ↥((⊤ : OpenSubgroup Q) : Subgroup Q)))) :=
857 inj_quotientConjugationTopologicalAbelianizationMap_on_openNormalSubgroupTop
858 (G := Q) U' hU'
859 exact hUTopEq ▸ hTop)
861/-- If an open normal subgroup in an open subgroup of a maximal finite-step solvable quotient
862contains the last derived term, then the quotient conjugation action on its topological
863abelianization is faithful. -/
864theorem
865 injective_quotientConjAbelianization_of_containsLastDerived_of_isClosedMap
866 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
867 (hG : IsAbFaithful G)
868 {m : ℕ} (hm : 2 ≤ m)
869 (hclosedπ : IsClosedMap (continuousToMaxSolvQuot G m))
870 (H : OpenSubgroup (MaxSolvQuot G m))
871 (N : OpenNormalSubgroup ↥(H : Subgroup (MaxSolvQuot G m)))
872 (hContain : containsLastDerived m H N) :
873 Function.Injective
874 (quotientConjugationTopologicalAbelianizationMap
875 (G := ↥(H : Subgroup (MaxSolvQuot G m)))
876 (N := (N : Subgroup ↥(H : Subgroup (MaxSolvQuot G m))))) := by
877 let Q : Type u := MaxSolvQuot G m
878 let π : G →ₜ* Q := continuousToMaxSolvQuot G m
879 let Hpre : OpenSubgroup G := preimageOpenSubgroup π H
880 have hHpreOpen : IsOpen ((Hpre : Subgroup G) : Set G) := Hpre.isOpen'
881 let φH : ↥(Hpre : Subgroup G) →ₜ* ↥(H : Subgroup Q) :=
883 let Npre : OpenNormalSubgroup ↥(Hpre : Subgroup G) := by
884 refine
885 { toOpenSubgroup := OpenSubgroup.comap (φH : ↥(Hpre : Subgroup G) →* ↥(H : Subgroup Q))
886 φH.continuous_toFun N.toOpenSubgroup
887 isNormal' := ?_ }
888 change ((N : Subgroup ↥(H : Subgroup Q)).comap
889 (φH : ↥(Hpre : Subgroup G) →* ↥(H : Subgroup Q))).Normal
890 infer_instance
891 let _ : (Npre : Subgroup ↥(Hpre : Subgroup G)).Normal := Npre.isNormal'
892 have hρpre :
893 Function.Injective
894 (quotientConjugationTopologicalAbelianizationMap
895 (G := ↥(Hpre : Subgroup G))
896 (N := (Npre : Subgroup ↥(Hpre : Subgroup G)))) := hG Hpre Npre
897 let Nrealized : OpenSubgroup Q := by
898 refine
899 ⟨(N : Subgroup ↥(H : Subgroup Q)).map ((H : Subgroup Q).subtype), ?_⟩
900 change IsOpen
901 (((fun y : ↥(H : Subgroup Q) => (y : Q)) ''
902 ((N : Subgroup ↥(H : Subgroup Q)) : Set ↥(H : Subgroup Q))))
903 exact H.isOpen'.isOpenMap_subtype_val _ N.isOpen'
904 have hNpreMap :
905 (Npre : Subgroup ↥(Hpre : Subgroup G)).map ((Hpre : Subgroup G).subtype) =
906 ((Nrealized : Subgroup Q).comap (π : G →* Q)) := by
907 ext x
908 constructor
909 · rintro ⟨y, hy, rfl⟩
910 change π y.1 ∈ Nrealized
911 exact ⟨φH y, hy, rfl⟩
912 · intro hx
913 change π x ∈ Nrealized at hx
914 rcases hx with ⟨⟨q, hqH⟩, hqN, hqx⟩
915 have hxHpre : x ∈ Hpre := by
916 change π x ∈ H
917 simpa [← hqx] using hqH
918 refine ⟨⟨x, hxHpre⟩, ?_, rfl⟩
919 change φH ⟨x, hxHpre⟩ ∈ N
920 have hqEq : (⟨q, hqH⟩ : H) = φH ⟨x, hxHpre⟩ := by
921 apply Subtype.ext
922 change q = π x
923 exact hqx
924 exact hqEq ▸ hqN
925 have hπsurj : Function.Surjective π := by
926 simpa [π, Q] using continuousToMaxSolvQuot_surjective (G := G) m
927 have hφHsurj : Function.Surjective φH := by
928 intro y
929 rcases hπsurj y.1 with ⟨x, hx⟩
930 have hxHpre : x ∈ Hpre := by
931 change π x ∈ H
932 rw [hx]
933 exact y.2
934 refine ⟨⟨x, hxHpre⟩, ?_⟩
935 apply Subtype.ext
936 change π x = y.1
937 exact hx
938 have hclosedφH : IsClosedMap φH := by
939 exact
941 (π := π) (Q₁ := (H : Subgroup Q)) hclosedπ
942 (Subgroup.isClosed_of_isOpen (H : Subgroup Q) H.isOpen')
943 have hclosedN :
944 IsClosedMap
945 (ProCGroups.ContinuousMonoidHom.restrictPreimage φH (N : Subgroup ↥(H : Subgroup Q))) := by
946 exact
948 (π := φH) (Q₁ := (N : Subgroup ↥(H : Subgroup Q))) hclosedφH
949 (Subgroup.isClosed_of_isOpen (N : Subgroup ↥(H : Subgroup Q)) N.isOpen')
950 have hder_preN :
951 topDerivedTop G (m - 1) ≤ ((Nrealized : Subgroup Q).comap (π : G →* Q)) := by
952 intro x hx
953 change π x ∈ Nrealized
954 have hxQ : π x ∈ topDerivedTop Q (m - 1) := by
955 exact (topDerivedTop_le_comap (f := π) (m := m - 1)) hx
956 rcases hContain (π x) hxQ with ⟨hxH, hxN⟩
957 exact ⟨⟨π x, hxH⟩, hxN, rfl⟩
958 have hkerN :
959 (ProCGroups.ContinuousMonoidHom.restrictPreimage φH (N : Subgroup ↥(H : Subgroup Q))).ker ≤
960 topDerivedTop ↥((Npre : Subgroup ↥(Hpre : Subgroup G))) 1 := by
961 intro x hx
962 have hxφ : φH x.1 = 1 := by
963 exact
965 (H := (N : Subgroup ↥(H : Subgroup Q))) (x := x)).1 hx
966 have hxπ : π x.1.1 = 1 := by
967 exact congrArg Subtype.val hxφ
968 have hxder : x.1.1 ∈ topDerivedTop G m := by
969 simpa [π, Q] using
970 (continuousToMaxSolvQuot_eq_one_iff (G := G) (m := m) (x := x.1.1)).1 hxπ
971 have hxder' :
972 x.1.1 ∈ closedDerivedSeries (G := G) ((Nrealized : Subgroup Q).comap (π : G →* Q)) 1 := by
973 have hm1 : 1 ≤ m := le_trans (by decide) hm
974 simpa [topDerivedTop] using
975 (mem_topDerived_one_of_mem_topDerived_of_le
976 (G := G) hm1 hder_preN (by simpa [topDerivedTop] using hxder))
977 have hmapN2 :
978 (closedDerivedSeries (G := ↥((Hpre : Subgroup G)))
979 (Npre : Subgroup ↥(Hpre : Subgroup G)) 1).map
980 ((Hpre : Subgroup G).subtype) =
981 closedDerivedSeries (G := G)
982 ((Npre : Subgroup ↥(Hpre : Subgroup G)).map ((Hpre : Subgroup G).subtype)) 1 := by
983 simpa [Hpre] using
984 (topDerived_one_map_subtype_eq_of_isClosed_subgroup
985 (G := G) (H := (Hpre : Subgroup G))
986 (K := (Npre : Subgroup ↥(Hpre : Subgroup G)))
987 (Subgroup.isClosed_of_isOpen _ hHpreOpen))
988 have hmapN1 :
989 (topDerivedTop ↥((Npre : Subgroup ↥(Hpre : Subgroup G))) 1).map
990 ((Npre : Subgroup ↥(Hpre : Subgroup G)).subtype) =
991 closedDerivedSeries (G := ↥((Hpre : Subgroup G)))
992 (Npre : Subgroup ↥(Hpre : Subgroup G)) 1 := by
993 have hmapTop :
994 ((⊤ : Subgroup ↥((Npre : Subgroup ↥(Hpre : Subgroup G)))).map
995 ((Npre : Subgroup ↥(Hpre : Subgroup G)).subtype)) =
996 (Npre : Subgroup ↥(Hpre : Subgroup G)) := by
997 ext y
998 constructor
999 · rintro ⟨x, -, rfl⟩
1000 exact x.2
1001 · intro hy
1002 exact ⟨⟨y, hy⟩, by simp only [Subgroup.coe_top, Set.mem_univ], rfl⟩
1003 calc
1004 (topDerivedTop ↥((Npre : Subgroup ↥(Hpre : Subgroup G))) 1).map
1005 ((Npre : Subgroup ↥(Hpre : Subgroup G)).subtype) =
1006 closedDerivedSeries (G := ↥((Hpre : Subgroup G)))
1007 (((⊤ : Subgroup ↥((Npre : Subgroup ↥(Hpre : Subgroup G)))).map
1008 ((Npre : Subgroup ↥(Hpre : Subgroup G)).subtype))) 1 := by
1009 simpa [topDerivedTop] using
1010 (topDerived_one_map_subtype_eq_of_isClosed_subgroup
1011 (G := ↥((Hpre : Subgroup G)))
1012 (H := (Npre : Subgroup ↥(Hpre : Subgroup G)))
1013 (K := (⊤ : Subgroup ↥((Npre : Subgroup ↥(Hpre : Subgroup G)))))
1014 (Subgroup.isClosed_of_isOpen _ Npre.isOpen'))
1015 _ = closedDerivedSeries (G := ↥((Hpre : Subgroup G)))
1016 (Npre : Subgroup ↥(Hpre : Subgroup G)) 1 := by
1017 simp only [hmapTop, closedDerivedSeries_succ, closedDerivedSeries_zero]
1018 have hxderMap :
1019 x.1.1 ∈ closedDerivedSeries (G := G)
1020 ((Npre : Subgroup ↥(Hpre : Subgroup G)).map ((Hpre : Subgroup G).subtype)) 1 := by
1021 simpa [hNpreMap] using hxder'
1022 have hxderHpre :
1023 x.1 ∈ closedDerivedSeries (G := ↥((Hpre : Subgroup G)))
1024 (Npre : Subgroup ↥(Hpre : Subgroup G)) 1 := by
1025 rw [← hmapN2] at hxderMap
1026 rcases hxderMap with ⟨y, hy, hyx⟩
1027 exact Subtype.ext hyx ▸ hy
1028 have hxderNpreMap :
1029 x.1 ∈ (topDerivedTop ↥((Npre : Subgroup ↥(Hpre : Subgroup G))) 1).map
1030 ((Npre : Subgroup ↥(Hpre : Subgroup G)).subtype) := by
1031 rw [hmapN1]
1032 exact hxderHpre
1033 rcases hxderNpreMap with ⟨y, hy, hyx⟩
1034 exact Subtype.ext hyx ▸ hy
1035 let qMap :
1036 (↥(Hpre : Subgroup G) ⧸ (Npre : Subgroup ↥(Hpre : Subgroup G))) →*
1037 (↥(H : Subgroup Q) ⧸ (N : Subgroup ↥(H : Subgroup Q))) :=
1038 QuotientGroup.map
1039 (N := (Npre : Subgroup ↥(Hpre : Subgroup G)))
1040 (M := (N : Subgroup ↥(H : Subgroup Q)))
1041 (f := (φH : ↥(Hpre : Subgroup G) →* ↥(H : Subgroup Q)))
1042 (by
1043 intro x hx
1044 exact hx)
1045 have hqMapKer : qMap.ker = ⊥ := by
1046 exact
1048 (f := (φH : ↥(Hpre : Subgroup G) →* ↥(H : Subgroup Q)))
1049 (N := (Npre : Subgroup ↥(Hpre : Subgroup G)))
1050 (M := (N : Subgroup ↥(H : Subgroup Q)))
1051 (h := by
1052 intro x hx
1053 exact hx)
1054 (hcomap := by
1055 rfl)
1056 have hqMapInj : Function.Injective qMap := by
1057 exact (MonoidHom.ker_eq_bot_iff (f := qMap)).1 hqMapKer
1058 have hqMapSurj : Function.Surjective qMap := by
1059 intro q
1060 obtain ⟨h, rfl⟩ := QuotientGroup.mk'_surjective (N : Subgroup ↥(H : Subgroup Q)) q
1061 rcases hφHsurj h with ⟨g, rfl⟩
1062 refine ⟨QuotientGroup.mk' (Npre : Subgroup ↥(Hpre : Subgroup G)) g, ?_⟩
1063 simp only [QuotientGroup.mk'_apply, QuotientGroup.map_mk, MonoidHom.coe_coe, qMap]
1064 let eQ :
1065 (↥(Hpre : Subgroup G) ⧸ (Npre : Subgroup ↥(Hpre : Subgroup G))) ≃*
1066 (↥(H : Subgroup Q) ⧸ (N : Subgroup ↥(H : Subgroup Q))) :=
1067 MulEquiv.ofBijective qMap ⟨hqMapInj, hqMapSurj⟩
1068 let eA :
1069 TopologicalAbelianization ↥(Npre : Subgroup ↥(Hpre : Subgroup G)) ≃*
1070 TopologicalAbelianization ↥(N : Subgroup ↥(H : Subgroup Q)) :=
1071 TopologicalGroup.restrictPreimage_topMaxSolvQuot_mulEquiv
1072 (π := φH) (Q₁ := (N : Subgroup ↥(H : Subgroup Q))) (m := 1)
1073 hφHsurj hclosedN hkerN
1074 have heA_mk (x : ↥(Npre : Subgroup ↥(Hpre : Subgroup G))) :
1075 eA (TopologicalAbelianization.mk ↥(Npre : Subgroup ↥(Hpre : Subgroup G)) x) =
1076 TopologicalAbelianization.mk ↥(N : Subgroup ↥(H : Subgroup Q))
1077 (ProCGroups.ContinuousMonoidHom.restrictPreimage φH (N : Subgroup ↥(H : Subgroup Q))
1078 x) := by
1079 dsimp [eA, TopologicalGroup.restrictPreimage_topMaxSolvQuot_mulEquiv]
1080 rfl
1081 let ρpre :
1082 (↥(Hpre : Subgroup G) ⧸ (Npre : Subgroup ↥(Hpre : Subgroup G))) →*
1083 MulAut (TopologicalAbelianization ↥(Npre : Subgroup ↥(Hpre : Subgroup G))) :=
1084 quotientConjugationTopologicalAbelianizationMap
1085 (G := ↥(Hpre : Subgroup G))
1086 (N := (Npre : Subgroup ↥(Hpre : Subgroup G)))
1087 let ρ :
1088 (↥(H : Subgroup Q) ⧸ (N : Subgroup ↥(H : Subgroup Q))) →*
1089 MulAut (TopologicalAbelianization ↥(N : Subgroup ↥(H : Subgroup Q))) :=
1090 quotientConjugationTopologicalAbelianizationMap
1091 (G := ↥(H : Subgroup Q))
1092 (N := (N : Subgroup ↥(H : Subgroup Q)))
1093 have haction_mk
1094 (g : ↥(Hpre : Subgroup G))
1095 (x : ↥(Npre : Subgroup ↥(Hpre : Subgroup G))) :
1096 eA
1097 (ρpre (QuotientGroup.mk' (Npre : Subgroup ↥(Hpre : Subgroup G)) g)
1098 (TopologicalAbelianization.mk ↥(Npre : Subgroup ↥(Hpre : Subgroup G)) x)) =
1099 ρ (QuotientGroup.mk' (N : Subgroup ↥(H : Subgroup Q)) (φH g))
1100 (eA (TopologicalAbelianization.mk ↥(Npre : Subgroup ↥(Hpre : Subgroup G)) x)) := by
1101 have hρpre_eval :
1102 ρpre (QuotientGroup.mk' (Npre : Subgroup ↥(Hpre : Subgroup G)) g)
1103 (TopologicalAbelianization.mk ↥(Npre : Subgroup ↥(Hpre : Subgroup G)) x) =
1104 TopologicalAbelianization.mk ↥(Npre : Subgroup ↥(Hpre : Subgroup G))
1105 ((MulAut.conjNormal g) x) := by
1106 simpa [ρpre] using
1107 (quotientConjugationTopologicalAbelianizationMap_mk_apply_mk
1108 (N := (Npre : Subgroup ↥(Hpre : Subgroup G))) (g := g) (n := x))
1109 have hconj :
1110 ProCGroups.ContinuousMonoidHom.restrictPreimage φH (N : Subgroup ↥(H : Subgroup Q))
1111 ((MulAut.conjNormal g) x) =
1112 (MulAut.conjNormal (φH g))
1113 (ProCGroups.ContinuousMonoidHom.restrictPreimage φH (N : Subgroup ↥(H : Subgroup Q))
1114 x) := by
1115 ext
1116 rfl
1117 rw [hρpre_eval, heA_mk (x := (MulAut.conjNormal g) x), heA_mk (x := x)]
1118 calc
1119 TopologicalAbelianization.mk ↥(N : Subgroup ↥(H : Subgroup Q))
1120 (ProCGroups.ContinuousMonoidHom.restrictPreimage φH (N : Subgroup ↥(H : Subgroup Q))
1121 ((MulAut.conjNormal g) x))
1123 TopologicalAbelianization.mk ↥(N : Subgroup ↥(H : Subgroup Q))
1124 ((MulAut.conjNormal (φH g))
1125 (ProCGroups.ContinuousMonoidHom.restrictPreimage φH (N : Subgroup ↥(H : Subgroup Q))
1126 x)) := by
1127 exact congrArg (TopologicalAbelianization.mk ↥(N : Subgroup ↥(H : Subgroup Q))) hconj
1128 _ =
1129 ρ (QuotientGroup.mk' (N : Subgroup ↥(H : Subgroup Q)) (φH g))
1130 (TopologicalAbelianization.mk ↥(N : Subgroup ↥(H : Subgroup Q))
1131 (ProCGroups.ContinuousMonoidHom.restrictPreimage φH (N : Subgroup ↥(H : Subgroup Q))
1132 x)) := by
1133 exact (quotientConjugationTopologicalAbelianizationMap_mk_apply_mk
1134 (N := (N : Subgroup ↥(H : Subgroup Q))) (g := φH g)
1136 Subgroup Q)) x)).symm
1137 have hρpre_inj : Function.Injective ρpre := by
1138 simpa [ρpre] using hρpre
1139 have hcomp :
1140 ∀ p : ↥(Hpre : Subgroup G) ⧸ (Npre : Subgroup ↥(Hpre : Subgroup G)),
1141 ρ (eQ p) = (MulAut.congr eA) (ρpre p) := by
1142 intro p
1143 obtain ⟨g, rfl⟩ := QuotientGroup.mk'_surjective
1144 (Npre : Subgroup ↥(Hpre : Subgroup G)) p
1145 ext z
1146 obtain ⟨zpre, rfl⟩ := eA.surjective z
1147 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective
1148 (Subgroup.topologicalClosure
1149 (commutator ↥(Npre : Subgroup ↥(Hpre : Subgroup G)))) zpre
1150 have heQ_mk :
1151 eQ (QuotientGroup.mk' (Npre : Subgroup ↥(Hpre : Subgroup G)) g) =
1152 QuotientGroup.mk' (N : Subgroup ↥(H : Subgroup Q)) (φH g) := by
1153 change
1154 qMap (QuotientGroup.mk' (Npre : Subgroup ↥(Hpre : Subgroup G)) g) =
1155 QuotientGroup.mk' (N : Subgroup ↥(H : Subgroup Q)) (φH g)
1156 dsimp [qMap]
1157 have hcongr_apply
1158 (a₀ : TopologicalAbelianization
1159 ↥(Npre : Subgroup ↥(Hpre : Subgroup G))) :
1160 (MulAut.congr eA)
1161 (ρpre (QuotientGroup.mk' (Npre : Subgroup ↥(Hpre : Subgroup G)) g))
1162 (eA a₀) =
1163 eA
1164 (ρpre
1165 (QuotientGroup.mk' (Npre : Subgroup ↥(Hpre : Subgroup G)) g)
1166 a₀) := by
1167 change
1168 eA
1169 (ρpre
1170 (QuotientGroup.mk' (Npre : Subgroup ↥(Hpre : Subgroup G)) g)
1171 (eA.symm (eA a₀))) =
1172 eA
1173 (ρpre
1174 (QuotientGroup.mk' (Npre : Subgroup ↥(Hpre : Subgroup G)) g)
1175 a₀)
1176 rw [eA.symm_apply_apply]
1177 rw [heQ_mk, hcongr_apply]
1178 exact (haction_mk g x).symm
1179 have hcomp_inj :
1180 Function.Injective (fun p : ↥(Hpre : Subgroup G) ⧸
1181 (Npre : Subgroup ↥(Hpre : Subgroup G)) => ρ (eQ p)) := by
1182 intro p₁ p₂ hp
1183 have hp' :
1184 (MulAut.congr eA) (ρpre p₁) = (MulAut.congr eA) (ρpre p₂) := by
1185 simpa [hcomp p₁, hcomp p₂] using hp
1186 have hp'' : ρpre p₁ = ρpre p₂ := (MulAut.congr eA).injective hp'
1187 exact hρpre_inj hp''
1188 intro q₁ q₂ hq
1189 rcases eQ.surjective q₁ with ⟨p₁, rfl⟩
1190 rcases eQ.surjective q₂ with ⟨p₂, rfl⟩
1191 exact congrArg eQ (hcomp_inj hq)
1193/--
1194Open normal subgroups inside open subgroups of a maximal finite-step solvable quotient inherit
1195faithful quotient conjugation actions once they contain the last derived subgroup.
1197theorem injective_quotientConjAbelianization_of_containsLastDerived_of_abFaithful
1198 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
1199 [CompactSpace G]
1200 (hG : IsAbFaithful G)
1201 {m : ℕ} (hm : 2 ≤ m)
1202 (H : OpenSubgroup (MaxSolvQuot G m))
1203 (N : OpenNormalSubgroup ↥(H : Subgroup (MaxSolvQuot G m)))
1204 (hContain : containsLastDerived (G := G) m H N) :
1205 Function.Injective
1206 (quotientConjugationTopologicalAbelianizationMap
1207 (G := ↥(H : Subgroup (MaxSolvQuot G m)))
1208 (N := (N : Subgroup ↥(H : Subgroup (MaxSolvQuot G m))))) := by
1209 exact
1210 injective_quotientConjAbelianization_of_containsLastDerived_of_isClosedMap
1211 (G := G) hG hm
1212 ((continuousToMaxSolvQuot G m).continuous_toFun.isClosedMap)
1213 H N hContain
1215/--
1216Ambient containment form of faithful quotient conjugation for open normal subgroups inside open
1217subgroups of a maximal finite-step solvable quotient.
1219theorem inj_quotientConjAbelianization_of_lastDerivedSubgroup_le_map_subtype_of_abFaithful
1220 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
1221 [CompactSpace G]
1222 (hG : IsAbFaithful G)
1223 {m : ℕ} (hm : 2 ≤ m)
1224 (H : OpenSubgroup (MaxSolvQuot G m))
1225 (N : OpenNormalSubgroup ↥(H : Subgroup (MaxSolvQuot G m)))
1226 (hN :
1227 lastDerivedSubgroup (G := G) m ≤
1228 (N : Subgroup ↥(H : Subgroup (MaxSolvQuot G m))).map
1229 ((H : Subgroup (MaxSolvQuot G m)).subtype)) :
1230 Function.Injective
1231 (quotientConjugationTopologicalAbelianizationMap
1232 (G := ↥(H : Subgroup (MaxSolvQuot G m)))
1233 (N := (N : Subgroup ↥(H : Subgroup (MaxSolvQuot G m))))) := by
1234 exact
1235 injective_quotientConjAbelianization_of_containsLastDerived_of_abFaithful
1236 (G := G) hG hm H N
1237 (containsLastDerived_of_lastDerivedSubgroup_le_map_subtype (G := G) hN)
1239/--
1240Open normal supergroups above the last derived subgroup inherit faithful quotient conjugation
1241actions under the ambient abelianization-faithful hypothesis.
1243theorem injective_quotientConjAbelianization_of_openNormalSupergroup_of_abFaithful
1244 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
1245 [CompactSpace G]
1246 (hG : IsAbFaithful G)
1247 {m : ℕ} (hm : 2 ≤ m)
1248 (U : OpenNormalSubgroup (MaxSolvQuot G m))
1249 (hU : lastDerivedSubgroup (G := G) m ≤ (U : Subgroup (MaxSolvQuot G m))) :
1250 Function.Injective
1251 (quotientConjugationTopologicalAbelianizationMap
1252 (G := MaxSolvQuot G m) (N := (U : Subgroup (MaxSolvQuot G m)))) := by
1253 let Q : Type u := MaxSolvQuot G m
1254 let UTop : OpenNormalSubgroup ↥((⊤ : OpenSubgroup Q) : Subgroup Q) := openNormalSubgroupTop U
1255 have hContain : containsLastDerived m (⊤ : OpenSubgroup Q) UTop := by
1256 intro x hx
1257 refine ⟨by simp only [OpenSubgroup.mem_top], ?_⟩
1258 have hxU : x ∈ U.toOpenSubgroup := hU hx
1259 change x ∈ U.toOpenSubgroup
1260 exact hxU
1261 have hTop :
1262 Function.Injective
1263 (quotientConjugationTopologicalAbelianizationMap
1264 (G := ↥((⊤ : OpenSubgroup Q) : Subgroup Q))
1265 (N := (UTop : Subgroup ↥((⊤ : OpenSubgroup Q) : Subgroup Q)))) := by
1266 exact
1267 injective_quotientConjAbelianization_of_containsLastDerived_of_abFaithful
1268 (G := G) (m := m) hG hm
1269 (H := (⊤ : OpenSubgroup Q)) (N := UTop) hContain
1270 exact
1271 inj_quotientConjugationTopologicalAbelianizationMap_of_openNormalSubgroupTop
1272 (G := Q) U hTop
1274/--
1275In a maximal finite-step solvable quotient, the center lies in the last derived subgroup under
1276the ambient abelianization-faithful hypothesis.
1278theorem center_le_lastDerivedSubgroup_of_isAbFaithful
1279 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
1280 [CompactSpace G] [TotallyDisconnectedSpace G]
1281 (hG : IsAbFaithful G)
1282 {m : ℕ} (hm : 1 ≤ m) :
1283 Subgroup.center (MaxSolvQuot G m) ≤ lastDerivedSubgroup (G := G) m := by
1284 by_cases hm1 : m = 1
1285 · subst hm1
1286 simp only [closedDerivedSeries_succ, closedDerivedSeries_zero, lastDerivedSubgroup,
1287 topDerivedTop, tsub_self,
1288 le_top]
1289 have hm2 : 2 ≤ m := Nat.succ_le_of_lt (lt_of_le_of_ne hm (Ne.symm hm1))
1290 intro z hz
1291 let Q : Type u := MaxSolvQuot G m
1292 letI : TotallyDisconnectedSpace Q := by
1293 dsimp [Q, MaxSolvQuot]
1295 (topDerivedTop G m)
1296 (show IsClosed ((topDerivedTop G m : Subgroup G) : Set G) by infer_instance)
1297 let K : Subgroup Q := lastDerivedSubgroup (G := G) m
1298 have hKNormal : K.Normal := by
1299 dsimp [K, lastDerivedSubgroup]
1300 infer_instance
1301 letI : K.Normal := hKNormal
1302 have hKClosed : IsClosed ((K : Subgroup Q) : Set Q) := by
1303 dsimp [K, lastDerivedSubgroup]
1304 infer_instance
1305 let Kclosed : ClosedSubgroup Q := ⟨K, hKClosed⟩
1306 change z ∈ K
1307 have hK_eq :
1308 K = sInf {N : Subgroup Q | IsOpen (N : Set Q) ∧ K ≤ N ∧ N.Normal} := by
1309 change (Kclosed : Subgroup Q) =
1310 sInf {N : Subgroup Q | IsOpen (N : Set Q) ∧ K ≤ N ∧ N.Normal}
1312 rw [hK_eq]
1313 simp only [Subgroup.mem_sInf]
1314 intro N hN
1315 let U : OpenNormalSubgroup Q :=
1316 { toSubgroup := N
1317 isOpen' := hN.1
1318 isNormal' := hN.2.2 }
1319 letI : (U : Subgroup Q).Normal := U.isNormal'
1320 have hρinj :
1321 Function.Injective
1322 (quotientConjugationTopologicalAbelianizationMap
1323 (G := Q) (N := (U : Subgroup Q))) :=
1324 injective_quotientConjAbelianization_of_openNormalSupergroup_of_abFaithful
1325 (G := G) (m := m) hG hm2 U hN.2.1
1326 have hρz :
1327 quotientConjugationTopologicalAbelianizationMap
1328 (G := Q) (N := (U : Subgroup Q))
1329 (QuotientGroup.mk' (U : Subgroup Q) z) = 1 :=
1330 quotientConjugationTopologicalAbelianizationMap_mk_eq_one_of_mem_center
1331 (G := Q) (N := (U : Subgroup Q)) (x := z) hz
1332 have hzU : z ∈ (U : Subgroup Q) := by
1333 apply (QuotientGroup.eq_one_iff (N := (U : Subgroup Q)) z).mp
1334 apply hρinj
1335 simpa using hρz
1336 simpa [U] using hzU
1338/--
1339If the center lies in a normal subgroup whose topological abelianization action has no
1340nontrivial fixed points, then injectivity of the natural map to topological abelianization
1341forces the ambient center to be trivial.
1343theorem center_eq_bot_of_center_le_of_noNontrivialFixedPoints_of_inj_topologicalAbelianization
1344 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
1345 {K : Subgroup Q} [K.Normal]
1346 (hcenter : Subgroup.center Q ≤ K)
1347 (hfixed :
1348 HasNoNontrivialFixedPoints
1349 (quotientConjugationTopologicalAbelianizationMap (G := Q) (N := K)))
1350 (hinj : Function.Injective (TopologicalAbelianization.mk ↥K)) :
1351 Subgroup.center Q = ⊥ := by
1352 rw [Subgroup.eq_bot_iff_forall]
1353 intro z hz
1354 have hzK : z ∈ K := hcenter hz
1355 let zK : K := ⟨z, hzK⟩
1356 have hzfix :
1357 ∀ q : Q ⧸ K,
1358 quotientConjugationTopologicalAbelianizationMap (G := Q) (N := K) q
1359 (TopologicalAbelianization.mk ↥K zK) =
1360 TopologicalAbelianization.mk ↥K zK := by
1361 intro q
1362 obtain ⟨g, rfl⟩ := QuotientGroup.mk'_surjective K q
1363 exact
1364 quotientConjAbMap_apply_mk_of_commute
1365 (G := Q) (N := K) (g := g) (x := zK)
1366 ((Subgroup.mem_center_iff.mp hz) g)
1367 have hzab1 : TopologicalAbelianization.mk ↥K zK = 1 := by
1368 exact hfixed (TopologicalAbelianization.mk ↥K zK) hzfix
1369 have hzK1 : zK = 1 := by
1370 exact hinj hzab1
1371 simpa [zK] using congrArg Subtype.val hzK1
1373end ProCGroups.FiniteStepSolvableQuotients