Source: ProCGroups.FiniteGeneration.CharacteristicChainsAndIndices

1import ProCGroups.FiniteGeneration.Basic

3/-!

4# Characteristic chains from bounded-index intersections

6For a topologically finitely generated profinite group, the intersection of

7all open subgroups of index at most \(n\) is open and topologically

8characteristic. These intersections form a descending countable basis at the

9identity.

10-/

12open Set

13open scoped Topology Pointwise

15namespace ProCGroups.FiniteGeneration

17universe u v w

19open ProCGroups.Generation

20open ProCGroups.ProC

22section IndexFamilies

24variable {G : Type u} [Group G] [TopologicalSpace G]

26/--

27The open subgroups of index at most \(n\). This is the bounded-index family whose intersection

28defines the characteristic core.

29-/

30def OpenSubgroupsOfIndexLE (G : Type u) [Group G] [TopologicalSpace G]

31 (n : ℕ) : Set (Subgroup G) :=

32 { H | IsOpen (H : Set G) ∧ Finite (G ⧸ H) ∧ Nat.card (G ⧸ H) ≤ n }

34/-- The family of open normal subgroups of index exactly \(n\). -/

35def OpenNormalSubgroupsOfIndex (G : Type u) [Group G] [TopologicalSpace G]

36 (n : ℕ) : Set (Subgroup G) :=

37 { U | U.Normal ∧ IsOpen (U : Set G) ∧ Finite (G ⧸ U) ∧ Nat.card (G ⧸ U) = n }

41variable {G : Type u} [Group G] [TopologicalSpace G]

43/-- Membership criterion for the finite set of open subgroups of index at most `n`. -/

44@[simp] theorem mem_openSubgroupsOfIndexLE {n : ℕ} {H : Subgroup G} :

45 H ∈ OpenSubgroupsOfIndexLE (G := G) n ↔

46 IsOpen (H : Set G) ∧ Finite (G ⧸ H) ∧ Nat.card (G ⧸ H) ≤ n :=

47 Iff.rfl

49/-- Membership criterion for the finite set of open normal subgroups of a fixed index. -/

50@[simp] theorem mem_openNormalSubgroupsOfIndex {n : ℕ} {U : Subgroup G} :

51 U ∈ OpenNormalSubgroupsOfIndex (G := G) n ↔

52 U.Normal ∧ IsOpen (U : Set G) ∧ Finite (G ⧸ U) ∧ Nat.card (G ⧸ U) = n :=

53 Iff.rfl

55/--

56The canonical bounded-index intersection

57`Vₙ = ⋂ {H ≤ G | H open and [G : H] ≤ n}`.

58-/

59def CharacteristicIndexIntersection (G : Type u) [Group G] [TopologicalSpace G]

60 (n : ℕ) : Subgroup G :=

61 sInf (OpenSubgroupsOfIndexLE (G := G) n)

63/-- The characteristic index intersection is the infimum of all open subgroups of bounded index. -/

64@[simp] theorem characteristicIndexIntersection_def (n : ℕ) :

65 CharacteristicIndexIntersection (G := G) n =

66 sInf (OpenSubgroupsOfIndexLE (G := G) n) :=

67 rfl

69/-- A group has only finitely many open subgroups of each prescribed index. -/

70def HasFiniteOpenSubgroupsOfIndex (G : Type u) [Group G] [TopologicalSpace G]

71 : Prop :=

72 ∀ n, Set.Finite

73 { H : Subgroup G | IsOpen (H : Set G) ∧ Finite (G ⧸ H) ∧ Nat.card (G ⧸ H) = n }

75/-- Normal-subgroup version of fixed-index finiteness. -/

76def HasFiniteOpenNormalSubgroupsOfIndex (G : Type u) [Group G] [TopologicalSpace G]

77 : Prop :=

78 ∀ n,

79 Set.Finite

80 { U : Subgroup G |

81 U.Normal ∧ IsOpen (U : Set G) ∧ Finite (G ⧸ U) ∧ Nat.card (G ⧸ U) = n }

83/--

84Finiteness of open subgroups of each index implies finiteness of open normal subgroups of each

85index.

86-/

87theorem HasFiniteOpenSubgroupsOfIndex.toHasFiniteOpenNormalSubgroupsOfIndex

88 (h : HasFiniteOpenSubgroupsOfIndex G) :

89 HasFiniteOpenNormalSubgroupsOfIndex G := by

90 intro n

91 refine (h n).subset ?_

92 intro U hU

93 exact ⟨hU.2.1, hU.2.2.1, hU.2.2.2⟩

95/-- Continuous homomorphisms are equal when they agree on a topological generating set. -/

96theorem continuousMonoidHom_eq_of_eqOn_topologicalGenerators

97 [IsTopologicalGroup G]

98 {R : Type v} [Group R] [TopologicalSpace R] [T2Space R]

99 {s : Finset G} (hsgen : TopologicallyGenerates (G := G) (↑s : Set G))

100 {f g : ContinuousMonoidHom G R}

101 (hfg : ∀ x ∈ (↑s : Set G), f x = g x) :

102 f = g := by

103 let K : Subgroup G := {

104 carrier := { x | f x = g x }

105 one_mem' := by simp only [mem_setOf_eq, map_one]

106 mul_mem' := by

107 intro a b ha hb

108 change f (a * b) = g (a * b)

109 rw [map_mul, map_mul, ha, hb]

110 inv_mem' := by

111 intro a ha

112 simpa using congrArg Inv.inv ha

113 }

