ProCGroups/FiniteGeneration/Basic.lean
1import Mathlib.GroupTheory.FreeGroup.Basic
2import ProCGroups.Generation.QuotientGeneratorConvergingPairs
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/FiniteGeneration/Basic.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Finite generation and characteristic chains
15Records finite generation criteria for profinite groups, finite-index/open-subgroup counting, characteristic cores, and index bounds.
16-/
18open Set
19open scoped Topology Pointwise
21namespace ProCGroups.FiniteGeneration
23universe u v w
25open ProCGroups.Generation
27section Basic
29variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31/-- Finitely generated as a topological group. -/
33 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop :=
34 ∃ s : Finset G, TopologicallyGenerates (G := G) (↑s : Set G)
36/-- A subgroup is characteristic if every continuous automorphism preserves it. -/
38 (G : Type u) [Group G] [TopologicalSpace G] (H : Subgroup G) : Prop :=
39 ∀ φ : G ≃ₜ* G, ∀ g : G, φ g ∈ H ↔ g ∈ H
41section Characteristic
43omit [IsTopologicalGroup G]
45/-- Membership in a characteristic subgroup is invariant under a continuous automorphism. -/
46theorem IsTopologicallyCharacteristic.apply_mem_iff {H : Subgroup G}
47 (hH : IsTopologicallyCharacteristic (G := G) H) (φ : G ≃ₜ* G) {g : G} :
48 φ g ∈ H ↔ g ∈ H :=
49 hH φ g
51/-- Intersections of characteristic subgroups are characteristic. -/
52theorem IsTopologicallyCharacteristic.inf {H K : Subgroup G}
53 (hH : IsTopologicallyCharacteristic (G := G) H) (hK : IsTopologicallyCharacteristic (G := G) K) :
54 IsTopologicallyCharacteristic (G := G) (H ⊓ K) := by
55 intro φ g
56 simp only [Subgroup.mem_inf, hH φ g, hK φ g]
58/-- Arbitrary infima of characteristic subgroups are characteristic. -/
59theorem IsTopologicallyCharacteristic.sInf {S : Set (Subgroup G)}
60 (hS : ∀ H ∈ S, IsTopologicallyCharacteristic (G := G) H) :
61 IsTopologicallyCharacteristic (G := G) (sInf S) := by
62 intro φ g
63 simp only [Subgroup.mem_sInf]
64 constructor
65 · intro hg H hH
66 exact (hS H hH φ g).1 (hg H hH)
67 · intro hg H hH
68 exact (hS H hH φ g).2 (hg H hH)
70/-- Indexed infima of characteristic subgroups are characteristic. -/
71theorem IsTopologicallyCharacteristic.iInf {ι : Sort*} {S : ι → Subgroup G}
72 (hS : ∀ i, IsTopologicallyCharacteristic (G := G) (S i)) :
73 IsTopologicallyCharacteristic (G := G) (iInf S) := by
74 intro φ g
75 simp only [Subgroup.mem_iInf]
76 constructor
77 · intro hg i
78 exact (hS i φ g).1 (hg i)
79 · intro hg i
80 exact (hS i φ g).2 (hg i)
82/-- The whole group is characteristic. -/
83@[simp] theorem IsTopologicallyCharacteristic.top :
84 IsTopologicallyCharacteristic (G := G) (⊤ : Subgroup G) := by
85 intro φ g
86 simp only [Subgroup.mem_top]
88end Characteristic
90/-- `G` can be topologically generated by at most `n` elements. -/
92 (n : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
93 Prop :=
94 ∃ s : Finset G, s.card ≤ n ∧ TopologicallyGenerates (G := G) (↑s : Set G)
96/-- Increasing the allowed number of generators preserves bounded topological generation. -/
97theorem TopologicallyGeneratedByAtMost.mono {m n : ℕ}
98 (hmn : m ≤ n)
99 (hG : TopologicallyGeneratedByAtMost (G := G) m) :
100 TopologicallyGeneratedByAtMost (G := G) n := by
101 rcases hG with ⟨s, hs, hgen⟩
102 exact ⟨s, hs.trans hmn, hgen⟩
104/-- A group is topologically finitely generated iff it is generated by at most `n` elements for
105some natural number `n`. -/
108 ∃ n, TopologicallyGeneratedByAtMost (G := G) n := by
109 constructor
110 · rintro ⟨s, hs⟩
111 exact ⟨s.card, s, le_rfl, hs⟩
112 · rintro ⟨_n, s, _hs, hgen⟩
113 exact ⟨s, hgen⟩
115omit [IsTopologicalGroup G] in
116/-- A finite set of elements converges to `1` in the profinite generating-family sense. -/
117theorem finiteSet_convergesToOne (s : Finset G) :
118 ConvergesToOne (G := G) (↑s : Set G) :=
119 ConvergesToOne.of_finite s.finite_toSet
121/-- If `G` is topologically generated by at most `n` elements, its topological rank is at most
122`n`. -/
123theorem topologicalRank_le_of_topologicallyGeneratedByAtMost {n : ℕ}
124 (h : TopologicallyGeneratedByAtMost (G := G) n) :
125 topologicalRank G ≤ n := by
126 rcases h with ⟨s, hs, hgen⟩
127 have hconv : ConvergesToOne (G := G) (↑s : Set G) :=
128 finiteSet_convergesToOne (G := G) s
129 calc
130 topologicalRank G ≤ Cardinal.mk (↑s : Set G) :=
131 topologicalRank_le_mk_of_generatesAndConvergesToOne (G := G) ⟨hgen, hconv⟩
132 _ = (s.card : Cardinal) := by
133 exact Cardinal.mk_coe_finset (s := s)
134 _ ≤ n := by
135 exact_mod_cast hs
137/-- The image of a topological generating family under a continuous surjective homomorphism
138topologically generates the codomain. -/
140 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
141 (φ : G →ₜ* H) (hφ : Function.Surjective φ)
142 {ι : Sort w} (g : ι → G)
143 (hg : TopologicallyGenerates (G := G) (Set.range g)) :
144 TopologicallyGenerates (G := H) (Set.range (φ ∘ g)) := by
145 simpa [Set.range_comp, Function.comp] using
147 (G := G) (H := H) φ hφ hg
149/-- Bounded topological generation descends along continuous surjective homomorphisms. -/
150theorem TopologicallyGeneratedByAtMost.of_surjective
151 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
152 (φ : G →ₜ* H) (hφ : Function.Surjective φ) {n : ℕ}
153 (hG : TopologicallyGeneratedByAtMost (G := G) n) :
154 TopologicallyGeneratedByAtMost (G := H) n := by
155 classical
156 rcases hG with ⟨s, hs, hgen⟩
157 refine ⟨s.image φ, (Finset.card_image_le).trans hs, ?_⟩
158 simpa [Finset.coe_image] using
160 (G := G) (H := H) φ hφ hgen
162/-- Topological finite generation descends along continuous surjective homomorphisms. -/
164 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
165 (φ : G →ₜ* H) (hφ : Function.Surjective φ)
166 (hG : TopologicallyFinitelyGenerated G) :
167 TopologicallyFinitelyGenerated H := by
169 rcases hG with ⟨n, hn⟩
170 exact ⟨n, TopologicallyGeneratedByAtMost.of_surjective (G := G) (H := H) φ hφ hn⟩
172/-- In the discrete case, topological generation is abstract subgroup generation. -/
174 [DiscreteTopology G] {X : Set G} :
175 TopologicallyGenerates (G := G) X ↔ Subgroup.closure X = ⊤ := by
176 have htc : (Subgroup.closure X).topologicalClosure = Subgroup.closure X := by
177 apply SetLike.ext'
178 rw [Subgroup.topologicalClosure_coe]
179 exact closure_discrete ((Subgroup.closure X : Subgroup G) : Set G)
180 rw [TopologicallyGenerates, htc]
182/-- A map from a free group onto a discrete topologically generated group is surjective.
185topological generation of the images of the chosen generators is exactly abstract generation. -/
187 {X : Type v} [DiscreteTopology G] (g : X → G)
188 (hg : TopologicallyGenerates (G := G) (Set.range g)) :
189 Function.Surjective (FreeGroup.lift g) := by
191 have hclosure_le_range :
192 Subgroup.closure (Set.range g) ≤ (FreeGroup.lift g).range := by
193 refine (Subgroup.closure_le (K := (FreeGroup.lift g).range)).2 ?_
194 rintro y ⟨x, rfl⟩
195 exact ⟨FreeGroup.of x, by simp only [FreeGroup.lift_apply_of]⟩
196 intro y
197 have hy : y ∈ Subgroup.closure (Set.range g) := by
198 rw [hg]
199 trivial
200 exact hclosure_le_range hy
202/-- A finite discrete group is topologically finitely generated. -/
203theorem topologicallyFinitelyGenerated_of_finite [Finite G] [DiscreteTopology G] :
204 TopologicallyFinitelyGenerated G := by
205 classical
206 letI : Fintype G := Fintype.ofFinite G
207 refine ⟨Finset.univ, ?_⟩
209 simp only [Finset.coe_univ, Subgroup.closure_univ]
211/-- If the topological rank of a profinite group is the natural number `n`, then the group is
212topologically generated by at most `n` elements. -/
214 (hG : ProCGroups.IsProfiniteGroup G) {n : ℕ}
215 (hd : topologicalRank G = n) :
216 TopologicallyGeneratedByAtMost (G := G) n := by
217 classical
218 let C : Set Cardinal := {κ : Cardinal |
219 ∃ X : Set G,
220 GeneratesAndConvergesToOne (G := G) X ∧ Cardinal.mk X = κ}
221 have hCne : C.Nonempty := by
222 rcases exists_generatorsConvergingToOne (G := G) hG with ⟨X, hX⟩
223 exact ⟨Cardinal.mk X, X, hX, rfl⟩
224 have hdmem : topologicalRank G ∈ C := by
225 simpa [topologicalRank, C] using (csInf_mem hCne)
226 rcases hdmem with ⟨X, hX, hXcard⟩
227 have hXlt : Cardinal.mk X < Cardinal.aleph0 := by
228 calc
229 Cardinal.mk X = topologicalRank G := hXcard
230 _ = n := hd
231 _ < Cardinal.aleph0 := Cardinal.natCast_lt_aleph0 (n := n)
232 letI : Finite X := (Cardinal.lt_aleph0_iff_finite (α := X)).mp hXlt
233 have hXfin : X.Finite := Set.toFinite X
234 let s : Finset G := hXfin.toFinset
235 have hs_card : s.card = n := by
236 have hs_mk : (s.card : Cardinal) = Cardinal.mk X := by
237 simpa [s] using (Cardinal.mk_coe_finset (s := hXfin.toFinset)).symm
238 exact_mod_cast (hs_mk.trans (hXcard.trans hd))
239 refine ⟨s, hs_card.le, ?_⟩
240 simpa [s] using hX.1
242/-- A finite upper bound on the topological rank gives an explicit generating tuple of that
243length. -/
245 (hG : TopologicallyFinitelyGenerated G) {n : ℕ} (hd : topologicalRank G ≤ n) :
246 ∃ g : Fin n → G, TopologicallyGenerates (G := G) (Set.range g) := by
247 classical
248 have hdfin : topologicalRank G < Cardinal.aleph0 := by
249 rcases hG with ⟨s, hs⟩
250 have hconv : ConvergesToOne (G := G) (↑s : Set G) :=
251 finiteSet_convergesToOne (G := G) s
252 have hdle : topologicalRank G ≤ Cardinal.mk (↑s : Set G) :=
253 topologicalRank_le_mk_of_generatesAndConvergesToOne (G := G) ⟨hs, hconv⟩
254 exact hdle.trans_lt <| by
255 have hsMk : Cardinal.mk (↑s : Set G) = (s.card : Cardinal) :=
256 Cardinal.mk_coe_finset (s := s)
257 rw [hsMk]
258 exact Cardinal.natCast_lt_aleph0 (n := s.card)
259 let m := Cardinal.toNat (topologicalRank G)
260 have hm : topologicalRank G = m := by
261 symm
262 exact Cardinal.cast_toNat_of_lt_aleph0 hdfin
263 have hExists : ∃ X : Set G, GeneratesAndConvergesToOne (G := G) X := by
264 rcases hG with ⟨s, hs⟩
265 exact ⟨(↑s : Set G), ⟨hs, finiteSet_convergesToOne (G := G) s⟩⟩
266 rcases exists_generatesAndConvergesToOne_card_eq_topologicalRank (G := G) hExists with
267 ⟨X, hX, hXcard⟩
268 have hXfin : X.Finite := by
269 have hXlt : Cardinal.mk X < Cardinal.aleph0 := by
270 calc
271 Cardinal.mk X = topologicalRank G := hXcard
272 _ = m := hm
273 _ < Cardinal.aleph0 := Cardinal.natCast_lt_aleph0 (n := m)
274 letI : Finite X := (Cardinal.lt_aleph0_iff_finite (α := X)).mp <| by
275 simpa using hXlt
276 exact Set.toFinite X
277 let s : Finset G := hXfin.toFinset
278 have hs_gen : TopologicallyGenerates (G := G) (↑s : Set G) := by
279 simpa [s] using hX.1
280 have hs_card : s.card = m := by
281 have hs_mk : (s.card : Cardinal) = Cardinal.mk X := by
282 simpa [s] using (Cardinal.mk_coe_finset (s := hXfin.toFinset)).symm
283 exact_mod_cast (hs_mk.trans (hXcard.trans hm))
284 have hmle : m ≤ n := by
285 simpa [m] using
286 (Cardinal.toNat_le_toNat hd (Cardinal.natCast_lt_aleph0 (n := n)))
287 have hs_le : s.card ≤ n := by
288 simpa [hs_card] using hmle
289 let e : Fin s.card ≃ s := by
290 simpa using (Fintype.equivFin s).symm
291 let g0 : Fin s.card → G := fun i => (e i : G)
292 have hs_subset_range : (↑s : Set G) ⊆ Set.range g0 := by
293 intro x hx
294 refine ⟨e.symm ⟨x, hx⟩, ?_⟩
295 simp only [Equiv.apply_symm_apply, g0]
296 have hg0 : TopologicallyGenerates (G := G) (Set.range g0) :=
297 topologicallyGenerates_mono hs_gen hs_subset_range
298 let g : Fin n → G := fun i =>
299 if hi : i.1 < s.card then g0 ⟨i.1, hi⟩ else 1
300 have hg0_subset : Set.range g0 ⊆ Set.range g := by
301 intro x hx
302 rcases hx with ⟨i, rfl⟩
303 refine ⟨Fin.castLE hs_le i, ?_⟩
304 have hi : (Fin.castLE hs_le i).1 < s.card := i.2
305 simp only [Fin.val_castLE, Fin.is_lt, ↓reduceDIte, Fin.eta, g]
306 exact ⟨g, topologicallyGenerates_mono hg0 hg0_subset⟩
308end Basic
311/-- If every finite stage of a surjective inverse system has topological rank at most `n`, then so
312does the inverse limit. -/
314 {I : Type v} [Preorder I]
315 (S : ProCGroups.InverseSystems.InverseSystem (I := I))
316 [Nonempty I] [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
317 [∀ i, IsTopologicalGroup (S.X i)] [∀ i, Finite (S.X i)]
318 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
319 (hdir : Directed (· ≤ ·) (id : I → I))
320 (hsurj : ∀ {i j : I} (hij : i ≤ j), Function.Surjective (S.map hij))
321 {n : ℕ} (hbound : ∀ i, topologicalRank (S.X i) ≤ n) :
322 topologicalRank S.inverseLimit ≤ n := by
323 classical
324 letI : ∀ i, DiscreteTopology (S.X i) := fun _ => by infer_instance
325 let T : ProCGroups.InverseSystems.InverseSystem (I := I) := {
326 X := fun i => { g : Fin n → S.X i // TopologicallyGenerates (G := S.X i) (Set.range g) }
327 topologicalSpace := fun _ => inferInstance
328 map := fun {i j} hij g =>
329 ⟨fun a => S.map hij (g.1 a), by
330 let φij : ContinuousMonoidHom (S.X j) (S.X i) :=
331 { toMonoidHom :=
332 { toFun := S.map hij
333 map_one' := ProCGroups.InverseSystems.IsGroupSystem.map_one (S := S) hij
334 map_mul' := ProCGroups.InverseSystems.IsGroupSystem.map_mul (S := S) hij }
335 continuous_toFun := S.continuous_map hij }
336 simpa [Function.comp] using
338 (G := S.X j) (H := S.X i) φij (hsurj hij) g.1 g.2⟩
339 continuous_map := fun {_i _j} _hij => by
340 exact continuous_of_discreteTopology
341 map_id := fun i => by
342 ext g a
343 simp only [InverseSystems.InverseSystem.map_id_apply, id_eq]
344 map_comp := fun hij hjk => by
345 ext g a
346 simp only [Function.comp_apply, InverseSystems.InverseSystem.map_comp_apply]}
347 have hTnonempty : ∀ i, Nonempty (T.X i) := by
348 intro i
349 have hfg : TopologicallyFinitelyGenerated (S.X i) :=
350 topologicallyFinitelyGenerated_of_finite (G := S.X i)
352 (G := S.X i) hfg (hbound i) with ⟨g, hg⟩
353 exact ⟨⟨g, hg⟩⟩
354 letI : ∀ i, Nonempty (T.X i) := hTnonempty
355 letI : ∀ i, Finite (T.X i) := fun _ => inferInstance
357 (S := T) hdir with ⟨x⟩
358 let g : Fin n → S.inverseLimit := fun a =>
359 ⟨fun i => (x.1 i).1 a, by
360 intro i j hij
361 have hcompat := congrArg Subtype.val (x.2 i j hij)
362 exact congrArg (fun f => f a) hcompat⟩
363 have hgproj : ∀ i, TopologicallyGenerates (G := S.X i) (S.projection i '' Set.range g) := by
364 intro i
365 rw [← Set.range_comp (S.projection i) g]
366 simpa [g, Function.comp] using (x.1 i).2
367 have hggen : TopologicallyGenerates (G := S.inverseLimit) (Set.range g) := by
368 exact
370 (S := S) hdir hsurj (X := Set.range g)).2 hgproj
371 let s : Finset S.inverseLimit := Finset.univ.image g
372 have hs_card : s.card ≤ n := by
373 simpa [s] using (Finset.card_image_le (f := g) (s := (Finset.univ : Finset (Fin n))))
374 have hsgen : TopologicallyGenerates (G := S.inverseLimit) (↑s : Set S.inverseLimit) := by
375 simpa [s, Finset.coe_image] using hggen
376 exact topologicalRank_le_of_topologicallyGeneratedByAtMost (G := S.inverseLimit)
377 ⟨s, hs_card, hsgen⟩
380end ProCGroups.FiniteGeneration