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

Source: ProCGroups.LocalWeight.CardinalInvariantsAndLocalWeight

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