114 have hKclosed : IsClosed ((K : Subgroup G) : Set G) := by

115 change IsClosed { x | f x = g x }

116 exact isClosed_eq f.continuous_toFun g.continuous_toFun

117 have hsub : Subgroup.closure (↑s : Set G) ≤ K := by

118 rw [Subgroup.closure_le]

119 intro x hx

120 exact hfg x hx

121 have htop : (⊤ : Subgroup G) ≤ K := by

122 have hcl :

123 (Subgroup.closure (↑s : Set G)).topologicalClosure ≤ K :=

124 Subgroup.topologicalClosure_minimal _ hsub hKclosed

125 rw [TopologicallyGenerates] at hsgen

126 simpa [hsgen] using hcl

127 ext x

128 simpa [K] using htop (show x ∈ (⊤ : Subgroup G) from by simp only [Subgroup.mem_top])

129

130/--

131A finitely generated profinite group admits only finitely many continuous homomorphisms into a

132fixed finite discrete target.

133-/

134theorem finite_continuousMonoidHom_to_finite_of_topologicallyFinitelyGenerated

135 [IsTopologicalGroup G]

136 {R : Type v} [Group R] [TopologicalSpace R] [T2Space R] [Finite R]

137 (hG : TopologicallyFinitelyGenerated G) :

138 Finite (ContinuousMonoidHom G R) := by

139 classical

140 rcases hG with ⟨s, hsgen⟩

141 let eval : ContinuousMonoidHom G R → ((↑s : Set G) → R) := fun φ x => φ x.1

142 have heval : Function.Injective eval := by

143 intro φ ψ hφψ

144 apply continuousMonoidHom_eq_of_eqOn_topologicalGenerators (G := G) hsgen

145 intro x hx

146 exact congrArg (fun k => k ⟨x, hx⟩) hφψ

147 exact Finite.of_injective eval heval

148

149/-- The chosen identification `G ⧸ H ≃ Fin n` for an index-`n` subgroup. -/

150noncomputable def openSubgroupIndexEquiv

151 (H : Subgroup G) (hHfinite : Finite (G ⧸ H)) {n : ℕ}

152 (hn : Nat.card (G ⧸ H) = n) :

153 (G ⧸ H) ≃ Fin n := by

154 classical

155 letI : Finite (G ⧸ H) := hHfinite

156 letI : Fintype (G ⧸ H) := Fintype.ofFinite (G ⧸ H)

157 refine Finite.equivFinOfCardEq ?_

158 simpa [Nat.card_eq_fintype_card] using hn

159

160/-- The coset action of `G` on the `n` cosets of an index-`n` subgroup, transported to `Fin n`. -/

161noncomputable def openSubgroupIndexAction

162 (H : Subgroup G) (hHfinite : Finite (G ⧸ H)) {n : ℕ}

163 (hn : Nat.card (G ⧸ H) = n) :

164 G →* Equiv.Perm (Fin n) := by

165 classical

166 let e := openSubgroupIndexEquiv (G := G) H hHfinite hn

167 exact e.permCongrHom.toMonoidHom.comp (MulAction.toPermHom G (G ⧸ H))

168

169/-- The image of the identity coset under the chosen `Fin n` identification. -/

170noncomputable def openSubgroupIndexBasepoint

171 (H : Subgroup G) (hHfinite : Finite (G ⧸ H)) {n : ℕ}

172 (hn : Nat.card (G ⧸ H) = n) : Fin n :=

173 openSubgroupIndexEquiv (G := G) H hHfinite hn (QuotientGroup.mk 1)

174

175/-- The finite permutation type has its canonical topological space structure. -/

176instance instTopologicalSpaceFinitePerm (n : ℕ) : TopologicalSpace (Equiv.Perm (Fin n)) :=

177 ⊥

178

179/-- The finite permutation type carries the discrete topology. -/

180instance instDiscreteTopologyFinitePerm (n : ℕ) : DiscreteTopology (Equiv.Perm (Fin n)) :=

181 ⟨rfl⟩

182

183/-- The finite permutation group is a topological group with the discrete topology. -/

184instance instIsTopologicalGroupFinitePerm (n : ℕ) : IsTopologicalGroup (Equiv.Perm (Fin n)) := by

185 infer_instance

186

187/-- The finite permutation type is finite. -/

188instance instFiniteFinitePerm (n : ℕ) : Finite (Equiv.Perm (Fin n)) := by

189 infer_instance

190

191/-- The finite coset action, viewed as a continuous homomorphism into a discrete permutation

192group. -/

193noncomputable def openSubgroupIndexContinuousHom

194 [IsTopologicalGroup G] [CompactSpace G]

195 (H : Subgroup G) (hH : IsOpen (H : Set G)) {n : ℕ}

196 (hHfinite : Finite (G ⧸ H)) (hn : Nat.card (G ⧸ H) = n) :

197 G →ₜ* Equiv.Perm (Fin n) := by

198 classical

199 let φ : G →* Equiv.Perm (Fin n) := openSubgroupIndexAction (G := G) H hHfinite hn

200 have hφker :

201 IsOpen ((φ.ker : Subgroup G) : Set G) := by

202 let e := openSubgroupIndexEquiv (G := G) H hHfinite hn

203 have hker :

204 φ.ker = (MulAction.toPermHom G (G ⧸ H)).ker := by

205 ext g

206 change e.permCongr (MulAction.toPerm g) = 1 ↔ MulAction.toPerm g = 1

