ProCGroups/LocalWeight/LocalWeightTheorems.lean
1import ProCGroups.LocalWeight.ClosedNormalDataAndTransfiniteSeries
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/LocalWeight/LocalWeightTheorems.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.ProC ProCGroups.Generation
28open ProCGroups.FiniteGeneration
31/-- 6.2(a). Closed generating subsets compute the local weight.
32-/
34 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
35 (X : Set G) (hG : IsProfiniteGroup G) (hXclosed : IsClosed X)
36 (hXgen : TopologicallyGenerates (G := G) X) (hXinfinite : Set.Infinite X) :
37 localWeight G = rho ↥X := by
38 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
39 letI : T2Space G := IsProfiniteGroup.t2Space hG
40 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
41 have hGinf : Infinite G := by
42 classical
43 by_contra hfin
44 letI : Finite G := not_infinite_iff_finite.mp hfin
45 exact hXinfinite (Set.toFinite X)
46 letI : Infinite G := hGinf
47 have hle : localWeight G ≤ rho ↥X :=
49 (G := G) X hG hXclosed hXgen hXinfinite
50 have hrho_le : rho ↥X ≤ localWeight G := by
51 have hBasis : TopologicalSpace.IsTopologicalBasis { U : Set G | IsClopen U } :=
53 calc
55 rho_subtype_le_rho_of_closed (X := G) (A := X) hXclosed
56 _ = weight G := (weight_eq_rho_of_clopenBasis (X := G) hBasis).symm
57 _ = localWeight G :=
58 (localWeight_eq_weight_of_infinite_profiniteGroup (G := G) hG).symm
59 exact le_antisymm hle hrho_le
61/-- 6.2(b). Infinite generating sets converging to `1` have cardinality `w₀(G)`.
62-/
64 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
65 (X : Set G) (hG : IsProfiniteGroup G)
66 (hX : GeneratesAndConvergesToOne (G := G) X) (hXinfinite : Set.Infinite X) :
67 Cardinal.mk X = localWeight G := by
68 letI : T2Space G := IsProfiniteGroup.t2Space hG
69 have hclosure : closure X = X ∪ ({1} : Set G) := by
70 exact (closure_generatorsConvergingToOne (G := G) hG hX.2).2 hXinfinite
71 have hClosureInf : Set.Infinite (closure X) := by
72 by_contra hfin
73 exact hXinfinite ((Set.not_infinite.mp hfin).subset subset_closure)
74 have hClosureGen : TopologicallyGenerates (G := G) (closure X) := by
75 exact (topologicallyGenerates_closure_iff (G := G) (X := X)).1 hX.1
76 have hClosureClosed : IsClosed (closure X) := isClosed_closure
77 calc
79 symm
81 (G := G) X hG hX hXinfinite hclosure
82 _ = localWeight G := by
83 simpa using
85 (G := G) (closure X) hG hClosureClosed hClosureGen hClosureInf).symm
90/-- 6.3. Infinite generator rank equals local weight.
91-/
93 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
94 (hG : IsProfiniteGroup G) (hdinf : Cardinal.aleph0 ≤ topologicalRank G) :
95 topologicalRank G = localWeight G := by
96 classical
97 obtain ⟨X, hX, hXle⟩ :=
99 (G := G) hG (κ := topologicalRank G) le_rfl
100 let C : Set Cardinal := {κ : Cardinal |
101 ∃ Y : Set G, GeneratesAndConvergesToOne (G := G) Y ∧ Cardinal.mk Y = κ}
102 have hd_le : topologicalRank G ≤ Cardinal.mk X := by
103 have hXmem : Cardinal.mk X ∈ C := by
104 exact ⟨X, hX, rfl⟩
105 simpa [topologicalRank, C] using (csInf_le' hXmem)
106 have hXcard : Cardinal.mk X = topologicalRank G := le_antisymm hXle hd_le
107 have hXinfinite : Set.Infinite X := by
108 refine setInfinite_of_cardinal_ge_aleph0 (X := X) ?_
109 calc
110 Cardinal.aleph0 ≤ topologicalRank G := hdinf
111 _ = Cardinal.mk X := hXcard.symm
112 calc
113 topologicalRank G = Cardinal.mk X := hXcard.symm
114 _ = localWeight G :=
116 (G := G) X hG hX hXinfinite
119end LocalWeight