ProCGroups/LocalWeight/MetrizabilityAndQuotients.lean

1import ProCGroups.FiniteGeneration.CharacteristicChainsAndIndices

2import ProCGroups.Generation.QuotientGeneratorConvergingPairs

3import ProCGroups.LocalWeight.CardinalInvariantsAndLocalWeight

4import ProCGroups.LocalWeight.SubgroupChains

5import ProCGroups.ProC.OpenNormalSubgroups.BasisAtOne

7/-

8PUBLIC_PAGE_SNAPSHOT

9generated_at: 2026-05-27T09:47:29+09:00

10lean_source: lean4/ProCGroups/LocalWeight/MetrizabilityAndQuotients.lean

11translation_root: data/translation

12purpose: identifies the local data snapshot used to build pages/

13placement: after imports, never before imports

14-/

15/-!

16# Local weight and quotient ranks

18Studies local weight, metrizability, quotient size bounds, and cardinal invariants of profinite groups.

19-/

21open Set

22open TopologicalSpace

23open Order

24open scoped Cardinal

25open scoped Topology Pointwise

27namespace ProCGroups.LocalWeight

29universe u

31open ProCGroups.ProC ProCGroups.Generation

32open ProCGroups.FiniteGeneration

35/-!

36# Metrizability And Quotients

38## Main declarations

39- `quotientLocalWeight`

40- `quotientLocalWeight_eq_localWeight`

41- `FiniteGroupClass.allFinite_normalSubgroupClosed`

42- `setInfinite_of_cardinal_ge_aleph0`

43- `17` more local declarations

45## Notes

46- Status: Complete

47-/

48section QuotientLocalWeightStatements

50section QuotientLocalWeight

52variable (G : Type u) [Group G] [TopologicalSpace G]

54/-- 6. Quotient local weight at the identity coset.

55-/

56noncomputable def quotientLocalWeight (H : Subgroup G) : Cardinal :=

57 localWeightAt (X := G ⧸ H) ((QuotientGroup.mk : G → G ⧸ H) 1)

59@[simp] theorem quotientLocalWeight_eq_localWeight (H : Subgroup G) [H.Normal] :

60 quotientLocalWeight (G := G) H = localWeight (G ⧸ H) :=

61 rfl

63/-- Enlarging the denominator subgroup does not increase quotient local weight. -/

64theorem quotientLocalWeight_mono_of_le

65 [IsTopologicalGroup G] {H K : Subgroup G} [H.Normal] [K.Normal] (hHK : H ≤ K) :

66 quotientLocalWeight (G := G) K ≤ quotientLocalWeight (G := G) H := by

67 let f : G ⧸ H → G ⧸ K := QuotientGroup.map H K (MonoidHom.id G) hHK

68 have hfcont : Continuous f := by

69 have hcomp : Continuous (f ∘ ((↑) : G → G ⧸ H)) := by

70 simpa [f, Function.comp] using

71 (QuotientGroup.continuous_mk : Continuous ((↑) : G → G ⧸ K))

72 exact (QuotientGroup.isOpenQuotientMap_mk (N := H)).continuous_comp_iff.mp hcomp

73 have hfopen : IsOpenMap f := by

74 intro U hUopen