207 have hperm_one :

208 e.permCongr (1 : Equiv.Perm (G ⧸ H)) = (1 : Equiv.Perm (Fin n)) := by

209 ext x

210 simp only [Equiv.permCongr_apply, Equiv.Perm.coe_one, id_eq, Equiv.apply_symm_apply]

211 rw [← hperm_one]

212 exact e.permCongr.injective.eq_iff

213 letI : Finite (G ⧸ H) := Subgroup.quotient_finite_of_isOpen H hH

214 letI : H.FiniteIndex := Subgroup.finiteIndex_of_finite_quotient (H := H)

215 have hHclosed : IsClosed ((H : Subgroup G) : Set G) :=

216 Subgroup.isClosed_of_isOpen H hH

217 letI : H.normalCore.FiniteIndex := Subgroup.finiteIndex_normalCore (H := H)

218 have hopenCore : IsOpen (((H.normalCore : Subgroup G) : Set G)) :=

219 H.normalCore.isOpen_of_isClosed_of_finiteIndex (H.normalCore_isClosed hHclosed)

220 simpa [hker, Subgroup.normalCore_eq_ker (H := H)] using hopenCore

221 have hφcont : Continuous φ := by

222 letI : UniformSpace G := IsTopologicalGroup.rightUniformSpace G

223 letI : UniformSpace (Equiv.Perm (Fin n)) :=

224 IsTopologicalGroup.rightUniformSpace (Equiv.Perm (Fin n))

225 have hφuc :

226 UniformContinuous φ :=

227 (IsUniformGroup.uniformContinuous_iff_isOpen_ker (f := φ)).2 hφker

228 exact hφuc.continuous

229 exact

230 { toMonoidHom := φ

231 continuous_toFun := hφcont }

232

233omit [TopologicalSpace G] in

234/-- Membership in an open subgroup is equivalent to fixing the basepoint in its coset action. -/

235theorem mem_openSubgroup_iff_indexAction_fix_basepoint

236 {H : Subgroup G} (hHfinite : Finite (G ⧸ H)) {n : ℕ}

237 (hn : Nat.card (G ⧸ H) = n) {g : G} :

238 g ∈ H ↔

239 openSubgroupIndexAction (G := G) H hHfinite hn g

240 (openSubgroupIndexBasepoint (G := G) H hHfinite hn) =

241 openSubgroupIndexBasepoint (G := G) H hHfinite hn := by

242 classical

243 let e := openSubgroupIndexEquiv (G := G) H hHfinite hn

244 constructor

245 · intro hg

246 have hq : QuotientGroup.mk (s := H) g = QuotientGroup.mk (s := H) 1 := by

247 simpa [QuotientGroup.eq] using hg

248 simpa [openSubgroupIndexAction, openSubgroupIndexBasepoint, e] using congrArg e hq

249 · intro hg

250 have hq :

251 QuotientGroup.mk (s := H) g = QuotientGroup.mk (s := H) 1 := by

252 apply e.injective

253 simpa [openSubgroupIndexAction, openSubgroupIndexBasepoint, e] using hg

254 simpa [QuotientGroup.eq] using hq

255

256/-- Finitely generated profinite groups have only finitely many open subgroups of each index. -/

257theorem hasFiniteOpenSubgroupsOfIndex_of_topologicallyFinitelyGenerated

258 [IsTopologicalGroup G] [CompactSpace G]

259 (hG : TopologicallyFinitelyGenerated G) :

260 HasFiniteOpenSubgroupsOfIndex G := by

261 intro n

262 classical

263 let S : Type u :=

