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

Source: ProCGroups.LocalWeight.ClosedNormalDataAndTransfiniteSeries

1import ProCGroups.Generation.WordProductsAndClosure
2import ProCGroups.LocalWeight.MetrizabilityAndQuotients
4/-!
5# Closed normal chains and local weight
7This file constructs ordinal-indexed descending chains of closed normal
8subgroups from local-weight bounds. Successive quotients lie in a prescribed
9finite-group class, and the resulting series recovers the corresponding
10cardinal bound without external assumption packages.
11-/
13open Set
14open TopologicalSpace
15open Order
16open scoped Cardinal
17open scoped Topology Pointwise
19namespace ProCGroups.LocalWeight
21universe u
23open ProCGroups.ProC ProCGroups.Generation
24open ProCGroups.FiniteGeneration
27section ClosedNormalSeriesStatements
30section ClosedNormalData
32variable (G : Type u) [Group G] [TopologicalSpace G]
34/-- A closed subgroup equipped with normality, for quotient constructions. -/
35structure ClosedNormalSubgroupData extends ClosedSubgroup G where
36 /-- The underlying closed subgroup is normal. -/
37 normal' : toSubgroup.Normal
39/-- Closed-normal-subgroup data coerces to its underlying closed subgroup. -/
40instance instCoeClosedNormalSubgroupData : Coe (ClosedNormalSubgroupData G) (Subgroup G) where
41 coe H := H.toSubgroup
43/-- The closed-normal-subgroup datum constructed by mk has the stated underlying subgroup. -/
44@[simp 900] theorem ClosedNormalSubgroupData.coe_mk
45 (H : Subgroup G) (hHclosed : IsClosed (H : Set G)) (hHnormal : H.Normal) :
46 ((⟨⟨H, hHclosed⟩, hHnormal⟩ : ClosedNormalSubgroupData G) : Subgroup G) = H :=
47 rfl
49/-- The closed-normal-subgroup data define a normal subgroup. -/
50instance ClosedNormalSubgroupData.instNormal
51 (H : ClosedNormalSubgroupData G) : H.toSubgroup.Normal :=
52 H.normal'
54/-- The subgroup packaged in closed-normal subgroup data is closed. -/
55@[simp 900] theorem ClosedNormalSubgroupData.isClosed
56 (H : ClosedNormalSubgroupData G) : IsClosed ((H : Subgroup G) : Set G) :=
57 H.isClosed'
59/-- The step quotient \(H/K\) for closed-normal subgroup chains. -/
60abbrev ClosedNormalSubgroupData.stepQuotient
61 (H K : ClosedNormalSubgroupData G) : Type u :=
62 H.toSubgroup ⧸ (K.toSubgroup.subgroupOf H.toSubgroup)
64end ClosedNormalData
66section TransfiniteSeries
68variable (C : FiniteGroupClass.{u})
69variable (G : Type u) [Group G] [TopologicalSpace G]
71/-- Transfinite closed normal series with finite-class step quotients. -/
72structure TransfiniteClosedNormalSeries
73 (C : FiniteGroupClass.{u}) (G : Type u) [Group G] [TopologicalSpace G]
74 [IsTopologicalGroup G] (μ : Ordinal) where
75 /-- The closed normal subgroup at each ordinal stage. -/
76 series : Ordinal → ClosedNormalSubgroupData G
77 /-- The series starts at the whole group. -/
78 top_eq : (series 0).toSubgroup = ⊤
79 /-- The series reaches the trivial subgroup at stage \(\mu\). -/
80 bot_eq : (series μ).toSubgroup = ⊥
81 /-- The series is antitone up to its terminal stage \(\mu\). -/
82 antitone' : ∀ ⦃lam ν : Ordinal⦄, lam ≤ ν → ν ≤ μ →
83 (series ν).toSubgroup ≤ (series lam).toSubgroup
84 /-- Every successor-step quotient before \(\mu\) belongs to the finite-group class \(C\). -/
85 step_mem' : ∀ ⦃lam : Ordinal⦄, lam < μ →
86 C (ClosedNormalSubgroupData.stepQuotient (G := G) (series lam) (series (succ lam)))
87 /-- At a nonzero limit stage, the series is the intersection of all preceding stages. -/
88 limit_eq_iInf' : ∀ ⦃lam : Ordinal⦄, lam ≤ μ → IsSuccLimit lam →
89 (series lam).toSubgroup =
90 iInf (fun ν : {ν : Ordinal // ν < lam} => (series ν.1).toSubgroup)
92end TransfiniteSeries
96end ClosedNormalSeriesStatements
99/--
100Successor-step lemma for transfinite closed-normal chains: a closed normal finite-index subgroup
101of a closed subgroup is obtained by intersecting that subgroup with an open normal subgroup of
102the ambient profinite group. The subgroup \(H\) is assumed closed in \(G\), and \(K\) is assumed
103closed and normal in \(G\).
104-/
105theorem closed_normal_subgroup_eq_inter_openNormal_of_finite_index
106 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
107 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
108 (H K : Subgroup G)
109 (hKclosed : IsClosed (K : Set G)) [K.Normal] (hKH : K ≤ H)
110 [Finite (H ⧸ K.subgroupOf H)] :
111 ∃ V : OpenNormalSubgroup G, K = H ⊓ (V : Subgroup G) := by
112 classical
113 letI : IsClosed (K : Set G) := hKclosed
114 letI : TotallyDisconnectedSpace (G ⧸ K) :=
116 let ψ : H →* G ⧸ K := (QuotientGroup.mk' K).comp H.subtype
117 have hKerEq : (K.subgroupOf H) = ψ.ker := by
118 ext x
119 constructor
120 · intro hx
121 simpa [MonoidHom.mem_ker, ψ] using
122 (QuotientGroup.eq_one_iff (N := K) x.1).2 hx
123 · intro hx
124 exact (QuotientGroup.eq_one_iff (N := K) x.1).1
125 (by simpa [MonoidHom.mem_ker, ψ] using hx)
126 let e₁ : H ⧸ (K.subgroupOf H) ≃* H ⧸ ψ.ker :=
127 QuotientGroup.quotientMulEquivOfEq hKerEq
128 letI : Finite (H ⧸ ψ.ker) := Finite.of_injective e₁.symm e₁.symm.injective
129 let e₂ : H ⧸ ψ.ker ≃* ψ.range := QuotientGroup.quotientKerEquivRange ψ
130 letI : Finite ψ.range := Finite.of_injective e₂.symm e₂.symm.injective
131 obtain ⟨W, hWbot⟩ :=
132 exists_openNormalSubgroup_inf_eq_bot_of_finite (G := G ⧸ K) ψ.range
133 let V : OpenNormalSubgroup G :=
134 OpenNormalSubgroup.comap (QuotientGroup.mk' K) QuotientGroup.continuous_mk W
135 refine ⟨V, ?_⟩
136 ext x
137 constructor
138 · intro hxK
139 refine ⟨hKH hxK, ?_⟩
140 change QuotientGroup.mk' K x ∈ W
141 have hmk : QuotientGroup.mk' K x = 1 :=
142 (QuotientGroup.eq_one_iff (N := K) x).2 hxK
143 rw [hmk]
144 exact W.one_mem
145 · intro hx
146 have hxW : QuotientGroup.mk' K x ∈ W := by
147 have hxV := hx.2
148 change QuotientGroup.mk' K x ∈ W.toOpenSubgroup at hxV
149 exact hxV
150 have hxRange : QuotientGroup.mk' K x ∈ ψ.range := by
151 exact ⟨⟨x, hx.1⟩, rfl⟩
152 have hxBot : QuotientGroup.mk' K x ∈ (⊥ : Subgroup (G ⧸ K)) := by
153 have hxInf : QuotientGroup.mk' K x ∈ ((W : Subgroup (G ⧸ K)) ⊓ ψ.range) :=
154 ⟨hxW, hxRange⟩
155 simpa [hWbot] using hxInf
156 have hxOne : QuotientGroup.mk' K x = 1 := by
157 simpa using hxBot
158 exact (QuotientGroup.eq_one_iff (N := K) x).1 hxOne
160/--
161If a quotient carries a neighborhood basis indexed by a family of open normal subgroups, then
162its local weight is bounded by the cardinality of that family.
163-/
164theorem localWeight_le_of_openNormal_family
165 (G : Type u) [Group G] [TopologicalSpace G]
166 {ι : Type u} {κ : Cardinal.{u}} (W : ι → OpenNormalSubgroup G)
167 (hWbasis : IsNeighborhoodBasisAt (X := G) (1 : G)
168 (Set.range fun i : ι => (((W i : Subgroup G) : Set G))))
169 (hWcard : Cardinal.mk ι ≤ κ) : localWeight G ≤ κ := by
170 classical
171 let f : ι → Set G := fun i => (((W i : Subgroup G) : Set G))
172 let chooseIdx : { V : Set G // V ∈ Set.range f } → ι :=
173 fun V => Classical.choose V.2
174 have hchoose : ∀ V : { V : Set G // V ∈ Set.range f }, f (chooseIdx V) = V.1 := by
175 intro V
176 exact Classical.choose_spec V.2
177 have hchoose_inj : Function.Injective chooseIdx := by
178 intro V₁ V₂ hEq
179 apply Subtype.ext
180 calc
181 V₁.1 = f (chooseIdx V₁) := (hchoose V₁).symm
182 _ = f (chooseIdx V₂) := by simp only [hEq]
183 _ = V₂.1 := hchoose V₂
184 simpa [localWeight] using
185 calc
186 localWeightAt (X := G) (1 : G) ≤ familyCardinal (X := G) (Set.range f) :=
187 localWeightAt_le_familyCardinal_of_basis (X := G) (x := (1 : G)) hWbasis
188 _ ≤ Cardinal.mk ι := by
189 unfold familyCardinal
190 exact Cardinal.mk_le_of_injective (f := chooseIdx) hchoose_inj
191 _ ≤ κ := hWcard
193/-- 6.5(d). Weight splitting formula over a closed normal subgroup. -/
194theorem localWeight_split_over_closedNormalSubgroup
195 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
196 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
197 (H : ClosedNormalSubgroupData G)
198 (hInf : Infinite ↥H.toSubgroup ∨ Infinite (G ⧸ H.toSubgroup)) :
199 localWeight G =
200 localWeight ↥H.toSubgroup + quotientLocalWeight (G := G) H.toSubgroup := by
201 classical
202 letI : CompactSpace ↥H.toSubgroup := by
203 simpa using H.isClosed.isClosedEmbedding_subtypeVal.compactSpace
204 letI : T2Space ↥H.toSubgroup := inferInstance
205 letI : TotallyDisconnectedSpace ↥H.toSubgroup := inferInstance
206 letI : IsClosed (H.toSubgroup : Set G) := H.isClosed
207 letI : TotallyDisconnectedSpace (G ⧸ H.toSubgroup) :=
209 rcases exists_openNormalNeighborhoodBasisAtOne_cardinal_le_localWeight
210 (G := G) with ⟨ιG, WG, hWGbasis, hWGcard⟩
211 have hHle : localWeight ↥H.toSubgroup ≤ localWeight G := by
212 let WH : ιG → OpenNormalSubgroup ↥H.toSubgroup := fun i =>
213 OpenNormalSubgroup.comap H.toSubgroup.subtype continuous_subtype_val (WG i)
214 have hWHbasis :
215 IsNeighborhoodBasisAt (X := ↥H.toSubgroup) (1 : ↥H.toSubgroup)
216 (Set.range fun i : ιG => (((WH i : Subgroup ↥H.toSubgroup) : Set ↥H.toSubgroup))) := by
217 refine ⟨?_, ?_⟩
218 · intro U hU
219 rcases hU with ⟨i, rfl⟩
220 constructor
221 · change IsOpen (((↑) : H.toSubgroup → G) ⁻¹' (((WG i : Subgroup G) : Set G)))
222 simpa using
223 (openNormalSubgroup_isOpen (G := G) (WG i)).preimage continuous_subtype_val
224 · simp only [OpenNormalSubgroup.toSubgroup_comap, Subgroup.comap_subtype,
225 SetLike.mem_coe, one_mem, WH]
226 · intro U hUopen hUone
227 rcases isOpen_induced_iff.mp hUopen with ⟨O, hOopen, hOeq⟩
228 have hOone : (1 : G) ∈ O := by
229 have : (1 : ↥H.toSubgroup) ∈ Subtype.val ⁻¹' O := by
230 simpa [hOeq] using hUone
231 simpa using this
232 rcases hWGbasis.2 O hOopen hOone with ⟨V, hVrange, hVsub⟩
233 rcases hVrange with ⟨i, rfl⟩
234 refine ⟨_, ⟨i, rfl⟩, ?_⟩
235 intro x hx
236 have hxO : (x : G) ∈ O := hVsub hx
237 rw [← hOeq]
238 exact hxO
239 exact localWeight_le_of_openNormal_family
240 (G := ↥H.toSubgroup) WH hWHbasis hWGcard
241 have hQle : quotientLocalWeight (G := G) H.toSubgroup ≤ localWeight G := by
242 let q : G →* G ⧸ H.toSubgroup := QuotientGroup.mk' H.toSubgroup
243 let BQ : Set (Set (G ⧸ H.toSubgroup)) :=
244 Set.range fun i : ιG => q '' (((WG i : Subgroup G) : Set G))
245 have hBQbasis :
246 IsNeighborhoodBasisAt (X := G ⧸ H.toSubgroup) (1 : G ⧸ H.toSubgroup) BQ := by
247 refine ⟨?_, ?_⟩
248 · intro U hU
249 rcases hU with ⟨i, rfl⟩
250 constructor
251 · exact (QuotientGroup.isOpenMap_coe (N := H.toSubgroup)) _
252 (openNormalSubgroup_isOpen (G := G) (WG i))
253 · refine ⟨1, ?_, ?_⟩
254 · exact (WG i).one_mem'
255 · simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_one, q]
256 · intro U hUopen hUone
257 have hpreOpen : IsOpen (q ⁻¹' U) := hUopen.preimage QuotientGroup.continuous_mk
258 have hpreOne : (1 : G) ∈ q ⁻¹' U := by
259 simpa [q] using hUone
260 rcases hWGbasis.2 (q ⁻¹' U) hpreOpen hpreOne with ⟨V, hVrange, hVsub⟩
261 rcases hVrange with ⟨i, rfl⟩
262 refine ⟨q '' (((WG i : Subgroup G) : Set G)), ⟨i, rfl⟩, ?_⟩
263 rintro _ ⟨g, hg, rfl⟩
264 exact hVsub hg
265 let chooseIdx : { U : Set (G ⧸ H.toSubgroup) // U ∈ BQ } → ιG :=
266 fun U => Classical.choose U.2
267 have hchoose :
268 ∀ U : { U : Set (G ⧸ H.toSubgroup) // U ∈ BQ },
269 q '' (((WG (chooseIdx U) : Subgroup G) : Set G)) = U.1 := by
270 intro U
271 exact Classical.choose_spec U.2
272 have hchoose_inj : Function.Injective chooseIdx := by
273 intro U₁ U₂ hEq
274 apply Subtype.ext
275 calc
276 U₁.1 = q '' (((WG (chooseIdx U₁) : Subgroup G) : Set G)) := (hchoose U₁).symm
277 _ = q '' (((WG (chooseIdx U₂) : Subgroup G) : Set G)) := by simp only [hEq,
278 OpenSubgroup.coe_toSubgroup]
279 _ = U₂.1 := hchoose U₂
280 have hBQcard : familyCardinal (X := G ⧸ H.toSubgroup) BQ ≤ Cardinal.mk ιG := by
281 unfold familyCardinal
282 exact Cardinal.mk_le_of_injective (f := chooseIdx) hchoose_inj
283 simpa [localWeight, quotientLocalWeight] using
284 (localWeightAt_le_familyCardinal_of_basis
285 (X := G ⧸ H.toSubgroup) (x := (1 : G ⧸ H.toSubgroup)) hBQbasis).trans
286 (hBQcard.trans hWGcard)
287 rcases exists_openNormalNeighborhoodBasisAtOne_cardinal_le_localWeight
288 (G := ↥H.toSubgroup) with ⟨ιH, KH, hKHbasis, hKHcard⟩
289 rcases exists_openNormalNeighborhoodBasisAtOne_cardinal_le_localWeight
290 (G := G ⧸ H.toSubgroup) with ⟨ιQ, QH, hQHbasis, hQHcard0⟩
291 have hQHcard : Cardinal.mk ιQ ≤ quotientLocalWeight (G := G) H.toSubgroup := by
292 simpa [quotientLocalWeight_eq_localWeight] using hQHcard0
293 have hιHne : Nonempty ιH := by
294 rcases hKHbasis.2 Set.univ isOpen_univ (by simp only [mem_univ]) with ⟨U, hUrange, _⟩
295 rcases hUrange with ⟨i, rfl⟩
296 exact ⟨i⟩
297 have hιQne : Nonempty ιQ := by
298 rcases hQHbasis.2 Set.univ isOpen_univ (by simp only [mem_univ]) with ⟨U, hUrange, _⟩
299 rcases hUrange with ⟨i, rfl⟩
300 exact ⟨i⟩
301 have hAmbientData :
302 ∀ i : ιH, ∃ O V : Set G,
303 IsOpen O ∧
304 (((↑) : H.toSubgroup → G) ⁻¹' O) = (((KH i : Subgroup ↥H.toSubgroup) : Set ↥H.toSubgroup)) ∧
305 IsOpen V ∧ (1 : G) ∈ V ∧
306 ∀ {a b : G}, a ∈ V → b ∈ V → a⁻¹ * b ∈ O := by
307 intro i
308 rcases isOpen_induced_iff.mp (openNormalSubgroup_isOpen (G := ↥H.toSubgroup) (KH i)) with
309 ⟨O, hOopen, hOeq⟩
310 have hOone : (1 : G) ∈ O := by
311 have : (1 : ↥H.toSubgroup) ∈ Subtype.val ⁻¹' O := by
312 rw [hOeq]
313 exact (KH i).one_mem'
314 exact this
315 have hOmem : O ∈ 𝓝 (1 : G) := hOopen.mem_nhds hOone
316 have hcont :
317 Continuous fun p : G × G => p.1⁻¹ * p.2 :=
318 (continuous_inv.comp continuous_fst).mul continuous_snd
319 have hmem :
320 {p : G × G | p.1⁻¹ * p.2 ∈ O} ∈ 𝓝 ((1 : G), (1 : G)) := by
321 exact hcont.continuousAt (by simpa using hOmem)
322 rcases mem_nhds_prod_iff.mp hmem with ⟨A, hA, B, hB, hAB⟩
323 rcases mem_nhds_iff.mp hA with ⟨A', hA'sub, hA'open, hA'one⟩
324 rcases mem_nhds_iff.mp hB with ⟨B', hB'sub, hB'open, hB'one⟩
325 refine ⟨O, A' ∩ B', hOopen, hOeq, hA'open.inter hB'open, ?_, ?_⟩
326 · exact ⟨hA'one, hB'one⟩
327 · intro a b ha hb
328 have haA : a ∈ A := hA'sub ha.1
329 have hbB : b ∈ B := hB'sub hb.2
330 exact hAB (show (a, b) ∈ A ×ˢ B from ⟨haA, hbB⟩)
331 choose OH VH hOHopen hOHeq hVHopen hVHone hVHdiff using hAmbientData
332 let q : G →* G ⧸ H.toSubgroup := QuotientGroup.mk' H.toSubgroup
333 let PH : ιQ → OpenNormalSubgroup G := fun j =>
334 OpenNormalSubgroup.comap q QuotientGroup.continuous_mk (QH j)
335 let B : Set (Set G) :=
336 Set.range fun ij : ιH × ιQ => VH ij.1 ∩ (((PH ij.2 : Subgroup G) : Set G))
337 have hBbasis : IsNeighborhoodBasisAt (X := G) (1 : G) B := by
338 refine ⟨?_, ?_⟩
339 · intro U hU
340 rcases hU with ⟨⟨i, j⟩, rfl⟩
341 constructor
342 · exact (hVHopen i).inter (openNormalSubgroup_isOpen (G := G) (PH j))
343 · exact ⟨hVHone i, by simp only [OpenNormalSubgroup.toSubgroup_comap, Subgroup.coe_comap,
344 QuotientGroup.coe_mk',
345 OpenSubgroup.coe_toSubgroup, mem_preimage, QuotientGroup.mk_one, SetLike.mem_coe, one_mem, PH, q]⟩
346 · intro U hUopen hUone
347 rcases hWGbasis.2 U hUopen hUone with ⟨Nset, hNrange, hNsubU⟩
348 rcases hNrange with ⟨n, rfl⟩
349 have hHNopen :
350 IsOpen (((↑) : H.toSubgroup → G) ⁻¹' (((WG n : Subgroup G) : Set G))) := by
351 simpa using (openNormalSubgroup_isOpen (G := G) (WG n)).preimage continuous_subtype_val
352 have hHNone :
353 (1 : H.toSubgroup) ∈
354 ((↑) : H.toSubgroup → G) ⁻¹' (((WG n : Subgroup G) : Set G)) := by
355 simp only [OpenSubgroup.coe_toSubgroup, mem_preimage, OneMemClass.coe_one,
356 SetLike.mem_coe, one_mem]
357 rcases hKHbasis.2
358 (((↑) : H.toSubgroup → G) ⁻¹' (((WG n : Subgroup G) : Set G)))
359 hHNopen hHNone with ⟨Kset, hKrange, hKsub⟩
360 rcases hKrange with ⟨i, rfl⟩
361 have hImageOpen :
362 IsOpen (((↑) : G → G ⧸ H.toSubgroup) '' ((((WG n : Subgroup G) : Set G) ∩ VH i))) := by
363 exact (QuotientGroup.isOpenMap_coe (N := H.toSubgroup)) _
364 ((openNormalSubgroup_isOpen (G := G) (WG n)).inter (hVHopen i))
365 have hImageOne :
366 (1 : G ⧸ H.toSubgroup) ∈
367 ((↑) : G → G ⧸ H.toSubgroup) '' ((((WG n : Subgroup G) : Set G) ∩ VH i)) := by
368 refine ⟨1, ?_, by simp only [QuotientGroup.mk_one]⟩
369 exact ⟨(WG n).one_mem', hVHone i⟩
370 rcases hQHbasis.2
371 (((↑) : G → G ⧸ H.toSubgroup) '' ((((WG n : Subgroup G) : Set G) ∩ VH i)))
372 hImageOpen hImageOne with ⟨Qset, hQrange, hQsub⟩
373 rcases hQrange with ⟨j, rfl⟩
374 refine ⟨VH i ∩ (((PH j : Subgroup G) : Set G)), ⟨(i, j), rfl⟩, ?_⟩
375 intro x hx
376 have hxV : x ∈ VH i := hx.1
377 have hxQ : q x ∈ ((QH j : Subgroup (G ⧸ H.toSubgroup)) : Set (G ⧸ H.toSubgroup)) := by
378 simpa [PH, OpenNormalSubgroup.mem_comap] using hx.2
379 rcases hQsub hxQ with ⟨y, hy, hyEq⟩
380 have hyN : y ∈ ((WG n : Subgroup G) : Set G) := hy.1
381 have hyV : y ∈ VH i := hy.2
382 have hyxH : y⁻¹ * x ∈ H.toSubgroup := by
383 exact (QuotientGroup.eq).1 (by simpa [q] using hyEq)
384 have hyxO : y⁻¹ * x ∈ OH i := hVHdiff i hyV hxV
385 have hyxK :
386 (⟨y⁻¹ * x, hyxH⟩ : H.toSubgroup) ∈
387 ((KH i : Subgroup ↥H.toSubgroup) : Set ↥H.toSubgroup) := by
388 rw [← hOHeq i]
389 exact hyxO
390 have hyxN : y⁻¹ * x ∈ ((WG n : Subgroup G) : Set G) := hKsub hyxK
391 have hxN : x ∈ ((WG n : Subgroup G) : Set G) := by
392 have hxeq : x = y * (y⁻¹ * x) := by simp only [mul_inv_cancel_left]
393 rw [hxeq]
394 exact (WG n).mul_mem hyN hyxN
395 exact hNsubU hxN
396 let chooseIdx : { U : Set G // U ∈ B } → ιH × ιQ :=
397 fun U => Classical.choose U.2
398 have hchoose :
399 ∀ U : { U : Set G // U ∈ B },
400 VH (chooseIdx U).1 ∩ (((PH (chooseIdx U).2 : Subgroup G) : Set G)) = U.1 := by
401 intro U
402 exact Classical.choose_spec U.2
403 have hchoose_inj : Function.Injective chooseIdx := by
404 intro U₁ U₂ hEq
405 apply Subtype.ext
406 calc
407 U₁.1 = VH (chooseIdx U₁).1 ∩ (((PH (chooseIdx U₁).2 : Subgroup G) : Set G)) :=
408 (hchoose U₁).symm
409 _ = VH (chooseIdx U₂).1 ∩ (((PH (chooseIdx U₂).2 : Subgroup G) : Set G)) := by
410 simp only [hEq, OpenSubgroup.coe_toSubgroup]
411 _ = U₂.1 := hchoose U₂
412 have hBcard :
413 familyCardinal (X := G) B ≤ Cardinal.mk (ιH × ιQ) := by
414 unfold familyCardinal
415 exact Cardinal.mk_le_of_injective (f := chooseIdx) hchoose_inj
416 have hProdLe :
417 Cardinal.mk (ιH × ιQ) ≤
418 localWeight ↥H.toSubgroup + quotientLocalWeight (G := G) H.toSubgroup := by
419 have hιHnz : Cardinal.mk ιH ≠ 0 :=
420 Cardinal.mk_ne_zero_iff.mpr hιHne
421 have hιQnz : Cardinal.mk ιQ ≠ 0 :=
422 Cardinal.mk_ne_zero_iff.mpr hιQne
423 cases hInf with
424 | inl hHinf =>
425 letI : Infinite ↥H.toSubgroup := hHinf
426 have hHaleph :
427 ℵ₀ ≤ localWeight ↥H.toSubgroup :=
428 aleph0_le_localWeight_of_infinite_profiniteGroup (G := ↥H.toSubgroup)
429 calc
430 Cardinal.mk (ιH × ιQ) = Cardinal.mk ιH * Cardinal.mk ιQ := by
431 rw [Cardinal.mk_prod]
432 simp only [Cardinal.lift_id]
433 _ ≤ localWeight ↥H.toSubgroup * Cardinal.mk ιQ := by
434 exact mul_le_mul' hKHcard le_rfl
435 _ = max (localWeight ↥H.toSubgroup) (Cardinal.mk ιQ) := by
436 exact Cardinal.mul_eq_max_of_aleph0_le_left hHaleph hιQnz
437 _ ≤ max (localWeight ↥H.toSubgroup) (quotientLocalWeight (G := G) H.toSubgroup) := by
438 exact max_le_max le_rfl hQHcard
439 _ = localWeight ↥H.toSubgroup + quotientLocalWeight (G := G) H.toSubgroup := by
440 symm
441 exact Cardinal.add_eq_max hHaleph
442 | inr hQinf =>
443 letI : Infinite (G ⧸ H.toSubgroup) := hQinf
444 have hQaleph :
445 ℵ₀ ≤ quotientLocalWeight (G := G) H.toSubgroup := by
446 simpa [quotientLocalWeight_eq_localWeight] using
447 aleph0_le_localWeight_of_infinite_profiniteGroup
448 (G := G ⧸ H.toSubgroup)
449 calc
450 Cardinal.mk (ιH × ιQ) = Cardinal.mk ιH * Cardinal.mk ιQ := by
451 rw [Cardinal.mk_prod]
452 simp only [Cardinal.lift_id]
453 _ ≤ Cardinal.mk ιH * quotientLocalWeight (G := G) H.toSubgroup := by
454 exact mul_le_mul' le_rfl hQHcard
455 _ = max (Cardinal.mk ιH) (quotientLocalWeight (G := G) H.toSubgroup) := by
456 exact Cardinal.mul_eq_max_of_aleph0_le_right hιHnz hQaleph
457 _ ≤ max (localWeight ↥H.toSubgroup) (quotientLocalWeight (G := G) H.toSubgroup) := by
458 exact max_le_max hKHcard le_rfl
459 _ = localWeight ↥H.toSubgroup + quotientLocalWeight (G := G) H.toSubgroup := by
460 symm
461 exact Cardinal.add_eq_max' hQaleph
462 have hUpper :
463 localWeight G ≤
464 localWeight ↥H.toSubgroup + quotientLocalWeight (G := G) H.toSubgroup := by
465 simpa [localWeight] using
466 (localWeightAt_le_familyCardinal_of_basis (X := G) (x := (1 : G)) hBbasis).trans
467 (hBcard.trans hProdLe)
468 have hLower :
469 localWeight ↥H.toSubgroup + quotientLocalWeight (G := G) H.toSubgroup ≤ localWeight G := by
470 cases hInf with
471 | inl hHinf =>
472 letI : Infinite ↥H.toSubgroup := hHinf
473 have hHaleph :
474 ℵ₀ ≤ localWeight ↥H.toSubgroup :=
475 aleph0_le_localWeight_of_infinite_profiniteGroup (G := ↥H.toSubgroup)
476 rw [Cardinal.add_eq_max hHaleph]
477 exact max_le_iff.mpr ⟨hHle, hQle⟩
478 | inr hQinf =>
479 letI : Infinite (G ⧸ H.toSubgroup) := hQinf
480 have hQaleph :
481 ℵ₀ ≤ quotientLocalWeight (G := G) H.toSubgroup := by
482 simpa [quotientLocalWeight_eq_localWeight] using
483 aleph0_le_localWeight_of_infinite_profiniteGroup
484 (G := G ⧸ H.toSubgroup)
485 rw [Cardinal.add_eq_max' hQaleph]
486 exact max_le_iff.mpr ⟨hHle, hQle⟩
487 exact le_antisymm hUpper hLower
489/-- Subadditivity of quotient local weight along a chain \(H \le K \le M\). -/
490theorem quotientLocalWeight_subadd_of_subgroup_chain
491 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
492 (H M K : ClosedNormalSubgroupData G)
493 (hHK : H.toSubgroup ≤ K.toSubgroup) :
494 quotientLocalWeight (G := ↥M.toSubgroup) (K.toSubgroup.subgroupOf M.toSubgroup) ≤
495 quotientLocalWeight (G := ↥M.toSubgroup) (H.toSubgroup.subgroupOf M.toSubgroup) +
496 quotientLocalWeight (G := ↥K.toSubgroup) (H.toSubgroup.subgroupOf K.toSubgroup) := by
497 let HM : Subgroup ↥M.toSubgroup := H.toSubgroup.subgroupOf M.toSubgroup
498 let KM : Subgroup ↥M.toSubgroup := K.toSubgroup.subgroupOf M.toSubgroup
499 have hHMK : HM ≤ KM := by
500 intro x hx
501 exact hHK hx
502 have hopen :
503 IsOpenMap (leftQuotientProjection HM KM hHMK : (↥M.toSubgroup ⧸ HM) → (↥M.toSubgroup ⧸ KM)) :=
504 by
505 intro U hU
506 have hpre :
507 IsOpen ((QuotientGroup.mk (s := HM)) ⁻¹' U) := by
508 exact ((QuotientGroup.isQuotientMap_mk HM).isOpen_preimage).2 hU
509 have himage :
510 leftQuotientProjection HM KM hHMK '' U =
511 (QuotientGroup.mk (s := KM)) '' ((QuotientGroup.mk (s := HM)) ⁻¹' U) := by
512 ext y
513 constructor
514 · rintro ⟨x, hxU, rfl⟩
515 revert hxU
516 refine Quotient.inductionOn x ?_
517 intro g hgU
518 refine ⟨g, hgU, ?_⟩
519 simp only [leftQuotientProjection_mk]
520 · rintro ⟨g, hgU, rfl⟩
521 refine ⟨QuotientGroup.mk (s := HM) g, hgU, ?_⟩
522 simp only [leftQuotientProjection_mk]
523 rw [himage]
524 exact (QuotientGroup.isOpenMap_coe (N := KM)) _ hpre
525 have hmon :
526 quotientLocalWeight (G := ↥M.toSubgroup) (K.toSubgroup.subgroupOf M.toSubgroup) ≤
527 quotientLocalWeight (G := ↥M.toSubgroup) (H.toSubgroup.subgroupOf M.toSubgroup) := by
528 have hle :=
529 localWeightAt_image_le_of_continuous_open
530 (X := (↥M.toSubgroup ⧸ HM)) (Y := (↥M.toSubgroup ⧸ KM))
531 (x := (1 : ↥M.toSubgroup ⧸ HM))
532 (f := leftQuotientProjection HM KM hHMK)
533 (continuous_leftQuotientProjection HM KM hHMK) hopen
534 have hmap_one :
535 leftQuotientProjection HM KM hHMK (1 : ↥M.toSubgroup ⧸ HM) = 1 := by
536 exact leftQuotientProjection_mk HM KM hHMK 1
537 rw [hmap_one] at hle
538 simpa [quotientLocalWeight, HM, KM] using hle
539 exact hmon.trans (self_le_add_right _ _)
541/--
542Forward direction: existence of a transfinite closed normal series from the local-weight bound.
543-/
544theorem build_transfiniteClosedNormalSeries_of_localWeight_le
545 (C : FiniteGroupClass.{u}) (G : Type u)
546 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
547 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
548 (μ : Ordinal) (hForm : FiniteGroupClass.Formation C)
549 (hNorm : FiniteGroupClass.NormalSubgroupClosed C) (hG : HasOpenNormalBasisInClass C G)
550 (hμ : localWeight G ≤ μ.card) :
551 Nonempty (TransfiniteClosedNormalSeries C G μ) := by
552 classical
553 let hIso : FiniteGroupClass.IsomClosed C :=
554 FiniteGroupClass.Formation.isomClosed (C := C) hForm
555 rcases exists_openNormalNeighborhoodBasisAtOne_inClass_cardinal_le_localWeight
556 (C := C) (G := G) hG with
557 ⟨ι, W, hWC, hWbasis, hWcard0⟩
558 have hιne : Nonempty ι := by
559 rcases hWbasis.2 Set.univ isOpen_univ (by simp only [mem_univ]) with ⟨U, hUrange, _⟩
560 rcases hUrange with ⟨i, rfl⟩
561 exact ⟨i⟩
562 letI : Nonempty ι := hιne
563 have hWcard : Cardinal.mk ι ≤ μ.card := hWcard0.trans hμ
564 have hEmb : Nonempty (ι ↪ Set.Iio μ) := by
565 have hWcardLift0 :
566 Cardinal.lift.{u + 1} (Cardinal.mk ι) ≤ Cardinal.lift.{u + 1} μ.card := by
567 exact (Cardinal.lift_le).2 hWcard
568 have hWcardLift :
569 Cardinal.lift.{u + 1} (Cardinal.mk ι) ≤ Cardinal.lift.{u} #(Set.Iio μ) := by
570 simpa [Cardinal.mk_Iio_ordinal, Cardinal.lift_lift] using hWcardLift0
571 exact Cardinal.lift_mk_le'.mp hWcardLift
572 let e : ι ↪ Set.Iio μ := Classical.choice hEmb
573 let σ : Set.Iio μ → ι := Function.invFun e
574 have hσ : ∀ i : ι, σ (e i) = i := by
575 intro i
576 exact Function.leftInverse_invFun e.injective i
577 let Wμ : Set.Iio μ → OpenNormalSubgroup G := fun a => W (σ a)
578 have hWμC : ∀ a : Set.Iio μ, C (G ⧸ (Wμ a : Subgroup G)) := by
579 intro a
580 exact hWC (σ a)
581 let B : Set (Set G) := Set.range fun i : ι => (((W i : Subgroup G) : Set G))
582 let Bμ : Set (Set G) := Set.range fun a : Set.Iio μ => (((Wμ a : Subgroup G) : Set G))
583 have hBμeq : Bμ = B := by
584 ext U
585 constructor
586 · rintro ⟨a, rfl⟩
587 exact ⟨σ a, rfl⟩
588 · rintro ⟨i, rfl⟩
589 exact ⟨e i, by simp only [hσ i, OpenSubgroup.coe_toSubgroup, Wμ]⟩
590 have hWμbasis : IsNeighborhoodBasisAt (X := G) (1 : G) Bμ := by
591 simpa [Bμ, B, hBμeq] using hWbasis
592 have hWμbot : iInf (fun a : Set.Iio μ => (Wμ a : Subgroup G)) = (⊥ : Subgroup G) := by
593 simpa [Bμ] using
594 iInf_eq_bot_of_openNormalNeighborhoodBasisAtOne (G := G) Wμ hWμbasis
595 let seriesSub : Ordinal → Subgroup G := fun lam =>
596 if hlam : lam ≤ μ then
597 iInf (fun a : Set.Iio lam => (Wμ ⟨a.1, lt_of_lt_of_le a.2 hlam⟩ : Subgroup G))
598 else ⊥
599 have hseriesClosed : ∀ lam : Ordinal, IsClosed (seriesSub lam : Set G) := by
600 intro lam
601 by_cases hlam : lam ≤ μ
602 · simpa [seriesSub, hlam] using
603 isClosed_iInter (fun a : Set.Iio lam =>
604 openNormalSubgroup_isClosed (G := G) (Wμ ⟨a.1, lt_of_lt_of_le a.2 hlam⟩))
605 · dsimp [seriesSub]
606 rw [dif_neg hlam]
607 simp only [Subgroup.coe_bot, finite_singleton, Finite.isClosed]
608 have hseriesNormal : ∀ lam : Ordinal, (seriesSub lam).Normal := by
609 intro lam
610 by_cases hlam : lam ≤ μ
611 · simpa [seriesSub, hlam] using
612 (show
613 (iInf (fun a : Set.Iio lam =>
614 (Wμ ⟨a.1, lt_of_lt_of_le a.2 hlam⟩ : Subgroup G))).Normal from
615 Subgroup.normal_iInf_normal fun a : Set.Iio lam =>
616 (show (Wμ ⟨a.1, lt_of_lt_of_le a.2 hlam⟩ : Subgroup G).Normal from inferInstance))
617 · simp [seriesSub, hlam]
618 let seriesData : Ordinal → ClosedNormalSubgroupData G := fun lam =>
619 { toSubgroup := seriesSub lam
620 isClosed' := hseriesClosed lam
621 normal' := hseriesNormal lam }
622 refine ⟨{
623 series := seriesData,
624 top_eq := ?_,
625 bot_eq := ?_,
626 antitone' := ?_,
627 step_mem' := ?_,
628 limit_eq_iInf' := ?_ }⟩
629 · ext x
630 simp only [zero_le, ↓reduceDIte, Subgroup.mem_iInf, OpenSubgroup.mem_toSubgroup,
631 IsEmpty.forall_iff,
632 Subgroup.mem_top, seriesSub, seriesData]
633 · simpa [seriesData, seriesSub] using hWμbot
634 · intro lam ν hlam hν x hx
635 have hlamμ : lam ≤ μ := hlam.trans hν
636 have hxall :
637 ∀ a : Set.Iio ν, x ∈ (Wμ ⟨a.1, lt_of_lt_of_le a.2 hν⟩ : Subgroup G) := by
638 simpa [seriesData, seriesSub, hν, Subgroup.mem_iInf] using hx
639 have hrestrict :
640 ∀ a : Set.Iio lam, x ∈ (Wμ ⟨a.1, lt_of_lt_of_le a.2 hlamμ⟩ : Subgroup G) := by
641 intro a
642 exact hxall ⟨a.1, lt_of_lt_of_le a.2 hlam⟩
643 simpa [seriesData, seriesSub, hlamμ, Subgroup.mem_iInf] using hrestrict
644 · intro lam hlam
645 let H : ClosedNormalSubgroupData G := seriesData lam
646 let K : ClosedNormalSubgroupData G := seriesData (succ lam)
647 let U : OpenNormalSubgroup G := Wμ ⟨lam, hlam⟩
648 let φ : H.toSubgroup →* G ⧸ (U : Subgroup G) :=
649 (QuotientGroup.mk' (U : Subgroup G)).comp H.toSubgroup.subtype
650 let L : Subgroup (G ⧸ (U : Subgroup G)) :=
651 Subgroup.map (QuotientGroup.mk' (U : Subgroup G)) H.toSubgroup
652 have hlamle : lam ≤ μ := hlam.le
653 have hsuccle : succ lam ≤ μ := succ_le_of_lt hlam
654 have hRangeEq : φ.range = L := by
655 ext y
656 constructor
657 · rintro ⟨x, rfl⟩
658 exact ⟨x, x.2, rfl⟩
659 · rintro ⟨x, hx, rfl⟩
660 exact ⟨⟨x, hx⟩, rfl⟩
661 letI : L.Normal := by
662 dsimp [L]
663 exact Subgroup.Normal.map H.normal' (QuotientGroup.mk' (U : Subgroup G))
664 (QuotientGroup.mk'_surjective (U : Subgroup G))
665 have hKmem :
666 ∀ {x : H.toSubgroup}, x.1 ∈ K.toSubgroup ↔ x.1 ∈ (U : Subgroup G) := by
667 intro x
668 constructor
669 · intro hxK
670 have hxall :
671 ∀ a : Set.Iio (succ lam),
672 x.1 ∈ (Wμ ⟨a.1, lt_of_lt_of_le a.2 hsuccle⟩ : Subgroup G) := by
673 change x.1 ∈ seriesSub (succ lam) at hxK
674 simp only [seriesSub, dif_pos hsuccle, Subgroup.mem_iInf] at hxK
675 exact hxK
676 simpa [U] using hxall ⟨lam, show lam ∈ Set.Iio (succ lam) from lt_succ lam⟩
677 · intro hxU
678 have hxH : x.1 ∈ H.toSubgroup := x.2
679 have hxHall :
680 ∀ a : Set.Iio lam,
681 x.1 ∈ (Wμ ⟨a.1, lt_of_lt_of_le a.2 hlamle⟩ : Subgroup G) := by
682 simpa [H, seriesData, seriesSub, hlamle, Subgroup.mem_iInf] using hxH
683 have hxKall :
684 ∀ a : Set.Iio (succ lam),
685 x.1 ∈ (Wμ ⟨a.1, lt_of_lt_of_le a.2 hsuccle⟩ : Subgroup G) := by
686 intro a
687 rcases eq_or_lt_of_le (lt_succ_iff.mp (show a.1 < succ lam from a.2)) with haEq | ha
688 · simpa [U, haEq] using hxU
689 · exact hxHall ⟨a.1, show a.1 ∈ Set.Iio lam from ha⟩
690 change x.1 ∈ seriesSub (succ lam)
691 simp only [seriesSub, dif_pos hsuccle, Subgroup.mem_iInf]
692 exact hxKall
693 have hKerEq : K.toSubgroup.subgroupOf H.toSubgroup = φ.ker := by
694 ext x
695 constructor
696 · intro hx
697 have hxU : x.1 ∈ (U : Subgroup G) := by
698 exact hKmem.1 (by simpa [Subgroup.mem_subgroupOf] using hx)
699 simpa [MonoidHom.mem_ker, φ] using
700 (QuotientGroup.eq_one_iff (N := (U : Subgroup G)) x.1).2 hxU
701 · intro hx
702 have hxU : x.1 ∈ (U : Subgroup G) := by
703 exact (QuotientGroup.eq_one_iff (N := (U : Subgroup G)) x.1).1
704 (by simpa [MonoidHom.mem_ker, φ] using hx)
705 have hxK : x.1 ∈ K.toSubgroup := hKmem.2 hxU
706 simpa [Subgroup.mem_subgroupOf] using hxK
707 have hL : C L := hNorm L (hWμC ⟨lam, hlam⟩)
708 have hStep : C (H.toSubgroup ⧸ K.toSubgroup.subgroupOf H.toSubgroup) := by
709 let e₁ : H.toSubgroup ⧸ K.toSubgroup.subgroupOf H.toSubgroup ≃* H.toSubgroup ⧸ φ.ker :=
710 QuotientGroup.quotientMulEquivOfEq hKerEq
711 exact hIso
712 ⟨(MulEquiv.subgroupCongr hRangeEq).symm.trans
713 (e₁.trans (QuotientGroup.quotientKerEquivRange φ)).symm⟩
714 hL
715 simpa [ClosedNormalSubgroupData.stepQuotient, H, K] using hStep
716 · intro lam hlam hLimit
717 ext x
718 constructor
719 · intro hx
720 have hxall :
721 ∀ a : Set.Iio lam, x ∈ (Wμ ⟨a.1, lt_of_lt_of_le a.2 hlam⟩ : Subgroup G) := by
722 simpa [seriesData, seriesSub, hlam, Subgroup.mem_iInf] using hx
723 have hxseries : ∀ ν : Set.Iio lam, x ∈ (seriesData ν.1).toSubgroup := by
724 intro ν
725 have hνμ : ν.1 ≤ μ := ν.2.le.trans hlam
726 have hrestrict :
727 ∀ a : Set.Iio ν.1,
728 x ∈ (Wμ ⟨a.1, lt_of_lt_of_le a.2 hνμ⟩ : Subgroup G) := by
729 intro a
730 exact hxall ⟨a.1, show a.1 < lam from lt_of_lt_of_le a.2 ν.2.le⟩
731 simpa [seriesData, seriesSub, hνμ, Subgroup.mem_iInf] using hrestrict
732 simpa [Subgroup.mem_iInf] using hxseries
733 · intro hx
734 have hxseries : ∀ ν : Set.Iio lam, x ∈ (seriesData ν.1).toSubgroup := by
735 simpa [Subgroup.mem_iInf] using hx
736 have hxall :
737 ∀ a : Set.Iio lam, x ∈ (Wμ ⟨a.1, lt_of_lt_of_le a.2 hlam⟩ : Subgroup G) := by
738 intro a
739 have hs : succ a.1 < lam := hLimit.succ_lt a.2
740 have hsμ : succ a.1 ≤ μ := hs.le.trans hlam
741 have hxin : x ∈ (seriesData (succ a.1)).toSubgroup := hxseries ⟨succ a.1, hs⟩
742 have hxsucc :
743 ∀ b : Set.Iio (succ a.1),
744 x ∈ (Wμ ⟨b.1, lt_of_lt_of_le b.2 hsμ⟩ : Subgroup G) := by
745 change x ∈ seriesSub (succ a.1) at hxin
746 simp only [seriesSub, dif_pos hsμ, Subgroup.mem_iInf] at hxin
747 exact hxin
748 simpa using hxsucc ⟨a.1, show a.1 ∈ Set.Iio (succ a.1) from lt_succ a.1⟩
749 simpa [seriesData, seriesSub, hlam, Subgroup.mem_iInf] using hxall
751end ProCGroups.LocalWeight