Yamaguchi Lean 4 Library
ProCGroups/FiniteGeneration/CharacteristicChainsAndIndices.lean
ProCGroups/FiniteGeneration/CharacteristicChainsAndIndices/Source

ProCGroups/FiniteGeneration/CharacteristicChainsAndIndices.lean

1import ProCGroups.FiniteGeneration.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/FiniteGeneration/CharacteristicChainsAndIndices.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Finite generation and characteristic chains
14Records finite generation criteria for profinite groups, finite-index/open-subgroup counting, characteristic cores, and index bounds.
15-/
17open Set
18open scoped Topology Pointwise
20namespace ProCGroups.FiniteGeneration
22universe u v w
24open ProCGroups.Generation
25open ProCGroups.ProC
28section CharacteristicChains
30variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
32/--
33A countable descending chain of open characteristic subgroups.
34This packages the standard bounded-index characteristic-chain data.
35-/
37 toSubgroup : ℕ → Subgroup G
38 zero_eq_top : toSubgroup 0 = ⊤
39 antitone : Antitone toSubgroup
40 isOpen' : ∀ n, IsOpen ((toSubgroup n : Set G))
41 isTopologicallyCharacteristic' : ∀ n, IsTopologicallyCharacteristic G (toSubgroup n)
43end CharacteristicChains
45section IndexFamilies
47variable {G : Type u} [Group G] [TopologicalSpace G]
49/-- A subgroup together with evidence that its quotient has finite cardinality. -/
50structure FiniteIndexSubgroup (G : Type u) [Group G] where
51 subgroup : Subgroup G
52 quotient_finite : Finite (G ⧸ subgroup)
56/-- The index of a finite-index subgroup. -/
57noncomputable def index (H : FiniteIndexSubgroup G) : Nat :=
58 haveI := H.quotient_finite
59 Nat.card (G ⧸ H.subgroup)
63/-- An open subgroup together with evidence that its quotient has finite cardinality. -/
64structure OpenSubgroupOfFiniteIndex (G : Type u) [Group G] [TopologicalSpace G] where
65 subgroup : OpenSubgroup G
66 quotient_finite : Finite (G ⧸ (subgroup : Subgroup G))
70/-- The index of an open finite-index subgroup. -/
71noncomputable def index (H : OpenSubgroupOfFiniteIndex G) : Nat :=
72 haveI := H.quotient_finite
73 Nat.card (G ⧸ (H.subgroup : Subgroup G))
77namespace OpenSubgroup
79/-- In a compact topological group, an open subgroup has finite index. -/
80def toFiniteIndex [IsTopologicalGroup G] [CompactSpace G] (U : OpenSubgroup G) :
82 subgroup := U
83 quotient_finite :=
84 Subgroup.quotient_finite_of_isOpen (U : Subgroup G) (openSubgroup_isOpen (G := G) U)
86end OpenSubgroup
88/--
89The open subgroups of index at most `n`.
90This is the bounded-index family whose intersection defines the characteristic core.
91-/
92def OpenSubgroupsOfIndexLE (G : Type u) [Group G] [TopologicalSpace G]
93 (n : ℕ) : Set (Subgroup G) :=
94 { H | IsOpen (H : Set G) ∧ Finite (G ⧸ H) ∧ Nat.card (G ⧸ H) ≤ n }
96/--
97The open normal subgroups of index exactly `n`.
98This is the fixed-index family used in the Hopfian finite-quotient argument.
99-/
100def OpenNormalSubgroupsOfIndex (G : Type u) [Group G] [TopologicalSpace G]
101 (n : ℕ) : Set (Subgroup G) :=
102 { U | U.Normal ∧ IsOpen (U : Set G) ∧ Finite (G ⧸ U) ∧ Nat.card (G ⧸ U) = n }
106variable {G : Type u} [Group G] [TopologicalSpace G]
108/-- Membership criterion for the finite set of open subgroups of index at most `n`. -/
109@[simp] theorem mem_openSubgroupsOfIndexLE {n : ℕ} {H : Subgroup G} :
110 H ∈ OpenSubgroupsOfIndexLE (G := G) n ↔
111 IsOpen (H : Set G) ∧ Finite (G ⧸ H) ∧ Nat.card (G ⧸ H) ≤ n :=
112 Iff.rfl
114/-- Membership criterion for the finite set of open normal subgroups of a fixed index. -/
115@[simp] theorem mem_openNormalSubgroupsOfIndex {n : ℕ} {U : Subgroup G} :
116 U ∈ OpenNormalSubgroupsOfIndex (G := G) n ↔
117 U.Normal ∧ IsOpen (U : Set G) ∧ Finite (G ⧸ U) ∧ Nat.card (G ⧸ U) = n :=
118 Iff.rfl
120/--
121The canonical bounded-index intersection
122`Vₙ = ⋂ {H ≤ G | H open and [G : H] ≤ n}`.
123-/
124def CharacteristicIndexIntersection (G : Type u) [Group G] [TopologicalSpace G]
125 (n : ℕ) : Subgroup G :=
126 sInf (OpenSubgroupsOfIndexLE (G := G) n)
128/-- The characteristic index intersection is the infimum of all open subgroups of bounded index. -/
129@[simp] theorem characteristicIndexIntersection_def (n : ℕ) :
131 sInf (OpenSubgroupsOfIndexLE (G := G) n) :=
132 rfl
134/--
135Basic bounded-index intersection package:
136the canonical bounded-index intersections are open, characteristic, descending,
137and cofinal among open subgroups.
138-/
140 isOpen' : ∀ n, IsOpen ((CharacteristicIndexIntersection (G := G) n : Set G))
141 isTopologicallyCharacteristic' : ∀ n, IsTopologicallyCharacteristic G (CharacteristicIndexIntersection (G := G) n)
142 antitone' : Antitone (CharacteristicIndexIntersection (G := G))
143 cofinal' :
144 ∀ U : Subgroup G, IsOpen (U : Set G) →
145 ∃ n, CharacteristicIndexIntersection (G := G) n ≤ U
147/-- A group has only finitely many open subgroups of each prescribed index. -/
148def HasFiniteOpenSubgroupsOfIndex (G : Type u) [Group G] [TopologicalSpace G]
149 : Prop :=
150 ∀ n, Set.Finite
151 { H : Subgroup G | IsOpen (H : Set G) ∧ Finite (G ⧸ H) ∧ Nat.card (G ⧸ H) = n }
153/-- Normal-subgroup version of fixed-index finiteness. -/
154def HasFiniteOpenNormalSubgroupsOfIndex (G : Type u) [Group G] [TopologicalSpace G]
155 : Prop :=
156 ∀ n,
157 Set.Finite
158 { U : Subgroup G |
159 U.Normal ∧ IsOpen (U : Set G) ∧ Finite (G ⧸ U) ∧ Nat.card (G ⧸ U) = n }
161/-- Finiteness of open subgroups of each index implies finiteness of open normal subgroups of each index. -/
162theorem HasFiniteOpenSubgroupsOfIndex.toHasFiniteOpenNormalSubgroupsOfIndex
165 intro n
166 refine (h n).subset ?_
167 intro U hU
168 exact ⟨hU.2.1, hU.2.2.1, hU.2.2.2⟩
170/-- Continuous homomorphisms are equal when they agree on a topological generating set. -/
172 [IsTopologicalGroup G]
173 {R : Type v} [Group R] [TopologicalSpace R] [T2Space R]
174 {s : Finset G} (hsgen : TopologicallyGenerates (G := G) (↑s : Set G))
175 {f g : ContinuousMonoidHom G R}
176 (hfg : ∀ x ∈ (↑s : Set G), f x = g x) :
177 f = g := by
178 let K : Subgroup G := {
179 carrier := { x | f x = g x }
180 one_mem' := by simp only [mem_setOf_eq, map_one]
181 mul_mem' := by
182 intro a b ha hb
183 change f (a * b) = g (a * b)
184 rw [map_mul, map_mul, ha, hb]
185 inv_mem' := by
186 intro a ha
187 simpa using congrArg Inv.inv ha
188 }
189 have hKclosed : IsClosed ((K : Subgroup G) : Set G) := by
190 change IsClosed { x | f x = g x }
191 exact isClosed_eq f.continuous_toFun g.continuous_toFun
192 have hsub : Subgroup.closure (↑s : Set G) ≤ K := by
193 rw [Subgroup.closure_le]
194 intro x hx
195 exact hfg x hx
196 have htop : (⊤ : Subgroup G) ≤ K := by
197 have hcl :
198 (Subgroup.closure (↑s : Set G)).topologicalClosure ≤ K :=
199 Subgroup.topologicalClosure_minimal _ hsub hKclosed
201 simpa [hsgen] using hcl
202 ext x
203 simpa [K] using htop (show x ∈ (⊤ : Subgroup G) from by simp only [Subgroup.mem_top])
205/-- A finitely generated profinite group admits only finitely many continuous homomorphisms
206into a fixed finite discrete target. -/
208 [IsTopologicalGroup G]
209 {R : Type v} [Group R] [TopologicalSpace R] [T2Space R] [Finite R]
211 Finite (ContinuousMonoidHom G R) := by
212 classical
213 rcases hG with ⟨s, hsgen⟩
214 let eval : ContinuousMonoidHom G R → ((↑s : Set G) → R) := fun φ x => φ x.1
215 have heval : Function.Injective eval := by
216 intro φ ψ hφψ
218 intro x hx
219 exact congrArg (fun k => k ⟨x, hx⟩) hφψ
220 exact Finite.of_injective eval heval
222/-- The chosen identification `G ⧸ H ≃ Fin n` for an index-`n` subgroup. -/
223noncomputable def openSubgroupIndexEquiv
224 (H : Subgroup G) (hHfinite : Finite (G ⧸ H)) {n : ℕ}
225 (hn : Nat.card (G ⧸ H) = n) :
226 (G ⧸ H) ≃ Fin n := by
227 classical
228 letI : Finite (G ⧸ H) := hHfinite
229 letI : Fintype (G ⧸ H) := Fintype.ofFinite (G ⧸ H)
230 refine Finite.equivFinOfCardEq ?_
231 simpa [Nat.card_eq_fintype_card] using hn
233/-- The coset action of `G` on the `n` cosets of an index-`n` subgroup, transported to `Fin n`. -/
234noncomputable def openSubgroupIndexAction
235 (H : Subgroup G) (hHfinite : Finite (G ⧸ H)) {n : ℕ}
236 (hn : Nat.card (G ⧸ H) = n) :
237 G →* Equiv.Perm (Fin n) := by
238 classical
239 let e := openSubgroupIndexEquiv (G := G) H hHfinite hn
240 exact e.permCongrHom.toMonoidHom.comp (MulAction.toPermHom G (G ⧸ H))
242/-- The image of the identity coset under the chosen `Fin n` identification. -/
244 (H : Subgroup G) (hHfinite : Finite (G ⧸ H)) {n : ℕ}
245 (hn : Nat.card (G ⧸ H) = n) : Fin n :=
246 openSubgroupIndexEquiv (G := G) H hHfinite hn (QuotientGroup.mk 1)
248instance instTopologicalSpaceFinitePerm (n : ℕ) : TopologicalSpace (Equiv.Perm (Fin n)) :=
249 ⊥
251instance instDiscreteTopologyFinitePerm (n : ℕ) : DiscreteTopology (Equiv.Perm (Fin n)) :=
252 ⟨rfl⟩
254instance instIsTopologicalGroupFinitePerm (n : ℕ) : IsTopologicalGroup (Equiv.Perm (Fin n)) := by
255 infer_instance
257instance instFiniteFinitePerm (n : ℕ) : Finite (Equiv.Perm (Fin n)) := by
258 infer_instance
260/-- The finite coset action, viewed as a continuous homomorphism into a discrete permutation
261group. -/
263 [IsTopologicalGroup G] [CompactSpace G]
264 (H : Subgroup G) (hH : IsOpen (H : Set G)) {n : ℕ}
265 (hHfinite : Finite (G ⧸ H)) (hn : Nat.card (G ⧸ H) = n) :
266 G →ₜ* Equiv.Perm (Fin n) := by
267 classical
268 let φ : G →* Equiv.Perm (Fin n) := openSubgroupIndexAction (G := G) H hHfinite hn
269 have hφker :
270 IsOpen ((φ.ker : Subgroup G) : Set G) := by
271 let e := openSubgroupIndexEquiv (G := G) H hHfinite hn
272 have hker :
273 φ.ker = (MulAction.toPermHom G (G ⧸ H)).ker := by
274 ext g
275 change e.permCongr (MulAction.toPerm g) = 1 ↔ MulAction.toPerm g = 1
276 have hperm_one :
277 e.permCongr (1 : Equiv.Perm (G ⧸ H)) = (1 : Equiv.Perm (Fin n)) := by
278 ext x
279 simp only [Equiv.permCongr_apply, Equiv.Perm.coe_one, id_eq, Equiv.apply_symm_apply]
280 rw [← hperm_one]
281 exact e.permCongr.injective.eq_iff
282 letI : Finite (G ⧸ H) := Subgroup.quotient_finite_of_isOpen H hH
283 letI : H.FiniteIndex := Subgroup.finiteIndex_of_finite_quotient (H := H)
284 have hHclosed : IsClosed ((H : Subgroup G) : Set G) :=
285 Subgroup.isClosed_of_isOpen H hH
286 letI : H.normalCore.FiniteIndex := Subgroup.finiteIndex_normalCore (H := H)
287 have hopenCore : IsOpen (((H.normalCore : Subgroup G) : Set G)) :=
288 H.normalCore.isOpen_of_isClosed_of_finiteIndex (H.normalCore_isClosed hHclosed)
289 simpa [hker, Subgroup.normalCore_eq_ker (H := H)] using hopenCore
290 have hφcont : Continuous φ := by
291 letI : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
292 letI : UniformSpace (Equiv.Perm (Fin n)) :=
293 IsTopologicalGroup.rightUniformSpace (Equiv.Perm (Fin n))
294 have hφuc :
295 UniformContinuous φ :=
296 (IsUniformGroup.uniformContinuous_iff_isOpen_ker (f := φ)).2 hφker
297 exact hφuc.continuous
298 exact
299 { toMonoidHom := φ
300 continuous_toFun := hφcont }
302omit [TopologicalSpace G] in
303/-- Membership in an open subgroup is equivalent to fixing the basepoint in its coset action. -/
305 {H : Subgroup G} (hHfinite : Finite (G ⧸ H)) {n : ℕ}
306 (hn : Nat.card (G ⧸ H) = n) {g : G} :
307 g ∈ H ↔
308 openSubgroupIndexAction (G := G) H hHfinite hn g
309 (openSubgroupIndexBasepoint (G := G) H hHfinite hn) =
310 openSubgroupIndexBasepoint (G := G) H hHfinite hn := by
311 classical
312 let e := openSubgroupIndexEquiv (G := G) H hHfinite hn
313 constructor
314 · intro hg
315 have hq : QuotientGroup.mk (s := H) g = QuotientGroup.mk (s := H) 1 := by
316 simpa [QuotientGroup.eq] using hg
318 · intro hg
319 have hq :
320 QuotientGroup.mk (s := H) g = QuotientGroup.mk (s := H) 1 := by
321 apply e.injective
323 simpa [QuotientGroup.eq] using hq
325/-- Finitely generated profinite groups have only finitely many open subgroups of each index. -/
327 [IsTopologicalGroup G] [CompactSpace G]
330 intro n
331 classical
332 let S : Type u :=
333 { H : Subgroup G // IsOpen (H : Set G) ∧ Finite (G ⧸ H) ∧ Nat.card (G ⧸ H) = n }
334 letI : TopologicalSpace (Equiv.Perm (Fin n)) := ⊥
335 letI : DiscreteTopology (Equiv.Perm (Fin n)) := ⟨rfl⟩
336 letI : IsTopologicalGroup (Equiv.Perm (Fin n)) := by infer_instance
337 letI : Finite (Equiv.Perm (Fin n)) := by infer_instance
338 let code : S → ContinuousMonoidHom G (Equiv.Perm (Fin n)) × Fin n := fun H =>
339 let φ := openSubgroupIndexAction (G := G) H.1 H.2.2.1 H.2.2.2
340 let e := openSubgroupIndexEquiv (G := G) H.1 H.2.2.1 H.2.2.2
341 let hφker :
342 IsOpen ((φ.ker : Subgroup G) : Set G) := by
343 letI : Finite (G ⧸ H.1) := H.2.2.1
344 letI : H.1.FiniteIndex := Subgroup.finiteIndex_of_finite_quotient (H := H.1)
345 have hHclosed : IsClosed ((H.1 : Subgroup G) : Set G) :=
346 Subgroup.isClosed_of_isOpen H.1 H.2.1
347 have hker :
348 φ.ker = (MulAction.toPermHom G (G ⧸ H.1)).ker := by
349 ext g
350 change
351 e.permCongr (MulAction.toPerm g) = 1 ↔ MulAction.toPerm g = 1
352 have hperm_one : e.permCongr (1 : Equiv.Perm (G ⧸ H.1)) = (1 : Equiv.Perm (Fin n)) := by
353 ext x
354 simp only [Equiv.permCongr_apply, Equiv.Perm.coe_one, id_eq, Equiv.apply_symm_apply]
355 rw [← hperm_one]
356 exact e.permCongr.injective.eq_iff
357 letI : H.1.normalCore.FiniteIndex := Subgroup.finiteIndex_normalCore (H := H.1)
358 have hopenCore : IsOpen (((H.1).normalCore : Subgroup G) : Set G) :=
359 (H.1).normalCore.isOpen_of_isClosed_of_finiteIndex ((H.1).normalCore_isClosed hHclosed)
360 simpa [hker, Subgroup.normalCore_eq_ker (H := H.1)] using hopenCore
361 let hφcont :
362 Continuous φ := by
363 letI : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
364 letI : UniformSpace (Equiv.Perm (Fin n)) :=
365 IsTopologicalGroup.rightUniformSpace (Equiv.Perm (Fin n))
366 have hφuc :
367 UniformContinuous φ :=
368 (IsUniformGroup.uniformContinuous_iff_isOpen_ker (f := φ)).2 hφker
369 exact hφuc.continuous
370 ({ toMonoidHom := φ
371 continuous_toFun := hφcont },
372 openSubgroupIndexBasepoint (G := G) H.1 H.2.2.1 H.2.2.2)
373 have hhomfinite : Finite (ContinuousMonoidHom G (Equiv.Perm (Fin n))) :=
375 (G := G) hG
376 let _ : Finite (ContinuousMonoidHom G (Equiv.Perm (Fin n)) × Fin n) := by
377 infer_instance
378 have hcode : Function.Injective code := by
379 intro H K hHK
380 apply Subtype.ext
381 ext g
382 rw [mem_openSubgroup_iff_indexAction_fix_basepoint (G := G) (H := H.1) H.2.2.1 H.2.2.2
383 (g := g),
384 mem_openSubgroup_iff_indexAction_fix_basepoint (G := G) (H := K.1) K.2.2.1 K.2.2.2
385 (g := g)]
386 exact Iff.of_eq <| by
387 simpa [code] using congrArg
388 (fun p : ContinuousMonoidHom G (Equiv.Perm (Fin n)) × Fin n => p.1 g p.2 = p.2) hHK
389 have hSfinite :
390 Finite
391 { H : Subgroup G //
392 IsOpen (H : Set G) ∧ Finite (G ⧸ H) ∧ Nat.card (G ⧸ H) = n } := by
393 simpa [S] using (Finite.of_injective code hcode)
394 exact @Set.toFinite (Subgroup G)
395 { H : Subgroup G | IsOpen (H : Set G) ∧ Finite (G ⧸ H) ∧ Nat.card (G ⧸ H) = n }
396 hSfinite
398/-- Bounding the index by `n` still yields only finitely many open subgroups. -/
400 (hfin : HasFiniteOpenSubgroupsOfIndex G) (n : ℕ) :
401 Set.Finite (OpenSubgroupsOfIndexLE (G := G) n) := by
402 classical
403 refine Set.Finite.subset ((Set.finite_le_nat n).biUnion fun m hm => hfin m) ?_
404 intro H hH
405 exact Set.mem_iUnion.2
406 ⟨Nat.card (G ⧸ H), Set.mem_iUnion.2 ⟨hH.2.2, ⟨hH.1, hH.2.1, rfl⟩⟩⟩
408/-- The infimum of a finite family of open subgroups is open. -/
409theorem Subgroup.isOpen_sInf_of_finite
410 {S : Set (Subgroup G)} (hS : S.Finite)
411 (hopen : ∀ H ∈ S, IsOpen (H : Set G)) :
412 IsOpen ((sInf S : Subgroup G) : Set G) := by
413 classical
414 induction S, hS using Set.Finite.induction_on with
415 | empty =>
416 simp only [sInf_empty, Subgroup.coe_top, isOpen_univ]
417 | @insert H S hHS hS ih =>
418 rw [sInf_insert]
419 exact (hopen H (by simp only [mem_insert_iff, true_or])).inter (ih fun K hK => hopen K (by simp only [mem_insert_iff, hK, or_true]))
421/-- The bounded-index characteristic intersection is open
422once the bounded-index family is finite. -/
424 (hfin : HasFiniteOpenSubgroupsOfIndex G) (n : ℕ) :
425 IsOpen ((CharacteristicIndexIntersection (G := G) n : Set G)) := by
426 apply Subgroup.isOpen_sInf_of_finite
428 · intro H hH
429 exact hH.1
431/-- The bounded-index characteristic intersections form a descending chain. -/
433 Antitone (CharacteristicIndexIntersection (G := G)) := by
434 intro m n hmn x hx
435 simp only [CharacteristicIndexIntersection, Subgroup.mem_sInf] at hx ⊢
436 intro H hH
437 exact hx H ⟨hH.1, hH.2.1, le_trans hH.2.2 hmn⟩
439/-- The finite-index characteristic intersection is characteristic. -/
441 [IsTopologicalGroup G] [CompactSpace G]
442 (n : ℕ) :
444 have hforward :
445 ∀ φ : G ≃ₜ* G, ∀ g : G,
447 φ g ∈ CharacteristicIndexIntersection (G := G) n := by
448 intro φ g hg
449 simp only [CharacteristicIndexIntersection, Subgroup.mem_sInf] at hg ⊢
450 intro H hH
451 have hcomap :
452 Subgroup.comap φ.toMonoidHom H ∈ OpenSubgroupsOfIndexLE (G := G) n := by
453 have hcomapOpen : IsOpen ((Subgroup.comap φ.toMonoidHom H : Subgroup G) : Set G) :=
454 hH.1.preimage φ.continuous_toFun
455 have hcomapFinite : Finite (G ⧸ Subgroup.comap φ.toMonoidHom H) :=
456 Subgroup.quotient_finite_of_isOpen (Subgroup.comap φ.toMonoidHom H) hcomapOpen
457 refine ⟨hcomapOpen, hcomapFinite, ?_⟩
458 simpa [Subgroup.index_eq_card] using
459 (Subgroup.index_comap_of_surjective (H := H) φ.surjective).le.trans hH.2.2
460 exact hg _ hcomap
461 intro φ g
462 constructor
463 · intro hg
464 simpa using hforward φ.symm (φ g) hg
465 · exact hforward φ g
467/-- Characteristic index intersections are cofinal among open subgroups. -/
469 [IsTopologicalGroup G] [CompactSpace G]
470 (U : Subgroup G) (hU : IsOpen (U : Set G)) :
471 ∃ n, CharacteristicIndexIntersection (G := G) n ≤ U := by
472 have hUfinite : Finite (G ⧸ U) :=
473 Subgroup.quotient_finite_of_isOpen U hU
474 refine ⟨Nat.card (G ⧸ U), ?_⟩
475 intro x hx
476 simp only [CharacteristicIndexIntersection, Subgroup.mem_sInf] at hx
477 exact hx U ⟨hU, hUfinite, le_rfl⟩
479/-- Fixed-index finiteness yields the full characteristic-intersection package. -/
481 [IsTopologicalGroup G] [CompactSpace G]
485 (G := G) hfin
486 isTopologicallyCharacteristic' :=
488 (G := G)
492/-- Convert characteristic index-intersection data into a characteristic open chain. -/
493def CharacteristicIndexIntersectionSpec.toCharacteristicOpenChain
496 toSubgroup
497 | 0 => ⊤
498 | n + 1 => CharacteristicIndexIntersection (G := G) n
499 zero_eq_top := rfl
500 antitone := by
501 intro m n hmn
502 cases m with
503 | zero =>
504 exact le_top
505 | succ m =>
506 cases n with
507 | zero =>
508 cases Nat.not_succ_le_zero m hmn
509 | succ n =>
510 exact hV.antitone' (Nat.succ_le_succ_iff.mp hmn)
511 isOpen' := by
512 intro n
513 cases n with
514 | zero =>
515 simp only [Subgroup.coe_top, isOpen_univ]
516 | succ n =>
517 exact hV.isOpen' n
518 isTopologicallyCharacteristic' := by
519 intro n
520 cases n with
521 | zero =>
522 simp only [IsTopologicallyCharacteristic.top]
523 | succ n =>
524 exact hV.isTopologicallyCharacteristic' n
526/-- A characteristic-intersection package produces a basis element
527inside any open neighborhood of `1`. -/
528theorem CharacteristicIndexIntersectionSpec.exists_subset_of_open_one_mem
529 [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
531 {U : Set G} (hUopen : IsOpen U) (h1U : (1 : G) ∈ U) :
532 ∃ n, ((CharacteristicIndexIntersection (G := G) n : Subgroup G) : Set G) ⊆ U := by
533 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hUopen h1U with ⟨N, hNU⟩
534 rcases hV.cofinal' (N : Subgroup G) (openNormalSubgroup_isOpen (G := G) N) with ⟨n, hn⟩
535 exact ⟨n, Set.Subset.trans hn hNU⟩
537/-- A characteristic-intersection package yields a countable characteristic open basis at the
538identity. -/
540 [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
542 ∃ V : ℕ → Subgroup G,
543 V 0 = ⊤ ∧
544 Antitone V ∧
545 (∀ n, IsOpen ((V n : Subgroup G) : Set G)) ∧
546 (∀ n, IsTopologicallyCharacteristic G (V n)) ∧
547 ∀ U : Set G, U ∈ 𝓝 (1 : G) → ∃ n, ((V n : Subgroup G) : Set G) ⊆ U := by
548 let V := hV.toCharacteristicOpenChain
549 refine ⟨V.toSubgroup, V.zero_eq_top, V.antitone, V.isOpen', V.isTopologicallyCharacteristic', ?_⟩
550 intro U hU
551 rcases mem_nhds_iff.mp hU with ⟨W, hWU, hWopen, h1W⟩
552 rcases hV.exists_subset_of_open_one_mem hWopen h1W with ⟨n, hn⟩
553 exact ⟨n + 1, Set.Subset.trans hn hWU⟩
555/-- Topologically finitely generated profinite groups have a countable characteristic open basis
556at the identity. -/
558 [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
560 ∃ V : ℕ → Subgroup G,
561 V 0 = ⊤ ∧
562 Antitone V ∧
563 (∀ n, IsOpen ((V n : Subgroup G) : Set G)) ∧
564 (∀ n, IsTopologicallyCharacteristic G (V n)) ∧
565 ∀ U : Set G, U ∈ 𝓝 (1 : G) → ∃ n, ((V n : Subgroup G) : Set G) ⊆ U := by
566 intro hG
571/-- Finitely generated profinite groups have finite fixed-index open-subgroup sets and a
572countable characteristic open basis at the identity. -/
574 [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
577 ∃ V : ℕ → Subgroup G,
578 V 0 = ⊤ ∧
579 Antitone V ∧
580 (∀ n, IsOpen ((V n : Subgroup G) : Set G)) ∧
581 (∀ n, IsTopologicallyCharacteristic G (V n)) ∧
582 ∀ U : Set G, U ∈ 𝓝 (1 : G) → ∃ n, ((V n : Subgroup G) : Set G) ⊆ U := by
586end IndexFamilies
589section HopfianStep
591variable {G : Type u} [Group G] [TopologicalSpace G]
593namespace Set
595/-- An injective self-map of a finite set is automatically surjective on that set. -/
596theorem Finite.surjOn_of_injOn_mapsTo {α : Type*} {s : Set α}
597 (hs : s.Finite) {f : α → α}
598 (hf : MapsTo f s s) (hinj : InjOn f s) :
599 SurjOn f s s := by
600 classical
601 let g : s → s := fun x => ⟨f x.1, hf x.2⟩
602 have hg_inj : Function.Injective g := by
603 intro x y hxy
604 apply Subtype.ext
605 exact hinj x.2 y.2 (congrArg Subtype.val hxy)
606 haveI := hs.to_subtype
607 have hg_surj : Function.Surjective g := Finite.surjective_of_injective hg_inj
608 intro y hy
609 rcases hg_surj ⟨y, hy⟩ with ⟨x, hx⟩
610 refine ⟨x.1, x.2, ?_⟩
611 exact congrArg Subtype.val hx
613end Set
615/--
616Open normal subgroups separate the identity from every nontrivial element.
617This is the abstract separation input behind the fixed-index Hopfian argument.
618-/
619def OpenNormalSeparatesPoints (G : Type u) [Group G] [TopologicalSpace G]
620 : Prop :=
621 ∀ x : G, x ≠ 1 → ∃ U : Subgroup G, U.Normal ∧ IsOpen (U : Set G) ∧ x ∉ U
623/--
624Kernel-separation criterion for Hopfian arguments. If every kernel element lies in every open
625normal subgroup, and open normal subgroups separate points, then the endomorphism is injective.
626-/
628 {φ : ContinuousMonoidHom G G}
629 (hker : ∀ U : Subgroup G, U.Normal → IsOpen (U : Set G) → φ.ker ≤ U)
631 Function.Injective φ := by
632 intro x y hxy
633 have hmem : x * y⁻¹ ∈ φ.ker := by
634 simp only [ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.mem_ker, MonoidHom.coe_coe, map_mul, hxy, map_inv,
635 mul_inv_cancel]
636 have hone : x * y⁻¹ = 1 := by
637 by_contra hne
638 obtain ⟨U, hU_normal, hU_open, hnotU⟩ := hsep (x * y⁻¹) hne
639 exact hnotU (hker U hU_normal hU_open hmem)
640 have hmul := congrArg (fun z => z * y) hone
641 simpa [mul_assoc] using hmul
643/--
644The preimage operator preserves the fixed-index family of open normal subgroups.
645-/
647 (φ : ContinuousMonoidHom G G) : Prop :=
648 ∀ n,
649 Set.MapsTo (fun U : Subgroup G => Subgroup.comap φ.toMonoidHom U)
653omit [TopologicalSpace G] in
654/-- Comap along a surjective homomorphism is injective on subgroups. -/
656 {H : Type v} [Group H]
657 (f : G →* H) (hf : Function.Surjective f) :
658 Function.Injective (Subgroup.comap f) := by
659 intro U V hUV
660 ext y
661 constructor <;> intro hy
662 · rcases hf y with ⟨x, rfl⟩
663 change x ∈ Subgroup.comap f V
664 have hx : x ∈ Subgroup.comap f U := hy
665 simpa [hUV] using hx
666 · rcases hf y with ⟨x, rfl⟩
667 change x ∈ Subgroup.comap f U
668 have hx : x ∈ Subgroup.comap f V := hy
669 simpa [hUV] using hx
671/-- Preimage under a surjective endomorphism is injective on each fixed-index open-normal family. -/
673 {φ : ContinuousMonoidHom G G}
674 (hφsurj : Function.Surjective φ) (n : ℕ) :
675 Set.InjOn (fun U : Subgroup G => Subgroup.comap φ.toMonoidHom U)
676 (OpenNormalSubgroupsOfIndex (G := G) n) := by
677 intro U hU V hV hEq
678 exact subgroupComap_injective_of_surjective (G := G) φ.toMonoidHom hφsurj hEq
680/--
681Surjectivity of the preimage operator on each index-`n` family of open normal subgroups.
682This is exactly the conclusion obtained from the finiteness
683of the family `Uₙ`.
684-/
686 (φ : ContinuousMonoidHom G G) : Prop :=
687 ∀ n,
688 Set.SurjOn (fun U : Subgroup G => Subgroup.comap φ.toMonoidHom U)
692/-- For finite groups, preimage along a surjective endomorphism is surjective on open normal subgroups of fixed index. -/
694 {φ : ContinuousMonoidHom G G}
696 (hφsurj : Function.Surjective φ)
699 intro n
701 (hs := hfin n)
702 (f := fun U : Subgroup G => Subgroup.comap φ.toMonoidHom U)
703 (hpres n)
706/--
707Abstract version of the main containment `ker φ ≤ U` for every open normal `U`,
708assuming the preimage map is surjective on each fixed-index family.
709-/
711 [IsTopologicalGroup G] [CompactSpace G]
712 {φ : ContinuousMonoidHom G G}
714 ∀ U : Subgroup G, U.Normal → IsOpen (U : Set G) → φ.ker ≤ U := by
715 intro U hU_normal hU_open
716 have hUfinite : Finite (G ⧸ U) :=
717 Subgroup.quotient_finite_of_isOpen U hU_open
718 let n : ℕ := Nat.card (G ⧸ U)
719 have hU : U ∈ OpenNormalSubgroupsOfIndex (G := G) n := by
720 exact ⟨hU_normal, hU_open, hUfinite, rfl⟩
721 rcases hφ n hU with ⟨V, hV, hEq⟩
722 rw [← hEq]
723 intro x hx
724 change φ x ∈ V
725 have hx1 : φ x = 1 := by
726 change φ x = 1 at hx
727 exact hx
728 rw [hx1]
729 exact V.one_mem
731/--
732The injectivity step in the fixed-index Hopfian argument, abstracted away from the finiteness argument.
733-/
735 [IsTopologicalGroup G] [CompactSpace G]
736 {φ : ContinuousMonoidHom G G}
739 Function.Injective φ := by
742 · exact hsep
744/--
745A topological group is continuously Hopfian if every surjective continuous endomorphism is
746injective.
747-/
748def ContinuousHopfian (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
749 ∀ φ : ContinuousMonoidHom G G, Function.Surjective φ → Function.Injective φ
751/-- Every surjective continuous endomorphism is induced by a continuous automorphism. -/
753 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
754 ∀ φ : ContinuousMonoidHom G G, Function.Surjective φ →
755 ∃ e : G ≃ₜ* G, ∀ x : G, e x = φ x
757/--
758Upgrade a continuous bijective endomorphism of a compact Hausdorff topological group
759to a continuous automorphism.
760-/
762 [CompactSpace G] [T2Space G]
763 (φ : ContinuousMonoidHom G G) (hφ : Function.Bijective φ) :
764 G ≃ₜ* G := by
765 let e : G ≃ G := Equiv.ofBijective φ hφ
766 let eh : G ≃ₜ G :=
767 e.toHomeomorphOfContinuousClosed φ.continuous_toFun
768 (Continuous.isClosedMap φ.continuous_toFun)
769 exact ContinuousMulEquiv.mk' eh (by
770 intro x y
771 exact φ.map_mul x y)
773/-- A continuously Hopfian group has all surjective continuous endomorphisms invertible. -/
775 [CompactSpace G] [T2Space G]
776 (hhopf : ContinuousHopfian G) :
778 intro φ hφsurj
780 (G := G) φ ⟨hhopf φ hφsurj, hφsurj⟩
781 refine ⟨e, ?_⟩
782 intro x
783 rfl
785/--
786Once the preimage-surjectivity statement on fixed-index open normal subgroups is available for
787all surjective continuous endomorphisms, the Hopfian conclusion follows formally.
788-/
790 [IsTopologicalGroup G] [CompactSpace G]
792 (hpre : ∀ φ : ContinuousMonoidHom G G, Function.Surjective φ →
795 intro φ hφsurj
796 exact injective_of_preimageSurjectiveOn_openNormalIndex (G := G) (hpre φ hφsurj) hsep
798/-- Finiteness of open normal subgroups of each index implies the continuous Hopfian property. -/
800 [IsTopologicalGroup G] [CompactSpace G]
803 (hpres :
804 ∀ φ : ContinuousMonoidHom G G, Function.Surjective φ →
808 intro φ hφsurj
810 (G := G) hfin hφsurj (hpres φ hφsurj)
812/-- Fixed-index finiteness of open normal subgroups implies the profinite Hopfian conclusion. -/
814 [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
817 (hpres :
818 ∀ φ : ContinuousMonoidHom G G, Function.Surjective φ →
824/-- In a profinite group, open normal subgroups separate
825the identity from every nontrivial element. -/
827 [IsTopologicalGroup G] [CompactSpace G] [T1Space G] [TotallyDisconnectedSpace G] :
829 intro x hx
830 let U : Set G := ({x} : Set G)ᶜ
831 have hUopen : IsOpen U := isClosed_singleton.isOpen_compl
832 have h1U : (1 : G) ∈ U := by
833 simpa [U, eq_comm] using hx
834 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hUopen h1U with ⟨N, hNU⟩
835 refine ⟨N, N.isNormal', openNormalSubgroup_isOpen (G := G) N, ?_⟩
836 intro hxN
837 have hxU : x ∈ U := hNU hxN
838 simp only [mem_compl_iff, mem_singleton_iff, not_true_eq_false, U] at hxU
840/-- Preimage along a surjective continuous endomorphism preserves open normal subgroups of fixed index. -/
842 [IsTopologicalGroup G] [CompactSpace G]
843 {φ : ContinuousMonoidHom G G} (hφsurj : Function.Surjective φ) :
845 intro n U hU
846 refine ⟨?_, ?_, ?_, ?_⟩
847 · exact hU.1.comap φ.toMonoidHom
848 · exact hU.2.1.preimage φ.continuous_toFun
849 · exact Subgroup.quotient_finite_of_isOpen
850 (Subgroup.comap φ.toMonoidHom U) (hU.2.1.preimage φ.continuous_toFun)
851 · simpa [Subgroup.index_eq_card] using
852 (Subgroup.index_comap_of_surjective (H := U) hφsurj).trans hU.2.2.2
854/-- A surjective continuous endomorphism of a topologically finitely generated profinite group is
855automatically a continuous automorphism. -/
857 [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
859 ∀ φ : ContinuousMonoidHom G G, Function.Surjective φ →
860 ∃ e : G ≃ₜ* G, ∀ x : G, e x = φ x := by
861 intro hG
864 · exact HasFiniteOpenSubgroupsOfIndex.toHasFiniteOpenNormalSubgroupsOfIndex
866 · intro φ hφsurj
869end HopfianStep
872end ProCGroups.FiniteGeneration