264 { H : Subgroup G // IsOpen (H : Set G) ∧ Finite (G ⧸ H) ∧ Nat.card (G ⧸ H) = n }

265 letI : TopologicalSpace (Equiv.Perm (Fin n)) := ⊥

266 letI : DiscreteTopology (Equiv.Perm (Fin n)) := ⟨rfl⟩

267 letI : IsTopologicalGroup (Equiv.Perm (Fin n)) := by infer_instance

268 letI : Finite (Equiv.Perm (Fin n)) := by infer_instance

269 let code : S → ContinuousMonoidHom G (Equiv.Perm (Fin n)) × Fin n := fun H =>

270 let φ := openSubgroupIndexAction (G := G) H.1 H.2.2.1 H.2.2.2

271 let e := openSubgroupIndexEquiv (G := G) H.1 H.2.2.1 H.2.2.2

272 let hφker :

273 IsOpen ((φ.ker : Subgroup G) : Set G) := by

274 letI : Finite (G ⧸ H.1) := H.2.2.1

275 letI : H.1.FiniteIndex := Subgroup.finiteIndex_of_finite_quotient (H := H.1)

276 have hHclosed : IsClosed ((H.1 : Subgroup G) : Set G) :=

277 Subgroup.isClosed_of_isOpen H.1 H.2.1

278 have hker :

279 φ.ker = (MulAction.toPermHom G (G ⧸ H.1)).ker := by

280 ext g

281 change

282 e.permCongr (MulAction.toPerm g) = 1 ↔ MulAction.toPerm g = 1

283 have hperm_one : e.permCongr (1 : Equiv.Perm (G ⧸ H.1)) = (1 : Equiv.Perm (Fin n)) := by

284 ext x

285 simp only [Equiv.permCongr_apply, Equiv.Perm.coe_one, id_eq, Equiv.apply_symm_apply]

286 rw [← hperm_one]

287 exact e.permCongr.injective.eq_iff

288 letI : H.1.normalCore.FiniteIndex := Subgroup.finiteIndex_normalCore (H := H.1)

289 have hopenCore : IsOpen (((H.1).normalCore : Subgroup G) : Set G) :=

290 (H.1).normalCore.isOpen_of_isClosed_of_finiteIndex ((H.1).normalCore_isClosed hHclosed)

291 simpa [hker, Subgroup.normalCore_eq_ker (H := H.1)] using hopenCore

292 let hφcont :

293 Continuous φ := by

294 letI : UniformSpace G := IsTopologicalGroup.rightUniformSpace G

295 letI : UniformSpace (Equiv.Perm (Fin n)) :=

296 IsTopologicalGroup.rightUniformSpace (Equiv.Perm (Fin n))

297 have hφuc :

298 UniformContinuous φ :=

299 (IsUniformGroup.uniformContinuous_iff_isOpen_ker (f := φ)).2 hφker

300 exact hφuc.continuous

301 ({ toMonoidHom := φ

302 continuous_toFun := hφcont },

303 openSubgroupIndexBasepoint (G := G) H.1 H.2.2.1 H.2.2.2)

304 have hhomfinite : Finite (ContinuousMonoidHom G (Equiv.Perm (Fin n))) :=

305 finite_continuousMonoidHom_to_finite_of_topologicallyFinitelyGenerated

306 (G := G) hG

307 let _ : Finite (ContinuousMonoidHom G (Equiv.Perm (Fin n)) × Fin n) := by

308 infer_instance

309 have hcode : Function.Injective code := by

310 intro H K hHK

311 apply Subtype.ext

312 ext g

313 rw [mem_openSubgroup_iff_indexAction_fix_basepoint (G := G) (H := H.1) H.2.2.1 H.2.2.2

314 (g := g),

315 mem_openSubgroup_iff_indexAction_fix_basepoint (G := G) (H := K.1) K.2.2.1 K.2.2.2

316 (g := g)]

317 have hφg := DFunLike.congr_fun

318 (congrArg ContinuousMonoidHom.toMonoidHom (congrArg Prod.fst hHK)) g

319 have hb := congrArg Prod.snd hHK

320 dsimp only [code] at hφg hb

321 exact Iff.of_eq <| by simp [hφg, hb]

322 have hSfinite :

323 Finite

324 { H : Subgroup G //

325 IsOpen (H : Set G) ∧ Finite (G ⧸ H) ∧ Nat.card (G ⧸ H) = n } := by

326 simpa [S] using (Finite.of_injective code hcode)

327 exact @Set.toFinite (Subgroup G)

328 { H : Subgroup G | IsOpen (H : Set G) ∧ Finite (G ⧸ H) ∧ Nat.card (G ⧸ H) = n }

329 hSfinite

330

331/-- Bounding the index by \(n\) still yields only finitely many open subgroups. -/

332theorem finite_openSubgroupsOfIndexLE_of_hasFiniteOpenSubgroupsOfIndex

333 (hfin : HasFiniteOpenSubgroupsOfIndex G) (n : ℕ) :

334 Set.Finite (OpenSubgroupsOfIndexLE (G := G) n) := by

335 classical

336 refine Set.Finite.subset ((Set.finite_le_nat n).biUnion fun m hm => hfin m) ?_

337 intro H hH

338 exact Set.mem_iUnion.2

339 ⟨Nat.card (G ⧸ H), Set.mem_iUnion.2 ⟨hH.2.2, ⟨hH.1, hH.2.1, rfl⟩⟩⟩

340

341/-- The infimum of a finite family of open subgroups is open. -/

342theorem Subgroup.isOpen_sInf_of_finite

343 {S : Set (Subgroup G)} (hS : S.Finite)

344 (hopen : ∀ H ∈ S, IsOpen (H : Set G)) :

345 IsOpen ((sInf S : Subgroup G) : Set G) := by

346 classical

347 induction S, hS using Set.Finite.induction_on with

348 | empty =>

349 simp only [sInf_empty, Subgroup.coe_top, isOpen_univ]

350 | @insert H S hHS hS ih =>

351 rw [sInf_insert]

352 exact (hopen H (by simp only [mem_insert_iff, true_or])).inter (ih fun K hK => hopen K (by

353 simp only [mem_insert_iff, hK, or_true]))

354

355/--

356The bounded-index characteristic intersection is open once the bounded-index family is finite.

357-/

358theorem characteristicIndexIntersection_isOpen_of_hasFiniteOpenSubgroupsOfIndex

359 (hfin : HasFiniteOpenSubgroupsOfIndex G) (n : ℕ) :

360 IsOpen ((CharacteristicIndexIntersection (G := G) n : Set G)) := by

361 apply Subgroup.isOpen_sInf_of_finite

362 · exact finite_openSubgroupsOfIndexLE_of_hasFiniteOpenSubgroupsOfIndex (G := G) hfin n

363 · intro H hH

364 exact hH.1

365

366/-- The bounded-index characteristic intersections form a descending chain. -/

367theorem characteristicIndexIntersection_antitone :

368 Antitone (CharacteristicIndexIntersection (G := G)) := by

369 intro m n hmn x hx

370 simp only [CharacteristicIndexIntersection, Subgroup.mem_sInf] at hx ⊢

371 intro H hH

372 exact hx H ⟨hH.1, hH.2.1, le_trans hH.2.2 hmn⟩

373

374/-- The finite-index characteristic intersection is characteristic. -/

375theorem characteristicIndexIntersection_isTopologicallyCharacteristic

376 [IsTopologicalGroup G] [CompactSpace G]

377 (n : ℕ) :

378 IsTopologicallyCharacteristic G (CharacteristicIndexIntersection (G := G) n) := by

379 have hforward :

380 ∀ φ : G ≃ₜ* G, ∀ g : G,

381 g ∈ CharacteristicIndexIntersection (G := G) n →

382 φ g ∈ CharacteristicIndexIntersection (G := G) n := by

383 intro φ g hg

384 simp only [CharacteristicIndexIntersection, Subgroup.mem_sInf] at hg ⊢

385 intro H hH

386 have hcomap :

387 Subgroup.comap φ.toMonoidHom H ∈ OpenSubgroupsOfIndexLE (G := G) n := by

388 have hcomapOpen : IsOpen ((Subgroup.comap φ.toMonoidHom H : Subgroup G) : Set G) :=

389 hH.1.preimage φ.continuous_toFun

390 have hcomapFinite : Finite (G ⧸ Subgroup.comap φ.toMonoidHom H) :=

391 Subgroup.quotient_finite_of_isOpen (Subgroup.comap φ.toMonoidHom H) hcomapOpen

392 refine ⟨hcomapOpen, hcomapFinite, ?_⟩

393 simpa [Subgroup.index_eq_card] using

394 (Subgroup.index_comap_of_surjective (H := H) φ.surjective).le.trans hH.2.2

395 exact hg _ hcomap

396 intro φ g

397 constructor

398 · intro hg

399 simpa using hforward φ.symm (φ g) hg

400 · exact hforward φ g

401

402/-- Characteristic index intersections are cofinal among open subgroups. -/

403theorem characteristicIndexIntersection_cofinal_of_openSubgroup

404 [IsTopologicalGroup G] [CompactSpace G]

405 (U : Subgroup G) (hU : IsOpen (U : Set G)) :

406 ∃ n, CharacteristicIndexIntersection (G := G) n ≤ U := by

407 have hUfinite : Finite (G ⧸ U) :=

408 Subgroup.quotient_finite_of_isOpen U hU

409 refine ⟨Nat.card (G ⧸ U), ?_⟩

410 intro x hx

411 simp only [CharacteristicIndexIntersection, Subgroup.mem_sInf] at hx

412 exact hx U ⟨hU, hUfinite, le_rfl⟩

413

414/--

415Topologically finitely generated profinite groups have a countable characteristic open basis at

416the identity.

417-/

418theorem exists_characteristicOpenBasis_of_topologicallyFinitelyGenerated

419 [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]

420 : TopologicallyFinitelyGenerated G →

421 ∃ V : ℕ → Subgroup G,

422 V 0 = ⊤ ∧

423 Antitone V ∧

424 (∀ n, IsOpen ((V n : Subgroup G) : Set G)) ∧

425 (∀ n, IsTopologicallyCharacteristic G (V n)) ∧

426 ∀ U : Set G, U ∈ 𝓝 (1 : G) → ∃ n, ((V n : Subgroup G) : Set G) ⊆ U := by

427 intro hG

428 have hfin : HasFiniteOpenSubgroupsOfIndex G :=

429 hasFiniteOpenSubgroupsOfIndex_of_topologicallyFinitelyGenerated (G := G) hG

430 let V : ℕ → Subgroup G

431 | 0 => ⊤

432 | n + 1 => CharacteristicIndexIntersection (G := G) n

433 refine ⟨V, rfl, ?_, ?_, ?_, ?_⟩

434 · intro m n hmn

435 cases m with

436 | zero =>

437 exact le_top

438 | succ m =>

439 cases n with

440 | zero =>

441 cases Nat.not_succ_le_zero m hmn

442 | succ n =>

443 exact characteristicIndexIntersection_antitone (G := G)

444 (Nat.succ_le_succ_iff.mp hmn)

445 · intro n

446 cases n with

447 | zero =>

448 exact isOpen_univ

449 | succ n =>

450 exact characteristicIndexIntersection_isOpen_of_hasFiniteOpenSubgroupsOfIndex

451 (G := G) hfin n

452 · intro n

453 cases n with

454 | zero =>

455 exact IsTopologicallyCharacteristic.top

456 | succ n =>

457 exact characteristicIndexIntersection_isTopologicallyCharacteristic

458 (G := G) n

459 · intro U hU

460 rcases mem_nhds_iff.mp hU with ⟨W, hWU, hWopen, h1W⟩

461 rcases exists_openNormalSubgroup_sub_open_nhds_of_one

462 (G := G) hWopen h1W with ⟨N, hNW⟩

463 rcases characteristicIndexIntersection_cofinal_of_openSubgroup

464 (G := G) (N : Subgroup G) (openNormalSubgroup_isOpen (G := G) N) with

465 ⟨n, hn⟩

466 exact ⟨n + 1, Set.Subset.trans hn (Set.Subset.trans hNW hWU)⟩

467

468/--

469Finitely generated profinite groups have finite fixed-index open-subgroup sets and a countable

470characteristic open basis at the identity.

471-/

472theorem finiteIndexOpenSubgroups_and_charBasis_of_tfg

473 [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]

474 (hG : TopologicallyFinitelyGenerated G) :

475 HasFiniteOpenSubgroupsOfIndex G ∧

476 ∃ V : ℕ → Subgroup G,

477 V 0 = ⊤ ∧

478 Antitone V ∧

479 (∀ n, IsOpen ((V n : Subgroup G) : Set G)) ∧

480 (∀ n, IsTopologicallyCharacteristic G (V n)) ∧

481 ∀ U : Set G, U ∈ 𝓝 (1 : G) → ∃ n, ((V n : Subgroup G) : Set G) ⊆ U := by

482 exact ⟨hasFiniteOpenSubgroupsOfIndex_of_topologicallyFinitelyGenerated (G := G) hG,

483 exists_characteristicOpenBasis_of_topologicallyFinitelyGenerated (G := G) hG⟩

484

485end IndexFamilies

486

487

488section HopfianStep

489

490variable {G : Type u} [Group G] [TopologicalSpace G]

491

492namespace Set

493

494/-- An injective self-map of a finite set is automatically surjective on that set. -/

495theorem Finite.surjOn_of_injOn_mapsTo {α : Type*} {s : Set α}

496 (hs : s.Finite) {f : α → α}

497 (hf : MapsTo f s s) (hinj : InjOn f s) :

498 SurjOn f s s := by

499 classical

500 let g : s → s := fun x => ⟨f x.1, hf x.2⟩

501 have hg_inj : Function.Injective g := by

502 intro x y hxy

503 apply Subtype.ext

504 exact hinj x.2 y.2 (congrArg Subtype.val hxy)

505 haveI := hs.to_subtype

506 have hg_surj : Function.Surjective g := Finite.surjective_of_injective hg_inj

507 intro y hy

508 rcases hg_surj ⟨y, hy⟩ with ⟨x, hx⟩

509 refine ⟨x.1, x.2, ?_⟩

510 exact congrArg Subtype.val hx

511

512end Set

513

514/-- Open normal subgroups separate the identity from every nontrivial element. -/

515def OpenNormalSeparatesPoints (G : Type u) [Group G] [TopologicalSpace G]

516 : Prop :=

517 ∀ x : G, x ≠ 1 → ∃ U : Subgroup G, U.Normal ∧ IsOpen (U : Set G) ∧ x ∉ U

518

519/--

520If every kernel element lies in every open normal subgroup and open normal subgroups separate

521points, then the endomorphism is injective.

522-/

523theorem injective_of_ker_le_every_openNormal

524 {φ : ContinuousMonoidHom G G}

525 (hker : ∀ U : Subgroup G, U.Normal → IsOpen (U : Set G) → φ.ker ≤ U)

526 (hsep : OpenNormalSeparatesPoints G) :

527 Function.Injective φ := by

528 intro x y hxy

529 have hmem : x * y⁻¹ ∈ φ.ker := by

530 simp only [ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.mem_ker, MonoidHom.coe_coe,

531 map_mul, hxy, map_inv,

532 mul_inv_cancel]

533 have hone : x * y⁻¹ = 1 := by

534 by_contra hne

535 obtain ⟨U, hU_normal, hU_open, hnotU⟩ := hsep (x * y⁻¹) hne

536 exact hnotU (hker U hU_normal hU_open hmem)

537 have hmul := congrArg (fun z => z * y) hone

538 simpa [mul_assoc] using hmul

539

540/-- The preimage operator preserves the fixed-index family of open normal subgroups. -/

541def PreimagePreservesOpenNormalSubgroupsOfIndex

542 (φ : ContinuousMonoidHom G G) : Prop :=

543 ∀ n,

544 Set.MapsTo (fun U : Subgroup G => Subgroup.comap φ.toMonoidHom U)

545 (OpenNormalSubgroupsOfIndex (G := G) n)

546 (OpenNormalSubgroupsOfIndex (G := G) n)

547

548omit [TopologicalSpace G] in

549/-- Comap along a surjective homomorphism is injective on subgroups. -/

550theorem subgroupComap_injective_of_surjective

551 {H : Type v} [Group H]

552 (f : G →* H) (hf : Function.Surjective f) :

553 Function.Injective (Subgroup.comap f) := by

554 intro U V hUV

555 ext y

556 constructor <;> intro hy

557 · rcases hf y with ⟨x, rfl⟩

558 change x ∈ Subgroup.comap f V

559 have hx : x ∈ Subgroup.comap f U := hy

560 simpa [hUV] using hx

561 · rcases hf y with ⟨x, rfl⟩

562 change x ∈ Subgroup.comap f U

563 have hx : x ∈ Subgroup.comap f V := hy

564 simpa [hUV] using hx

565

566/-- Preimage under a surjective endomorphism is injective on each fixed-index open-normal family. -/

567theorem preimage_injectiveOn_openNormalSubgroupsOfIndex

568 {φ : ContinuousMonoidHom G G}

569 (hφsurj : Function.Surjective φ) (n : ℕ) :

570 Set.InjOn (fun U : Subgroup G => Subgroup.comap φ.toMonoidHom U)

571 (OpenNormalSubgroupsOfIndex (G := G) n) := by

572 intro U hU V hV hEq

573 exact subgroupComap_injective_of_surjective (G := G) φ.toMonoidHom hφsurj hEq

574

575/--

576Surjectivity of the preimage operator on each family of open normal subgroups of index \(n\).

577This is exactly the conclusion obtained from the finiteness of the family \(U_n\).

578-/

579def PreimageSurjectiveOnOpenNormalSubgroupsOfIndex

580 (φ : ContinuousMonoidHom G G) : Prop :=

581 ∀ n,

582 Set.SurjOn (fun U : Subgroup G => Subgroup.comap φ.toMonoidHom U)

583 (OpenNormalSubgroupsOfIndex (G := G) n)

584 (OpenNormalSubgroupsOfIndex (G := G) n)

585

586/--

587For finite groups, preimage along a surjective endomorphism is surjective on open normal

588subgroups of fixed index.

589-/

590theorem preimageSurjectiveOn_openNormalSubgroupsOfIndex_of_finite

591 {φ : ContinuousMonoidHom G G}

592 (hfin : HasFiniteOpenNormalSubgroupsOfIndex G)

593 (hφsurj : Function.Surjective φ)

594 (hpres : PreimagePreservesOpenNormalSubgroupsOfIndex (G := G) φ) :

595 PreimageSurjectiveOnOpenNormalSubgroupsOfIndex (G := G) φ := by

596 intro n

597 exact Set.Finite.surjOn_of_injOn_mapsTo

598 (hs := hfin n)

599 (f := fun U : Subgroup G => Subgroup.comap φ.toMonoidHom U)

600 (hpres n)

601 (preimage_injectiveOn_openNormalSubgroupsOfIndex (G := G) hφsurj n)

602

603/--

604If the preimage map is surjective on every fixed-index open-normal family, then \(\ker \varphi

605\le U\) for every open normal subgroup \(U\).

606-/

607theorem ker_le_every_openNormal_of_preimageSurjectiveOn_index

608 [IsTopologicalGroup G] [CompactSpace G]

609 {φ : ContinuousMonoidHom G G}

610 (hφ : PreimageSurjectiveOnOpenNormalSubgroupsOfIndex (G := G) φ) :

611 ∀ U : Subgroup G, U.Normal → IsOpen (U : Set G) → φ.ker ≤ U := by

612 intro U hU_normal hU_open

613 have hUfinite : Finite (G ⧸ U) :=

614 Subgroup.quotient_finite_of_isOpen U hU_open

615 let n : ℕ := Nat.card (G ⧸ U)

616 have hU : U ∈ OpenNormalSubgroupsOfIndex (G := G) n := by

617 exact ⟨hU_normal, hU_open, hUfinite, rfl⟩

618 rcases hφ n hU with ⟨V, hV, hEq⟩

619 rw [← hEq]

620 intro x hx

621 change φ x ∈ V

622 have hx1 : φ x = 1 := by

623 change φ x = 1 at hx

624 exact hx

625 rw [hx1]

626 exact V.one_mem

627

628/-- The fixed-index Hopfian kernel-separation hypotheses imply injectivity. -/

629theorem injective_of_preimageSurjectiveOn_openNormalIndex

630 [IsTopologicalGroup G] [CompactSpace G]

631 {φ : ContinuousMonoidHom G G}

632 (hφ : PreimageSurjectiveOnOpenNormalSubgroupsOfIndex (G := G) φ)

633 (hsep : OpenNormalSeparatesPoints G) :

634 Function.Injective φ := by

635 apply injective_of_ker_le_every_openNormal

636 · exact ker_le_every_openNormal_of_preimageSurjectiveOn_index (G := G) hφ

637 · exact hsep

638

639/--

640A topological group is continuously Hopfian if every surjective continuous endomorphism is

641injective.

642-/

643def ContinuousHopfian (G : Type u) [Group G] [TopologicalSpace G] : Prop :=

644 ∀ φ : ContinuousMonoidHom G G, Function.Surjective φ → Function.Injective φ

645

646/-- Every surjective continuous endomorphism is induced by a continuous automorphism. -/

647def SurjectiveContinuousEndomorphismsAreAutomorphisms

648 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=

649 ∀ φ : ContinuousMonoidHom G G, Function.Surjective φ →

650 ∃ e : G ≃ₜ* G, ∀ x : G, e x = φ x

651

652/--

653Upgrade a continuous bijective endomorphism of a compact Hausdorff topological group to a

654continuous automorphism.

655-/

656noncomputable def ContinuousMonoidHom.toContinuousMulEquivOfBijective

657 [CompactSpace G] [T2Space G]

658 (φ : ContinuousMonoidHom G G) (hφ : Function.Bijective φ) :

659 G ≃ₜ* G := by

660 let e : G ≃ G := Equiv.ofBijective φ hφ

661 let eh : G ≃ₜ G :=

662 e.toHomeomorphOfContinuousClosed φ.continuous_toFun

663 (Continuous.isClosedMap φ.continuous_toFun)

664 exact ContinuousMulEquiv.mk' eh (by

665 intro x y

666 exact φ.map_mul x y)

