Source: ProCGroups.LocalWeight.GeneratingSetsConvergingToOne
1import ProCGroups.LocalWeight.LocalWeightTheorems
3/-!
4# Generating sets converging to one
6Countable descending open-normal bases are characterized by generating sets that converge to the
7identity along open subgroups. For nonempty profinite groups this yields a characterization of
8metrizability by a countable convergent generating set.
9-/
11open Set
12open TopologicalSpace
13open Order
14open scoped Cardinal
15open scoped Topology Pointwise
17namespace ProCGroups.LocalWeight
19universe u
21open ProCGroups.Generation ProCGroups.ProC ProCGroups.FiniteGeneration
24/--
25A generating set converging to \(1\) is countable exactly when the profinite group admits a
26countable descending open-normal chain at the identity.
27-/
28theorem cardinal_le_aleph0_iff_hasCountableDescendingOpenNormalChainAtOne
29 {G : Type u}
30 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
32 (X : Set G) (hX : GeneratesAndConvergesToOneAlongOpenSubgroups (G := G) X) :
33 Cardinal.mk X ≤ ℵ₀ ↔
35 constructor
36 · intro hXcount
37 by_cases hXinfinite : Set.Infinite X
38 · have hlocal : localWeight G ≤ ℵ₀ := by
39 simpa [cardinalEqLocalWeight_of_generatesAndConvergesToOneAlongOpenSubgroups_infinite
40 (G := G) X hX hXinfinite] using hXcount
41 exact hasCountableDescendingOpenNormalChainAtOne_of_localWeight_le_aleph0
42 (G := G) hlocal
43 · letI : Finite X := Set.not_infinite.mp hXinfinite
44 have hXfinite : X.Finite := Set.toFinite X
45 let s : Finset G := hXfinite.toFinset
46 have hsgen : TopologicallyFinitelyGenerated G := by
47 refine ⟨s, ?_⟩
48 simpa [s] using hX.1
49 exact hasCountableDescendingOpenNormalChainAtOne_of_topologicallyFinitelyGenerated
50 (G := G) hsgen
51 · intro hchain
52 rcases hchain with ⟨U, _hUanti, hUbasis⟩
53 have hBasis : IsNeighborhoodBasisAt (X := G) (1 : G)
54 (Set.range fun n : ℕ => (((U n : Subgroup G) : Set G))) := by
55 constructor
56 · intro V hV
57 rcases hV with ⟨n, rfl⟩
58 exact ⟨openNormalSubgroup_isOpen (G := G) (U n), (U n).one_mem'⟩
59 · intro V hVopen h1V
60 rcases hUbasis V hVopen h1V with ⟨n, hnV⟩
61 exact ⟨((U n : Subgroup G) : Set G), ⟨n, rfl⟩, hnV⟩
62 have hlocal : localWeight G ≤ ℵ₀ := by
63 calc
64 localWeight G ≤
65 familyCardinal (X := G) (Set.range fun n : ℕ => (((U n : Subgroup G) : Set G))) := by
66 simpa [localWeight] using
67 localWeightAt_le_familyCardinal_of_basis (X := G) (x := (1 : G)) hBasis
68 _ ≤ ℵ₀ := by
69 unfold familyCardinal
70 exact Cardinal.mk_le_aleph0_iff.mpr
71 (Set.countable_range (fun n : ℕ => (((U n : Subgroup G) : Set G))))
72 by_cases hXinfinite : Set.Infinite X
73 · calc
74 Cardinal.mk X = localWeight G :=
75 cardinalEqLocalWeight_of_generatesAndConvergesToOneAlongOpenSubgroups_infinite
76 (G := G) X hX hXinfinite
77 _ ≤ ℵ₀ := hlocal
78 · letI : Finite X := Set.not_infinite.mp hXinfinite
79 exact ((Cardinal.lt_aleph0_iff_finite (α := X)).2 inferInstance).le
81/--
82A profinite group is metrizable exactly when it admits a countable generating set converging to
83\(1\).
84-/
85theorem nonempty_metrizableSpace_iff_exists_countable_generatingSetConvergingToOne
86 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
87 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] :
88 Nonempty (MetrizableSpace G) ↔
89 ∃ X : Set G, GeneratesAndConvergesToOneAlongOpenSubgroups (G := G) X ∧ Countable X := by
90 constructor
91 · intro hmetr
92 rcases exists_generatorsConvergingToOne (G := G) with ⟨X, hX⟩
93 refine ⟨X, hX, ?_⟩
94 have hchain : ProCGroups.ProC.HasCountableOpenNormalBasisAtOne G := by
95 exact (metrizable_iff_hasCountableDescendingOpenNormalChainAtOne
96 (G := G)).1 hmetr
97 have hXcount : Cardinal.mk X ≤ ℵ₀ := by
98 exact
99 ((cardinal_le_aleph0_iff_hasCountableDescendingOpenNormalChainAtOne
100 (G := G) X hX)).2 hchain
101 exact Cardinal.mk_le_aleph0_iff.mp hXcount
102 · rintro ⟨X, hX, hXcount⟩
103 have hchain : ProCGroups.ProC.HasCountableOpenNormalBasisAtOne G := by
104 exact
105 ((cardinal_le_aleph0_iff_hasCountableDescendingOpenNormalChainAtOne
106 (G := G) X hX)).1
107 (Cardinal.mk_le_aleph0_iff.mpr hXcount)
108 exact (metrizable_iff_hasCountableDescendingOpenNormalChainAtOne
109 (G := G)).2 hchain
111end ProCGroups.LocalWeight