Source: ProCGroups.LocalWeight.MetrizabilityAndQuotients
1import ProCGroups.FiniteGeneration.CharacteristicChainsAndIndices
2import ProCGroups.Generation.QuotientGeneratorConvergingPairs
3import ProCGroups.LocalWeight.CardinalInvariantsAndLocalWeight
4import ProCGroups.LocalWeight.SubgroupChains
5import ProCGroups.ProC.OpenNormalSubgroups.BasisAtOne
7/-!
8# Local weight, quotients, and metrizability
10This file develops local weight for quotients and open subgroups, relates countable local weight
11to descending open-normal chains, and characterizes metrizability of profinite groups. It also
12records consequences of topological finite generation.
13-/
15open Set
16open TopologicalSpace
17open Order
18open scoped Cardinal
19open scoped Topology Pointwise
21namespace ProCGroups.LocalWeight
23universe u
25open ProCGroups.ProC ProCGroups.Generation
26open ProCGroups.FiniteGeneration
29section QuotientLocalWeightStatements
31section QuotientLocalWeight
33variable (G : Type u) [Group G] [TopologicalSpace G]
35/-- 6. Quotient local weight at the identity coset. -/
36noncomputable def quotientLocalWeight (H : Subgroup G) : Cardinal :=
37 localWeightAt (X := G ⧸ H) ((QuotientGroup.mk : G → G ⧸ H) 1)
39/--
40The quotient by a closed normal subgroup has the expected local weight computed from finite
41quotients.
42-/
43@[simp] theorem quotientLocalWeight_eq_localWeight (H : Subgroup G) [H.Normal] :
44 quotientLocalWeight (G := G) H = localWeight (G ⧸ H) :=
45 rfl
47/-- Enlarging the denominator subgroup does not increase quotient local weight. -/
48theorem quotientLocalWeight_mono_of_le
49 [IsTopologicalGroup G] {H K : Subgroup G} [H.Normal] [K.Normal] (hHK : H ≤ K) :
50 quotientLocalWeight (G := G) K ≤ quotientLocalWeight (G := G) H := by
51 let f : G ⧸ H → G ⧸ K := QuotientGroup.map H K (MonoidHom.id G) hHK
52 have hfcont : Continuous f := by
53 have hcomp : Continuous (f ∘ ((↑) : G → G ⧸ H)) := by
54 have hcomp_eq :
55 f ∘ ((↑) : G → G ⧸ H) = ((↑) : G → G ⧸ K) := by
56 funext g
57 simp [f]
58 rw [hcomp_eq]
59 exact QuotientGroup.continuous_mk
60 exact (QuotientGroup.isOpenQuotientMap_mk (N := H)).continuous_comp_iff.mp hcomp
61 have hfopen : IsOpenMap f := by
62 intro U hUopen
63 have hpreOpen : IsOpen (((↑) : G → G ⧸ H) ⁻¹' U) := by
64 exact hUopen.preimage QuotientGroup.continuous_mk
65 have himage :
66 f '' U = ((↑) : G → G ⧸ K) '' (((↑) : G → G ⧸ H) ⁻¹' U) := by
67 ext y
68 constructor
69 · rintro ⟨x, hx, rfl⟩
70 rcases Quotient.exists_rep x with ⟨g, rfl⟩
71 exact ⟨g, hx, by simp only [QuotientGroup.map_mk, MonoidHom.id_apply, f]⟩
72 · rintro ⟨g, hg, rfl⟩
73 exact ⟨((↑) : G → G ⧸ H) g, hg, by simp only [QuotientGroup.map_mk, MonoidHom.id_apply, f]⟩
74 rw [himage]
75 exact QuotientGroup.isOpenMap_coe _ hpreOpen
76 have hle :=
77 localWeightAt_image_le_of_continuous_open
78 (X := G ⧸ H) (Y := G ⧸ K) (f := f) (x := 1) hfcont hfopen
79 have hf_one : f (1 : G ⧸ H) = 1 := by
80 simp [f]
81 rw [hf_one] at hle
82 simpa [quotientLocalWeight] using hle
84end QuotientLocalWeight
86/-- An open subgroup has the same local weight as the ambient profinite group. -/
87theorem localWeight_openSubgroup_eq
88 (G : Type u) [Group G] [TopologicalSpace G]
89 (H : OpenSubgroup G) :
90 localWeight ↥(H : Subgroup G) = localWeight G := by
91 have hle : localWeight ↥(H : Subgroup G) ≤ localWeight G := by
92 rcases exists_neighborhoodBasisAt_cardinal_le_of_localWeightAt_le
93 (X := G) (x := (1 : G)) (κ := localWeight G) le_rfl with
94 ⟨B, hBbasis, hBcard⟩
95 let ι : Type u := {U : Set G // U ∈ B}
96 let C : Set (Set ↥(H : Subgroup G)) :=
97 Set.range fun i : ι => ((↑) : ↥(H : Subgroup G) → G) ⁻¹' i.1
98 have hCbasis :
99 IsNeighborhoodBasisAt (X := ↥(H : Subgroup G)) (1 : ↥(H : Subgroup G)) C := by
100 constructor
101 · intro V hV
102 rcases hV with ⟨i, rfl⟩
103 constructor
104 · exact (hBbasis.1 i.1 i.2).1.preimage continuous_subtype_val
105 · simpa using (hBbasis.1 i.1 i.2).2
106 · intro V hVopen hVone
107 rcases isOpen_induced_iff.mp hVopen with ⟨O, hOopen, hOeq⟩
108 have hOone : (1 : G) ∈ O := by
109 have : (1 : ↥(H : Subgroup G)) ∈ ((↑) : ↥(H : Subgroup G) → G) ⁻¹' O := by
110 simpa [hOeq] using hVone
111 simpa using this
112 have hOHopen : IsOpen (O ∩ (H : Set G)) := hOopen.inter H.isOpen'
113 have hOHone : (1 : G) ∈ O ∩ (H : Set G) := by
114 exact ⟨hOone, H.one_mem⟩
115 rcases hBbasis.2 (O ∩ (H : Set G)) hOHopen hOHone with ⟨U, hUrange, hUsub⟩
116 refine ⟨((↑) : ↥(H : Subgroup G) → G) ⁻¹' U, ?_, ?_⟩
117 · exact ⟨⟨U, hUrange⟩, rfl⟩
118 · intro x hx
119 have hx' : (x : G) ∈ O ∩ (H : Set G) := hUsub hx
120 rw [← hOeq]
121 exact hx'.1
122 have hCcard :
123 familyCardinal (X := ↥(H : Subgroup G)) C ≤ localWeight G := by
124 calc
125 familyCardinal (X := ↥(H : Subgroup G)) C ≤ Cardinal.mk ι := by
126 unfold familyCardinal C
127 exact Cardinal.mk_range_le
128 _ = familyCardinal (X := G) B := by rfl
129 _ ≤ localWeight G := hBcard
130 simpa [localWeight] using
131 (localWeightAt_le_familyCardinal_of_basis
132 (X := ↥(H : Subgroup G)) (x := (1 : ↥(H : Subgroup G))) hCbasis).trans hCcard
133 have hge : localWeight G ≤ localWeight ↥(H : Subgroup G) := by
134 simpa [localWeight] using
135 (localWeightAt_image_le_of_continuous_open
136 (X := ↥(H : Subgroup G)) (Y := G)
137 (f := ((↑) : ↥(H : Subgroup G) → G)) (x := (1 : ↥(H : Subgroup G)))
138 continuous_subtype_val H.isOpen'.isOpenMap_subtype_val)
139 exact le_antisymm hle hge
144end QuotientLocalWeightStatements
146section FiniteGroupClassHelpers
148/-- The class of all finite groups is closed under normal subgroups. -/
149theorem FiniteGroupClass.allFinite_normalSubgroupClosed :
150 FiniteGroupClass.NormalSubgroupClosed FiniteGroupClass.allFinite := by
151 intro G _ N _ hfin
152 letI : Finite G := by
153 simpa [FiniteGroupClass.allFinite] using hfin
154 letI : Finite N := Finite.of_injective (fun n : N => (n : G)) (by
155 intro n₁ n₂ h
156 exact Subtype.ext (show (n₁ : G) = n₂ from h))
157 simpa [FiniteGroupClass.allFinite]
159/-- A set whose cardinality is at least \(\aleph_0\) is infinite. -/
160theorem setInfinite_of_cardinal_ge_aleph0
161 {α : Type u} (X : Set α) (hX : ℵ₀ ≤ Cardinal.mk X) : Set.Infinite X := by
162 classical
163 by_contra hXfin
164 letI : Finite X := Set.not_infinite.mp hXfin
165 have hlt : Cardinal.mk X < ℵ₀ :=
166 (Cardinal.lt_aleph0_iff_finite (α := X)).2 inferInstance
167 exact not_lt_of_ge hX hlt
169/--
170A profinite group with \(w_0(G) \le \aleph_0\) admits a countable descending open-normal basis
171at \(1\).
172-/
173theorem hasCountableDescendingOpenNormalChainAtOne_of_localWeight_le_aleph0
174 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
175 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
176 (hcount : localWeight G ≤ ℵ₀) :
178 classical
179 rcases exists_openNormalNeighborhoodBasisAtOne_cardinal_le_localWeight
180 (G := G) with ⟨ι, W, hWbasis, hWcard⟩
181 have hιcount : Countable ι := Cardinal.mk_le_aleph0_iff.mp (hWcard.trans hcount)
182 have hιne : Nonempty ι := by
183 rcases hWbasis.2 Set.univ isOpen_univ (by simp only [mem_univ]) with ⟨U, hUrange, _hUsub⟩
184 rcases hUrange with ⟨i, rfl⟩
185 exact ⟨i⟩
186 letI : Countable ι := hιcount
187 letI : Nonempty ι := hιne
188 obtain ⟨e, he⟩ := exists_surjective_nat ι
189 let V : ℕ → OpenNormalSubgroup G := fun n => W (e n)
190 let U : ℕ → OpenNormalSubgroup G :=
191 Nat.rec (V 0) (fun n Un => Un ⊓ V (n + 1))
192 let USub : ℕ → Subgroup G := fun n => (U n).toOpenSubgroup.toSubgroup
193 have hstep : ∀ n, U (n + 1) ≤ U n := by
194 intro n
195 simp only [inf_le_left, U]
196 have hUanti' : Antitone U := antitone_nat_of_succ_le hstep
197 have hUanti : Antitone USub := by
198 intro m n hmn x hx
199 exact hUanti' hmn hx
200 have hUV : ∀ n, U n ≤ V n := by
201 intro n
202 cases n with
203 | zero =>
204 exact le_rfl
205 | succ n =>
206 simp only [inf_le_right, U]
207 refine ⟨U, hUanti, ?_⟩
208 intro O hOopen h1O
209 rcases hWbasis.2 O hOopen h1O with ⟨S, hSrange, hSO⟩
210 rcases hSrange with ⟨i, rfl⟩
211 rcases he i with ⟨n, rfl⟩
212 refine ⟨n, ?_⟩
213 intro x hx
214 exact hSO (hUV n hx)
216section CharacteristicHelpers
218variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
220/-- A topologically characteristic subgroup is normal. -/
221theorem IsTopologicallyCharacteristic.normal {H : Subgroup G}
222 (hH : IsTopologicallyCharacteristic G H) : H.Normal := by
223 classical
224 refine ⟨?_⟩
225 intro x hx g
226 let conj : G ≃ₜ* G :=
227 ContinuousMulEquiv.mk'
228 ((Homeomorph.mulLeft g).trans (Homeomorph.mulRight g⁻¹))
229 (by
230 intro y z
231 simp only [Homeomorph.trans_apply, Homeomorph.coe_mulLeft, Homeomorph.coe_mulRight,
232 mul_assoc,
233 inv_mul_cancel_left])
234 have hmem : conj x ∈ H ↔ x ∈ H := by
235 exact IsTopologicallyCharacteristic.apply_mem_iff (G := G) (H := H) hH conj (g := x)
236 simpa [conj] using hmem.2 hx
238end CharacteristicHelpers
242/--
243Helper criterion: metrizability is equivalent to a countable descending open-normal basis at
244\(1\).
245-/
246theorem metrizable_iff_hasCountableDescendingOpenNormalChainAtOne
247 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
248 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] :
249 Nonempty (MetrizableSpace G) ↔ ProCGroups.ProC.HasCountableOpenNormalBasisAtOne G := by
250 constructor
251 · intro hmetr
252 letI : MetrizableSpace G := hmetr.some
253 letI : FirstCountableTopology G := inferInstance
254 obtain ⟨u, hu, _⟩ := IsTopologicalGroup.exists_antitone_basis_nhds_one (G := G)
255 have hV :
256 ∀ n, ∃ V : Set G, V ⊆ u n ∧ IsOpen V ∧ (1 : G) ∈ V := by
257 intro n
258 rcases mem_nhds_iff.mp (hu.mem n) with ⟨V, hVu, hVopen, h1V⟩
259 exact ⟨V, hVu, hVopen, h1V⟩
260 choose V hVu hVopen h1V using hV
261 have hN :
262 ∀ n, ∃ N : OpenNormalSubgroup G, (N : Set G) ⊆ V n := by
263 intro n
264 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) (hVopen n) (h1V n) with
265 ⟨N, hNV⟩
266 exact ⟨N, hNV⟩
267 choose N hNV using hN
268 let U : ℕ → OpenNormalSubgroup G :=
269 Nat.rec (N 0) (fun n Un => Un ⊓ N (n + 1))
270 have hstep : ∀ n, U (n + 1) ≤ U n := by
271 intro n
272 change U n ⊓ N (n + 1) ≤ U n
273 exact inf_le_left
274 have hUanti' : Antitone U := antitone_nat_of_succ_le hstep
275 have hUanti : Antitone (fun n => (U n).toSubgroup) := by
276 intro m n hmn
277 exact hUanti' hmn
278 have hUN : ∀ n, U n ≤ N n := by
279 intro n
280 cases n with
281 | zero =>
282 simp only [Nat.rec_zero, le_refl, U]
283 | succ n =>
284 change U n ⊓ N (n + 1) ≤ N (n + 1)
285 exact inf_le_right
286 refine ⟨U, hUanti, ?_⟩
287 intro O hOopen h1O
288 have hOnhds : O ∈ 𝓝 (1 : G) := IsOpen.mem_nhds hOopen h1O
289 rcases hu.mem_iff.1 hOnhds with ⟨n, hnuO⟩
290 refine ⟨n, ?_⟩
291 intro x hx
292 have hxN : x ∈ (N n : Subgroup G) := hUN n hx
293 have hxV : x ∈ V n := hNV n hxN
294 exact hnuO (hVu n hxV)
295 · intro hchain
296 rcases hchain with ⟨U, _hUanti, hUbasis⟩
297 have hnhds :
298 (𝓝 (1 : G)).HasBasis (fun _ : ℕ => True)
299 (fun n : ℕ => (((U n : Subgroup G) : Set G))) := by
300 refine ⟨fun s => ?_⟩
301 constructor
302 · intro hs
303 rcases mem_nhds_iff.mp hs with ⟨V, hVs, hVopen, h1V⟩
304 rcases hUbasis V hVopen h1V with ⟨n, hnV⟩
305 exact ⟨n, trivial, hnV.trans hVs⟩
306 · rintro ⟨n, -, hns⟩
307 exact Filter.mem_of_superset
308 (IsOpen.mem_nhds (openNormalSubgroup_isOpen (G := G) (U n)) (U n).one_mem') hns
309 letI : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
310 haveI : (𝓝 (1 : G)).IsCountablyGenerated :=
311 Filter.HasCountableBasis.isCountablyGenerated ⟨hnhds, Set.to_countable _⟩
312 haveI : IsUniformGroup G := IsUniformGroup.of_compactSpace
313 haveI : (uniformity G).IsCountablyGenerated :=
314 IsUniformGroup.uniformity_countably_generated (α := G)
315 exact ⟨UniformSpace.metrizableSpace (X := G)⟩
317/--
318Topologically finitely generated profinite groups have a countable descending open-normal basis
319at \(1\).
320-/
321theorem hasCountableDescendingOpenNormalChainAtOne_of_topologicallyFinitelyGenerated
322 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
323 [CompactSpace G] [TotallyDisconnectedSpace G]
324 (hgen : TopologicallyFinitelyGenerated G) :
326 rcases exists_characteristicOpenBasis_of_topologicallyFinitelyGenerated (G := G) hgen with
327 ⟨V, _hV0, hVanti, hVopen, hVchar, hVbasis⟩
328 refine ⟨
329 (fun n =>
330 { toOpenSubgroup := ⟨V n, hVopen n⟩
332 (G := G) (H := V n) (hH := hVchar n) }),
333 ?_,
334 ?_⟩
335 · intro m n hmn x hx
336 exact hVanti hmn hx
337 · intro W hW h1W
338 exact hVbasis W (IsOpen.mem_nhds hW h1W)
340end FiniteGroupClassHelpers
343end ProCGroups.LocalWeight