667

668/-- A continuously Hopfian group has all surjective continuous endomorphisms invertible. -/

669theorem surjectiveContinuousEndomorphismsAreAutomorphisms_of_continuousHopfian

670 [CompactSpace G] [T2Space G]

671 (hhopf : ContinuousHopfian G) :

672 SurjectiveContinuousEndomorphismsAreAutomorphisms G := by

673 intro φ hφsurj

674 let e := ContinuousMonoidHom.toContinuousMulEquivOfBijective

675 (G := G) φ ⟨hhopf φ hφsurj, hφsurj⟩

676 refine ⟨e, ?_⟩

677 intro x

678 rfl

679

680/--

681Once the preimage-surjectivity statement on fixed-index open normal subgroups is available for

682all surjective continuous endomorphisms, the Hopfian conclusion follows mathematically.

683-/

684theorem continuousHopfian_of_preimageSurjectiveOn_openNormalIndex

685 [IsTopologicalGroup G] [CompactSpace G]

686 (hsep : OpenNormalSeparatesPoints G)

687 (hpre : ∀ φ : ContinuousMonoidHom G G, Function.Surjective φ →

688 PreimageSurjectiveOnOpenNormalSubgroupsOfIndex (G := G) φ) :

689 ContinuousHopfian G := by

690 intro φ hφsurj

