ProCGroups/LocalWeight/GeneratingSetsConvergingToOne.lean
1import ProCGroups.LocalWeight.LocalWeightTheorems
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/LocalWeight/GeneratingSetsConvergingToOne.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
14Studies local weight, metrizability, quotient size bounds, and cardinal invariants of profinite groups.
15-/
17open Set
18open TopologicalSpace
19open Order
20open scoped Cardinal
21open scoped Topology Pointwise
23namespace ProCGroups.LocalWeight
25universe u
27open ProCGroups.Generation ProCGroups.ProC ProCGroups.FiniteGeneration
30/-- A generating set converging to `1` is countable exactly when the profinite group admits a
31countable descending open-normal chain at the identity. -/
33 {G : Type u}
34 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
35 (X : Set G) :
36 IsProfiniteGroup G →
37 GeneratesAndConvergesToOne (G := G) X →
38 (Cardinal.mk X ≤ ℵ₀ ↔
40 intro hG hX
41 constructor
42 · intro hXcount
43 by_cases hXinfinite : Set.Infinite X
44 · have hlocal : localWeight G ≤ ℵ₀ := by
46 (G := G) X hG hX hXinfinite] using hXcount
48 (G := G) hG hlocal
49 · letI : Finite X := Set.not_infinite.mp hXinfinite
50 have hXfinite : X.Finite := Set.toFinite X
51 let s : Finset G := hXfinite.toFinset
52 have hsgen : TopologicallyFinitelyGenerated G := by
53 refine ⟨s, ?_⟩
54 simpa [s] using hX.1
55 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
56 letI : T2Space G := IsProfiniteGroup.t2Space hG
57 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
59 (G := G) hsgen
60 · intro hchain
61 rcases hchain with ⟨U, _hUanti, hUbasis⟩
62 have hBasis : IsNeighborhoodBasisAt (X := G) (1 : G)
63 (Set.range fun n : ℕ => (((U n : Subgroup G) : Set G))) := by
64 constructor
65 · intro V hV
66 rcases hV with ⟨n, rfl⟩
67 exact ⟨openNormalSubgroup_isOpen (G := G) (U n), (U n).one_mem'⟩
68 · intro V hVopen h1V
69 rcases hUbasis V hVopen h1V with ⟨n, hnV⟩
70 exact ⟨((U n : Subgroup G) : Set G), ⟨n, rfl⟩, hnV⟩
71 have hlocal : localWeight G ≤ ℵ₀ := by
72 calc
73 localWeight G ≤
74 familyCardinal (X := G) (Set.range fun n : ℕ => (((U n : Subgroup G) : Set G))) := by
75 simpa [localWeight] using
76 localWeightAt_le_familyCardinal_of_basis (X := G) (x := (1 : G)) hBasis
77 _ ≤ ℵ₀ := by
78 unfold familyCardinal
79 exact Cardinal.mk_le_aleph0_iff.mpr
80 (Set.countable_range (fun n : ℕ => (((U n : Subgroup G) : Set G))))
81 by_cases hXinfinite : Set.Infinite X
82 · calc
83 Cardinal.mk X = localWeight G :=
85 (G := G) X hG hX hXinfinite
86 _ ≤ ℵ₀ := hlocal
87 · letI : Finite X := Set.not_infinite.mp hXinfinite
88 exact ((Cardinal.lt_aleph0_iff_finite (α := X)).2 inferInstance).le
90/-- A profinite group is metrizable exactly when it admits a countable generating set converging
91to `1`. -/
93 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
94 IsProfiniteGroup G →
95 (Nonempty (MetrizableSpace G) ↔
96 ∃ X : Set G, GeneratesAndConvergesToOne (G := G) X ∧ Countable X) := by
97 intro hG
98 letI : T2Space G := IsProfiniteGroup.t2Space hG
99 constructor
100 · intro hmetr
101 rcases exists_generatorsConvergingToOne (G := G) hG with ⟨X, hX⟩
102 refine ⟨X, hX, ?_⟩
103 have hchain : ProCGroups.ProC.HasCountableOpenNormalBasisAtOne G := by
105 (G := G) hG).1 hmetr
106 have hXcount : Cardinal.mk X ≤ ℵ₀ := by
107 exact
109 (G := G) X)
110 hG hX).2 hchain
111 exact Cardinal.mk_le_aleph0_iff.mp hXcount
112 · rintro ⟨X, hX, hXcount⟩
113 have hchain : ProCGroups.ProC.HasCountableOpenNormalBasisAtOne G := by
114 exact
116 (G := G) X)
117 hG hX).1
118 (Cardinal.mk_le_aleph0_iff.mpr hXcount)
120 (G := G) hG).2 hchain
122end LocalWeight