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

ProCGroups/FiniteStepSolvableQuotients/AbelianActions/Faithful.lean

1import Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
2import ProCGroups.FiniteStepSolvableQuotients.Abelianization
3import ProCGroups.ProC.Quotients.ClosedNormal
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/FiniteStepSolvableQuotients/AbelianActions/Faithful.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Finite-step solvable quotients
16Develops topological derived series, maximal solvable quotients of bounded derived length, commutator closure formulas, and abelian-action consequences.
17-/
19open scoped Topology
21namespace ProCGroups.FiniteStepSolvableQuotients
23open ProCGroups.Abelian
25universe u v
27/-- An action has no nontrivial fixed points if every globally fixed element is trivial. -/
29 {Q : Type u} [Group Q]
30 {A : Type v} [Group A]
31 (ρ : Q →* MulAut A) : Prop :=
32 ∀ a : A, (∀ q : Q, ρ q a = a) → a = 1
34/-- Every open subgroup acts faithfully on the topological abelianization of each open normal
35subgroup. -/
37 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : Prop :=
38 ∀ H : OpenSubgroup G,
39 ∀ N : OpenNormalSubgroup ↥(H : Subgroup G),
40 Function.Injective
42 (G := ↥(H : Subgroup G)) (N := (N : Subgroup ↥(H : Subgroup G))))
44/-- The same open normal subgroup viewed inside the top open subgroup. -/
46 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
47 (U : OpenNormalSubgroup G) :
48 OpenNormalSubgroup ↥((⊤ : OpenSubgroup G) : Subgroup G) where
49 toOpenSubgroup :=
50 OpenSubgroup.comap ((⊤ : Subgroup G).subtype) continuous_subtype_val U.toOpenSubgroup
51 isNormal' := by
52 change ((U : Subgroup G).comap ((⊤ : Subgroup G).subtype)).Normal
53 infer_instance
55/-- Injectivity on the top-open-subgroup model implies injectivity in the ambient group. -/
57 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
58 (U : OpenNormalSubgroup G)
59 (hTop :
60 Function.Injective
62 (G := ↥((⊤ : OpenSubgroup G) : Subgroup G))
63 (N := (openNormalSubgroupTop U : Subgroup ↥((⊤ : OpenSubgroup G) : Subgroup G))))) :
64 Function.Injective
66 (G := G) (N := (U : Subgroup G))) := by
67 let Gtop : Type u := ↥((⊤ : OpenSubgroup G) : Subgroup G)
68 let UTop : OpenNormalSubgroup Gtop := openNormalSubgroupTop U
69 let eG : Gtop ≃ₜ* G := OpenSubgroup.topContinuousMulEquiv G
70 let eU : ↥(UTop : Subgroup Gtop) ≃ₜ* ↥(U : Subgroup G) := by
71 simpa [UTop, Gtop, openNormalSubgroupTop] using
72 (Subgroup.subgroupOfContinuousMulEquivOfLe (H := (U : Subgroup G))
73 (K := (⊤ : Subgroup G)) le_top)
74 let eAb : TopologicalAbelianization ↥(UTop : Subgroup Gtop) ≃ₜ*
75 TopologicalAbelianization ↥(U : Subgroup G) :=
76 TopologicalAbelianization.congr (G := ↥(UTop : Subgroup Gtop))
77 (H := ↥(U : Subgroup G)) eU
78 let qMap : G ⧸ (U : Subgroup G) →*
79 Gtop ⧸ (UTop : Subgroup Gtop) :=
80 QuotientGroup.map (N := (U : Subgroup G)) (M := (UTop : Subgroup Gtop))
81 (f := eG.symm.toMonoidHom) (by
82 intro x hx
83 change (OpenSubgroup.topContinuousMulEquiv G).symm x ∈ UTop
84 simpa [UTop, openNormalSubgroupTop] using hx)
85 have hqMapKer : qMap.ker = ⊥ := by
87 (f := eG.symm.toMonoidHom)
88 (N := (U : Subgroup G))
89 (M := (UTop : Subgroup Gtop))
90 (h := by
91 intro x hx
92 change (OpenSubgroup.topContinuousMulEquiv G).symm x ∈ UTop
93 simpa [UTop, openNormalSubgroupTop] using hx)
94 (hcomap := by
95 ext x
96 constructor
97 · intro hx
98 simpa [UTop, openNormalSubgroupTop] using hx
99 · intro hx
100 simpa [UTop, openNormalSubgroupTop] using hx)
101 have hqMapInj : Function.Injective qMap := by
102 exact (MonoidHom.ker_eq_bot_iff (f := qMap)).1 hqMapKer
103 let ρTop : Gtop ⧸ (UTop : Subgroup Gtop) →*
104 MulAut (TopologicalAbelianization ↥(UTop : Subgroup Gtop)) :=
106 (G := Gtop) (N := (UTop : Subgroup Gtop))
107 let ρU : G ⧸ (U : Subgroup G) →*
108 MulAut (TopologicalAbelianization ↥(U : Subgroup G)) :=
110 (G := G) (N := (U : Subgroup G))
111 have haction_mk
112 (g : G)
113 (x : ↥(UTop : Subgroup Gtop)) :
114 eAb
115 (ρTop (QuotientGroup.mk' (UTop : Subgroup Gtop) (eG.symm g))
116 (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x)) =
117 ρU (QuotientGroup.mk' (U : Subgroup G) g)
118 (eAb (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x)) := by
119 have hconj :
120 eU ((MulAut.conjNormal (eG.symm g)) x) =
121 (MulAut.conjNormal g) (eU x) := by
122 ext
123 rfl
124 rw [show ρTop (QuotientGroup.mk' (UTop : Subgroup Gtop) (eG.symm g))
125 (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x) =
126 TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop)
127 ((MulAut.conjNormal (eG.symm g)) x) by
128 simpa [ρTop] using
130 (N := (UTop : Subgroup Gtop)) (g := eG.symm g) (n := x))]
131 rw [show
132 eAb (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop)
133 ((MulAut.conjNormal (eG.symm g)) x)) =
134 TopologicalAbelianization.mk ↥(U : Subgroup G)
135 (eU ((MulAut.conjNormal (eG.symm g)) x)) by
136 rfl]
137 rw [show
138 eAb (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x) =
139 TopologicalAbelianization.mk ↥(U : Subgroup G) (eU x) by
140 rfl]
141 rw [hconj]
142 change TopologicalAbelianization.mk ↥(U : Subgroup G)
143 ((MulAut.conjNormal g) (eU x)) =
144 quotientConjugationTopologicalAbelianizationMap (G := G) (N := (U : Subgroup G))
145 (QuotientGroup.mk' (U : Subgroup G) g)
146 (TopologicalAbelianization.mk ↥(U : Subgroup G) (eU x))
148 (N := (U : Subgroup G)) (g := g) (n := eU x)).symm
149 have hcomp :
150 ∀ q : G ⧸ (U : Subgroup G),
151 ρU q = (MulAut.congr eAb.toMulEquiv) (ρTop (qMap q)) := by
152 intro q
153 obtain ⟨g, rfl⟩ := QuotientGroup.mk'_surjective (U : Subgroup G) q
154 ext a
155 obtain ⟨apre, rfl⟩ := eAb.surjective a
156 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective
157 (Subgroup.closedCommutator (UTop : Subgroup Gtop)) apre
158 simpa [MulAut.congr, qMap] using haction_mk g x
159 intro q₁ q₂ hq
160 have hcongr : (MulAut.congr eAb.toMulEquiv) (ρTop (qMap q₁)) =
161 (MulAut.congr eAb.toMulEquiv) (ρTop (qMap q₂)) := by
162 simpa [ρU, hcomp q₁, hcomp q₂] using hq
163 have htopEq : ρTop (qMap q₁) = ρTop (qMap q₂) :=
164 (MulAut.congr eAb.toMulEquiv).injective hcongr
165 exact hqMapInj (hTop htopEq)
167/-- Injectivity in the ambient group transfers to the corresponding open normal subgroup inside the
168top open subgroup model. -/
170 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
171 (U : OpenNormalSubgroup G)
172 (hU :
173 Function.Injective
175 (G := G) (N := (U : Subgroup G)))) :
176 Function.Injective
178 (G := ↥((⊤ : OpenSubgroup G) : Subgroup G))
179 (N := (openNormalSubgroupTop U : Subgroup ↥((⊤ : OpenSubgroup G) : Subgroup G)))) := by
180 let Gtop : Type u := ↥((⊤ : OpenSubgroup G) : Subgroup G)
181 let UTop : OpenNormalSubgroup Gtop := openNormalSubgroupTop U
182 let eG : Gtop ≃ₜ* G := OpenSubgroup.topContinuousMulEquiv G
183 let eU : ↥(UTop : Subgroup Gtop) ≃ₜ* ↥(U : Subgroup G) := by
184 simpa [UTop, Gtop, openNormalSubgroupTop] using
185 (Subgroup.subgroupOfContinuousMulEquivOfLe (H := (U : Subgroup G))
186 (K := (⊤ : Subgroup G)) le_top)
187 let eAb : TopologicalAbelianization ↥(UTop : Subgroup Gtop) ≃ₜ*
188 TopologicalAbelianization ↥(U : Subgroup G) :=
189 TopologicalAbelianization.congr (G := ↥(UTop : Subgroup Gtop))
190 (H := ↥(U : Subgroup G)) eU
191 let qMap : Gtop ⧸ (UTop : Subgroup Gtop) →* G ⧸ (U : Subgroup G) :=
192 QuotientGroup.map (N := (UTop : Subgroup Gtop)) (M := (U : Subgroup G))
193 (f := eG.toMonoidHom) (by
194 intro x hx
196 simpa [UTop, openNormalSubgroupTop] using hx)
197 have hqMapKer : qMap.ker = ⊥ := by
199 (f := eG.toMonoidHom)
200 (N := (UTop : Subgroup Gtop))
201 (M := (U : Subgroup G))
202 (h := by
203 intro x hx
205 simpa [UTop, openNormalSubgroupTop] using hx)
206 (hcomap := by
207 ext x
208 constructor
209 · intro hx
211 simpa [UTop, openNormalSubgroupTop] using hx
212 · intro hx
214 simpa [UTop, openNormalSubgroupTop] using hx)
215 have hqMapInj : Function.Injective qMap := by
216 exact (MonoidHom.ker_eq_bot_iff (f := qMap)).1 hqMapKer
217 let ρTop : Gtop ⧸ (UTop : Subgroup Gtop) →*
218 MulAut (TopologicalAbelianization ↥(UTop : Subgroup Gtop)) :=
220 (G := Gtop) (N := (UTop : Subgroup Gtop))
221 let ρU : G ⧸ (U : Subgroup G) →*
222 MulAut (TopologicalAbelianization ↥(U : Subgroup G)) :=
224 (G := G) (N := (U : Subgroup G))
225 have haction_mk
226 (g : Gtop)
227 (x : ↥(UTop : Subgroup Gtop)) :
228 eAb
229 (ρTop (QuotientGroup.mk' (UTop : Subgroup Gtop) g)
230 (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x)) =
231 ρU (QuotientGroup.mk' (U : Subgroup G) (eG g))
232 (eAb (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x)) := by
233 have hconj :
234 eU ((MulAut.conjNormal g) x) =
235 (MulAut.conjNormal (eG g)) (eU x) := by
236 ext
237 rfl
238 rw [show ρTop (QuotientGroup.mk' (UTop : Subgroup Gtop) g)
239 (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x) =
240 TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop)
241 ((MulAut.conjNormal g) x) by
242 simpa [ρTop] using
244 (N := (UTop : Subgroup Gtop)) (g := g) (n := x))]
245 rw [show eAb (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop)
246 ((MulAut.conjNormal g) x)) =
247 TopologicalAbelianization.mk ↥(U : Subgroup G) (eU ((MulAut.conjNormal g) x)) by
248 rfl]
249 rw [show eAb (TopologicalAbelianization.mk ↥(UTop : Subgroup Gtop) x) =
250 TopologicalAbelianization.mk ↥(U : Subgroup G) (eU x) by
251 rfl]
252 rw [hconj]
253 change TopologicalAbelianization.mk ↥(U : Subgroup G)
254 ((MulAut.conjNormal (eG g)) (eU x)) =
255 quotientConjugationTopologicalAbelianizationMap (G := G) (N := (U : Subgroup G))
256 (QuotientGroup.mk' (U : Subgroup G) (eG g))
257 (TopologicalAbelianization.mk ↥(U : Subgroup G) (eU x))
259 (N := (U : Subgroup G)) (g := eG g) (n := eU x)).symm
260 have hcomp :
261 ∀ q : Gtop ⧸ (UTop : Subgroup Gtop),
262 ρU (qMap q) = (MulAut.congr eAb.toMulEquiv) (ρTop q) := by
263 intro q
264 obtain ⟨g, rfl⟩ := QuotientGroup.mk'_surjective (UTop : Subgroup Gtop) q
265 ext a
266 obtain ⟨apre, rfl⟩ := eAb.surjective a
267 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective
268 (Subgroup.closedCommutator (UTop : Subgroup Gtop)) apre
269 simpa [MulAut.congr, qMap] using haction_mk g x
270 intro q₁ q₂ hq
271 have hcongr :
272 ρU (qMap q₁) = ρU (qMap q₂) := by
273 simpa [hcomp q₁, hcomp q₂] using congrArg (MulAut.congr eAb.toMulEquiv) hq
274 exact hqMapInj (hU hcongr)
276/-- A nontrivial element is omitted by some open normal subgroup. -/
278 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
279 [CompactSpace G] [TotallyDisconnectedSpace G]
280 {x : G} (hx : x ≠ 1) :
281 ∃ U : OpenNormalSubgroup G, x ∉ (U : Subgroup G) := by
282 let W : Set G := ({x} : Set G)ᶜ
283 have hWOpen : IsOpen W := isClosed_singleton.isOpen_compl
284 have h1W : (1 : G) ∈ W := by
285 simpa [W, eq_comm] using hx
287 (G := G) hWOpen h1W with ⟨U, hUW⟩
288 refine ⟨U, ?_⟩
289 intro hxU
290 have hxW : x ∈ W := hUW hxU
291 simp only [Set.mem_compl_iff, Set.mem_singleton_iff, not_true_eq_false, W] at hxW
293/-- Faithfulness of the conjugation action on every open normal subgroup of the top open subgroup
294forces the ambient center to be trivial. -/
296 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
297 [CompactSpace Q] [TotallyDisconnectedSpace Q]
298 (hfaithful :
299 ∀ U : OpenNormalSubgroup ↥((⊤ : OpenSubgroup Q) : Subgroup Q),
300 Function.Injective
302 (G := ↥((⊤ : OpenSubgroup Q) : Subgroup Q))
303 (N := (U : Subgroup ↥((⊤ : OpenSubgroup Q) : Subgroup Q))))) :
304 Subgroup.center Q = ⊥ := by
305 rw [Subgroup.eq_bot_iff_forall]
306 intro z hz
307 by_contra hzne
308 rcases exists_openNormalSubgroup_not_mem_of_ne_one (G := Q) (x := z) hzne with ⟨U, hzU⟩
309 let Gtop : Type u := ↥((⊤ : OpenSubgroup Q) : Subgroup Q)
310 let zTop : Gtop := ⟨z, by simp only [OpenSubgroup.toSubgroup_top, Subgroup.mem_top]⟩
311 let UTop : OpenNormalSubgroup Gtop := openNormalSubgroupTop U
312 let ρ : (Gtop ⧸ (UTop : Subgroup Gtop)) →*
313 MulAut (TopologicalAbelianization ↥(UTop : Subgroup Gtop)) :=
315 (G := Gtop)
316 (N := (UTop : Subgroup Gtop))
317 have hzTop : zTop ∈ Subgroup.center Gtop := by
318 rw [Subgroup.mem_center_iff] at hz ⊢
319 intro y
320 ext
321 exact hz y
322 have hρz :
323 ρ (QuotientGroup.mk' (UTop : Subgroup Gtop) zTop) = 1 := by
324 dsimp [ρ]
325 exact
327 (G := Gtop) (N := (UTop : Subgroup Gtop)) (x := zTop) hzTop
328 have hzTop_mem :
329 zTop ∈ (UTop : Subgroup Gtop) := by
330 apply (QuotientGroup.eq_one_iff
331 (N := (UTop : Subgroup Gtop)) zTop).mp
332 apply hfaithful UTop
333 simpa using hρz
334 have hzU' : z ∈ (U : Subgroup Q) := by
335 simpa [UTop, zTop] using hzTop_mem
336 exact hzU hzU'
338/-- An `ab`-faithful profinite group has trivial center. -/
340 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
341 [CompactSpace G] [TotallyDisconnectedSpace G]
342 (hG : IsAbFaithful G) :
343 Subgroup.center G = ⊥ := by
345 intro U
346 simpa using hG ⊤ U
348/-- Every open subgroup of an `ab`-faithful profinite group has trivial center. -/
350 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
351 [CompactSpace G] [TotallyDisconnectedSpace G]
352 (hG : IsAbFaithful G) (H : OpenSubgroup G) :
353 Subgroup.center ↥((H : Subgroup G)) = ⊥ := by
354 have hHClosed : IsClosed (((H : OpenSubgroup G) : Set G)) := H.isClosed
355 haveI : CompactSpace ↥((H : OpenSubgroup G) : Subgroup G) := by
356 simpa using
357 (inferInstance : CompactSpace (⟨(H : Subgroup G), hHClosed⟩ : ClosedSubgroup G))
358 haveI : TotallyDisconnectedSpace ↥((H : OpenSubgroup G) : Subgroup G) := by
359 infer_instance
360 exact
362 (Q := ↥((H : OpenSubgroup G) : Subgroup G))
363 (fun U => by
364 let Q : Type u := ↥((H : OpenSubgroup G) : Subgroup G)
365 let e : ↥((⊤ : OpenSubgroup Q) : Subgroup Q) ≃ₜ* Q :=
367 let U' : OpenNormalSubgroup Q :=
368 OpenNormalSubgroup.comap (e.symm : Q →* ↥((⊤ : OpenSubgroup Q) : Subgroup Q))
369 e.symm.continuous_toFun U
370 have hUTopEq : openNormalSubgroupTop U' = U := by
371 ext x
372 rfl
373 have hU' :
374 Function.Injective
376 (G := Q) (N := (U' : Subgroup Q))) := hG H U'
377 have hTop :
378 Function.Injective
380 (G := ↥((⊤ : OpenSubgroup Q) : Subgroup Q))
382 Subgroup ↥((⊤ : OpenSubgroup Q) : Subgroup Q)))) :=
384 (G := Q) U' hU'
385 exact hUTopEq ▸ hTop)
387/-- If an open normal subgroup in an open subgroup of a maximal finite-step solvable quotient
388contains the last derived term, then the quotient conjugation action on its topological
389abelianization is faithful. -/
390theorem
391 injective_quotientConjAbelianization_of_containsLastDerived_of_isClosedMap
392 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
393 (hG : IsAbFaithful G)
394 {m : ℕ} (hm : 2 ≤ m)
395 (hclosedπ : IsClosedMap (continuousToMaxSolvQuot G m))
396 (H : OpenSubgroup (MaxSolvQuot G m))
397 (N : OpenNormalSubgroup ↥(H : Subgroup (MaxSolvQuot G m)))
398 (hContain : containsLastDerived m H N) :
399 Function.Injective
401 (G := ↥(H : Subgroup (MaxSolvQuot G m)))
402 (N := (N : Subgroup ↥(H : Subgroup (MaxSolvQuot G m))))) := by
403 let Q : Type u := MaxSolvQuot G m
404 let π : G →ₜ* Q := continuousToMaxSolvQuot G m
405 let Hpre : OpenSubgroup G := preimageOpenSubgroup π H
406 have hHpreOpen : IsOpen ((Hpre : Subgroup G) : Set G) := Hpre.isOpen'
407 let φH : ↥(Hpre : Subgroup G) →ₜ* ↥(H : Subgroup Q) :=
408 π.restrictPreimage (H : Subgroup Q)
409 let Npre : OpenNormalSubgroup ↥(Hpre : Subgroup G) := by
410 refine
411 { toOpenSubgroup := OpenSubgroup.comap (φH : ↥(Hpre : Subgroup G) →* ↥(H : Subgroup Q))
412 φH.continuous_toFun N.toOpenSubgroup
413 isNormal' := ?_ }
414 change ((N : Subgroup ↥(H : Subgroup Q)).comap
415 (φH : ↥(Hpre : Subgroup G) →* ↥(H : Subgroup Q))).Normal
416 infer_instance
417 let _ : (Npre : Subgroup ↥(Hpre : Subgroup G)).Normal := Npre.isNormal'
418 have hρpre :
419 Function.Injective
421 (G := ↥(Hpre : Subgroup G))
422 (N := (Npre : Subgroup ↥(Hpre : Subgroup G)))) := hG Hpre Npre
423 let Nrealized : OpenSubgroup Q := by
424 refine
425 ⟨(N : Subgroup ↥(H : Subgroup Q)).map ((H : Subgroup Q).subtype), ?_⟩
426 change IsOpen
427 (((fun y : ↥(H : Subgroup Q) => (y : Q)) ''
428 ((N : Subgroup ↥(H : Subgroup Q)) : Set ↥(H : Subgroup Q))))
429 exact H.isOpen'.isOpenMap_subtype_val _ N.isOpen'
430 have hNpreMap :
431 (Npre : Subgroup ↥(Hpre : Subgroup G)).map ((Hpre : Subgroup G).subtype) =
432 ((Nrealized : Subgroup Q).comap (π : G →* Q)) := by
433 ext x
434 constructor
435 · rintro ⟨y, hy, rfl⟩
436 change π y.1 ∈ Nrealized
437 exact ⟨φH y, hy, rfl⟩
438 · intro hx
439 change π x ∈ Nrealized at hx
440 rcases hx with ⟨⟨q, hqH⟩, hqN, hqx⟩
441 have hxHpre : x ∈ Hpre := by
442 change π x ∈ H
443 simpa [← hqx] using hqH
444 refine ⟨⟨x, hxHpre⟩, ?_, rfl⟩
445 change φH ⟨x, hxHpre⟩ ∈ N
446 have hqEq : (⟨q, hqH⟩ : H) = φH ⟨x, hxHpre⟩ := by
447 exact Subtype.ext (by simpa [φH] using hqx)
448 exact hqEq ▸ hqN
449 have hπsurj : Function.Surjective π := by
450 simpa [π, Q] using continuousToMaxSolvQuot_surjective (G := G) m
451 have hφHsurj : Function.Surjective φH := by
452 simpa [φH, Hpre, π] using
453 π.restrictPreimage_surjective hπsurj (H : Subgroup Q)
454 have hclosedφH : IsClosedMap φH := by
455 exact
457 (π := π) (Q₁ := (H : Subgroup Q)) hclosedπ
458 (Subgroup.isClosed_of_isOpen (H : Subgroup Q) H.isOpen')
459 have hclosedN :
460 IsClosedMap
461 (φH.restrictPreimage (N : Subgroup ↥(H : Subgroup Q))) := by
462 exact
464 (π := φH) (Q₁ := (N : Subgroup ↥(H : Subgroup Q))) hclosedφH
465 (Subgroup.isClosed_of_isOpen (N : Subgroup ↥(H : Subgroup Q)) N.isOpen')
466 have hder_preN :
467 topDerivedTop G (m - 1) ≤ ((Nrealized : Subgroup Q).comap (π : G →* Q)) := by
468 intro x hx
469 change π x ∈ Nrealized
470 have hxQ : π x ∈ topDerivedTop Q (m - 1) := by
471 exact (topDerivedTop_le_comap (f := π) (m := m - 1)) hx
472 rcases hContain (π x) hxQ with ⟨hxH, hxN⟩
473 exact ⟨⟨π x, hxH⟩, hxN, rfl⟩
474 have hkerN :
475 (φH.restrictPreimage (N : Subgroup ↥(H : Subgroup Q))).ker ≤
476 topDerivedTop ↥((Npre : Subgroup ↥(Hpre : Subgroup G))) 1 := by
477 intro x hx
478 have hxφ : φH x.1 = 1 := by
479 exact
480 (φH.restrictPreimage_eq_one_iff (N : Subgroup ↥(H : Subgroup Q)) x).1 hx
481 have hxπ : π x.1.1 = 1 := by
482 exact congrArg Subtype.val hxφ
483 have hxder : x.1.1 ∈ topDerivedTop G m := by
484 simpa [π, Q] using
485 (continuousToMaxSolvQuot_eq_one_iff (G := G) (m := m) (x := x.1.1)).1 hxπ
486 have hxder' :
487 x.1.1 ∈ closedDerivedSeries (G := G) ((Nrealized : Subgroup Q).comap (π : G →* Q)) 1 := by
488 have hm1 : 1 ≤ m := le_trans (by decide) hm
489 simpa [topDerivedTop] using
491 (G := G) hm1 hder_preN (by simpa [topDerivedTop] using hxder))
492 have hmapN2 :
493 (closedDerivedSeries (G := ↥((Hpre : Subgroup G)))
494 (Npre : Subgroup ↥(Hpre : Subgroup G)) 1).map
495 ((Hpre : Subgroup G).subtype) =
497 ((Npre : Subgroup ↥(Hpre : Subgroup G)).map ((Hpre : Subgroup G).subtype)) 1 := by
498 simpa [Hpre] using
500 (G := G) (H := (Hpre : Subgroup G))
501 (K := (Npre : Subgroup ↥(Hpre : Subgroup G)))
502 (Subgroup.isClosed_of_isOpen _ hHpreOpen))
503 have hmapN1 :
504 (topDerivedTop ↥((Npre : Subgroup ↥(Hpre : Subgroup G))) 1).map
505 ((Npre : Subgroup ↥(Hpre : Subgroup G)).subtype) =
506 closedDerivedSeries (G := ↥((Hpre : Subgroup G)))
507 (Npre : Subgroup ↥(Hpre : Subgroup G)) 1 := by
508 have hmapTop :
509 ((⊤ : Subgroup ↥((Npre : Subgroup ↥(Hpre : Subgroup G)))).map
510 ((Npre : Subgroup ↥(Hpre : Subgroup G)).subtype)) =
511 (Npre : Subgroup ↥(Hpre : Subgroup G)) := by
512 ext y
513 constructor
514 · rintro ⟨x, -, rfl⟩
515 exact x.2
516 · intro hy
517 exact ⟨⟨y, hy⟩, by simp only [Subgroup.coe_top, Set.mem_univ], rfl⟩
518 calc
519 (topDerivedTop ↥((Npre : Subgroup ↥(Hpre : Subgroup G))) 1).map
520 ((Npre : Subgroup ↥(Hpre : Subgroup G)).subtype) =
521 closedDerivedSeries (G := ↥((Hpre : Subgroup G)))
522 (((⊤ : Subgroup ↥((Npre : Subgroup ↥(Hpre : Subgroup G)))).map
523 ((Npre : Subgroup ↥(Hpre : Subgroup G)).subtype))) 1 := by
524 simpa [topDerivedTop] using
526 (G := ↥((Hpre : Subgroup G)))
527 (H := (Npre : Subgroup ↥(Hpre : Subgroup G)))
528 (K := (⊤ : Subgroup ↥((Npre : Subgroup ↥(Hpre : Subgroup G)))))
529 (Subgroup.isClosed_of_isOpen _ Npre.isOpen'))
530 _ = closedDerivedSeries (G := ↥((Hpre : Subgroup G)))
531 (Npre : Subgroup ↥(Hpre : Subgroup G)) 1 := by
533 have hxderMap :
534 x.1.1 ∈ closedDerivedSeries (G := G)
535 ((Npre : Subgroup ↥(Hpre : Subgroup G)).map ((Hpre : Subgroup G).subtype)) 1 := by
536 simpa [hNpreMap] using hxder'
537 have hxderHpre :
538 x.1 ∈ closedDerivedSeries (G := ↥((Hpre : Subgroup G)))
539 (Npre : Subgroup ↥(Hpre : Subgroup G)) 1 := by
540 rw [← hmapN2] at hxderMap
541 rcases hxderMap with ⟨y, hy, hyx⟩
542 exact Subtype.ext hyx ▸ hy
543 have hxderNpreMap :
544 x.1 ∈ (topDerivedTop ↥((Npre : Subgroup ↥(Hpre : Subgroup G))) 1).map
545 ((Npre : Subgroup ↥(Hpre : Subgroup G)).subtype) := by
546 rw [hmapN1]
547 exact hxderHpre
548 rcases hxderNpreMap with ⟨y, hy, hyx⟩
549 exact Subtype.ext hyx ▸ hy
550 let qMap :
551 (↥(Hpre : Subgroup G) ⧸ (Npre : Subgroup ↥(Hpre : Subgroup G))) →*
552 (↥(H : Subgroup Q) ⧸ (N : Subgroup ↥(H : Subgroup Q))) :=
553 QuotientGroup.map
554 (N := (Npre : Subgroup ↥(Hpre : Subgroup G)))
555 (M := (N : Subgroup ↥(H : Subgroup Q)))
556 (f := (φH : ↥(Hpre : Subgroup G) →* ↥(H : Subgroup Q)))
557 (by
558 intro x hx
559 exact hx)
560 have hqMapKer : qMap.ker = ⊥ := by
561 exact
563 (f := (φH : ↥(Hpre : Subgroup G) →* ↥(H : Subgroup Q)))
564 (N := (Npre : Subgroup ↥(Hpre : Subgroup G)))
565 (M := (N : Subgroup ↥(H : Subgroup Q)))
566 (h := by
567 intro x hx
568 exact hx)
569 (hcomap := by
570 rfl)
571 have hqMapInj : Function.Injective qMap := by
572 exact (MonoidHom.ker_eq_bot_iff (f := qMap)).1 hqMapKer
573 have hqMapSurj : Function.Surjective qMap := by
574 intro q
575 obtain ⟨h, rfl⟩ := QuotientGroup.mk'_surjective (N : Subgroup ↥(H : Subgroup Q)) q
576 rcases hφHsurj h with ⟨g, rfl⟩
577 refine ⟨QuotientGroup.mk' (Npre : Subgroup ↥(Hpre : Subgroup G)) g, ?_⟩
578 simp only [QuotientGroup.mk'_apply, QuotientGroup.map_mk, MonoidHom.coe_coe, qMap]
579 let eQ :
580 (↥(Hpre : Subgroup G) ⧸ (Npre : Subgroup ↥(Hpre : Subgroup G))) ≃*
581 (↥(H : Subgroup Q) ⧸ (N : Subgroup ↥(H : Subgroup Q))) :=
582 MulEquiv.ofBijective qMap ⟨hqMapInj, hqMapSurj⟩
583 let eA :
584 TopologicalAbelianization ↥(Npre : Subgroup ↥(Hpre : Subgroup G)) ≃*
585 TopologicalAbelianization ↥(N : Subgroup ↥(H : Subgroup Q)) :=
586 TopologicalGroup.restrictPreimage_topMaxSolvQuot_mulEquiv
587 (π := φH) (Q₁ := (N : Subgroup ↥(H : Subgroup Q))) (m := 1)
588 hφHsurj hclosedN hkerN
589 have heA_mk (x : ↥(Npre : Subgroup ↥(Hpre : Subgroup G))) :
590 eA (TopologicalAbelianization.mk ↥(Npre : Subgroup ↥(Hpre : Subgroup G)) x) =
591 TopologicalAbelianization.mk ↥(N : Subgroup ↥(H : Subgroup Q))
592 (φH.restrictPreimage (N : Subgroup ↥(H : Subgroup Q)) x) := by
593 dsimp [eA, TopologicalGroup.restrictPreimage_topMaxSolvQuot_mulEquiv]
594 rfl
595 let ρpre :
596 (↥(Hpre : Subgroup G) ⧸ (Npre : Subgroup ↥(Hpre : Subgroup G))) →*
597 MulAut (TopologicalAbelianization ↥(Npre : Subgroup ↥(Hpre : Subgroup G))) :=
599 (G := ↥(Hpre : Subgroup G))
600 (N := (Npre : Subgroup ↥(Hpre : Subgroup G)))
601 let ρ :
602 (↥(H : Subgroup Q) ⧸ (N : Subgroup ↥(H : Subgroup Q))) →*
603 MulAut (TopologicalAbelianization ↥(N : Subgroup ↥(H : Subgroup Q))) :=
605 (G := ↥(H : Subgroup Q))
606 (N := (N : Subgroup ↥(H : Subgroup Q)))
607 have haction_mk
608 (g : ↥(Hpre : Subgroup G))
609 (x : ↥(Npre : Subgroup ↥(Hpre : Subgroup G))) :
610 eA
611 (ρpre (QuotientGroup.mk' (Npre : Subgroup ↥(Hpre : Subgroup G)) g)
612 (TopologicalAbelianization.mk ↥(Npre : Subgroup ↥(Hpre : Subgroup G)) x)) =
613 ρ (QuotientGroup.mk' (N : Subgroup ↥(H : Subgroup Q)) (φH g))
614 (eA (TopologicalAbelianization.mk ↥(Npre : Subgroup ↥(Hpre : Subgroup G)) x)) := by
615 have hρpre_eval :
616 ρpre (QuotientGroup.mk' (Npre : Subgroup ↥(Hpre : Subgroup G)) g)
617 (TopologicalAbelianization.mk ↥(Npre : Subgroup ↥(Hpre : Subgroup G)) x) =
618 TopologicalAbelianization.mk ↥(Npre : Subgroup ↥(Hpre : Subgroup G))
619 ((MulAut.conjNormal g) x) := by
620 simpa [ρpre] using
622 (N := (Npre : Subgroup ↥(Hpre : Subgroup G))) (g := g) (n := x))
623 have hconj :
624 φH.restrictPreimage (N : Subgroup ↥(H : Subgroup Q))
625 ((MulAut.conjNormal g) x) =
626 (MulAut.conjNormal (φH g))
627 (φH.restrictPreimage (N : Subgroup ↥(H : Subgroup Q)) x) := by
628 ext
629 rfl
630 rw [hρpre_eval, heA_mk (x := (MulAut.conjNormal g) x), heA_mk (x := x)]
631 calc
632 TopologicalAbelianization.mk ↥(N : Subgroup ↥(H : Subgroup Q))
633 (φH.restrictPreimage (N : Subgroup ↥(H : Subgroup Q))
634 ((MulAut.conjNormal g) x))
635 =
636 TopologicalAbelianization.mk ↥(N : Subgroup ↥(H : Subgroup Q))
637 ((MulAut.conjNormal (φH g))
638 (φH.restrictPreimage (N : Subgroup ↥(H : Subgroup Q)) x)) := by
639 exact congrArg (TopologicalAbelianization.mk ↥(N : Subgroup ↥(H : Subgroup Q))) hconj
640 _ =
641 ρ (QuotientGroup.mk' (N : Subgroup ↥(H : Subgroup Q)) (φH g))
642 (TopologicalAbelianization.mk ↥(N : Subgroup ↥(H : Subgroup Q))
643 (φH.restrictPreimage (N : Subgroup ↥(H : Subgroup Q)) x)) := by
645 (N := (N : Subgroup ↥(H : Subgroup Q))) (g := φH g)
646 (n := φH.restrictPreimage (N : Subgroup ↥(H : Subgroup Q)) x)).symm
647 have hρpre_inj : Function.Injective ρpre := by
648 simpa [ρpre] using hρpre
649 have hcomp :
650 ∀ p : ↥(Hpre : Subgroup G) ⧸ (Npre : Subgroup ↥(Hpre : Subgroup G)),
651 ρ (eQ p) = (MulAut.congr eA) (ρpre p) := by
652 intro p
653 obtain ⟨g, rfl⟩ := QuotientGroup.mk'_surjective
654 (Npre : Subgroup ↥(Hpre : Subgroup G)) p
655 ext z
656 obtain ⟨zpre, rfl⟩ := eA.surjective z
657 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective
658 (Subgroup.topologicalClosure
659 (commutator ↥(Npre : Subgroup ↥(Hpre : Subgroup G)))) zpre
660 simpa [MulAut.congr] using haction_mk g x
661 have hcomp_inj :
662 Function.Injective (fun p : ↥(Hpre : Subgroup G) ⧸
663 (Npre : Subgroup ↥(Hpre : Subgroup G)) => ρ (eQ p)) := by
664 intro p₁ p₂ hp
665 have hp' :
666 (MulAut.congr eA) (ρpre p₁) = (MulAut.congr eA) (ρpre p₂) := by
667 simpa [hcomp p₁, hcomp p₂] using hp
668 have hp'' : ρpre p₁ = ρpre p₂ := (MulAut.congr eA).injective hp'
669 exact hρpre_inj hp''
670 intro q₁ q₂ hq
671 rcases eQ.surjective q₁ with ⟨p₁, rfl⟩
672 rcases eQ.surjective q₂ with ⟨p₂, rfl⟩
673 exact congrArg eQ (hcomp_inj hq)
675/-- Open normal subgroups inside open subgroups of a maximal finite-step solvable quotient inherit
676faithful quotient conjugation actions once they contain the last derived subgroup. -/
678 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
679 [CompactSpace G] [TotallyDisconnectedSpace G]
680 (hG : IsAbFaithful G)
681 {m : ℕ} (hm : 2 ≤ m)
682 (H : OpenSubgroup (MaxSolvQuot G m))
683 (N : OpenNormalSubgroup ↥(H : Subgroup (MaxSolvQuot G m)))
684 (hContain : containsLastDerived (G := G) m H N) :
685 Function.Injective
687 (G := ↥(H : Subgroup (MaxSolvQuot G m)))
688 (N := (N : Subgroup ↥(H : Subgroup (MaxSolvQuot G m))))) := by
689 exact
690 injective_quotientConjAbelianization_of_containsLastDerived_of_isClosedMap
691 (G := G) hG hm
692 ((continuousToMaxSolvQuot G m).continuous_toFun.isClosedMap)
693 H N hContain
695/-- Ambient containment form of faithful quotient conjugation for open normal subgroups inside
696open subgroups of a maximal finite-step solvable quotient. -/
698 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
699 [CompactSpace G] [TotallyDisconnectedSpace G]
700 (hG : IsAbFaithful G)
701 {m : ℕ} (hm : 2 ≤ m)
702 (H : OpenSubgroup (MaxSolvQuot G m))
703 (N : OpenNormalSubgroup ↥(H : Subgroup (MaxSolvQuot G m)))
704 (hN :
705 lastDerivedSubgroup (G := G) m ≤
706 (N : Subgroup ↥(H : Subgroup (MaxSolvQuot G m))).map
707 ((H : Subgroup (MaxSolvQuot G m)).subtype)) :
708 Function.Injective
710 (G := ↥(H : Subgroup (MaxSolvQuot G m)))
711 (N := (N : Subgroup ↥(H : Subgroup (MaxSolvQuot G m))))) := by
712 exact
714 (G := G) hG hm H N
717/-- Open normal supergroups above the last derived subgroup inherit faithful quotient
718conjugation actions under the ambient `ab`-faithful hypothesis. -/
720 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
721 [CompactSpace G] [TotallyDisconnectedSpace G]
722 (hG : IsAbFaithful G)
723 {m : ℕ} (hm : 2 ≤ m)
724 (U : OpenNormalSubgroup (MaxSolvQuot G m))
725 (hU : lastDerivedSubgroup (G := G) m ≤ (U : Subgroup (MaxSolvQuot G m))) :
726 Function.Injective
728 (G := MaxSolvQuot G m) (N := (U : Subgroup (MaxSolvQuot G m)))) := by
729 let Q : Type u := MaxSolvQuot G m
730 let UTop : OpenNormalSubgroup ↥((⊤ : OpenSubgroup Q) : Subgroup Q) := openNormalSubgroupTop U
731 have hContain : containsLastDerived m (⊤ : OpenSubgroup Q) UTop := by
732 intro x hx
733 refine ⟨by simp only [OpenSubgroup.mem_top], ?_⟩
734 simpa [openNormalSubgroupTop] using hU hx
735 have hTop :
736 Function.Injective
738 (G := ↥((⊤ : OpenSubgroup Q) : Subgroup Q))
739 (N := (UTop : Subgroup ↥((⊤ : OpenSubgroup Q) : Subgroup Q)))) := by
740 exact
742 (G := G) (m := m) hG hm
743 (H := (⊤ : OpenSubgroup Q)) (N := UTop) hContain
744 exact
746 (G := Q) U hTop
748/-- In a maximal finite-step solvable quotient, the center lies in the last derived subgroup under
749the ambient `ab`-faithful hypothesis. -/
751 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
752 [CompactSpace G] [TotallyDisconnectedSpace G]
753 (hG : IsAbFaithful G)
754 {m : ℕ} (hm : 1 ≤ m) :
755 Subgroup.center (MaxSolvQuot G m) ≤ lastDerivedSubgroup (G := G) m := by
756 by_cases hm1 : m = 1
757 · subst hm1
759 le_top]
760 have hm2 : 2 ≤ m := Nat.succ_le_of_lt (lt_of_le_of_ne hm (Ne.symm hm1))
761 intro z hz
762 let Q : Type u := MaxSolvQuot G m
763 have hGprof : ProCGroups.IsProfiniteGroup G := by
764 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
765 have hQprof : ProCGroups.IsProfiniteGroup Q := by
766 simpa [Q, MaxSolvQuot] using
768 (G := G) hGprof
769 (show IsClosed ((topDerivedTop G m : Subgroup G) : Set G) by infer_instance))
770 letI : TotallyDisconnectedSpace Q := ProCGroups.IsProfiniteGroup.totallyDisconnectedSpace hQprof
771 let K : Subgroup Q := lastDerivedSubgroup (G := G) m
772 have hKNormal : K.Normal := by
774 infer_instance
775 letI : K.Normal := hKNormal
776 let Kclosed : ClosedSubgroup Q := ⟨K, by
777 simpa [Q, K] using (show IsClosed ((topDerivedTop Q (m - 1) : Subgroup Q) : Set Q) by
778 infer_instance)⟩
779 change z ∈ K
780 have hK_eq :
781 K = sInf {N : Subgroup Q | IsOpen (N : Set Q) ∧ K ≤ N ∧ N.Normal} := by
782 change (Kclosed : Subgroup Q) =
783 sInf {N : Subgroup Q | IsOpen (N : Set Q) ∧ K ≤ N ∧ N.Normal}
785 rw [hK_eq]
786 simp only [Subgroup.mem_sInf]
787 intro N hN
788 let U : OpenNormalSubgroup Q :=
789 { toSubgroup := N
790 isOpen' := hN.1
791 isNormal' := hN.2.2 }
792 letI : (U : Subgroup Q).Normal := U.isNormal'
793 have hρinj :
794 Function.Injective
796 (G := Q) (N := (U : Subgroup Q))) :=
798 (G := G) (m := m) hG hm2 U hN.2.1
799 have hρz :
801 (G := Q) (N := (U : Subgroup Q))
802 (QuotientGroup.mk' (U : Subgroup Q) z) = 1 :=
804 (G := Q) (N := (U : Subgroup Q)) (x := z) hz
805 have hzU : z ∈ (U : Subgroup Q) := by
806 apply (QuotientGroup.eq_one_iff (N := (U : Subgroup Q)) z).mp
807 apply hρinj
808 simpa using hρz
809 simpa [U] using hzU
811/-- If the center lies in a normal subgroup whose topological abelianization action has no
812nontrivial fixed points, then injectivity of the natural map to topological abelianization forces
813the ambient center to be trivial. -/
815 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
816 {K : Subgroup Q} [K.Normal]
817 (hcenter : Subgroup.center Q ≤ K)
818 (hfixed :
821 (hinj : Function.Injective (TopologicalAbelianization.mk ↥K)) :
822 Subgroup.center Q = ⊥ := by
823 rw [Subgroup.eq_bot_iff_forall]
824 intro z hz
825 have hzK : z ∈ K := hcenter hz
826 let zK : K := ⟨z, hzK⟩
827 have hzfix :
828 ∀ q : Q ⧸ K,
830 (TopologicalAbelianization.mk ↥K zK) =
831 TopologicalAbelianization.mk ↥K zK := by
832 intro q
833 obtain ⟨g, rfl⟩ := QuotientGroup.mk'_surjective K q
834 exact
836 (G := Q) (N := K) (g := g) (x := zK)
837 ((Subgroup.mem_center_iff.mp hz) g)
838 have hzab1 : TopologicalAbelianization.mk ↥K zK = 1 := by
839 exact hfixed (TopologicalAbelianization.mk ↥K zK) hzfix
840 have hzK1 : zK = 1 := by
841 exact hinj hzab1
842 simpa [zK] using congrArg Subtype.val hzK1
844end ProCGroups.FiniteStepSolvableQuotients