691 exact injective_of_preimageSurjectiveOn_openNormalIndex (G := G) (hpre φ hφsurj) hsep

692

693/-- Finiteness of open normal subgroups of each index implies the continuous Hopfian property. -/

694theorem continuousHopfian_of_finiteOpenNormalSubgroupsOfIndex

695 [IsTopologicalGroup G] [CompactSpace G]

696 (hsep : OpenNormalSeparatesPoints G)

697 (hfin : HasFiniteOpenNormalSubgroupsOfIndex G)

698 (hpres :

699 ∀ φ : ContinuousMonoidHom G G, Function.Surjective φ →

700 PreimagePreservesOpenNormalSubgroupsOfIndex (G := G) φ) :

701 ContinuousHopfian G := by

702 apply continuousHopfian_of_preimageSurjectiveOn_openNormalIndex (G := G) hsep

703 intro φ hφsurj

704 exact preimageSurjectiveOn_openNormalSubgroupsOfIndex_of_finite

705 (G := G) hfin hφsurj (hpres φ hφsurj)

706

707/-- Fixed-index finiteness of open normal subgroups implies the profinite Hopfian conclusion. -/

708theorem surjContinuousEndomorphismsAreAutomorphisms_of_finiteOpenNormalSubgroupsOfIndex

709 [IsTopologicalGroup G] [CompactSpace G] [T2Space G]

