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

ProCGroups/LocalWeight/CardinalInvariantsAndLocalWeight.lean

1import Mathlib.SetTheory.Cardinal.Arithmetic
2import ProCGroups.FiniteGeneration.CharacteristicChainsAndIndices
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/LocalWeight/CardinalInvariantsAndLocalWeight.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 v
28open ProCGroups.ProC ProCGroups.Generation
29open ProCGroups.FiniteGeneration
31section CardinalInvariants
33variable (X : Type u) [TopologicalSpace X]
35/-- The cardinality of a family of subsets, viewed as a subtype. -/
36noncomputable def familyCardinal (B : Set (Set X)) : Cardinal :=
37 Cardinal.mk { U : Set X // U ∈ B }
39/-- a family `B` is a neighborhood basis at `x` if each member of `B`
40is an open neighborhood of `x`, and every open neighborhood of `x` contains an element
41of `B`. -/
42def IsNeighborhoodBasisAt (x : X) (B : Set (Set X)) : Prop :=
43 (∀ U ∈ B, IsOpen U ∧ x ∈ U) ∧
44 ∀ V, IsOpen V → x ∈ V → ∃ U ∈ B, U ⊆ V
46/-- the weight `w(X)` is the least cardinality of a basis of open sets. -/
47noncomputable def weight : Cardinal :=
48 sInf { κ : Cardinal |
49 ∃ B : Set (Set X), IsTopologicalBasis B ∧ familyCardinal (X := X) B ≤ κ }
51/-- `ρ(X)` is the cardinality of the set of all clopen subsets of `X`. -/
52noncomputable def rho : Cardinal :=
53 familyCardinal (X := X) { U : Set X | IsClopen U }
55/-- the local weight at `x` is the least
56cardinality of a neighborhood basis at `x`. -/
57noncomputable def localWeightAt (x : X) : Cardinal :=
58 sInf { κ : Cardinal |
59 ∃ B : Set (Set X),
60 IsNeighborhoodBasisAt (X := X) x B ∧ familyCardinal (X := X) B ≤ κ }
62/-- Any explicit basis bounds the weight from above. -/
63theorem weight_le_familyCardinal_of_basis {B : Set (Set X)} (hB : IsTopologicalBasis B) :
64 weight X ≤ familyCardinal (X := X) B := by
65 unfold weight
66 have hmem :
67 familyCardinal (X := X) B ∈ { κ : Cardinal |
68 ∃ B : Set (Set X), IsTopologicalBasis B ∧ familyCardinal (X := X) B ≤ κ } := by
69 exact ⟨B, hB, le_rfl⟩
70 exact csInf_le (OrderBot.bddBelow _) hmem
72/-- Any explicit neighborhood basis at `x` bounds the local weight from above. -/
73theorem localWeightAt_le_familyCardinal_of_basis {x : X} {B : Set (Set X)}
74 (hB : IsNeighborhoodBasisAt (X := X) x B) :
75 localWeightAt X x ≤ familyCardinal (X := X) B := by
77 have hmem :
78 familyCardinal (X := X) B ∈ { κ : Cardinal |
79 ∃ B : Set (Set X),
80 IsNeighborhoodBasisAt (X := X) x B ∧ familyCardinal (X := X) B ≤ κ } := by
81 exact ⟨B, hB, le_rfl⟩
82 exact csInf_le (OrderBot.bddBelow _) hmem
84/-- If the singleton `{x}` is open, then the local weight at `x` is at most `1`. -/
85theorem localWeightAt_le_one_of_isOpen_singleton {x : X} (hx : IsOpen ({x} : Set X)) :
86 localWeightAt X x ≤ 1 := by
87 classical
88 let B : Set (Set X) := { {x} }
89 have hB : IsNeighborhoodBasisAt (X := X) x B := by
90 refine ⟨?_, ?_⟩
91 · intro U hU
92 rcases Set.mem_singleton_iff.mp hU with rfl
93 exact ⟨hx, by simp only [mem_singleton_iff]⟩
94 · intro V hVopen hxV
95 refine ⟨{x}, by simp only [mem_singleton_iff, B], ?_⟩
96 intro y hy
97 rcases Set.mem_singleton_iff.mp hy with rfl
98 exact hxV
99 calc
100 localWeightAt X x ≤ familyCardinal (X := X) B :=
102 _ = 1 := by
103 simp only [familyCardinal, mem_singleton_iff, Cardinal.mk_fintype, Fintype.card_unique, Nat.cast_one, B]
105omit [TopologicalSpace X] in
106/-- Monotonicity of `familyCardinal` under inclusion of families. -/
107theorem familyCardinal_mono {B C : Set (Set X)} (hBC : B ⊆ C) :
108 familyCardinal (X := X) B ≤ familyCardinal (X := X) C := by
110 exact Cardinal.mk_le_of_injective
111 (f := fun U : { U : Set X // U ∈ B } => ⟨U.1, hBC U.2⟩)
112 (by
113 intro U V hUV
114 exact Subtype.ext (congrArg (fun W : { U : Set X // U ∈ C } => W.1) hUV))
116/-- Any family of clopen sets injects into the type of all clopen subsets, so its cardinality is
117bounded by `ρ(X)`. -/
119 (hB : ∀ U ∈ B, IsClopen U) :
120 familyCardinal (X := X) B ≤ rho X := by
122 let f : { U : Set X // U ∈ B } → { U : Set X // IsClopen U } :=
123 fun U => ⟨U.1, hB U.1 U.2⟩
124 refine Cardinal.mk_le_of_injective (f := f) ?_
125 intro U V hUV
126 exact Subtype.ext (congrArg (fun W : { U : Set X // IsClopen U } => W.1) hUV)
128/-- A finite basis on a `T₁` space forces the underlying space itself to be finite. -/
129theorem finite_of_finite_basisSubtype [T1Space X] {B : Set (Set X)}
130 (hB : IsTopologicalBasis B) [Finite { U : Set X // U ∈ B }] : Finite X := by
131 classical
132 let β : Type u := { U : Set X // U ∈ B }
133 letI : Fintype β := Fintype.ofFinite β
134 let code : X → Set β := fun x => { U | x ∈ (U : Set X) }
135 have hcode : Function.Injective code := by
136 intro x y hxy
137 by_contra hne
138 have hx_mem : x ∈ ({y}ᶜ : Set X) := by
139 change x ∉ ({y} : Set X)
140 intro hxy
141 exact hne (by simpa [Set.mem_singleton_iff] using hxy)
142 have hOpen : IsOpen ({y}ᶜ : Set X) :=
143 (isClosed_singleton : IsClosed ({y} : Set X)).isOpen_compl
144 rcases hB.exists_subset_of_mem_open hx_mem hOpen with ⟨U, hUB, hxU, hUsub⟩
145 have hyU : y ∉ U := by
146 intro hyU
147 have : y ∈ ({y}ᶜ : Set X) := hUsub hyU
148 have hnot : y ∉ ({y} : Set X) := by
149 change y ∉ ({y} : Set X)
150 exact this
151 exact hnot (Set.mem_singleton_iff.mpr rfl)
152 have hxCode : (⟨U, hUB⟩ : β) ∈ code x := by
153 simpa [code] using hxU
154 have hyCode : (⟨U, hUB⟩ : β) ∈ code y := by
155 simpa [hxy] using hxCode
156 exact hyU (by simpa [code] using hyCode)
157 exact Finite.of_injective code hcode
159/-- An infinite `T₁` space cannot have a finite topological basis. -/
160theorem infinite_familySubtype_of_basis [T1Space X] [Infinite X] {B : Set (Set X)}
161 (hB : IsTopologicalBasis B) : Infinite { U : Set X // U ∈ B } := by
162 classical
163 by_contra hfinite
164 letI : Finite { U : Set X // U ∈ B } := not_infinite_iff_finite.mp hfinite
165 have hXfin : Finite X := finite_of_finite_basisSubtype (X := X) hB
166 exact hXfin.false
168/-- In a compact space, every clopen set is the union of finitely many members of any chosen
169topological basis. -/
170theorem exists_finset_basisSUnion_eq_of_isClopen [CompactSpace X] {B : Set (Set X)}
171 (hB : IsTopologicalBasis B) {U : Set X} (hU : IsClopen U) :
172 ∃ s : Finset { V : Set X // V ∈ B },
173 U = ⋃₀ (Subtype.val '' (↑s : Set { V : Set X // V ∈ B })) := by
174 classical
175 obtain ⟨s, hs⟩ :=
176 eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open B hB U hU.isClosed.isCompact
177 hU.isOpen
178 refine ⟨s, ?_⟩
179 simpa only [Set.sUnion_image] using hs
181/-- in an infinite
182compact Hausdorff space, every basis controls the number of clopen subsets. -/
183theorem rho_le_familyCardinal_of_basis [CompactSpace X] [T2Space X] [Infinite X]
184 {B : Set (Set X)} (hB : IsTopologicalBasis B) :
185 rho X ≤ familyCardinal (X := X) B := by
186 classical
187 let β : Type u := { U : Set X // U ∈ B }
188 have hβinf : Infinite β := infinite_familySubtype_of_basis (X := X) hB
189 letI : Infinite β := hβinf
190 let encode : { U : Set X // IsClopen U } → Finset β :=
191 fun U =>
192 Classical.choose
193 (exists_finset_basisSUnion_eq_of_isClopen (X := X) hB (U := U.1) U.2)
194 have hencode :
195 ∀ U : { U : Set X // IsClopen U },
196 U.1 = ⋃₀ (Subtype.val '' (↑(encode U) : Set β)) := by
197 intro U
198 exact Classical.choose_spec
199 (exists_finset_basisSUnion_eq_of_isClopen (X := X) hB (U := U.1) U.2)
200 have henc_inj : Function.Injective encode := by
201 intro U V hUV
202 apply Subtype.ext
203 calc
204 U.1 = ⋃₀ (Subtype.val '' (↑(encode U) : Set β)) := hencode U
205 _ = ⋃₀ (Subtype.val '' (↑(encode V) : Set β)) := by simp only [hUV, sUnion_image, SetLike.mem_coe, iUnion_coe_set]
206 _ = V.1 := (hencode V).symm
208 calc
209 Cardinal.mk { U : Set X // IsClopen U } ≤ Cardinal.mk (Finset β) :=
210 Cardinal.mk_le_of_injective (f := encode) henc_inj
211 _ = Cardinal.mk β := by
212 exact Cardinal.mk_finset_of_infinite β
213 _ = Cardinal.mk { U : Set X // U ∈ B } := by
214 rfl
216/-- 6.1(a), reverse inequality in weight form. -/
217theorem rho_le_weight [CompactSpace X] [T2Space X] [Infinite X] :
218 rho X ≤ weight X := by
219 unfold weight
220 refine le_csInf ?_ ?_
221 · refine ⟨familyCardinal (X := X) { U : Set X | IsOpen U }, ?_⟩
222 exact ⟨{ U : Set X | IsOpen U }, isTopologicalBasis_opens, le_rfl⟩
223 intro κ hκ
224 rcases hκ with ⟨B, hB, hcard⟩
225 exact le_trans (rho_le_familyCardinal_of_basis (X := X) hB) hcard
227/-- Every global basis yields a local basis at any chosen point, so the local weight is always
228bounded by the weight. -/
229theorem localWeightAt_le_weight {x : X} :
230 localWeightAt X x ≤ weight X := by
231 unfold weight
232 refine le_csInf ?_ ?_
233 · refine ⟨familyCardinal (X := X) { U : Set X | IsOpen U }, ?_⟩
234 exact ⟨{ U : Set X | IsOpen U }, isTopologicalBasis_opens, le_rfl⟩
235 · intro κ hκ
236 rcases hκ with ⟨B, hB, hBcard⟩
237 let Bx : Set (Set X) := { U : Set X | U ∈ B ∧ x ∈ U }
238 have hBx : IsNeighborhoodBasisAt (X := X) x Bx := by
239 constructor
240 · intro U hU
241 exact ⟨hB.isOpen hU.1, hU.2⟩
242 · intro V hVopen hxV
243 rcases hB.exists_subset_of_mem_open hxV hVopen with ⟨U, hUB, hxU, hUsub⟩
244 exact ⟨U, ⟨hUB, hxU⟩, hUsub⟩
245 calc
246 localWeightAt X x ≤ familyCardinal (X := X) Bx :=
248 _ ≤ familyCardinal (X := X) B :=
250 intro U hU
251 exact hU.1)
252 _ ≤ κ := hBcard
254/-- any clopen basis bounds the weight by `ρ(X)`. -/
256 (hB : ∃ B : Set (Set X), IsTopologicalBasis B ∧ ∀ U ∈ B, IsClopen U) :
257 weight X ≤ rho X := by
258 rcases hB with ⟨B, hBasis, hClopen⟩
259 calc
260 weight X ≤ familyCardinal (X := X) B :=
262 _ ≤ rho X :=
265/-- Any clopen basis of an infinite compact Hausdorff space has cardinality exactly `ρ(X)`. -/
266theorem familyCardinal_eq_rho_of_clopenBasis [CompactSpace X] [T2Space X] [Infinite X]
267 {B : Set (Set X)} (hB : IsTopologicalBasis B) (hClopen : ∀ U ∈ B, IsClopen U) :
268 familyCardinal (X := X) B = rho X := by
269 apply le_antisymm
270 · exact familyCardinal_le_rho_of_clopenFamily (X := X) hClopen
271 · exact rho_le_familyCardinal_of_basis (X := X) hB
273/-- A variant of the preceding lemma for the special case where the set of all clopen subsets is
274already known to be a topological basis. -/
276 (hBasis : IsTopologicalBasis { U : Set X | IsClopen U }) :
277 weight X ≤ rho X := by
278 calc
279 weight X ≤ familyCardinal (X := X) { U : Set X | IsClopen U } :=
281 _ = rho X := rfl
283/-- 6.1(a) in the special case where all clopen subsets already form a basis. -/
284theorem weight_eq_rho_of_clopenBasis [CompactSpace X] [T2Space X] [Infinite X]
285 (hBasis : IsTopologicalBasis { U : Set X | IsClopen U }) :
286 weight X = rho X := by
287 apply le_antisymm
288 · exact weight_le_rho_of_clopenBasis (X := X) hBasis
289 · exact rho_le_weight (X := X)
291/-- any clopen neighborhood basis at `x` bounds the
292local weight at `x` by `ρ(X)`. -/
294 (hB : ∃ B : Set (Set X),
295 IsNeighborhoodBasisAt (X := X) x B ∧ ∀ U ∈ B, IsClopen U) :
296 localWeightAt X x ≤ rho X := by
297 rcases hB with ⟨B, hBasis, hClopen⟩
298 calc
299 localWeightAt X x ≤ familyCardinal (X := X) B :=
301 _ ≤ rho X :=
304end CardinalInvariants
306section LocalWeightOfGroups
308variable (G : Type u) [Group G] [TopologicalSpace G]
310/-- the local weight `w₀(G)` of a topological group is the local weight at `1`.
312The continuity assumptions needed for later results are imposed where they are used; the cardinal
313invariant itself only depends on the underlying topology and distinguished point. -/
314noncomputable def localWeight : Cardinal :=
315 localWeightAt (X := G) (1 : G)
317/-- The local weight of a topological group is bounded by its weight. -/
319 localWeight G ≤ weight G := by
320 simpa [localWeight] using
321 (localWeightAt_le_weight (X := G) (x := (1 : G)))
323/-- 6.1(b), easy direction at the identity. -/
325 (hB : ∃ B : Set (Set G),
326 IsNeighborhoodBasisAt (X := G) (1 : G) B ∧ ∀ U ∈ B, IsClopen U) :
327 localWeight G ≤ rho G := by
328 simpa [localWeight] using
331end LocalWeightOfGroups
333section GroupTranslateBases
335variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
337/-- The family of all left translates of members of `B`. This is the global basis naturally
338associated to a neighborhood basis at `1`. -/
339def leftTranslateFamily (B : Set (Set G)) : Set (Set G) :=
340 { V : Set G | ∃ g : G, ∃ U ∈ B, V = g • U }
342/-- In a group, left translates of a neighborhood basis at `1` form a topological basis.
343 -/
345 (hB : IsNeighborhoodBasisAt (X := G) (1 : G) B) :
346 IsTopologicalBasis (leftTranslateFamily (G := G) B) := by
347 refine TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds ?_ ?_
348 · intro V hV
349 rcases hV with ⟨g, U, hUB, rfl⟩
350 exact (hB.1 U hUB).1.leftCoset g
351 · intro g V hgV hOpenV
352 have hOpenPre : IsOpen (g⁻¹ • V) := hOpenV.leftCoset g⁻¹
353 have hmemPre : (1 : G) ∈ g⁻¹ • V := by
354 exact ⟨g, hgV, by simp only [smul_eq_mul, inv_mul_cancel]⟩
355 rcases hB.2 (g⁻¹ • V) hOpenPre hmemPre with ⟨U, hUB, hUsub⟩
356 refine ⟨g • U, ⟨g, U, hUB, rfl⟩, ?_, ?_⟩
357 · exact ⟨1, (hB.1 U hUB).2, by simp only [smul_eq_mul, mul_one]⟩
358 · intro y hy
359 rcases hy with ⟨u, huU, rfl⟩
360 rcases hUsub huU with ⟨v, hvV, rfl⟩
361 simpa [mul_assoc] using hvV
363/-- Any neighborhood basis at `1` yields a global basis whose cardinality is the cardinality of
364its translate family. -/
366 (hB : IsNeighborhoodBasisAt (X := G) (1 : G) B) :
367 weight G ≤ familyCardinal (X := G) (leftTranslateFamily (G := G) B) := by
371end GroupTranslateBases
373section GroupTranslateClopen
375variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
377/-- Left translation preserves clopen subsets in a topological group. -/
378theorem IsClopen.leftTranslate {U : Set G} (hU : IsClopen U) (g : G) :
379 IsClopen (g • U) := by
380 constructor
381 · exact hU.1.leftCoset g
382 · exact hU.2.leftCoset g
384/-- if the identity has a clopen neighborhood
385basis, then `w(G) ≤ ρ(G)`. The remaining work for the full proposition is the comparison with
386`w₀(G)` in the exact cardinality-preserving form used in the book. -/
388 (hB : ∃ B : Set (Set G),
389 IsNeighborhoodBasisAt (X := G) (1 : G) B ∧ ∀ U ∈ B, IsClopen U) :
390 weight G ≤ rho G := by
391 rcases hB with ⟨B, hBasis, hClopen⟩
393 refine ⟨leftTranslateFamily (G := G) B,
395 intro V hV
396 rcases hV with ⟨g, U, hUB, rfl⟩
397 exact IsClopen.leftTranslate (G := G) (hClopen U hUB) g
399end GroupTranslateClopen
402/-- A continuous homomorphism out of a profinite group is determined by any topological
403generating set.
404-/
406 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
407 {R : Type v} [Group R] [TopologicalSpace R] [T2Space R]
408 {X : Set G} (hXgen : TopologicallyGenerates (G := G) X)
409 {f g : ContinuousMonoidHom G R} (hfg : Set.EqOn f g X) :
410 f = g := by
411 let K : Subgroup G := {
412 carrier := { x | f x = g x }
413 one_mem' := by simp only [mem_setOf_eq, map_one]
414 mul_mem' := by
415 intro a b ha hb
416 change f (a * b) = g (a * b)
417 rw [map_mul, map_mul, ha, hb]
418 inv_mem' := by
419 intro a ha
420 simpa using congrArg Inv.inv ha
421 }
422 have hKclosed : IsClosed ((K : Subgroup G) : Set G) := by
423 change IsClosed { x | f x = g x }
424 exact isClosed_eq f.continuous_toFun g.continuous_toFun
425 have hsub : Subgroup.closure X ≤ K := by
426 rw [Subgroup.closure_le]
427 intro x hx
428 exact hfg hx
429 have htop : (⊤ : Subgroup G) ≤ K := by
430 have hcl :
431 (Subgroup.closure X).topologicalClosure ≤ K :=
432 Subgroup.topologicalClosure_minimal _ hsub hKclosed
433 change (Subgroup.closure X).topologicalClosure = ⊤ at hXgen
434 rw [hXgen] at hcl
435 simpa using hcl
436 ext x
437 simpa [K] using htop (show x ∈ (⊤ : Subgroup G) from by simp only [Subgroup.mem_top])
439/-- A finite discrete codomain yields at most `ρ(X)` continuous maps from a profinite space.
440-/
442 (X : Type u) [TopologicalSpace X] [CompactSpace X] [T2Space X]
443 [TotallyDisconnectedSpace X] [Infinite X]
444 (H : Type v) [Finite H] [TopologicalSpace H] [DiscreteTopology H] :
445 Cardinal.mk C(X, H) ≤ Cardinal.lift (rho X) := by
446 classical
447 by_cases hH : Nonempty H
448 · let β : Type u := { U : Set X // IsClopen U }
449 have hβinf : Infinite β := by
450 simpa [β] using
452 (B := { U : Set X | IsClopen U })
454 (X := X)))
455 letI : Infinite β := hβinf
456 letI : Fintype H := Fintype.ofFinite H
457 let encode : C(X, H) → H → β := fun f h =>
458 ⟨f ⁻¹' ({h} : Set H), by
459 refine ⟨?_, ?_⟩
460 · simpa using (isClosed_discrete ({h} : Set H)).preimage f.continuous_toFun
461 · simpa using (isOpen_discrete ({h} : Set H)).preimage f.continuous_toFun⟩
462 have hencode_inj : Function.Injective encode := by
463 intro f g hfg
464 ext x
465 have hx : x ∈ (encode f (f x)).1 := by
466 simp only [mem_preimage, mem_singleton_iff, encode]
467 have hx' : x ∈ (encode g (f x)).1 := by
468 simpa [hfg] using hx
469 simpa [eq_comm, encode] using hx'
470 have hAlephLe : Cardinal.aleph0 ≤ Cardinal.lift (rho X) := by
471 apply (Cardinal.aleph0_le_lift).2
472 simp only [rho, familyCardinal, mem_setOf_eq, Cardinal.aleph0_le_mk, β]
473 have hHcardPos : 1 ≤ Fintype.card H := Fintype.card_pos_iff.mpr hH
474 calc
475 Cardinal.mk C(X, H) ≤ Cardinal.mk (H → β) :=
476 Cardinal.mk_le_of_injective (f := encode) hencode_inj
477 _ = Cardinal.lift (Cardinal.mk β) ^ Cardinal.lift (Cardinal.mk H) := by
478 rw [Cardinal.mk_arrow]
479 _ = Cardinal.lift (rho X) ^ Fintype.card H := by
480 rw [Cardinal.mk_fintype H, Cardinal.lift_natCast]
481 rfl
482 _ = Cardinal.lift (rho X) :=
483 Cardinal.power_nat_eq hAlephLe hHcardPos
484 · have hEmpty : IsEmpty H := not_nonempty_iff.mp hH
485 letI : IsEmpty H := hEmpty
486 letI : Nonempty X := inferInstance
487 haveI : IsEmpty (X → H) := by infer_instance
488 haveI : IsEmpty C(X, H) := by
489 refine ⟨fun f => ?_⟩
490 exact isEmptyElim (f (Classical.choice ‹Nonempty X›))
491 have hzero : Cardinal.mk C(X, H) = 0 := by
492 rw [Cardinal.mk_eq_zero_iff]
493 infer_instance
494 rw [hzero]
495 exact Cardinal.zero_le _
497/-- Passing to a closed subspace does not increase `ρ`.
498-/
500 (X : Type u) [TopologicalSpace X] [CompactSpace X] [T2Space X]
501 [TotallyDisconnectedSpace X] {A : Set X} (hAclosed : IsClosed A) :
502 rho ↥A ≤ rho X := by
503 classical
504 have hlift :
505 ∀ U : { U : Set A // IsClopen U }, ∃ C : { C : Set X // IsClopen C },
506 Subtype.val ⁻¹' C.1 = U.1 := by
507 intro U
508 rcases isOpen_induced_iff.mp U.2.2 with ⟨O, hOopen, hOeq⟩
509 rcases isClosed_induced_iff.mp U.2.1 with ⟨F, hFclosed, hFeq⟩
510 have hAF_subset_O : A ∩ F ⊆ O := by
511 intro x hx
512 have hxU : (⟨x, hx.1⟩ : A) ∈ U.1 := by
513 rw [← hFeq]
514 simpa using hx.2
515 rw [← hOeq] at hxU
516 simpa using hxU
517 rcases exists_clopen_of_closed_subset_open
518 (Z := A ∩ F) (U := O) (hAclosed.inter hFclosed) hOopen hAF_subset_O with
519 ⟨C, hCclopen, hAF_sub_C, hCsubO⟩
520 refine ⟨⟨C, hCclopen⟩, ?_⟩
521 ext x
522 constructor
523 · intro hxC
524 have hxO : x.1 ∈ O := hCsubO hxC
525 rw [← hOeq]
526 simpa using hxO
527 · intro hxU
528 have hxF : x.1 ∈ F := by
529 have hxF' : x ∈ (Subtype.val ⁻¹' F : Set A) := by
530 rwa [← hFeq] at hxU
531 simpa using hxF'
532 exact hAF_sub_C ⟨x.2, hxF⟩
533 choose liftClopen hLiftClopen using hlift
535 refine Cardinal.mk_le_of_injective (f := liftClopen) ?_
536 intro U V hUV
537 apply Subtype.ext
538 have hpre :
539 (Subtype.val ⁻¹' (liftClopen U).1 : Set A) =
540 (Subtype.val ⁻¹' (liftClopen V).1 : Set A) := by
541 simpa using congrArg (fun C : { C : Set X // IsClopen C } =>
542 (Subtype.val ⁻¹' C.1 : Set A)) hUV
543 rw [hLiftClopen U, hLiftClopen V] at hpre
544 exact hpre
546/-- The finite coset action, viewed as a continuous homomorphism into a discrete permutation
547group. This local-weight facade uses the finite-generation construction and only fills in the
548finite-quotient proof from openness. -/
550 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
551 (H : Subgroup G) (hH : IsOpen (H : Set G)) {n : ℕ} (hn : Nat.card (G ⧸ H) = n) :
552 ContinuousMonoidHom G (Equiv.Perm (Fin n)) :=
553 ProCGroups.FiniteGeneration.openSubgroupIndexContinuousHom
554 (G := G) H hH (Subgroup.quotient_finite_of_isOpen H hH) hn
556/-- The clopen-subset cardinal `ρ` is a topological invariant. -/
558 (X Y : Type u) [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) :
559 rho X = rho Y := by
560 classical
562 refine Cardinal.mk_congr ?_
563 refine
564 { toFun := fun U => ⟨e.symm ⁻¹' U.1, U.2.preimage e.symm.continuous⟩
565 invFun := fun V => ⟨e ⁻¹' V.1, V.2.preimage e.continuous⟩
566 left_inv := ?_
567 right_inv := ?_ }
568 · intro U
569 apply Subtype.ext
570 ext x
571 simp only [mem_setOf_eq, mem_preimage, Homeomorph.symm_apply_apply]
572 · intro V
573 apply Subtype.ext
574 ext y
575 simp only [mem_setOf_eq, mem_preimage, Homeomorph.apply_symm_apply]
577/-- For an infinite discrete space `X`, the one-point compactification has exactly `#X` clopen
578subsets: finite subsets coming from `X`, and complements of finite subsets. -/
580 (X : Type u) [TopologicalSpace X] [DiscreteTopology X] [Infinite X] :
581 rho (OnePoint X) = Cardinal.mk X := by
582 classical
583 let imageClopen : Finset X → Set (OnePoint X) :=
584 fun s => ((↑) '' (s : Set X) : Set (OnePoint X))
585 have hImageClopen : ∀ s : Finset X, IsClopen (imageClopen s) := by
586 intro s
587 constructor
588 · exact (OnePoint.isClosed_image_coe (s := (s : Set X))).2
589 ⟨s.finite_toSet.isClosed, s.finite_toSet.isCompact⟩
590 · exact (OnePoint.isOpen_image_coe (s := (s : Set X))).2 (isOpen_discrete _)
591 have himage_eq_of_notMem_infty {s : Set (OnePoint X)} (hs : OnePoint.infty ∉ s) :
592 ((↑) '' (((↑) : X → OnePoint X) ⁻¹' s) : Set (OnePoint X)) = s := by
593 ext z
594 cases z using OnePoint.rec with
595 | infty =>
596 simp only [mem_image, mem_preimage, OnePoint.coe_ne_infty, and_false, exists_const, hs]
597 | coe x =>
598 simp only [mem_image, mem_preimage, OnePoint.some_eq_iff, exists_eq_right]
599 let decode : Finset X ⊕ Finset X → { U : Set (OnePoint X) // IsClopen U }
600 | Sum.inl s => ⟨imageClopen s, hImageClopen s⟩
601 | Sum.inr s => ⟨(imageClopen s)ᶜ,
602 ⟨(hImageClopen s).2.isClosed_compl, (hImageClopen s).1.isOpen_compl⟩⟩
603 let code : { U : Set (OnePoint X) // IsClopen U } → Finset X ⊕ Finset X := fun U => by
604 by_cases hinfty : OnePoint.infty ∈ U.1
605 · have hfinite :
606 ((((↑) : X → OnePoint X) ⁻¹' (U.1ᶜ : Set (OnePoint X))) : Set X).Finite := by
607 have hcompact :
608 IsCompact (((↑) : X → OnePoint X) ⁻¹' (U.1ᶜ : Set (OnePoint X))) := by
609 exact ((OnePoint.isClosed_iff_of_notMem (s := U.1ᶜ) (by simpa using hinfty)
610 ).1 U.2.2.isClosed_compl).2
611 exact isCompact_iff_finite.mp hcompact
612 exact Sum.inr hfinite.toFinset
613 · have hfinite :
614 ((((↑) : X → OnePoint X) ⁻¹' U.1) : Set X).Finite := by
615 have hcompact :
616 IsCompact (((↑) : X → OnePoint X) ⁻¹' U.1 : Set X) := by
617 exact ((OnePoint.isClosed_iff_of_notMem (s := U.1) hinfty).1 U.2.1).2
618 exact isCompact_iff_finite.mp hcompact
619 exact Sum.inl hfinite.toFinset
620 have hdecode_code :
621 Function.LeftInverse decode code := by
622 intro U
623 dsimp [code]
624 by_cases hinfty : OnePoint.infty ∈ U.1
625 · simp only [hinfty, decode]
626 apply Subtype.ext
627 have hfinite :
628 ((((↑) : X → OnePoint X) ⁻¹' (U.1ᶜ : Set (OnePoint X))) : Set X).Finite := by
629 have hcompact :
630 IsCompact (((↑) : X → OnePoint X) ⁻¹' (U.1ᶜ : Set (OnePoint X))) := by
631 exact ((OnePoint.isClosed_iff_of_notMem (s := U.1ᶜ) (by simpa using hinfty)
632 ).1 U.2.2.isClosed_compl).2
633 exact isCompact_iff_finite.mp hcompact
634 change (((↑) '' ((hfinite.toFinset : Set X)) : Set (OnePoint X))ᶜ) = U.1
635 rw [hfinite.coe_toFinset]
636 rw [himage_eq_of_notMem_infty (s := U.1ᶜ) (by simpa using hinfty)]
637 simp only [compl_compl]
638 · simp only [hinfty, decode]
639 apply Subtype.ext
640 have hfinite :
641 ((((↑) : X → OnePoint X) ⁻¹' U.1) : Set X).Finite := by
642 have hcompact :
643 IsCompact (((↑) : X → OnePoint X) ⁻¹' U.1 : Set X) := by
644 exact ((OnePoint.isClosed_iff_of_notMem (s := U.1) hinfty).1 U.2.1).2
645 exact isCompact_iff_finite.mp hcompact
646 change ((↑) '' ((hfinite.toFinset : Set X)) : Set (OnePoint X)) = U.1
647 rw [hfinite.coe_toFinset]
648 exact himage_eq_of_notMem_infty (s := U.1) hinfty
649 have hupper : rho (OnePoint X) ≤ Cardinal.mk X := by
651 calc
652 Cardinal.mk { U : Set (OnePoint X) // IsClopen U } ≤ Cardinal.mk (Finset X ⊕ Finset X) :=
653 Cardinal.mk_le_of_injective (f := code) hdecode_code.injective
654 _ = Cardinal.mk (Finset X) + Cardinal.mk (Finset X) := by
655 rw [Cardinal.mk_sum]
656 simp only [Cardinal.mk_finset_of_infinite, Cardinal.lift_id, Cardinal.add_mk_eq_max, max_self]
657 _ = Cardinal.mk X + Cardinal.mk X := by
658 simp only [Cardinal.mk_finset_of_infinite X, Cardinal.add_mk_eq_max, max_self]
659 _ = Cardinal.mk X := Cardinal.add_eq_self (Cardinal.aleph0_le_mk X)
660 have hlower : Cardinal.mk X ≤ rho (OnePoint X) := by
661 let singletonClopen : X → { U : Set (OnePoint X) // IsClopen U } := fun x =>
662 ⟨({(x : OnePoint X)} : Set (OnePoint X)), by
663 constructor
664 · rw [← Set.image_singleton]
665 exact (OnePoint.isClosed_image_coe (s := ({x} : Set X))).2
666 ⟨(Set.finite_singleton x).isClosed, (Set.finite_singleton x).isCompact⟩
667 · rw [← Set.image_singleton]
668 exact (OnePoint.isOpen_image_coe (s := ({x} : Set X))).2
669 (isOpen_discrete ({x} : Set X))⟩
670 have hsingle_inj : Function.Injective singletonClopen := by
671 intro x y hxy
672 have hset :
673 ({(x : OnePoint X)} : Set (OnePoint X)) = ({(y : OnePoint X)} : Set (OnePoint X)) :=
674 congrArg Subtype.val hxy
675 simpa using Set.singleton_injective hset
677 exact Cardinal.mk_le_of_injective (f := singletonClopen) hsingle_inj
678 exact le_antisymm hupper hlower
681 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
682 (X : Set G) (hG : IsProfiniteGroup G)
683 (hX : GeneratesAndConvergesToOne (G := G) X) (hXinfinite : Set.Infinite X)
684 (hclosure : closure X = X ∪ ({1} : Set G)) :
685 rho ↥(closure X) = Cardinal.mk X := by
686 letI : T2Space G := IsProfiniteGroup.t2Space hG
687 by_cases h1X : (1 : G) ∈ X
688 · let Y : Set G := X \ ({1} : Set G)
689 have hYunion : Y ∪ ({1} : Set G) = X := by
690 ext x
691 by_cases hx : x = 1
692 · subst hx
693 simp only [union_singleton, h1X, insert_diff_self_of_mem, Y]
694 · simp only [union_singleton, insert_diff_singleton, mem_insert_iff, hx, false_or, Y]
695 have hYinf : Set.Infinite Y := by
696 by_contra hfin
697 have hXfin : Set.Finite X := by
698 rw [← hYunion]
699 exact (Set.not_infinite.mp hfin).union (Set.finite_singleton 1)
700 exact hXinfinite hXfin
701 have hYconv : ConvergesToOne (G := G) Y := by
702 have hconvUnion : ConvergesToOne (G := G) (Y ∪ ({1} : Set G)) := by
703 simpa [hYunion] using hX.2
704 exact (ConvergesToOne.union_one_iff (G := G) (X := Y)).1 hconvUnion
705 have hclosureY : closure Y = X := by
706 calc
707 closure Y = Y ∪ ({1} : Set G) := by
708 exact (closure_generatorsConvergingToOne (G := G) hG hYconv).2 hYinf
709 _ = X := hYunion
710 have h1notY : (1 : G) ∉ Y := by
711 simp only [mem_diff, mem_singleton_iff, not_true_eq_false, and_false, not_false_eq_true, Y]
712 letI : Infinite Y := Set.infinite_coe_iff.mpr hYinf
713 have hYdiff : Y \ ({1} : Set G) = Y := by
714 ext y
715 by_cases hy : y = 1
716 · subst hy
717 simp only [sdiff_idem, mem_diff, mem_singleton_iff, not_true_eq_false, and_false, Y]
718 · simp only [sdiff_idem, mem_diff, mem_singleton_iff, hy, not_false_eq_true, and_true, Y]
719 have hdiscY : IsDiscrete Y := by
720 rcases closure_generatorsConvergingToOne (G := G) hG hYconv with ⟨hdisc, _⟩
721 simpa [hYdiff] using hdisc
722 letI : DiscreteTopology ↥Y := (isDiscrete_iff_discreteTopology).mp hdiscY
723 have hinsertY : Set.insert (1 : G) Y = X := by
724 ext y
725 constructor
726 · intro hy
727 rcases Set.mem_insert_iff.mp hy with rfl | hyY
728 · exact h1X
729 · exact hyY.1
730 · intro hyX
731 by_cases hy : y = 1
732 · exact Set.mem_insert_iff.mpr (Or.inl hy)
733 · exact Set.mem_insert_iff.mpr (Or.inr (by simpa [Y, hy] using hyX))
734 have hcardY : Cardinal.mk Y = Cardinal.mk X := by
735 calc
736 Cardinal.mk Y = Cardinal.mk Y + 1 := by
737 symm
738 exact Cardinal.add_one_eq (Cardinal.aleph0_le_mk Y)
739 _ = Cardinal.mk (Set.insert (1 : G) Y) := by
740 simpa using (Cardinal.mk_insert h1notY).symm
741 _ = Cardinal.mk X := Cardinal.mk_congr (Equiv.setCongr hinsertY)
742 have hclosureX_eq : closure X = X := by
743 simpa [Set.insert_eq_of_mem h1X] using hclosure
744 have hclosureXY : closure X = closure Y := by
745 rw [hclosureX_eq, hclosureY]
746 calc
747 rho ↥(closure X) = rho ↥(closure Y) := by
748 exact rho_eq_of_homeomorph _ _ (Homeomorph.setCongr hclosureXY)
749 _ = rho (OnePoint Y) := by
752 (G := G) hG hYconv hYinf h1notY).symm)
754 _ = Cardinal.mk X := hcardY
755 · letI : Infinite X := Set.infinite_coe_iff.mpr hXinfinite
756 have hXdiff : X \ ({1} : Set G) = X := by
757 ext x
758 by_cases hx : x = 1
759 · subst hx
760 simp only [h1X, not_false_eq_true, diff_singleton_eq_self]
761 · simp only [mem_diff, mem_singleton_iff, hx, not_false_eq_true, and_true]
762 have hdiscX : IsDiscrete X := by
763 rcases closure_generatorsConvergingToOne (G := G) hG hX.2 with ⟨hdisc, _⟩
764 simpa [hXdiff] using hdisc
765 letI : DiscreteTopology ↥X := (isDiscrete_iff_discreteTopology).mp hdiscX
766 calc
767 rho ↥(closure X) = rho (OnePoint X) := by
770 (G := G) hG hX.2 hXinfinite h1X).symm)
774 {X : Type u} [TopologicalSpace X] {x : X} {κ : Cardinal}
775 (hcount : localWeightAt (X := X) x ≤ κ) :
776 ∃ B : Set (Set X), IsNeighborhoodBasisAt (X := X) x B ∧ familyCardinal (X := X) B ≤ κ := by
777 let B0 : Set (Set X) := {V | IsOpen V ∧ x ∈ V}
778 have hB0 : IsNeighborhoodBasisAt (X := X) x B0 := by
779 constructor
780 · intro U hU
781 exact hU
782 · intro V hVopen hVx
783 exact ⟨V, ⟨hVopen, hVx⟩, subset_rfl⟩
784 have hS : Set.Nonempty
785 {κ' : Cardinal | ∃ B : Set (Set X), IsNeighborhoodBasisAt (X := X) x B ∧
786 familyCardinal (X := X) B ≤ κ'} := by
787 refine ⟨familyCardinal (X := X) B0, ?_⟩
788 exact ⟨B0, hB0, le_rfl⟩
789 rcases (show
790 ∃ B : Set (Set X), IsNeighborhoodBasisAt (X := X) x B ∧
791 familyCardinal (X := X) B ≤ localWeightAt (X := X) x from by
792 simpa [localWeightAt] using (csInf_mem (s := {κ' : Cardinal | ∃ B : Set (Set X),
793 IsNeighborhoodBasisAt (X := X) x B ∧ familyCardinal (X := X) B ≤ κ'}) hS)
794 ) with ⟨B, hBbasis, hBcard⟩
795 exact ⟨B, hBbasis, hBcard.trans hcount⟩
797/-- Open maps do not increase local weight at the image point. -/
799 {X : Type u} {Y : Type u} [TopologicalSpace X] [TopologicalSpace Y]
800 {f : X → Y} {x : X} (hfcont : Continuous f) (hfopen : IsOpenMap f) :
801 localWeightAt (X := Y) (f x) ≤ localWeightAt (X := X) x := by
803 (X := X) (x := x) (κ := localWeightAt (X := X) x) le_rfl with
804 ⟨B, hBbasis, hBcard⟩
805 let ι : Type u := { U : Set X // U ∈ B }
806 let C : Set (Set Y) := Set.range fun i : ι => f '' i.1
807 have hCbasis : IsNeighborhoodBasisAt (X := Y) (f x) C := by
808 constructor
809 · intro V hV
810 rcases hV with ⟨i, rfl⟩
811 constructor
812 · exact hfopen _ ((hBbasis.1 i.1 i.2).1)
813 · exact ⟨x, (hBbasis.1 i.1 i.2).2, rfl⟩
814 · intro V hVopen hfxV
815 have hpreOpen : IsOpen (f ⁻¹' V) := hVopen.preimage hfcont
816 have hxpre : x ∈ f ⁻¹' V := hfxV
817 rcases hBbasis.2 (f ⁻¹' V) hpreOpen hxpre with ⟨U, hUB, hUsub⟩
818 refine ⟨f '' U, ?_, ?_⟩
819 · exact ⟨⟨U, hUB⟩, rfl⟩
820 · rintro y ⟨z, hzU, rfl⟩
821 exact hUsub hzU
822 have hCcard : familyCardinal (X := Y) C ≤ localWeightAt (X := X) x := by
823 calc
824 familyCardinal (X := Y) C ≤ Cardinal.mk ι := by
826 exact Cardinal.mk_range_le
827 _ = familyCardinal (X := X) B := by rfl
828 _ ≤ localWeightAt (X := X) x := hBcard
829 exact (localWeightAt_le_familyCardinal_of_basis (X := Y) (x := f x) hCbasis).trans hCcard
831/-- In a profinite group, the identity admits a neighborhood basis of open normal subgroups whose
832indexing cardinality is bounded by `w₀(G)`.
833-/
835 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
837 ∃ ι : Type u, ∃ W : ι → OpenNormalSubgroup G,
838 IsNeighborhoodBasisAt (X := G) (1 : G)
839 (Set.range fun i : ι => (((W i : Subgroup G) : Set G))) ∧
840 Cardinal.mk ι ≤ localWeight G := by
841 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
842 letI : T2Space G := IsProfiniteGroup.t2Space hG
843 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
845 (X := G) (x := (1 : G)) (κ := localWeight G) le_rfl with
846 ⟨B, hBbasis, hBcard⟩
847 let ι : Type u := { U : Set G // U ∈ B }
848 have hchoose :
849 ∀ i : ι, ∃ N : OpenNormalSubgroup G, (N : Set G) ⊆ i.1 := by
850 intro i
851 have hi : IsOpen i.1 ∧ (1 : G) ∈ i.1 := hBbasis.1 i.1 i.2
853 ⟨N, hN⟩
854 exact ⟨N, hN⟩
855 choose W hW using hchoose
856 refine ⟨ι, W, ?_, ?_⟩
857 · constructor
858 · intro U hU
859 rcases hU with ⟨i, rfl⟩
860 exact ⟨openNormalSubgroup_isOpen (G := G) (W i), (W i).one_mem'⟩
861 · intro V hVopen h1V
862 rcases hBbasis.2 V hVopen h1V with ⟨U, hUB, hUV⟩
863 refine ⟨((W ⟨U, hUB⟩ : Subgroup G) : Set G), ?_, ?_⟩
864 · exact ⟨⟨U, hUB⟩, rfl⟩
865 · exact (hW ⟨U, hUB⟩).trans hUV
866 · simpa [familyCardinal, ι] using hBcard
868/-- In a pro-`C` group, the identity admits a neighborhood basis of open normal subgroups whose
869quotients lie in `C`, still indexed by at most `w₀(G)`. -/
871 (C : FiniteGroupClass.{u}) (G : Type u)
872 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
873 (hG : IsProCGroup C G) :
874 ∃ ι : Type u, ∃ W : ι → OpenNormalSubgroup G,
875 (∀ i, C (G ⧸ (W i : Subgroup G))) ∧
876 IsNeighborhoodBasisAt (X := G) (1 : G)
877 (Set.range fun i : ι => (((W i : Subgroup G) : Set G))) ∧
878 Cardinal.mk ι ≤ localWeight G := by
880 ⟨ι, W, hWbasis, hWcard⟩
881 have hchoose :
882 ∀ i : ι, ∃ U : OpenNormalSubgroup G,
883 C (G ⧸ (U : Subgroup G)) ∧ (((U : Subgroup G) : Set G)) ⊆ ((W i : Subgroup G) : Set G) := by
884 intro i
885 rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one
886 (openNormalSubgroup_isOpen (G := G) (W i)) (W i).one_mem' with ⟨U, hUW⟩
887 exact ⟨U.1, U.2, hUW⟩
888 choose U hUC hUsub using hchoose
889 refine ⟨ι, U, hUC, ?_, hWcard⟩
890 constructor
891 · intro V hV
892 rcases hV with ⟨i, rfl⟩
893 exact ⟨openNormalSubgroup_isOpen (G := G) (U i), (U i).one_mem'⟩
894 · intro V hVopen hVone
895 rcases hWbasis.2 V hVopen hVone with ⟨W', hW'range, hW'sub⟩
896 rcases hW'range with ⟨i, rfl⟩
897 refine ⟨((U i : Subgroup G) : Set G), ?_, (hUsub i).trans hW'sub⟩
898 exact ⟨i, rfl⟩
900/-- A neighborhood basis at `1` consisting of open normal subgroups has trivial intersection. -/
902 (G : Type u) [Group G] [TopologicalSpace G] [T2Space G]
903 {ι : Type v} (W : ι → OpenNormalSubgroup G)
904 (hWbasis : IsNeighborhoodBasisAt (X := G) (1 : G)
905 (Set.range fun i : ι => (((W i : Subgroup G) : Set G)))) :
906 iInf (fun i => (W i : Subgroup G)) = (⊥ : Subgroup G) := by
907 ext x
908 constructor
909 · intro hx
910 by_cases hx1 : x = 1
911 · simp only [hx1, one_mem]
912 · have hxall : ∀ i : ι, x ∈ (W i : Subgroup G) := by
913 rw [Subgroup.mem_iInf] at hx
914 exact hx
915 have hOpen : IsOpen ({x}ᶜ : Set G) := isClosed_singleton.isOpen_compl
916 have hOne : (1 : G) ∈ ({x}ᶜ : Set G) := by
917 simpa [Set.mem_compl_iff, eq_comm] using hx1
918 rcases hWbasis.2 ({x}ᶜ : Set G) hOpen hOne with ⟨U, hUrange, hUsub⟩
919 rcases hUrange with ⟨i, rfl⟩
920 have : x ∈ ({x}ᶜ : Set G) := hUsub (hxall i)
921 simp only [mem_compl_iff, mem_singleton_iff, not_true_eq_false] at this
922 · intro hx
923 have hx1 : x = 1 := by
924 exact Subgroup.mem_bot.mp hx
925 simp only [hx1, one_mem]
927/-- A closed topological generating subset of an infinite profinite group has clopen cardinal at
928least the local weight.
929-/
931 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
932 (X : Set G) (hG : IsProfiniteGroup G) (hXclosed : IsClosed X)
933 (hXgen : TopologicallyGenerates (G := G) X) (hXinfinite : Set.Infinite X) :
934 localWeight G ≤ rho ↥X := by
935 classical
936 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
937 letI : T2Space G := IsProfiniteGroup.t2Space hG
938 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
939 letI : CompactSpace ↥X := by
940 simpa using hXclosed.isClosedEmbedding_subtypeVal.compactSpace
941 letI : T2Space ↥X := by infer_instance
942 letI : TotallyDisconnectedSpace ↥X := by infer_instance
943 letI : Infinite ↥X := hXinfinite.to_subtype
945 ⟨ι, W, hWbasis, _hWcard⟩
946 let B : Set (Set G) := Set.range fun i : ι => (((W i : Subgroup G) : Set G))
947 have hBbasis : IsNeighborhoodBasisAt (X := G) (1 : G) B := by
948 simpa [B] using hWbasis
949 have hRhoAleph : ℵ₀ ≤ rho ↥X := by
950 have hBasis : IsTopologicalBasis { U : Set ↥X | IsClopen U } :=
952 have hInfClopen :
953 Infinite { U : Set ↥X // U ∈ ({ U : Set ↥X | IsClopen U } : Set (Set ↥X)) } :=
955 (B := ({ U : Set ↥X | IsClopen U } : Set (Set ↥X))) hBasis
956 letI : Infinite { U : Set ↥X // IsClopen U } := by
957 change Infinite { U : Set ↥X // U ∈ ({ U : Set ↥X | IsClopen U } : Set (Set ↥X)) }
958 exact hInfClopen
960 exact Cardinal.aleph0_le_mk { U : Set ↥X // IsClopen U }
961 have hBcard : familyCardinal (X := G) B ≤ rho ↥X := by
962 let rep : { V : Set G // V ∈ B } → ι :=
963 fun V => Classical.choose V.2
964 have hrep : ∀ V : { V : Set G // V ∈ B }, (((W (rep V) : Subgroup G) : Set G)) = V.1 := by
965 intro V
966 exact Classical.choose_spec V.2
967 let homCode : { V : Set G // V ∈ B } → Σ n : ℕ, ContinuousMonoidHom G (Equiv.Perm (Fin n)) :=
968 fun V => by
969 let U : OpenNormalSubgroup G := W (rep V)
970 let n : ℕ := Nat.card (G ⧸ (U : Subgroup G))
971 let φ : ContinuousMonoidHom G (Equiv.Perm (Fin n)) :=
972 openSubgroupIndexContinuousHom (G := G) (U : Subgroup G)
974 (show Nat.card (G ⧸ (U : Subgroup G)) = n from by simp only [n])
975 exact ⟨n, φ⟩
976 have hhomCode_inj : Function.Injective homCode := by
977 intro V₁ V₂ hEq
978 let U₁ : OpenNormalSubgroup G := W (rep V₁)
979 let U₂ : OpenNormalSubgroup G := W (rep V₂)
980 let n₁ : ℕ := Nat.card (G ⧸ (U₁ : Subgroup G))
981 let n₂ : ℕ := Nat.card (G ⧸ (U₂ : Subgroup G))
982 have hn₁ : Nat.card (G ⧸ (U₁ : Subgroup G)) = n₁ := by simp only [n₁]
983 have hn₂ : Nat.card (G ⧸ (U₂ : Subgroup G)) = n₂ := by simp only [n₂]
984 let φ₁ : ContinuousMonoidHom G (Equiv.Perm (Fin n₁)) :=
985 openSubgroupIndexContinuousHom (G := G) (U₁ : Subgroup G)
986 (openNormalSubgroup_isOpen (G := G) U₁) hn₁
987 let φ₂ : ContinuousMonoidHom G (Equiv.Perm (Fin n₂)) :=
988 openSubgroupIndexContinuousHom (G := G) (U₂ : Subgroup G)
989 (openNormalSubgroup_isOpen (G := G) U₂) hn₂
990 have hEq' :
991 (Sigma.mk n₁ φ₁ : Σ n : ℕ, ContinuousMonoidHom G (Equiv.Perm (Fin n))) =
992 (Sigma.mk n₂ φ₂ : Σ n : ℕ, ContinuousMonoidHom G (Equiv.Perm (Fin n))) := by
993 simpa [homCode, U₁, U₂, n₁, n₂, φ₁, φ₂] using hEq
994 have hker₁ : (φ₁.ker : Subgroup G) = (U₁ : Subgroup G) := by
995 have hU₁finite : Finite (G ⧸ (U₁ : Subgroup G)) :=
996 Subgroup.quotient_finite_of_isOpen (U₁ : Subgroup G)
998 let e := openSubgroupIndexEquiv (G := G) (U₁ : Subgroup G)
999 hU₁finite hn₁
1000 have hkerAction :
1001 (φ₁.ker : Subgroup G) =
1002 (MulAction.toPermHom G (G ⧸ (U₁ : Subgroup G))).ker := by
1003 ext g
1004 change e.permCongr (MulAction.toPerm g) = 1 ↔ MulAction.toPerm g = 1
1005 have hperm_one :
1006 e.permCongr (1 : Equiv.Perm (G ⧸ (U₁ : Subgroup G))) =
1007 (1 : Equiv.Perm (Fin n₁)) := by
1008 ext x
1009 simp only [Equiv.permCongr_apply, Equiv.Perm.coe_one, id_eq, Equiv.apply_symm_apply]
1010 rw [← hperm_one]
1011 exact e.permCongr.injective.eq_iff
1012 letI : ((U₁ : Subgroup G)).Normal := U₁.isNormal'
1013 calc
1014 (φ₁.ker : Subgroup G) = (MulAction.toPermHom G (G ⧸ (U₁ : Subgroup G))).ker :=
1015 hkerAction
1016 _ = (U₁ : Subgroup G).normalCore := by
1017 symm
1018 exact Subgroup.normalCore_eq_ker (H := (U₁ : Subgroup G))
1019 _ = (U₁ : Subgroup G) := Subgroup.normalCore_eq_self (U₁ : Subgroup G)
1020 have hker₂ : (φ₂.ker : Subgroup G) = (U₂ : Subgroup G) := by
1021 have hU₂finite : Finite (G ⧸ (U₂ : Subgroup G)) :=
1022 Subgroup.quotient_finite_of_isOpen (U₂ : Subgroup G)
1024 let e := openSubgroupIndexEquiv (G := G) (U₂ : Subgroup G)
1025 hU₂finite hn₂
1026 have hkerAction :
1027 (φ₂.ker : Subgroup G) =
1028 (MulAction.toPermHom G (G ⧸ (U₂ : Subgroup G))).ker := by
1029 ext g
1030 change e.permCongr (MulAction.toPerm g) = 1 ↔ MulAction.toPerm g = 1
1031 have hperm_one :
1032 e.permCongr (1 : Equiv.Perm (G ⧸ (U₂ : Subgroup G))) =
1033 (1 : Equiv.Perm (Fin n₂)) := by
1034 ext x
1035 simp only [Equiv.permCongr_apply, Equiv.Perm.coe_one, id_eq, Equiv.apply_symm_apply]
1036 rw [← hperm_one]
1037 exact e.permCongr.injective.eq_iff
1038 letI : ((U₂ : Subgroup G)).Normal := U₂.isNormal'
1039 calc
1040 (φ₂.ker : Subgroup G) = (MulAction.toPermHom G (G ⧸ (U₂ : Subgroup G))).ker :=
1041 hkerAction
1042 _ = (U₂ : Subgroup G).normalCore := by
1043 symm
1044 exact Subgroup.normalCore_eq_ker (H := (U₂ : Subgroup G))
1045 _ = (U₂ : Subgroup G) := Subgroup.normalCore_eq_self (U₂ : Subgroup G)
1046 have hkerEq : (φ₁.ker : Subgroup G) = (φ₂.ker : Subgroup G) := by
1047 exact congrArg (fun p : Σ n : ℕ, ContinuousMonoidHom G (Equiv.Perm (Fin n)) =>
1048 (p.2.ker : Subgroup G)) hEq'
1049 have hsub :
1050 (U₁ : Subgroup G) = (U₂ : Subgroup G) := by
1051 calc
1052 (U₁ : Subgroup G) = (φ₁.ker : Subgroup G) := hker₁.symm
1053 _ = (φ₂.ker : Subgroup G) := hkerEq
1054 _ = (U₂ : Subgroup G) := hker₂
1055 apply Subtype.ext
1056 calc
1057 V₁.1 = (((U₁ : Subgroup G) : Set G)) := (hrep V₁).symm
1058 _ = (((U₂ : Subgroup G) : Set G)) := by simp only [hsub, OpenSubgroup.coe_toSubgroup]
1059 _ = V₂.1 := hrep V₂
1060 have hhom_le :
1061 Cardinal.mk (Σ n : ℕ, ContinuousMonoidHom G (Equiv.Perm (Fin n))) ≤
1062 Cardinal.mk (Σ n : ℕ, C(↥X, Equiv.Perm (Fin n))) := by
1063 refine Cardinal.mk_le_of_injective
1064 (f := fun p => ⟨p.1, {
1065 toFun := fun x => p.2 x.1
1066 continuous_toFun := p.2.continuous_toFun.comp continuous_subtype_val }⟩) ?_
1067 intro a b h
1068 cases a with
1069 | mk n φ =>
1070 cases b with
1071 | mk m ψ =>
1072 have hnm : n = m := (Sigma.mk.inj_iff.mp h).1
1073 subst m
1074 have hrest :
1075 ({ toFun := fun x : X => φ x.1
1076 continuous_toFun := φ.continuous_toFun.comp continuous_subtype_val } :
1077 C(↥X, Equiv.Perm (Fin n))) =
1078 { toFun := fun x : X => ψ x.1
1079 continuous_toFun := ψ.continuous_toFun.comp continuous_subtype_val } := by
1080 exact eq_of_heq (Sigma.mk.inj_iff.mp h).2
1081 have hEqOn : Set.EqOn φ ψ X := by
1082 intro x hx
1083 have := congrArg (fun f : C(↥X, Equiv.Perm (Fin n)) => f ⟨x, hx⟩) hrest
1084 exact this
1085 have hφ : φ = ψ :=
1087 (G := G) hXgen hEqOn
1088 subst hφ
1089 rfl
1090 have hsigma_le :
1091 Cardinal.mk (Σ n : ℕ, C(↥X, Equiv.Perm (Fin n))) ≤ rho ↥X := by
1092 let ρ : Cardinal := rho ↥X
1093 let f : ℕ → Cardinal := fun n => Cardinal.mk (C(↥X, Equiv.Perm (Fin n)))
1094 have hf_le : ∀ n, f n ≤ ρ := by
1095 intro n
1096 simpa [f, ρ] using
1097 (cardinal_continuousMap_to_finite_le_rho (X := ↥X) (H := Equiv.Perm (Fin n)))
1098 calc
1099 Cardinal.mk (Σ n : ℕ, C(↥X, Equiv.Perm (Fin n))) = Cardinal.sum f := by
1100 exact Cardinal.mk_sigma (fun n : ℕ => C(↥X, Equiv.Perm (Fin n)))
1101 _ ≤ Cardinal.sum (fun _ : ℕ => ρ) := by
1102 apply Cardinal.sum_le_sum
1103 intro n
1104 exact hf_le n
1105 _ = Cardinal.lift.{u} ℵ₀ * ρ := by
1106 convert (Cardinal.sum_const.{0, u} ℕ ρ) using 1
1107 simp only [Cardinal.lift_id, Cardinal.mk_eq_aleph0, Cardinal.lift_aleph0, Cardinal.lift_uzero, ρ]
1108 _ = ρ := by
1109 rw [Cardinal.lift_id, mul_comm]
1110 simpa [ρ] using Cardinal.mul_aleph0_eq hRhoAleph
1111 _ = rho ↥X := by rfl
1113 exact ((Cardinal.mk_le_of_injective (f := homCode) hhomCode_inj).trans hhom_le).trans hsigma_le
1114 simpa [localWeight, B] using
1115 (localWeightAt_le_familyCardinal_of_basis (X := G) (x := (1 : G)) hBbasis).trans hBcard
1117/-- An infinite profinite group has local weight at least `ℵ₀`.
1120 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Infinite G]
1122 ℵ₀ ≤ localWeight G := by
1123 by_contra h
1124 have hlt : localWeight G < ℵ₀ := lt_of_not_ge h
1125 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
1126 letI : T2Space G := IsProfiniteGroup.t2Space hG
1127 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
1129 (G := G) hG with ⟨ι, W, hWbasis, hWcard⟩
1130 have hιfinite : Finite ι := by
1131 exact Cardinal.lt_aleph0_iff_finite.mp (lt_of_le_of_lt hWcard hlt)
1132 letI : Finite ι := hιfinite
1133 let U : Set G := ⋂ i : ι, (((W i : Subgroup G) : Set G))
1134 have hUopen : IsOpen U := by
1135 refine isOpen_iInter_of_finite ?_
1136 intro i
1137 exact openNormalSubgroup_isOpen (G := G) (W i)
1138 have h1U : (1 : G) ∈ U := by
1139 refine Set.mem_iInter.2 ?_
1140 intro i
1141 exact (W i).one_mem'
1142 have hUsubset : U ⊆ ({1} : Set G) := by
1143 intro x hx
1144 by_cases hx1 : x = 1
1145 · simp only [hx1, mem_singleton_iff]
1146 · have hVopen : IsOpen ({x}ᶜ : Set G) := by
1147 exact (isClosed_singleton : IsClosed ({x} : Set G)).isOpen_compl
1148 have h1V : (1 : G) ∈ ({x}ᶜ : Set G) := by
1149 simpa [eq_comm] using hx1
1150 rcases hWbasis.2 ({x}ᶜ : Set G) hVopen h1V with ⟨V, hVrange, hVsub⟩
1151 rcases hVrange with ⟨i, rfl⟩
1152 have hxi : x ∈ (((W i : Subgroup G) : Set G)) := by
1153 exact Set.mem_iInter.mp hx i
1154 have : x ∈ ({x}ᶜ : Set G) := hVsub hxi
1155 simp only [mem_compl_iff, mem_singleton_iff, not_true_eq_false] at this
1156 have hsingleton_subset : ({1} : Set G) ⊆ U := by
1157 intro x hx
1158 rcases Set.mem_singleton_iff.mp hx with rfl
1159 exact h1U
1160 have hUeq : U = ({1} : Set G) := Subset.antisymm hUsubset hsingleton_subset
1161 have hOneOpen : IsOpen ({1} : Set G) := by
1162 simpa [hUeq] using hUopen
1163 letI : DiscreteTopology G := discreteTopology_of_isOpen_singleton_one hOneOpen
1164 have hfinite : Finite G := finite_of_compact_of_discrete
1165 letI : Finite G := hfinite
1166 exact not_finite G
1170/-- 6.1(b). Local weight equals weight for an infinite profinite group.
1173 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Infinite G]
1175 localWeight G = weight G := by
1176 classical
1177 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
1178 letI : T2Space G := IsProfiniteGroup.t2Space hG
1179 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
1180 have hAleph : ℵ₀ ≤ localWeight G :=
1183 (G := G) hG with ⟨ι, W, hWbasis, hWcard⟩
1184 let B : Set (Set G) := Set.range fun i : ι => (((W i : Subgroup G) : Set G))
1185 have hBbasis : IsNeighborhoodBasisAt (X := G) (1 : G) B := by
1186 simpa [B] using hWbasis
1187 have hweight_le :
1188 weight G ≤ familyCardinal (X := G) (leftTranslateFamily (G := G) B) :=
1190 (G := G) hBbasis
1191 let decode :
1192 (Σ i : ι, G ⧸ (W i : Subgroup G)) →
1193 { V : Set G // V ∈ leftTranslateFamily (G := G) B } := fun p =>
1194 ⟨Quotient.out p.2 • (((W p.1 : Subgroup G) : Set G)), by
1195 exact ⟨Quotient.out p.2, (((W p.1 : Subgroup G) : Set G)), ⟨p.1, rfl⟩, rfl⟩⟩
1196 have hdecode_surj : Function.Surjective decode := by
1197 intro V
1198 rcases V with ⟨V, hV⟩
1199 rcases hV with ⟨g, U, hU, hVeq⟩
1200 rcases hU with ⟨i, hi⟩
1201 refine ⟨⟨i, (QuotientGroup.mk' (W i : Subgroup G)) g⟩, ?_⟩
1202 apply Subtype.ext
1203 have hquot :
1204 (QuotientGroup.mk' (W i : Subgroup G))
1205 (Quotient.out ((QuotientGroup.mk' (W i : Subgroup G)) g)) =
1206 (QuotientGroup.mk' (W i : Subgroup G)) g := by
1207 exact Quotient.out_eq' ((QuotientGroup.mk' (W i : Subgroup G)) g)
1208 have hmem :
1209 (Quotient.out ((QuotientGroup.mk' (W i : Subgroup G)) g))⁻¹ * g ∈ (W i : Subgroup G) :=
1210 (QuotientGroup.eq).1 hquot
1211 calc
1212 ↑(decode ⟨i, (QuotientGroup.mk' (W i : Subgroup G)) g⟩) =
1213 Quotient.out ((QuotientGroup.mk' (W i : Subgroup G)) g) •
1214 (((W i : Subgroup G) : Set G)) := by
1215 rfl
1216 _ = g • (((W i : Subgroup G) : Set G)) := by
1217 simpa using (leftCoset_eq_iff (s := (W i : Subgroup G))).2 hmem
1218 _ = g • U := by
1219 simp only [hi]
1220 _ = V := hVeq.symm
1221 have htranslate_card :
1222 familyCardinal (X := G) (leftTranslateFamily (G := G) B) ≤ localWeight G := by
1224 calc
1225 Cardinal.mk { V : Set G // V ∈ leftTranslateFamily (G := G) B } ≤
1226 Cardinal.mk (Σ i : ι, G ⧸ (W i : Subgroup G)) :=
1227 Cardinal.mk_le_of_surjective (f := decode) hdecode_surj
1228 _ = Cardinal.sum (fun i : ι => Cardinal.mk (G ⧸ (W i : Subgroup G))) := by
1229 exact Cardinal.mk_sigma (fun i : ι => G ⧸ (W i : Subgroup G))
1230 _ ≤ Cardinal.sum (fun _ : ι => ℵ₀) := by
1231 refine Cardinal.sum_le_sum _ _ ?_
1232 intro i
1233 letI : Finite (G ⧸ (W i : Subgroup G)) :=
1235 exact Cardinal.mk_le_aleph0_iff.mpr inferInstance
1236 _ = Cardinal.mk ι * ℵ₀ := by
1237 exact Cardinal.sum_const' ι ℵ₀
1238 _ ≤ localWeight G * localWeight G := by
1239 exact mul_le_mul' hWcard hAleph
1240 _ = localWeight G := Cardinal.mul_eq_self hAleph
1241 exact le_antisymm (localWeight_le_weight (G := G)) (hweight_le.trans htranslate_card)
1246/-- For an infinite profinite space, the weight agrees with the clopen cardinal invariant, and
1247every clopen basis has the same cardinality. -/
1249 (X : Type u) [TopologicalSpace X] [Infinite X] :
1251 weight X = rho X ∧
1252 ∀ B : Set (Set X), IsTopologicalBasis B → (∀ U ∈ B, IsClopen U) →
1253 familyCardinal (X := X) B = rho X := by
1254 intro hX
1256 ⟨hcompact, hT2, hBasis⟩
1257 letI : CompactSpace X := hcompact
1258 letI : T2Space X := hT2
1259 refine ⟨weight_eq_rho_of_clopenBasis (X := X) hBasis, ?_⟩
1260 intro B hB hBclopen
1261 exact familyCardinal_eq_rho_of_clopenBasis (X := X) hB hBclopen
1263/-- For an infinite profinite group, local weight, weight, and the clopen cardinal invariant all
1264coincide. -/
1266 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Infinite G] :
1268 localWeight G = weight G ∧ weight G = rho G := by
1269 intro hG
1270 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
1271 letI : T2Space G := IsProfiniteGroup.t2Space hG
1272 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
1273 have hBasis : TopologicalSpace.IsTopologicalBasis { U : Set G | IsClopen U } :=
1276 exact weight_eq_rho_of_clopenBasis (X := G) hBasis
1280end ProCGroups.LocalWeight