75 have hpreOpen : IsOpen (((↑) : G → G ⧸ H) ⁻¹' U) := by

76 exact hUopen.preimage QuotientGroup.continuous_mk

77 have himage :

78 f '' U = ((↑) : G → G ⧸ K) '' (((↑) : G → G ⧸ H) ⁻¹' U) := by

79 ext y

80 constructor

81 · rintro ⟨x, hx, rfl⟩

82 rcases Quotient.exists_rep x with ⟨g, rfl⟩

83 exact ⟨g, hx, by simp only [QuotientGroup.map_mk, MonoidHom.id_apply, f]⟩

84 · rintro ⟨g, hg, rfl⟩

85 exact ⟨((↑) : G → G ⧸ H) g, hg, by simp only [QuotientGroup.map_mk, MonoidHom.id_apply, f]⟩

86 rw [himage]

87 exact QuotientGroup.isOpenMap_coe _ hpreOpen

88 simpa [quotientLocalWeight, f] using

89 localWeightAt_image_le_of_continuous_open

90 (X := G ⧸ H) (Y := G ⧸ K) (f := f) hfcont hfopen

92end QuotientLocalWeight

94/-- Open subgroups have the same local weight as the ambient topological group. -/

95theorem localWeight_openSubgroup_eq

96 (G : Type u) [Group G] [TopologicalSpace G]

97 (H : OpenSubgroup G) :

98 localWeight ↥(H : Subgroup G) = localWeight G := by

99 have hle : localWeight ↥(H : Subgroup G) ≤ localWeight G := by

100 rcases exists_neighborhoodBasisAt_cardinal_le_of_localWeightAt_le

101 (X := G) (x := (1 : G)) (κ := localWeight G) le_rfl with

102 ⟨B, hBbasis, hBcard⟩

103 let ι : Type u := {U : Set G // U ∈ B}

104 let C : Set (Set ↥(H : Subgroup G)) :=

105 Set.range fun i : ι => ((↑) : ↥(H : Subgroup G) → G) ⁻¹' i.1

106 have hCbasis :

107 IsNeighborhoodBasisAt (X := ↥(H : Subgroup G)) (1 : ↥(H : Subgroup G)) C := by

108 constructor

109 · intro V hV

110 rcases hV with ⟨i, rfl⟩

111 constructor

112 · exact (hBbasis.1 i.1 i.2).1.preimage continuous_subtype_val

113 · simpa using (hBbasis.1 i.1 i.2).2

114 · intro V hVopen hVone

115 rcases isOpen_induced_iff.mp hVopen with ⟨O, hOopen, hOeq⟩

116 have hOone : (1 : G) ∈ O := by

117 have : (1 : ↥(H : Subgroup G)) ∈ ((↑) : ↥(H : Subgroup G) → G) ⁻¹' O := by

118 simpa [hOeq] using hVone

119 simpa using this

120 have hOHopen : IsOpen (O ∩ (H : Set G)) := hOopen.inter H.isOpen'

121 have hOHone : (1 : G) ∈ O ∩ (H : Set G) := by

122 exact ⟨hOone, H.one_mem⟩

123 rcases hBbasis.2 (O ∩ (H : Set G)) hOHopen hOHone with ⟨U, hUrange, hUsub⟩

124 refine ⟨((↑) : ↥(H : Subgroup G) → G) ⁻¹' U, ?_, ?_⟩

125 · exact ⟨⟨U, hUrange⟩, rfl⟩

126 · intro x hx

127 have hx' : (x : G) ∈ O ∩ (H : Set G) := hUsub hx

128 rw [← hOeq]

129 exact hx'.1

130 have hCcard :

131 familyCardinal (X := ↥(H : Subgroup G)) C ≤ localWeight G := by

132 calc

133 familyCardinal (X := ↥(H : Subgroup G)) C ≤ Cardinal.mk ι := by

134 unfold familyCardinal C

135 exact Cardinal.mk_range_le

136 _ = familyCardinal (X := G) B := by rfl

137 _ ≤ localWeight G := hBcard

138 simpa [localWeight] using

139 (localWeightAt_le_familyCardinal_of_basis

140 (X := ↥(H : Subgroup G)) (x := (1 : ↥(H : Subgroup G))) hCbasis).trans hCcard

141 have hge : localWeight G ≤ localWeight ↥(H : Subgroup G) := by

142 simpa [localWeight] using

143 (localWeightAt_image_le_of_continuous_open

144 (X := ↥(H : Subgroup G)) (Y := G)

145 (f := ((↑) : ↥(H : Subgroup G) → G)) (x := (1 : ↥(H : Subgroup G)))

146 continuous_subtype_val H.isOpen'.isOpenMap_subtype_val)

147 exact le_antisymm hle hge

152end QuotientLocalWeightStatements

153

154section FiniteGroupClassHelpers

155

156theorem FiniteGroupClass.allFinite_normalSubgroupClosed :

157 FiniteGroupClass.NormalSubgroupClosed FiniteGroupClass.allFinite := by

158 intro G _ N _ hfin

159 letI : Finite G := by

160 simpa [FiniteGroupClass.allFinite] using hfin

161 letI : Finite N := Finite.of_injective (fun n : N => (n : G)) (by

162 intro n₁ n₂ h

163 exact Subtype.ext (show (n₁ : G) = n₂ from h))

164 simpa [FiniteGroupClass.allFinite]

165

166theorem setInfinite_of_cardinal_ge_aleph0

167 {α : Type u} (X : Set α) (hX : ℵ₀ ≤ Cardinal.mk X) : Set.Infinite X := by

168 classical

169 by_contra hXfin

170 letI : Finite X := Set.not_infinite.mp hXfin

171 have hlt : Cardinal.mk X < ℵ₀ :=

172 (Cardinal.lt_aleph0_iff_finite (α := X)).2 inferInstance

173 exact not_lt_of_ge hX hlt

174

175/-- A profinite group with `w₀(G) ≤ ℵ₀` admits a countable descending open-normal basis at `1`.

176-/

177theorem hasCountableDescendingOpenNormalChainAtOne_of_localWeight_le_aleph0

178 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

179 (hG : IsProfiniteGroup G) (hcount : localWeight G ≤ ℵ₀) :

180 ProCGroups.ProC.HasCountableOpenNormalBasisAtOne G := by

181 classical

182 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG

183 letI : T2Space G := IsProfiniteGroup.t2Space hG

184 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG

185 rcases exists_openNormalNeighborhoodBasisAtOne_cardinal_le_localWeight

186 (G := G) hG with ⟨ι, W, hWbasis, hWcard⟩

187 have hιcount : Countable ι := Cardinal.mk_le_aleph0_iff.mp (hWcard.trans hcount)

188 have hιne : Nonempty ι := by

189 rcases hWbasis.2 Set.univ isOpen_univ (by simp only [mem_univ]) with ⟨U, hUrange, _hUsub⟩

190 rcases hUrange with ⟨i, rfl⟩

191 exact ⟨i⟩

192 letI : Countable ι := hιcount

193 letI : Nonempty ι := hιne

194 obtain ⟨e, he⟩ := exists_surjective_nat ι

195 let V : ℕ → OpenNormalSubgroup G := fun n => W (e n)

196 let U : ℕ → OpenNormalSubgroup G :=

197 Nat.rec (V 0) (fun n Un => Un ⊓ V (n + 1))

198 let USub : ℕ → Subgroup G := fun n => (U n).toOpenSubgroup.toSubgroup

199 have hstep : ∀ n, U (n + 1) ≤ U n := by

200 intro n

201 simp only [inf_le_left, U]

202 have hUanti' : Antitone U := antitone_nat_of_succ_le hstep

203 have hUanti : Antitone USub := by

204 intro m n hmn x hx

205 exact hUanti' hmn hx

206 have hUV : ∀ n, U n ≤ V n := by

207 intro n

208 cases n with

209 | zero =>

210 exact le_rfl

211 | succ n =>

212 simp only [inf_le_right, U]

213 refine ⟨U, hUanti, ?_⟩

214 intro O hOopen h1O

215 rcases hWbasis.2 O hOopen h1O with ⟨S, hSrange, hSO⟩

216 rcases hSrange with ⟨i, rfl⟩

217 rcases he i with ⟨n, rfl⟩

218 refine ⟨n, ?_⟩

219 intro x hx

220 exact hSO (hUV n hx)

221

222section CharacteristicHelpers

223

224variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

225

226theorem IsTopologicallyCharacteristic.normal {H : Subgroup G}

227 (hH : IsTopologicallyCharacteristic G H) : H.Normal := by

228 classical

229 refine ⟨?_⟩

230 intro x hx g

231 let conj : G ≃ₜ* G :=

232 ContinuousMulEquiv.mk'

233 ((Homeomorph.mulLeft g).trans (Homeomorph.mulRight g⁻¹))

234 (by

235 intro y z

236 simp only [Homeomorph.trans_apply, Homeomorph.coe_mulLeft, Homeomorph.coe_mulRight, mul_assoc,

237 inv_mul_cancel_left])

238 have hmem : conj x ∈ H ↔ x ∈ H := by

239 exact IsTopologicallyCharacteristic.apply_mem_iff (G := G) (H := H) hH conj (g := x)

240 simpa [conj] using hmem.2 hx

241

242end CharacteristicHelpers

243

244

245

246/--

247Helper criterion: metrizability is equivalent to a countable descending open-normal basis at `1`.

248-/

249theorem metrizable_iff_hasCountableDescendingOpenNormalChainAtOne

250 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

251 (hG : IsProfiniteGroup G) :

252 Nonempty (MetrizableSpace G) ↔ ProCGroups.ProC.HasCountableOpenNormalBasisAtOne G := by

253 constructor

254 · intro hmetr

255 letI : MetrizableSpace G := hmetr.some

256 letI : FirstCountableTopology G := inferInstance

257 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG

258 letI : T2Space G := IsProfiniteGroup.t2Space hG

259 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG

260 obtain ⟨u, hu, _⟩ := IsTopologicalGroup.exists_antitone_basis_nhds_one (G := G)

261 have hV :

262 ∀ n, ∃ V : Set G, V ⊆ u n ∧ IsOpen V ∧ (1 : G) ∈ V := by

263 intro n

264 rcases mem_nhds_iff.mp (hu.mem n) with ⟨V, hVu, hVopen, h1V⟩

265 exact ⟨V, hVu, hVopen, h1V⟩

266 choose V hVu hVopen h1V using hV

267 have hN :

268 ∀ n, ∃ N : OpenNormalSubgroup G, (N : Set G) ⊆ V n := by

269 intro n

270 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) (hVopen n) (h1V n) with

271 ⟨N, hNV⟩

272 exact ⟨N, hNV⟩

273 choose N hNV using hN

274 let U : ℕ → OpenNormalSubgroup G :=

275 Nat.rec (N 0) (fun n Un => Un ⊓ N (n + 1))

276 have hstep : ∀ n, U (n + 1) ≤ U n := by

277 intro n

278 change U n ⊓ N (n + 1) ≤ U n

279 exact inf_le_left

280 have hUanti' : Antitone U := antitone_nat_of_succ_le hstep

281 have hUanti : Antitone (fun n => (U n).toSubgroup) := by

282 intro m n hmn

283 exact hUanti' hmn

284 have hUN : ∀ n, U n ≤ N n := by

285 intro n

286 cases n with

287 | zero =>

288 simp only [Nat.rec_zero, le_refl, U]

289 | succ n =>

290 change U n ⊓ N (n + 1) ≤ N (n + 1)

291 exact inf_le_right

292 refine ⟨U, hUanti, ?_⟩

293 intro O hOopen h1O

294 have hOnhds : O ∈ 𝓝 (1 : G) := IsOpen.mem_nhds hOopen h1O

295 rcases hu.mem_iff.1 hOnhds with ⟨n, hnuO⟩

296 refine ⟨n, ?_⟩

297 intro x hx

298 have hxN : x ∈ (N n : Subgroup G) := hUN n hx

299 have hxV : x ∈ V n := hNV n hxN

300 exact hnuO (hVu n hxV)

301 · intro hchain

302 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG

303 letI : T2Space G := IsProfiniteGroup.t2Space hG

304 rcases hchain with ⟨U, _hUanti, hUbasis⟩

305 have hnhds :

306 (𝓝 (1 : G)).HasBasis (fun _ : ℕ => True)

307 (fun n : ℕ => (((U n : Subgroup G) : Set G))) := by

308 refine ⟨fun s => ?_⟩

309 constructor

310 · intro hs

311 rcases mem_nhds_iff.mp hs with ⟨V, hVs, hVopen, h1V⟩

312 rcases hUbasis V hVopen h1V with ⟨n, hnV⟩

313 exact ⟨n, trivial, hnV.trans hVs⟩

314 · rintro ⟨n, -, hns⟩

315 exact Filter.mem_of_superset

316 (IsOpen.mem_nhds (openNormalSubgroup_isOpen (G := G) (U n)) (U n).one_mem') hns

317 letI : UniformSpace G := IsTopologicalGroup.rightUniformSpace G

318 haveI : (𝓝 (1 : G)).IsCountablyGenerated :=

319 Filter.HasCountableBasis.isCountablyGenerated ⟨hnhds, Set.to_countable _⟩

320 haveI : IsUniformGroup G := IsUniformGroup.of_compactSpace

321 haveI : (uniformity G).IsCountablyGenerated :=

322 IsUniformGroup.uniformity_countably_generated (α := G)

323 exact ⟨UniformSpace.metrizableSpace (X := G)⟩

324

325/-- Any explicit cardinal bound on `topologicalRank G` yields a generating set converging to `1` of the same

326size. This is the direct bridge from the Section 2.5 generator invariant to the Section 2.6

327cardinality language. -/

328theorem hasGeneratingSetConvergingToOneOfCardinalLE_of_d_le

329 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

330 (hG : IsProfiniteGroup G) {κ : Cardinal} (hd : topologicalRank G ≤ κ) :

331 ∃ X : Set G, GeneratesAndConvergesToOne (G := G) X ∧ Cardinal.mk X ≤ κ := by

332 classical

333 letI : T2Space G := IsProfiniteGroup.t2Space hG

334 let C : Set Cardinal := {κ' : Cardinal |

335 ∃ X : Set G, GeneratesAndConvergesToOne (G := G) X ∧ Cardinal.mk X = κ'}

336 have hCne : C.Nonempty := by

337 rcases exists_generatorsConvergingToOne (G := G) hG with ⟨X, hX⟩

338 exact ⟨Cardinal.mk X, X, hX, rfl⟩

339 have hdmem : topologicalRank G ∈ C := by

340 simpa [topologicalRank, C] using (csInf_mem hCne)

341 rcases hdmem with ⟨X, hX, hXcard⟩

342 refine ⟨X, hX, ?_⟩

343 calc

344 Cardinal.mk X = topologicalRank G := hXcard

345 _ ≤ κ := hd

346

347/-- Topologically finitely generated profinite groups have a countable descending open-normal

348basis at `1`. -/

349theorem hasCountableDescendingOpenNormalChainAtOne_of_topologicallyFinitelyGenerated

350 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

351 [CompactSpace G] [TotallyDisconnectedSpace G]

352 (hgen : TopologicallyFinitelyGenerated G) :

353 ProCGroups.ProC.HasCountableOpenNormalBasisAtOne G := by

354 rcases exists_characteristicOpenBasis_of_topologicallyFinitelyGenerated (G := G) hgen with

355 ⟨V, _hV0, hVanti, hVopen, hVchar, hVbasis⟩

356 refine ⟨

357 (fun n =>

358 { toOpenSubgroup := ⟨V n, hVopen n⟩

359 isNormal' := ProCGroups.LocalWeight.IsTopologicallyCharacteristic.normal

360 (G := G) (H := V n) (hH := hVchar n) }),

361 ?_,

362 ?_⟩

363 · intro m n hmn x hx

364 exact hVanti hmn hx

365 · intro W hW h1W

366 exact hVbasis W (IsOpen.mem_nhds hW h1W)

367

368end FiniteGroupClassHelpers

369

370

371end LocalWeight