710 (hsep : OpenNormalSeparatesPoints G)

711 (hfin : HasFiniteOpenNormalSubgroupsOfIndex G)

712 (hpres :

713 ∀ φ : ContinuousMonoidHom G G, Function.Surjective φ →

714 PreimagePreservesOpenNormalSubgroupsOfIndex (G := G) φ) :

715 SurjectiveContinuousEndomorphismsAreAutomorphisms G := by

716 apply surjectiveContinuousEndomorphismsAreAutomorphisms_of_continuousHopfian

717 exact continuousHopfian_of_finiteOpenNormalSubgroupsOfIndex (G := G) hsep hfin hpres

718

719/--

720In a profinite group, open normal subgroups separate the identity from every nontrivial element.

721-/

722theorem openNormalSeparatesPoints_of_profinite

723 [IsTopologicalGroup G] [CompactSpace G] [T1Space G] [TotallyDisconnectedSpace G] :

724 OpenNormalSeparatesPoints G := by

725 intro x hx

726 let U : Set G := ({x} : Set G)ᶜ

727 have hUopen : IsOpen U := isClosed_singleton.isOpen_compl

728 have h1U : (1 : G) ∈ U := by

729 simpa [U, eq_comm] using hx

730 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hUopen h1U with ⟨N, hNU⟩

