Yamaguchi Lean 4 Library
ProCGroups/LocalWeight/ClosedNormalDataAndTransfiniteSeries.lean
ProCGroups/LocalWeight/ClosedNormalDataAndTransfiniteSeries/Source

ProCGroups/LocalWeight/ClosedNormalDataAndTransfiniteSeries.lean

1import ProCGroups.Generation.WordProductsAndClosure
2import ProCGroups.LocalWeight.MetrizabilityAndQuotients
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/LocalWeight/ClosedNormalDataAndTransfiniteSeries.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Local weight and quotient ranks
15Studies local weight, metrizability, quotient size bounds, and cardinal invariants of profinite groups.
16-/
18open Set
19open TopologicalSpace
20open Order
21open scoped Cardinal
22open scoped Topology Pointwise
24namespace ProCGroups.LocalWeight
26universe u
28open ProCGroups.ProC ProCGroups.Generation
29open ProCGroups.FiniteGeneration
32section ClosedNormalSeriesStatements
35section ClosedNormalData
37variable (G : Type u) [Group G] [TopologicalSpace G]
39/-- Bundled closed normal subgroup data for quotient constructions. -/
41 toSubgroup : Subgroup G
42 isClosed' : IsClosed (toSubgroup : Set G)
43 normal' : toSubgroup.Normal
45instance instCoeClosedNormalSubgroupData : Coe (ClosedNormalSubgroupData G) (Subgroup G) where
46 coe H := H.toSubgroup
48@[simp 900] theorem ClosedNormalSubgroupData.coe_mk
49 (H : Subgroup G) (hHclosed : IsClosed (H : Set G)) (hHnormal : H.Normal) :
50 ((⟨H, hHclosed, hHnormal⟩ : ClosedNormalSubgroupData G) : Subgroup G) = H :=
51 rfl
53@[simp 900] theorem ClosedNormalSubgroupData.normal
54 (H : ClosedNormalSubgroupData G) : H.toSubgroup.Normal :=
55 H.normal'
57instance ClosedNormalSubgroupData.instNormal
58 (H : ClosedNormalSubgroupData G) : H.toSubgroup.Normal :=
59 H.normal'
61@[simp 900] theorem ClosedNormalSubgroupData.isClosed
62 (H : ClosedNormalSubgroupData G) : IsClosed ((H : Subgroup G) : Set G) :=
63 H.isClosed'
65/-- The step quotient `H/K` for closed-normal subgroup chains. -/
66abbrev ClosedNormalSubgroupData.stepQuotient
67 (H K : ClosedNormalSubgroupData G) : Type u :=
68 H.toSubgroup ⧸ (K.toSubgroup.subgroupOf H.toSubgroup)
70end ClosedNormalData
72section TransfiniteSeries
74variable (C : FiniteGroupClass.{u})
75variable (G : Type u) [Group G] [TopologicalSpace G]
77/-- Transfinite closed normal series with finite-class step quotients. -/
79 (C : FiniteGroupClass.{u}) (G : Type u) [Group G] [TopologicalSpace G]
80 [IsTopologicalGroup G] (μ : Ordinal) where
81 series : Ordinal → ClosedNormalSubgroupData G
82 top_eq : (series 0).toSubgroup = ⊤
83 bot_eq : (series μ).toSubgroup = ⊥
84 antitone' : ∀ ⦃lam ν : Ordinal⦄, lam ≤ ν → ν ≤ μ →
85 (series ν).toSubgroup ≤ (series lam).toSubgroup
86 step_mem' : ∀ ⦃lam : Ordinal⦄, lam < μ →
87 C (ClosedNormalSubgroupData.stepQuotient (G := G) (series lam) (series (succ lam)))
88 limit_eq_iInf' : ∀ ⦃lam : Ordinal⦄, lam ≤ μ → IsSuccLimit lam →
89 (series lam).toSubgroup =
90 iInf (fun ν : {ν : Ordinal // ν < lam} => (series ν.1).toSubgroup)
91 localWeight_le_cardinal' : localWeight G ≤ μ.card
93/-- 6.5. Relative transfinite closed normal series starting at `H`.
94-/
96 (C : FiniteGroupClass.{u}) (G : Type u) [Group G] [TopologicalSpace G]
97 [IsTopologicalGroup G] (H : ClosedNormalSubgroupData G) (μ : Ordinal) where
98 series : Ordinal → ClosedNormalSubgroupData G
99 start_eq : (series 0).toSubgroup = H.toSubgroup
100 bot_eq : (series μ).toSubgroup = ⊥
101 antitone' : ∀ ⦃lam ν : Ordinal⦄, lam ≤ ν → ν ≤ μ →
102 (series ν).toSubgroup ≤ (series lam).toSubgroup
103 step_mem' : ∀ ⦃lam : Ordinal⦄, lam < μ →
104 C (ClosedNormalSubgroupData.stepQuotient (G := G) (series lam) (series (succ lam)))
105 limit_eq_iInf' : ∀ ⦃lam : Ordinal⦄, lam ≤ μ → IsSuccLimit lam →
106 (series lam).toSubgroup =
107 iInf (fun ν : {ν : Ordinal // ν < lam} => (series ν.1).toSubgroup)
109/-- 6.5(b). Maximal successor-step condition in the relative series.
110-/
112 (C : FiniteGroupClass.{u}) (G : Type u) [Group G] [TopologicalSpace G]
113 (A B : ClosedNormalSubgroupData G) : Prop :=
114 B.toSubgroup ≤ A.toSubgroup ∧
115 C (ClosedNormalSubgroupData.stepQuotient (G := G) A B) ∧
117 D.toSubgroup ≤ A.toSubgroup →
118 C (ClosedNormalSubgroupData.stepQuotient (G := G) A D) →
119 B.toSubgroup ≤ D.toSubgroup →
120 D.toSubgroup = B.toSubgroup ∨ D.toSubgroup = A.toSubgroup
122end TransfiniteSeries
126end ClosedNormalSeriesStatements
129/-- Successor-step lemma for transfinite closed-normal chains: a closed normal
130finite-index subgroup of a closed subgroup is obtained by intersecting that subgroup with an open
131normal subgroup of the ambient profinite group.
133The subgroup `H` is assumed closed in `G`, and `K` is assumed closed and normal in `G`. -/
135 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
136 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
137 (H K : Subgroup G)
138 (hKclosed : IsClosed (K : Set G)) [K.Normal] (hKH : K ≤ H)
139 [Finite (H ⧸ K.subgroupOf H)] :
140 ∃ V : OpenNormalSubgroup G, K = H ⊓ (V : Subgroup G) := by
141 classical
142 let hG : IsProfiniteGroup G := ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
143 let hQ : IsProfiniteGroup (G ⧸ K) :=
145 letI : CompactSpace (G ⧸ K) := IsProfiniteGroup.compactSpace hQ
146 letI : T2Space (G ⧸ K) := IsProfiniteGroup.t2Space hQ
147 letI : TotallyDisconnectedSpace (G ⧸ K) := IsProfiniteGroup.totallyDisconnectedSpace hQ
148 let ψ : H →* G ⧸ K := (QuotientGroup.mk' K).comp H.subtype
149 have hKerEq : (K.subgroupOf H) = ψ.ker := by
150 ext x
151 constructor
152 · intro hx
153 simpa [MonoidHom.mem_ker, ψ] using
154 (QuotientGroup.eq_one_iff (N := K) x.1).2 hx
155 · intro hx
156 exact (QuotientGroup.eq_one_iff (N := K) x.1).1
157 (by simpa [MonoidHom.mem_ker, ψ] using hx)
158 let e₁ : H ⧸ (K.subgroupOf H) ≃* H ⧸ ψ.ker :=
159 QuotientGroup.quotientMulEquivOfEq hKerEq
160 letI : Finite (H ⧸ ψ.ker) := Finite.of_injective e₁.symm e₁.symm.injective
161 let e₂ : H ⧸ ψ.ker ≃* ψ.range := QuotientGroup.quotientKerEquivRange ψ
162 letI : Finite ψ.range := Finite.of_injective e₂.symm e₂.symm.injective
163 obtain ⟨W, hWbot⟩ :=
165 let V : OpenNormalSubgroup G :=
166 OpenNormalSubgroup.comap (QuotientGroup.mk' K) QuotientGroup.continuous_mk W
167 refine ⟨V, ?_⟩
168 ext x
169 constructor
170 · intro hxK
171 refine ⟨hKH hxK, ?_⟩
172 change QuotientGroup.mk' K x ∈ W
173 have hmk : QuotientGroup.mk' K x = 1 :=
174 (QuotientGroup.eq_one_iff (N := K) x).2 hxK
175 rw [hmk]
176 exact W.one_mem
177 · intro hx
178 have hxW : QuotientGroup.mk' K x ∈ W := by
179 simpa [V] using hx.2
180 have hxRange : QuotientGroup.mk' K x ∈ ψ.range := by
181 exact ⟨⟨x, hx.1⟩, rfl⟩
182 have hxBot : QuotientGroup.mk' K x ∈ (⊥ : Subgroup (G ⧸ K)) := by
183 have hxInf : QuotientGroup.mk' K x ∈ ((W : Subgroup (G ⧸ K)) ⊓ ψ.range) :=
184 ⟨hxW, hxRange⟩
185 simpa [hWbot] using hxInf
186 have hxOne : QuotientGroup.mk' K x = 1 := by
187 simpa using hxBot
188 exact (QuotientGroup.eq_one_iff (N := K) x).1 hxOne
190/-- If a quotient carries a neighborhood basis indexed by a family of open normal subgroups, then
191its local weight is bounded by the cardinality of that family. -/
193 (G : Type u) [Group G] [TopologicalSpace G]
194 {ι : Type u} {κ : Cardinal.{u}} (W : ι → OpenNormalSubgroup G)
195 (hWbasis : IsNeighborhoodBasisAt (X := G) (1 : G)
196 (Set.range fun i : ι => (((W i : Subgroup G) : Set G))))
197 (hWcard : Cardinal.mk ι ≤ κ) : localWeight G ≤ κ := by
198 classical
199 let f : ι → Set G := fun i => (((W i : Subgroup G) : Set G))
200 let chooseIdx : { V : Set G // V ∈ Set.range f } → ι :=
201 fun V => Classical.choose V.2
202 have hchoose : ∀ V : { V : Set G // V ∈ Set.range f }, f (chooseIdx V) = V.1 := by
203 intro V
204 exact Classical.choose_spec V.2
205 have hchoose_inj : Function.Injective chooseIdx := by
206 intro V₁ V₂ hEq
207 apply Subtype.ext
208 calc
209 V₁.1 = f (chooseIdx V₁) := (hchoose V₁).symm
210 _ = f (chooseIdx V₂) := by simp only [hEq]
211 _ = V₂.1 := hchoose V₂
212 simpa [localWeight] using
213 calc
214 localWeightAt (X := G) (1 : G) ≤ familyCardinal (X := G) (Set.range f) :=
215 localWeightAt_le_familyCardinal_of_basis (X := G) (x := (1 : G)) hWbasis
216 _ ≤ Cardinal.mk ι := by
218 exact Cardinal.mk_le_of_injective (f := chooseIdx) hchoose_inj
219 _ ≤ κ := hWcard
221/-- Finite-case refinement for descending closed-normal chains. Starting from the finite collection
222`{H ∩ G_λ}`, one inserts finitely many intermediate subgroups until every successor step is either
223unchanged or maximal with respect to belonging to `C`. -/
225 (G : Type u)
226 [Group G] [TopologicalSpace G] [T1Space G]
228 ∃ chain : Finset (ClosedNormalSubgroupData G),
229 H ∈ chain ∧
230 ({ toSubgroup := (⊥ : Subgroup G)
231 isClosed' := isClosed_singleton
232 normal' := by infer_instance } : ClosedNormalSubgroupData G) ∈ chain := by
233 classical
234 let botData : ClosedNormalSubgroupData G :=
235 { toSubgroup := (⊥ : Subgroup G)
236 isClosed' := isClosed_singleton
237 normal' := by infer_instance }
238 refine ⟨{H, botData}, by simp only [Finset.mem_insert, Finset.mem_singleton, true_or, botData], by simp only [Finset.mem_insert, Finset.mem_singleton, or_true, botData]⟩
240/-- 6.5(d). Weight splitting formula over a closed normal subgroup.
241-/
243 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
245 (hInf : Infinite ↥H.toSubgroup ∨ Infinite (G ⧸ H.toSubgroup)) :
247 localWeight ↥H.toSubgroup + quotientLocalWeight (G := G) H.toSubgroup := by
248 classical
249 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
250 letI : T2Space G := IsProfiniteGroup.t2Space hG
251 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
252 let hHpro : IsProfiniteGroup ↥H.toSubgroup :=
253 IsProfiniteGroup.of_isClosed_subgroup (G := G) hG H.toSubgroup H.isClosed
254 let hQpro : IsProfiniteGroup (G ⧸ H.toSubgroup) :=
255 isProfinite_quotient_closedNormal (G := G) hG H.isClosed
256 letI : CompactSpace ↥H.toSubgroup := IsProfiniteGroup.compactSpace hHpro
257 letI : T2Space ↥H.toSubgroup := IsProfiniteGroup.t2Space hHpro
258 letI : TotallyDisconnectedSpace ↥H.toSubgroup :=
259 IsProfiniteGroup.totallyDisconnectedSpace hHpro
260 letI : CompactSpace (G ⧸ H.toSubgroup) := IsProfiniteGroup.compactSpace hQpro
261 letI : T2Space (G ⧸ H.toSubgroup) := IsProfiniteGroup.t2Space hQpro
262 letI : TotallyDisconnectedSpace (G ⧸ H.toSubgroup) :=
263 IsProfiniteGroup.totallyDisconnectedSpace hQpro
265 (G := G) hG with ⟨ιG, WG, hWGbasis, hWGcard⟩
266 have hHle : localWeight ↥H.toSubgroup ≤ localWeight G := by
267 let WH : ιG → OpenNormalSubgroup ↥H.toSubgroup := fun i =>
268 OpenNormalSubgroup.comap H.toSubgroup.subtype continuous_subtype_val (WG i)
269 have hWHbasis :
270 IsNeighborhoodBasisAt (X := ↥H.toSubgroup) (1 : ↥H.toSubgroup)
271 (Set.range fun i : ιG => (((WH i : Subgroup ↥H.toSubgroup) : Set ↥H.toSubgroup))) := by
272 refine ⟨?_, ?_⟩
273 · intro U hU
274 rcases hU with ⟨i, rfl⟩
275 constructor
276 · change IsOpen (((↑) : H.toSubgroup → G) ⁻¹' (((WG i : Subgroup G) : Set G)))
277 simpa using
278 (openNormalSubgroup_isOpen (G := G) (WG i)).preimage continuous_subtype_val
279 · simp only [OpenNormalSubgroup.toSubgroup_comap, Subgroup.comap_subtype, SetLike.mem_coe, one_mem, WH]
280 · intro U hUopen hUone
281 rcases isOpen_induced_iff.mp hUopen with ⟨O, hOopen, hOeq⟩
282 have hOone : (1 : G) ∈ O := by
283 have : (1 : ↥H.toSubgroup) ∈ Subtype.val ⁻¹' O := by
284 simpa [hOeq] using hUone
285 simpa using this
286 rcases hWGbasis.2 O hOopen hOone with ⟨V, hVrange, hVsub⟩
287 rcases hVrange with ⟨i, rfl⟩
288 refine ⟨_, ⟨i, rfl⟩, ?_⟩
289 intro x hx
290 have hxO : (x : G) ∈ O := hVsub hx
291 rw [← hOeq]
292 exact hxO
294 (G := ↥H.toSubgroup) WH hWHbasis hWGcard
295 have hQle : quotientLocalWeight (G := G) H.toSubgroup ≤ localWeight G := by
296 let q : G →* G ⧸ H.toSubgroup := QuotientGroup.mk' H.toSubgroup
297 let BQ : Set (Set (G ⧸ H.toSubgroup)) :=
298 Set.range fun i : ιG => q '' (((WG i : Subgroup G) : Set G))
299 have hBQbasis :
300 IsNeighborhoodBasisAt (X := G ⧸ H.toSubgroup) (1 : G ⧸ H.toSubgroup) BQ := by
301 refine ⟨?_, ?_⟩
302 · intro U hU
303 rcases hU with ⟨i, rfl⟩
304 constructor
305 · exact (QuotientGroup.isOpenMap_coe (N := H.toSubgroup)) _
306 (openNormalSubgroup_isOpen (G := G) (WG i))
307 · refine ⟨1, ?_, ?_⟩
308 · exact (WG i).one_mem'
309 · simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_one, q]
310 · intro U hUopen hUone
311 have hpreOpen : IsOpen (q ⁻¹' U) := hUopen.preimage QuotientGroup.continuous_mk
312 have hpreOne : (1 : G) ∈ q ⁻¹' U := by
313 simpa [q] using hUone
314 rcases hWGbasis.2 (q ⁻¹' U) hpreOpen hpreOne with ⟨V, hVrange, hVsub⟩
315 rcases hVrange with ⟨i, rfl⟩
316 refine ⟨q '' (((WG i : Subgroup G) : Set G)), ⟨i, rfl⟩, ?_⟩
317 rintro _ ⟨g, hg, rfl⟩
318 exact hVsub hg
319 let chooseIdx : { U : Set (G ⧸ H.toSubgroup) // U ∈ BQ } → ιG :=
320 fun U => Classical.choose U.2
321 have hchoose :
322 ∀ U : { U : Set (G ⧸ H.toSubgroup) // U ∈ BQ },
323 q '' (((WG (chooseIdx U) : Subgroup G) : Set G)) = U.1 := by
324 intro U
325 exact Classical.choose_spec U.2
326 have hchoose_inj : Function.Injective chooseIdx := by
327 intro U₁ U₂ hEq
328 apply Subtype.ext
329 calc
330 U₁.1 = q '' (((WG (chooseIdx U₁) : Subgroup G) : Set G)) := (hchoose U₁).symm
331 _ = q '' (((WG (chooseIdx U₂) : Subgroup G) : Set G)) := by simp only [hEq, OpenSubgroup.coe_toSubgroup]
332 _ = U₂.1 := hchoose U₂
333 have hBQcard : familyCardinal (X := G ⧸ H.toSubgroup) BQ ≤ Cardinal.mk ιG := by
335 exact Cardinal.mk_le_of_injective (f := chooseIdx) hchoose_inj
338 (X := G ⧸ H.toSubgroup) (x := (1 : G ⧸ H.toSubgroup)) hBQbasis).trans
339 (hBQcard.trans hWGcard)
341 (G := ↥H.toSubgroup) hHpro with ⟨ιH, KH, hKHbasis, hKHcard⟩
343 (G := G ⧸ H.toSubgroup) hQpro with ⟨ιQ, QH, hQHbasis, hQHcard0⟩
344 have hQHcard : Cardinal.mk ιQ ≤ quotientLocalWeight (G := G) H.toSubgroup := by
346 have hιHne : Nonempty ιH := by
347 rcases hKHbasis.2 Set.univ isOpen_univ (by simp only [mem_univ]) with ⟨U, hUrange, _⟩
348 rcases hUrange with ⟨i, rfl⟩
349 exact ⟨i⟩
350 have hιQne : Nonempty ιQ := by
351 rcases hQHbasis.2 Set.univ isOpen_univ (by simp only [mem_univ]) with ⟨U, hUrange, _⟩
352 rcases hUrange with ⟨i, rfl⟩
353 exact ⟨i⟩
354 have hAmbientData :
355 ∀ i : ιH, ∃ O V : Set G,
356 IsOpen O ∧
357 (((↑) : H.toSubgroup → G) ⁻¹' O) = (((KH i : Subgroup ↥H.toSubgroup) : Set ↥H.toSubgroup)) ∧
358 IsOpen V ∧ (1 : G) ∈ V ∧
359 ∀ {a b : G}, a ∈ V → b ∈ V → a⁻¹ * b ∈ O := by
360 intro i
361 rcases isOpen_induced_iff.mp (openNormalSubgroup_isOpen (G := ↥H.toSubgroup) (KH i)) with
362 ⟨O, hOopen, hOeq⟩
363 have hOone : (1 : G) ∈ O := by
364 have : (1 : ↥H.toSubgroup) ∈ Subtype.val ⁻¹' O := by
365 rw [hOeq]
366 exact (KH i).one_mem'
367 exact this
368 have hOmem : O ∈ 𝓝 (1 : G) := hOopen.mem_nhds hOone
369 have hcont :
370 Continuous fun p : G × G => p.1⁻¹ * p.2 :=
371 (continuous_inv.comp continuous_fst).mul continuous_snd
372 have hmem :
373 {p : G × G | p.1⁻¹ * p.2 ∈ O} ∈ 𝓝 ((1 : G), (1 : G)) := by
374 exact hcont.continuousAt (by simpa using hOmem)
375 rcases mem_nhds_prod_iff.mp hmem with ⟨A, hA, B, hB, hAB⟩
376 rcases mem_nhds_iff.mp hA with ⟨A', hA'sub, hA'open, hA'one⟩
377 rcases mem_nhds_iff.mp hB with ⟨B', hB'sub, hB'open, hB'one⟩
378 refine ⟨O, A' ∩ B', hOopen, hOeq, hA'open.inter hB'open, ?_, ?_⟩
379 · exact ⟨hA'one, hB'one⟩
380 · intro a b ha hb
381 have haA : a ∈ A := hA'sub ha.1
382 have hbB : b ∈ B := hB'sub hb.2
383 exact hAB (show (a, b) ∈ A ×ˢ B from ⟨haA, hbB⟩)
384 choose OH VH hOHopen hOHeq hVHopen hVHone hVHdiff using hAmbientData
385 let q : G →* G ⧸ H.toSubgroup := QuotientGroup.mk' H.toSubgroup
386 let PH : ιQ → OpenNormalSubgroup G := fun j =>
387 OpenNormalSubgroup.comap q QuotientGroup.continuous_mk (QH j)
388 let B : Set (Set G) :=
389 Set.range fun ij : ιH × ιQ => VH ij.1 ∩ (((PH ij.2 : Subgroup G) : Set G))
390 have hBbasis : IsNeighborhoodBasisAt (X := G) (1 : G) B := by
391 refine ⟨?_, ?_⟩
392 · intro U hU
393 rcases hU with ⟨⟨i, j⟩, rfl⟩
394 constructor
395 · exact (hVHopen i).inter (openNormalSubgroup_isOpen (G := G) (PH j))
396 · exact ⟨hVHone i, by simp only [OpenNormalSubgroup.toSubgroup_comap, Subgroup.coe_comap, QuotientGroup.coe_mk',
397 OpenSubgroup.coe_toSubgroup, mem_preimage, QuotientGroup.mk_one, SetLike.mem_coe, one_mem, PH, q]⟩
398 · intro U hUopen hUone
399 rcases hWGbasis.2 U hUopen hUone with ⟨Nset, hNrange, hNsubU⟩
400 rcases hNrange with ⟨n, rfl⟩
401 have hHNopen :
402 IsOpen (((↑) : H.toSubgroup → G) ⁻¹' (((WG n : Subgroup G) : Set G))) := by
403 simpa using (openNormalSubgroup_isOpen (G := G) (WG n)).preimage continuous_subtype_val
404 have hHNone :
405 (1 : H.toSubgroup) ∈
406 ((↑) : H.toSubgroup → G) ⁻¹' (((WG n : Subgroup G) : Set G)) := by
407 simp only [OpenSubgroup.coe_toSubgroup, mem_preimage, OneMemClass.coe_one, SetLike.mem_coe, one_mem]
408 rcases hKHbasis.2
409 (((↑) : H.toSubgroup → G) ⁻¹' (((WG n : Subgroup G) : Set G)))
410 hHNopen hHNone with ⟨Kset, hKrange, hKsub⟩
411 rcases hKrange with ⟨i, rfl⟩
412 have hImageOpen :
413 IsOpen (((↑) : G → G ⧸ H.toSubgroup) '' ((((WG n : Subgroup G) : Set G) ∩ VH i))) := by
414 exact (QuotientGroup.isOpenMap_coe (N := H.toSubgroup)) _
415 ((openNormalSubgroup_isOpen (G := G) (WG n)).inter (hVHopen i))
416 have hImageOne :
417 (1 : G ⧸ H.toSubgroup) ∈
418 ((↑) : G → G ⧸ H.toSubgroup) '' ((((WG n : Subgroup G) : Set G) ∩ VH i)) := by
419 refine ⟨1, ?_, by simp only [QuotientGroup.mk_one]⟩
420 exact ⟨(WG n).one_mem', hVHone i⟩
421 rcases hQHbasis.2
422 (((↑) : G → G ⧸ H.toSubgroup) '' ((((WG n : Subgroup G) : Set G) ∩ VH i)))
423 hImageOpen hImageOne with ⟨Qset, hQrange, hQsub⟩
424 rcases hQrange with ⟨j, rfl⟩
425 refine ⟨VH i ∩ (((PH j : Subgroup G) : Set G)), ⟨(i, j), rfl⟩, ?_⟩
426 intro x hx
427 have hxV : x ∈ VH i := hx.1
428 have hxQ : q x ∈ ((QH j : Subgroup (G ⧸ H.toSubgroup)) : Set (G ⧸ H.toSubgroup)) := by
429 simpa [PH, OpenNormalSubgroup.mem_comap] using hx.2
430 rcases hQsub hxQ with ⟨y, hy, hyEq⟩
431 have hyN : y ∈ ((WG n : Subgroup G) : Set G) := hy.1
432 have hyV : y ∈ VH i := hy.2
433 have hyxH : y⁻¹ * x ∈ H.toSubgroup := by
434 exact (QuotientGroup.eq).1 (by simpa [q] using hyEq)
435 have hyxO : y⁻¹ * x ∈ OH i := hVHdiff i hyV hxV
436 have hyxK :
437 (⟨y⁻¹ * x, hyxH⟩ : H.toSubgroup) ∈
438 ((KH i : Subgroup ↥H.toSubgroup) : Set ↥H.toSubgroup) := by
439 rw [← hOHeq i]
440 exact hyxO
441 have hyxN : y⁻¹ * x ∈ ((WG n : Subgroup G) : Set G) := hKsub hyxK
442 have hxN : x ∈ ((WG n : Subgroup G) : Set G) := by
443 have hxeq : x = y * (y⁻¹ * x) := by simp only [mul_inv_cancel_left]
444 rw [hxeq]
445 exact (WG n).mul_mem hyN hyxN
446 exact hNsubU hxN
447 let chooseIdx : { U : Set G // U ∈ B } → ιH × ιQ :=
448 fun U => Classical.choose U.2
449 have hchoose :
450 ∀ U : { U : Set G // U ∈ B },
451 VH (chooseIdx U).1 ∩ (((PH (chooseIdx U).2 : Subgroup G) : Set G)) = U.1 := by
452 intro U
453 exact Classical.choose_spec U.2
454 have hchoose_inj : Function.Injective chooseIdx := by
455 intro U₁ U₂ hEq
456 apply Subtype.ext
457 calc
458 U₁.1 = VH (chooseIdx U₁).1 ∩ (((PH (chooseIdx U₁).2 : Subgroup G) : Set G)) :=
459 (hchoose U₁).symm
460 _ = VH (chooseIdx U₂).1 ∩ (((PH (chooseIdx U₂).2 : Subgroup G) : Set G)) := by
461 simp only [hEq, OpenSubgroup.coe_toSubgroup]
462 _ = U₂.1 := hchoose U₂
463 have hBcard :
464 familyCardinal (X := G) B ≤ Cardinal.mk (ιH × ιQ) := by
466 exact Cardinal.mk_le_of_injective (f := chooseIdx) hchoose_inj
467 have hProdLe :
468 Cardinal.mk (ιH × ιQ) ≤
469 localWeight ↥H.toSubgroup + quotientLocalWeight (G := G) H.toSubgroup := by
470 have hιHnz : Cardinal.mk ιH ≠ 0 :=
471 Cardinal.mk_ne_zero_iff.mpr hιHne
472 have hιQnz : Cardinal.mk ιQ ≠ 0 :=
473 Cardinal.mk_ne_zero_iff.mpr hιQne
474 cases hInf with
475 | inl hHinf =>
476 letI : Infinite ↥H.toSubgroup := hHinf
477 have hHaleph :
478 ℵ₀ ≤ localWeight ↥H.toSubgroup :=
480 calc
481 Cardinal.mk (ιH × ιQ) = Cardinal.mk ιH * Cardinal.mk ιQ := by
482 rw [Cardinal.mk_prod]
483 simp only [Cardinal.lift_id]
484 _ ≤ localWeight ↥H.toSubgroup * Cardinal.mk ιQ := by
485 exact mul_le_mul' hKHcard le_rfl
486 _ = max (localWeight ↥H.toSubgroup) (Cardinal.mk ιQ) := by
487 exact Cardinal.mul_eq_max_of_aleph0_le_left hHaleph hιQnz
488 _ ≤ max (localWeight ↥H.toSubgroup) (quotientLocalWeight (G := G) H.toSubgroup) := by
489 exact max_le_max le_rfl hQHcard
490 _ = localWeight ↥H.toSubgroup + quotientLocalWeight (G := G) H.toSubgroup := by
491 symm
492 exact Cardinal.add_eq_max hHaleph
493 | inr hQinf =>
494 letI : Infinite (G ⧸ H.toSubgroup) := hQinf
495 have hQaleph :
496 ℵ₀ ≤ quotientLocalWeight (G := G) H.toSubgroup := by
499 (G := G ⧸ H.toSubgroup) hQpro
500 calc
501 Cardinal.mk (ιH × ιQ) = Cardinal.mk ιH * Cardinal.mk ιQ := by
502 rw [Cardinal.mk_prod]
503 simp only [Cardinal.lift_id]
504 _ ≤ Cardinal.mk ιH * quotientLocalWeight (G := G) H.toSubgroup := by
505 exact mul_le_mul' le_rfl hQHcard
506 _ = max (Cardinal.mk ιH) (quotientLocalWeight (G := G) H.toSubgroup) := by
507 exact Cardinal.mul_eq_max_of_aleph0_le_right hιHnz hQaleph
508 _ ≤ max (localWeight ↥H.toSubgroup) (quotientLocalWeight (G := G) H.toSubgroup) := by
509 exact max_le_max hKHcard le_rfl
510 _ = localWeight ↥H.toSubgroup + quotientLocalWeight (G := G) H.toSubgroup := by
511 symm
512 exact Cardinal.add_eq_max' hQaleph
513 have hUpper :
515 localWeight ↥H.toSubgroup + quotientLocalWeight (G := G) H.toSubgroup := by
516 simpa [localWeight] using
517 (localWeightAt_le_familyCardinal_of_basis (X := G) (x := (1 : G)) hBbasis).trans
518 (hBcard.trans hProdLe)
519 have hLower :
520 localWeight ↥H.toSubgroup + quotientLocalWeight (G := G) H.toSubgroup ≤ localWeight G := by
521 cases hInf with
522 | inl hHinf =>
523 letI : Infinite ↥H.toSubgroup := hHinf
524 have hHaleph :
525 ℵ₀ ≤ localWeight ↥H.toSubgroup :=
527 rw [Cardinal.add_eq_max hHaleph]
528 exact max_le_iff.mpr ⟨hHle, hQle⟩
529 | inr hQinf =>
530 letI : Infinite (G ⧸ H.toSubgroup) := hQinf
531 have hQaleph :
532 ℵ₀ ≤ quotientLocalWeight (G := G) H.toSubgroup := by
535 (G := G ⧸ H.toSubgroup) hQpro
536 rw [Cardinal.add_eq_max' hQaleph]
537 exact max_le_iff.mpr ⟨hHle, hQle⟩
538 exact le_antisymm hUpper hLower
540/-- Subadditivity of quotient local weight along a chain `H ≤ K ≤ M`. -/
542 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
544 (hHK : H.toSubgroup ≤ K.toSubgroup) :
545 quotientLocalWeight (G := ↥M.toSubgroup) (K.toSubgroup.subgroupOf M.toSubgroup) ≤
546 quotientLocalWeight (G := ↥M.toSubgroup) (H.toSubgroup.subgroupOf M.toSubgroup) +
547 quotientLocalWeight (G := ↥K.toSubgroup) (H.toSubgroup.subgroupOf K.toSubgroup) := by
548 let HM : Subgroup ↥M.toSubgroup := H.toSubgroup.subgroupOf M.toSubgroup
549 let KM : Subgroup ↥M.toSubgroup := K.toSubgroup.subgroupOf M.toSubgroup
550 have hHMK : HM ≤ KM := by
551 intro x hx
552 exact hHK hx
553 have hopen :
554 IsOpenMap (leftQuotientProjection HM KM hHMK : (↥M.toSubgroup ⧸ HM) → (↥M.toSubgroup ⧸ KM)) :=
555 by
556 intro U hU
557 have hpre :
558 IsOpen ((QuotientGroup.mk (s := HM)) ⁻¹' U) := by
559 exact ((QuotientGroup.isQuotientMap_mk HM).isOpen_preimage).2 hU
560 have himage :
561 leftQuotientProjection HM KM hHMK '' U =
562 (QuotientGroup.mk (s := KM)) '' ((QuotientGroup.mk (s := HM)) ⁻¹' U) := by
563 ext y
564 constructor
565 · rintro ⟨x, hxU, rfl⟩
566 revert hxU
567 refine Quotient.inductionOn x ?_
568 intro g hgU
569 refine ⟨g, hgU, ?_⟩
571 · rintro ⟨g, hgU, rfl⟩
572 refine ⟨QuotientGroup.mk (s := HM) g, hgU, ?_⟩
574 rw [himage]
575 exact (QuotientGroup.isOpenMap_coe (N := KM)) _ hpre
576 have hmon :
577 quotientLocalWeight (G := ↥M.toSubgroup) (K.toSubgroup.subgroupOf M.toSubgroup) ≤
578 quotientLocalWeight (G := ↥M.toSubgroup) (H.toSubgroup.subgroupOf M.toSubgroup) := by
579 simpa [quotientLocalWeight, HM, KM] using
581 (X := (↥M.toSubgroup ⧸ HM)) (Y := (↥M.toSubgroup ⧸ KM))
582 (x := (1 : ↥M.toSubgroup ⧸ HM))
583 (f := leftQuotientProjection HM KM hHMK)
585 exact hmon.trans (self_le_add_right _ _)
587/--
588Forward direction: existence of a transfinite closed normal series from the local-weight
589bound.
590-/
592 (C : FiniteGroupClass.{u}) (G : Type u)
593 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
594 (μ : Ordinal) (hForm : FiniteGroupClass.Formation C)
595 (hNorm : FiniteGroupClass.NormalSubgroupClosed C) (hG : IsProCGroup C G)
596 (hμ : localWeight G ≤ μ.card) :
597 Nonempty (TransfiniteClosedNormalSeries C G μ) := by
598 classical
599 letI : CompactSpace G := IsProCGroup.compactSpace hG
600 letI : T2Space G := IsProCGroup.t2Space hG
601 letI : TotallyDisconnectedSpace G := IsProCGroup.totallyDisconnectedSpace hG
602 let hIso : FiniteGroupClass.IsomClosed C :=
603 FiniteGroupClass.Formation.isomClosed (C := C) hForm
605 (C := C) (G := G) hG with
606 ⟨ι, W, hWC, hWbasis, hWcard0⟩
607 have hιne : Nonempty ι := by
608 rcases hWbasis.2 Set.univ isOpen_univ (by simp only [mem_univ]) with ⟨U, hUrange, _⟩
609 rcases hUrange with ⟨i, rfl⟩
610 exact ⟨i⟩
611 letI : Nonempty ι := hιne
612 have hWcard : Cardinal.mk ι ≤ μ.card := hWcard0.trans hμ
613 have hEmb : Nonempty (ι ↪ Set.Iio μ) := by
614 have hWcardLift0 :
615 Cardinal.lift.{u + 1} (Cardinal.mk ι) ≤ Cardinal.lift.{u + 1} μ.card := by
616 exact (Cardinal.lift_le).2 hWcard
617 have hWcardLift :
618 Cardinal.lift.{u + 1} (Cardinal.mk ι) ≤ Cardinal.lift.{u} #(Set.Iio μ) := by
619 simpa [Ordinal.mk_Iio_ordinal, Cardinal.lift_lift] using hWcardLift0
620 exact Cardinal.lift_mk_le'.mp hWcardLift
621 let e : ι ↪ Set.Iio μ := Classical.choice hEmb
622 let σ : Set.Iio μ → ι := Function.invFun e
623 have hσ : ∀ i : ι, σ (e i) = i := by
624 intro i
625 exact Function.leftInverse_invFun e.injective i
626 let Wμ : Set.Iio μ → OpenNormalSubgroup G := fun a => W (σ a)
627 have hWμC : ∀ a : Set.Iio μ, C (G ⧸ (Wμ a : Subgroup G)) := by
628 intro a
629 exact hWC (σ a)
630 let B : Set (Set G) := Set.range fun i : ι => (((W i : Subgroup G) : Set G))
631 let Bμ : Set (Set G) := Set.range fun a : Set.Iio μ => (((Wμ a : Subgroup G) : Set G))
632 have hBμeq : Bμ = B := by
633 ext U
634 constructor
635 · rintro ⟨a, rfl⟩
636 exact ⟨σ a, rfl⟩
637 · rintro ⟨i, rfl⟩
638 exact ⟨e i, by simp only [hσ i, OpenSubgroup.coe_toSubgroup, Wμ]⟩
639 have hWμbasis : IsNeighborhoodBasisAt (X := G) (1 : G) Bμ := by
640 simpa [Bμ, B, hBμeq] using hWbasis
641 have hWμbot : iInf (fun a : Set.Iio μ => (Wμ a : Subgroup G)) = (⊥ : Subgroup G) := by
642 simpa [Bμ] using
644 let seriesSub : Ordinal → Subgroup G := fun lam =>
645 if hlam : lam ≤ μ then
646 iInf (fun a : Set.Iio lam => (Wμ ⟨a.1, lt_of_lt_of_le a.2 hlam⟩ : Subgroup G))
647 else ⊥
648 have hseriesClosed : ∀ lam : Ordinal, IsClosed (seriesSub lam : Set G) := by
649 intro lam
650 by_cases hlam : lam ≤ μ
651 · simpa [seriesSub, hlam] using
652 isClosed_iInter (fun a : Set.Iio lam =>
653 openNormalSubgroup_isClosed (G := G) (Wμ ⟨a.1, lt_of_lt_of_le a.2 hlam⟩))
654 · dsimp [seriesSub]
655 rw [dif_neg hlam]
656 simp only [Subgroup.coe_bot, finite_singleton, Finite.isClosed]
657 have hseriesNormal : ∀ lam : Ordinal, (seriesSub lam).Normal := by
658 intro lam
659 by_cases hlam : lam ≤ μ
660 · simpa [seriesSub, hlam] using
661 (show
662 (iInf (fun a : Set.Iio lam =>
663 (Wμ ⟨a.1, lt_of_lt_of_le a.2 hlam⟩ : Subgroup G))).Normal from
664 Subgroup.normal_iInf_normal fun a : Set.Iio lam =>
665 (show (Wμ ⟨a.1, lt_of_lt_of_le a.2 hlam⟩ : Subgroup G).Normal from inferInstance))
666 · simpa [seriesSub, hlam] using (show (⊥ : Subgroup G).Normal by infer_instance)
667 let seriesData : Ordinal → ClosedNormalSubgroupData G := fun lam =>
668 { toSubgroup := seriesSub lam
669 isClosed' := hseriesClosed lam
670 normal' := hseriesNormal lam }
671 refine ⟨{
672 series := seriesData,
673 top_eq := ?_,
674 bot_eq := ?_,
675 antitone' := ?_,
676 step_mem' := ?_,
677 limit_eq_iInf' := ?_,
678 localWeight_le_cardinal' := hμ }⟩
679 · ext x
680 simp only [zero_le, ↓reduceDIte, Subgroup.mem_iInf, OpenSubgroup.mem_toSubgroup, IsEmpty.forall_iff,
681 Subgroup.mem_top, seriesSub, seriesData]
682 · simpa [seriesData, seriesSub] using hWμbot
683 · intro lam ν hlam hν x hx
684 have hlamμ : lam ≤ μ := hlam.trans hν
685 have hxall :
686 ∀ a : Set.Iio ν, x ∈ (Wμ ⟨a.1, lt_of_lt_of_le a.2 hν⟩ : Subgroup G) := by
687 simpa [seriesData, seriesSub, hν, Subgroup.mem_iInf] using hx
688 have hrestrict :
689 ∀ a : Set.Iio lam, x ∈ (Wμ ⟨a.1, lt_of_lt_of_le a.2 hlamμ⟩ : Subgroup G) := by
690 intro a
691 exact hxall ⟨a.1, lt_of_lt_of_le a.2 hlam⟩
692 simpa [seriesData, seriesSub, hlamμ, Subgroup.mem_iInf] using hrestrict
693 · intro lam hlam
694 let H : ClosedNormalSubgroupData G := seriesData lam
695 let K : ClosedNormalSubgroupData G := seriesData (succ lam)
696 let U : OpenNormalSubgroup G := Wμ ⟨lam, hlam⟩
697 let φ : H.toSubgroup →* G ⧸ (U : Subgroup G) :=
698 (QuotientGroup.mk' (U : Subgroup G)).comp H.toSubgroup.subtype
699 let L : Subgroup (G ⧸ (U : Subgroup G)) :=
700 Subgroup.map (QuotientGroup.mk' (U : Subgroup G)) H.toSubgroup
701 have hlamle : lam ≤ μ := hlam.le
702 have hsuccle : succ lam ≤ μ := succ_le_of_lt hlam
703 have hRangeEq : φ.range = L := by
704 ext y
705 constructor
706 · rintro ⟨x, rfl⟩
707 exact ⟨x, x.2, rfl⟩
708 · rintro ⟨x, hx, rfl⟩
709 exact ⟨⟨x, hx⟩, rfl⟩
710 letI : L.Normal := by
711 dsimp [L]
712 exact Subgroup.Normal.map H.normal (QuotientGroup.mk' (U : Subgroup G))
713 (QuotientGroup.mk'_surjective (U : Subgroup G))
714 have hKmem :
715 ∀ {x : H.toSubgroup}, x.1 ∈ K.toSubgroup ↔ x.1 ∈ (U : Subgroup G) := by
716 intro x
717 constructor
718 · intro hxK
719 have hxall :
720 ∀ a : Set.Iio (succ lam),
721 x.1 ∈ (Wμ ⟨a.1, lt_of_lt_of_le a.2 hsuccle⟩ : Subgroup G) := by
722 simpa [K, seriesData, seriesSub, hsuccle, Subgroup.mem_iInf] using hxK
723 simpa [U] using hxall ⟨lam, show lam ∈ Set.Iio (succ lam) from lt_succ lam⟩
724 · intro hxU
725 have hxH : x.1 ∈ H.toSubgroup := x.2
726 have hxHall :
727 ∀ a : Set.Iio lam,
728 x.1 ∈ (Wμ ⟨a.1, lt_of_lt_of_le a.2 hlamle⟩ : Subgroup G) := by
729 simpa [H, seriesData, seriesSub, hlamle, Subgroup.mem_iInf] using hxH
730 have hxKall :
731 ∀ a : Set.Iio (succ lam),
732 x.1 ∈ (Wμ ⟨a.1, lt_of_lt_of_le a.2 hsuccle⟩ : Subgroup G) := by
733 intro a
734 rcases eq_or_lt_of_le (lt_succ_iff.mp (show a.1 < succ lam from a.2)) with haEq | ha
735 · simpa [U, haEq] using hxU
736 · exact hxHall ⟨a.1, show a.1 ∈ Set.Iio lam from ha⟩
737 simpa [K, seriesData, seriesSub, hsuccle, Subgroup.mem_iInf] using hxKall
738 have hKerEq : K.toSubgroup.subgroupOf H.toSubgroup = φ.ker := by
739 ext x
740 constructor
741 · intro hx
742 have hxU : x.1 ∈ (U : Subgroup G) := by
743 exact hKmem.1 (by simpa [Subgroup.mem_subgroupOf] using hx)
744 simpa [MonoidHom.mem_ker, φ] using
745 (QuotientGroup.eq_one_iff (N := (U : Subgroup G)) x.1).2 hxU
746 · intro hx
747 have hxU : x.1 ∈ (U : Subgroup G) := by
748 exact (QuotientGroup.eq_one_iff (N := (U : Subgroup G)) x.1).1
749 (by simpa [MonoidHom.mem_ker, φ] using hx)
750 have hxK : x.1 ∈ K.toSubgroup := hKmem.2 hxU
751 simpa [Subgroup.mem_subgroupOf] using hxK
752 have hL : C L := hNorm L (hWμC ⟨lam, hlam⟩)
753 have hStep : C (H.toSubgroup ⧸ K.toSubgroup.subgroupOf H.toSubgroup) := by
754 let e₁ : H.toSubgroup ⧸ K.toSubgroup.subgroupOf H.toSubgroup ≃* H.toSubgroup ⧸ φ.ker :=
755 QuotientGroup.quotientMulEquivOfEq hKerEq
756 exact hIso
757 ⟨(MulEquiv.subgroupCongr hRangeEq).symm.trans
758 (e₁.trans (QuotientGroup.quotientKerEquivRange φ)).symm⟩
759 hL
760 simpa [ClosedNormalSubgroupData.stepQuotient, H, K] using hStep
761 · intro lam hlam hLimit
762 ext x
763 constructor
764 · intro hx
765 have hxall :
766 ∀ a : Set.Iio lam, x ∈ (Wμ ⟨a.1, lt_of_lt_of_le a.2 hlam⟩ : Subgroup G) := by
767 simpa [seriesData, seriesSub, hlam, Subgroup.mem_iInf] using hx
768 have hxseries : ∀ ν : Set.Iio lam, x ∈ (seriesData ν.1).toSubgroup := by
769 intro ν
770 have hνμ : ν.1 ≤ μ := ν.2.le.trans hlam
771 have hrestrict :
772 ∀ a : Set.Iio ν.1,
773 x ∈ (Wμ ⟨a.1, lt_of_lt_of_le a.2 hνμ⟩ : Subgroup G) := by
774 intro a
775 exact hxall ⟨a.1, show a.1 < lam from lt_of_lt_of_le a.2 ν.2.le⟩
776 simpa [seriesData, seriesSub, hνμ, Subgroup.mem_iInf] using hrestrict
777 simpa [Subgroup.mem_iInf] using hxseries
778 · intro hx
779 have hxseries : ∀ ν : Set.Iio lam, x ∈ (seriesData ν.1).toSubgroup := by
780 simpa [Subgroup.mem_iInf] using hx
781 have hxall :
782 ∀ a : Set.Iio lam, x ∈ (Wμ ⟨a.1, lt_of_lt_of_le a.2 hlam⟩ : Subgroup G) := by
783 intro a
784 have hs : succ a.1 < lam := hLimit.succ_lt a.2
785 have hsμ : succ a.1 ≤ μ := hs.le.trans hlam
786 have hxin : x ∈ (seriesData (succ a.1)).toSubgroup := hxseries ⟨succ a.1, hs⟩
787 have hxsucc :
788 ∀ b : Set.Iio (succ a.1),
789 x ∈ (Wμ ⟨b.1, lt_of_lt_of_le b.2 hsμ⟩ : Subgroup G) := by
790 simpa [seriesData, seriesSub, hsμ, Subgroup.mem_iInf] using hxin
791 simpa using hxsucc ⟨a.1, show a.1 ∈ Set.Iio (succ a.1) from lt_succ a.1⟩
792 simpa [seriesData, seriesSub, hlam, Subgroup.mem_iInf] using hxall
794/-- Transfinite-series bound for local weight, proved by induction on the series index. -/
796 (C : FiniteGroupClass.{u}) (G : Type u)
797 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
798 (μ : Ordinal)
800 localWeight G ≤ μ.card := by
801 exact S.localWeight_le_cardinal'
803/-- External choice data for a transfinite series with small quotient local weights. -/
805 (C : FiniteGroupClass.{u}) (G : Type u)
806 [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Infinite G] : Prop where
807 exists_series :
808 FiniteGroupClass.Formation C →
809 FiniteGroupClass.NormalSubgroupClosed C →
810 IsProCGroup C G →
811 ∃ μ : Ordinal, ∃ S : TransfiniteClosedNormalSeries C G μ,
812 ∀ lam : Ordinal, lam < μ →
813 quotientLocalWeight (G := G) (S.series lam).toSubgroup < localWeight G
815/-- Build a transfinite closed-normal series whose proper stages have smaller quotient local
816weight. -/
818 (C : FiniteGroupClass.{u}) (G : Type u)
819 [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Infinite G]
821 (hForm : FiniteGroupClass.Formation C)
822 (hNorm : FiniteGroupClass.NormalSubgroupClosed C) (hG : IsProCGroup C G) :
823 ∃ μ : Ordinal, ∃ S : TransfiniteClosedNormalSeries C G μ,
824 ∀ lam : Ordinal, lam < μ →
825 quotientLocalWeight (G := G) (S.series lam).toSubgroup < localWeight G := by
826 exact D.exists_series hForm hNorm hG
830/-- Local weight is bounded by `μ.card` exactly when there exists a transfinite closed normal
831series of length `μ`. -/
833 (C : FiniteGroupClass.{u}) {G : Type u}
834 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
835 {μ : Ordinal} :
836 FiniteGroupClass.Formation C →
837 FiniteGroupClass.NormalSubgroupClosed C →
838 IsProCGroup C G →
839 (localWeight G ≤ μ.card ↔ Nonempty (TransfiniteClosedNormalSeries C G μ)) := by
840 intro hForm hNorm hG
841 constructor
842 · intro hμ
844 (C := C) (G := G) μ hForm hNorm hG hμ
845 · intro hS
847 (C := C) (G := G) μ hS.some
849/-- There exists a transfinite closed normal series whose successive ambient quotient local
850weights are strictly smaller than the original local weight. -/
852 (C : FiniteGroupClass.{u}) (G : Type u)
853 [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Infinite G] :
855 FiniteGroupClass.Formation C →
856 FiniteGroupClass.NormalSubgroupClosed C →
857 IsProCGroup C G →
858 ∃ μ : Ordinal.{u}, ∃ S : TransfiniteClosedNormalSeries C G μ,
859 ∀ lam : Ordinal.{u}, lam < μ →
860 quotientLocalWeight (G := G) (S.series lam).toSubgroup < localWeight G := by
861 intro D hForm hNorm hG
863 (C := C) (G := G) D hForm hNorm hG
867/-- External construction data for the relative transfinite-series refinement in §6.5. -/
869 (C : FiniteGroupClass.{u}) (G : Type u)
870 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
871 (H : ClosedNormalSubgroupData G) : Prop where
872 exists_series :
873 FiniteGroupClass.Formation C →
874 FiniteGroupClass.NormalSubgroupClosed C →
875 IsProCGroup C G →
876 ∃ μ : Ordinal, ∃ S : RelativeTransfiniteClosedNormalSeries C G H μ,
877 ((Finite ↥H.toSubgroup → μ.card < ℵ₀) ∧
878 (Infinite ↥H.toSubgroup → μ.card = localWeight ↥H.toSubgroup)) ∧
879 (∀ lam : Ordinal, lam < μ →
880 (S.series (succ lam)).toSubgroup = (S.series lam).toSubgroup ∨
881 IsMaximalClosedNormalStep C G (S.series lam) (S.series (succ lam))) ∧
882 ((Infinite ↥H.toSubgroup ∨ Infinite (G ⧸ H.toSubgroup)) →
884 localWeight ↥H.toSubgroup + quotientLocalWeight (G := G) H.toSubgroup) ∧
886 H.toSubgroup ≤ M.toSubgroup →
887 Infinite ↥H.toSubgroup →
888 quotientLocalWeight (G := ↥M.toSubgroup)
889 (H.toSubgroup.subgroupOf M.toSubgroup) < localWeight G →
890 ∀ lam : Ordinal, lam < μ →
891 quotientLocalWeight (G := ↥M.toSubgroup)
892 ((S.series lam).toSubgroup.subgroupOf M.toSubgroup) < localWeight G)
894/-- 6.5. Relative transfinite-series refinement inside a closed normal subgroup.
895-/
897 (C : FiniteGroupClass.{u}) (G : Type u)
898 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
901 (hForm : FiniteGroupClass.Formation C)
902 (hNorm : FiniteGroupClass.NormalSubgroupClosed C) (hG : IsProCGroup C G) :
903 ∃ μ : Ordinal, ∃ S : RelativeTransfiniteClosedNormalSeries C G H μ,
904 ((Finite ↥H.toSubgroup → μ.card < ℵ₀) ∧
905 (Infinite ↥H.toSubgroup → μ.card = localWeight ↥H.toSubgroup)) ∧
906 (∀ lam : Ordinal, lam < μ →
907 (S.series (succ lam)).toSubgroup = (S.series lam).toSubgroup ∨
908 IsMaximalClosedNormalStep C G (S.series lam) (S.series (succ lam))) ∧
909 ((Infinite ↥H.toSubgroup ∨ Infinite (G ⧸ H.toSubgroup)) →
911 localWeight ↥H.toSubgroup + quotientLocalWeight (G := G) H.toSubgroup) ∧
913 H.toSubgroup ≤ M.toSubgroup →
914 Infinite ↥H.toSubgroup →
915 quotientLocalWeight (G := ↥M.toSubgroup)
916 (H.toSubgroup.subgroupOf M.toSubgroup) < localWeight G →
917 ∀ lam : Ordinal, lam < μ →
918 quotientLocalWeight (G := ↥M.toSubgroup)
919 ((S.series lam).toSubgroup.subgroupOf M.toSubgroup) < localWeight G) := by
920 exact D.exists_series hForm hNorm hG
928/-- A closed normal subgroup admits a relative transfinite closed normal series with the expected
929cardinality and quotient-local-weight control. -/
931 (C : FiniteGroupClass.{u}) (G : Type u)
932 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
935 FiniteGroupClass.Formation C →
936 FiniteGroupClass.NormalSubgroupClosed C →
937 IsProCGroup C G →
938 ∃ μ : Ordinal.{u}, ∃ S : RelativeTransfiniteClosedNormalSeries C G H μ,
939 ((Finite ↥H.toSubgroup → μ.card < ℵ₀) ∧
940 (Infinite ↥H.toSubgroup → μ.card = localWeight ↥H.toSubgroup)) ∧
941 (∀ lam : Ordinal.{u}, lam < μ →
942 (S.series (succ lam)).toSubgroup = (S.series lam).toSubgroup ∨
943 IsMaximalClosedNormalStep C G (S.series lam) (S.series (succ lam))) ∧
944 ((Infinite ↥H.toSubgroup ∨ Infinite (G ⧸ H.toSubgroup)) →
946 localWeight ↥H.toSubgroup + quotientLocalWeight (G := G) H.toSubgroup) ∧
948 H.toSubgroup ≤ M.toSubgroup →
949 Infinite ↥H.toSubgroup →
950 quotientLocalWeight (G := ↥M.toSubgroup)
951 (H.toSubgroup.subgroupOf M.toSubgroup) < localWeight G →
952 ∀ lam : Ordinal.{u}, lam < μ →
953 quotientLocalWeight (G := ↥M.toSubgroup)
954 ((S.series lam).toSubgroup.subgroupOf M.toSubgroup) < localWeight G) := by
955 intro D hForm hNorm hG
957 (C := C) (G := G) H D hForm hNorm hG
961end LocalWeight