731 refine ⟨N, N.isNormal', openNormalSubgroup_isOpen (G := G) N, ?_⟩

732 intro hxN

733 have hxU : x ∈ U := hNU hxN

734 simp only [mem_compl_iff, mem_singleton_iff, not_true_eq_false, U] at hxU

735

736/--

737Preimage along a surjective continuous endomorphism preserves open normal subgroups of fixed

738index.

739-/

740theorem preimagePreservesOpenNormalSubgroupsOfIndex_of_surjective

741 [IsTopologicalGroup G] [CompactSpace G]

742 {φ : ContinuousMonoidHom G G} (hφsurj : Function.Surjective φ) :

743 PreimagePreservesOpenNormalSubgroupsOfIndex (G := G) φ := by

744 intro n U hU

745 refine ⟨?_, ?_, ?_, ?_⟩

746 · exact hU.1.comap φ.toMonoidHom

747 · exact hU.2.1.preimage φ.continuous_toFun

748 · exact Subgroup.quotient_finite_of_isOpen

749 (Subgroup.comap φ.toMonoidHom U) (hU.2.1.preimage φ.continuous_toFun)

750 · simpa [Subgroup.index_eq_card] using

751 (Subgroup.index_comap_of_surjective (H := U) hφsurj).trans hU.2.2.2

752

753/--

754A surjective continuous endomorphism of a topologically finitely generated profinite group is

755automatically a continuous automorphism.

756-/

757theorem surjContinuousEndomorphismsAreAutomorphisms_of_topologicallyFinitelyGenerated

758 [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

759 : TopologicallyFinitelyGenerated G →

760 ∀ φ : ContinuousMonoidHom G G, Function.Surjective φ →

761 ∃ e : G ≃ₜ* G, ∀ x : G, e x = φ x := by

762 intro hG

763 apply surjContinuousEndomorphismsAreAutomorphisms_of_finiteOpenNormalSubgroupsOfIndex

764 · exact openNormalSeparatesPoints_of_profinite (G := G)

765 · exact HasFiniteOpenSubgroupsOfIndex.toHasFiniteOpenNormalSubgroupsOfIndex

766 (h := hasFiniteOpenSubgroupsOfIndex_of_topologicallyFinitelyGenerated (G := G) hG)

767 · intro φ hφsurj

768 exact preimagePreservesOpenNormalSubgroupsOfIndex_of_surjective (G := G) hφsurj

769

770end HopfianStep

771

772

773end ProCGroups.FiniteGeneration