Yamaguchi Lean 4 Library
ReidemeisterSchreier/Profinite/OpenSubgroups/RankBound.lean
ReidemeisterSchreier/Profinite/OpenSubgroups/RankBound/Source

ReidemeisterSchreier/Profinite/OpenSubgroups/RankBound.lean

1import ReidemeisterSchreier.Discrete.OpenSubgroups.FreeBasis
2import ReidemeisterSchreier.Profinite.OpenSubgroups.Basic
3import ProCGroups.FiniteGeneration.Basic
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ReidemeisterSchreier/Profinite/OpenSubgroups/RankBound.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Profinite open-subgroup Schreier theory
16Profinite open subgroup quotients, finite permutation targets, dense free models, exact right Schreier generation, and topological rank bounds.
17-/
19open Set
20open scoped Topology Pointwise
22namespace ReidemeisterSchreier
23namespace Profinite
25open ProCGroups
26open ProCGroups.FiniteGeneration
27open ReidemeisterSchreier.Discrete.OpenSubgroups
29universe u
31/-- Cardinal form of the Schreier rank transform for an open subgroup of finite index `n`.
33For finite rank this is the usual Schreier transform `1 + n * (d - 1)`. For infinite
34cardinals the finite-index transform stabilizes at the original cardinal. -/
35noncomputable def schreierRankTransformCardinal (κ : Cardinal) (n : ℕ) : Cardinal :=
36 if _ : κ < Cardinal.aleph0 then
37 (_root_.ReidemeisterSchreier.Schreier.rankTransform κ.toNat n : Cardinal)
38 else κ
40@[simp] theorem schreierRankTransformCardinal_natCast (d n : ℕ) :
42 (_root_.ReidemeisterSchreier.Schreier.rankTransform d n : Cardinal) := by
43 simp only [schreierRankTransformCardinal, Cardinal.natCast_lt_aleph0, ↓reduceDIte, Cardinal.toNat_natCast]
46 {κ : Cardinal} (hκ : Cardinal.aleph0 ≤ κ) (n : ℕ) :
48 simp only [schreierRankTransformCardinal, not_lt.mpr hκ, ↓reduceDIte]
50@[simp 900] theorem schreierRankTransformCardinal_mk_finite (X : Type u) [Finite X] (n : ℕ) :
51 schreierRankTransformCardinal (Cardinal.mk X) n =
52 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) n : Cardinal) := by
53 classical
54 letI : Fintype X := Fintype.ofFinite X
55 simp only [Cardinal.mk_fintype, schreierRankTransformCardinal_natCast, Nat.card_eq_fintype_card]
57@[simp 900] theorem schreierRankTransformCardinal_mk_infinite (X : Type u) [Infinite X] (n : ℕ) :
58 schreierRankTransformCardinal (Cardinal.mk X) n = Cardinal.mk X :=
62/-- An open subgroup of a finitely generated profinite group satisfies the usual Schreier
63bound on the minimal number of topological generators. -/
65 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
66 (hG : IsProfiniteGroup G) {d : ℕ} (hd : Generation.topologicalRank G = d)
67 (U : OpenSubgroup G) :
68 Generation.topologicalRank ↥(U : Subgroup G) ≤
69 (_root_.ReidemeisterSchreier.Schreier.rankTransform d (Nat.card (G ⧸ (U : Subgroup G))) : Cardinal) := by
70 classical
71 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
72 letI : T2Space G := IsProfiniteGroup.t2Space hG
73 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
74 cases d with
75 | zero =>
76 rcases
78 (G := G) hG hd with ⟨s, hs, hsgen⟩
79 have hs0 : s.card = 0 := Nat.eq_zero_of_le_zero hs
80 have hsempty : s = ∅ := Finset.card_eq_zero.mp hs0
81 have hgenEmpty : Generation.TopologicallyGenerates (G := G) (∅ : Set G) := by
82 simpa [hsempty] using hsgen
83 have hdenseOne : Dense ({1} : Set G) := by
84 have hdenseBot :
85 Dense (((Subgroup.closure (∅ : Set G)) : Subgroup G) : Set G) :=
86 (Generation.topologicallyGenerates_iff_dense (G := G) (X := (∅ : Set G))).1
87 hgenEmpty
88 simpa using hdenseBot
89 have hsingleton :
90 ({1} : Set G) = (Set.univ : Set G) := by
91 exact (closure_eq_iff_isClosed.mpr isClosed_singleton).symm.trans hdenseOne.closure_eq
92 haveI : Subsingleton G := ⟨fun x y => by
93 have hx : x = 1 := by
94 have hxmem : x ∈ ({1} : Set G) := by
95 simp only [hsingleton, mem_univ]
96 simpa using hxmem
97 have hy : y = 1 := by
98 have hymem : y ∈ ({1} : Set G) := by
99 simp only [hsingleton, mem_univ]
100 simpa using hymem
101 rw [hx, hy]⟩
102 have hbot_top : (⊥ : Subgroup ↥(U : Subgroup G)) = ⊤ := by
103 ext x
104 constructor
105 · intro _
106 trivial
107 · intro _
108 exact Subsingleton.elim _ _
109 have hgenEmptyU :
110 Generation.TopologicallyGenerates (G := ↥(U : Subgroup G))
111 (∅ : Set ↥(U : Subgroup G)) := by
112 rw [Generation.TopologicallyGenerates]
113 have htopClosure : (⊤ : Subgroup ↥(U : Subgroup G)).topologicalClosure = ⊤ :=
114 top_unique (Subgroup.le_topologicalClosure _)
115 simpa [hbot_top] using htopClosure
116 have hconvEmptyU :
117 Generation.ConvergesToOne (G := ↥(U : Subgroup G))
118 (∅ : Set ↥(U : Subgroup G)) := by
119 intro V
120 simp only [empty_diff, finite_empty]
121 have hbound : Generation.topologicalRank ↥(U : Subgroup G) ≤ (0 : Cardinal) := by
122 change sInf {κ : Cardinal |
123 ∃ X : Set ↥(U : Subgroup G),
124 Generation.GeneratesAndConvergesToOne (G := ↥(U : Subgroup G)) X ∧
125 Cardinal.mk X = κ} ≤ 0
126 refine csInf_le' ?_
127 exact ⟨∅, ⟨hgenEmptyU, hconvEmptyU⟩, by simp only [Cardinal.mk_eq_zero]⟩
128 simpa using hbound
129 | succ n =>
130 have hgenAtMost :
133 (G := G) hG hd
134 have hfg_iff :
136 ∃ m, TopologicallyGeneratedByAtMost (G := G) m :=
137 by
138 simpa using
140 (G := G))
142 exact hfg_iff.2 ⟨n + 1, hgenAtMost⟩
143 have hdle : Generation.topologicalRank G ≤ ((n + 1 : ℕ) : Cardinal) := by
144 rw [hd]
145 obtain ⟨g, hg⟩ :=
147 (G := G) (n := n + 1) hfg hdle
148 let φ : FreeGroup (Fin (n + 1)) →* G := FreeGroup.lift g
149 let D : Subgroup G := φ.range
150 have hg_subset : Set.range g ⊆ (D : Set G) := by
151 rintro _ ⟨i, rfl⟩
152 exact ⟨FreeGroup.of i, by simp only [FreeGroup.lift_apply_of, φ]⟩
153 have hDgen : Generation.TopologicallyGenerates (G := G) (D : Set G) :=
155 have hDdenseClosure :
156 Dense (((Subgroup.closure (D : Set G)) : Subgroup G) : Set G) :=
157 (Generation.topologicallyGenerates_iff_dense (G := G) (X := (D : Set G))).1 hDgen
158 have hD_dense : Dense ((D : Set G)) := by
159 simpa [Subgroup.closure_eq D] using hDdenseClosure
160 let I : Subgroup G := (U : Subgroup G) ⊓ D
161 have hIU_dense : Dense ((I.subgroupOf (U : Subgroup G)) : Set ↥(U : Subgroup G)) := by
162 rw [Subtype.dense_iff]
163 have himage :
164 ((↑) : ↥(U : Subgroup G) → G) '' ((I.subgroupOf (U : Subgroup G)) :
165 Set ↥(U : Subgroup G)) =
166 ((U : Set G) ∩ (D : Set G)) := by
167 have hmap :
168 (((I.subgroupOf (U : Subgroup G)).map (U : Subgroup G).subtype : Subgroup G) :
169 Set G) =
170 ((U : Set G) ∩ (D : Set G)) := by
171 rw [Subgroup.map_subgroupOf_eq_of_le]
172 · rfl
173 · exact inf_le_left
174 exact
175 (Subgroup.coe_map (U : Subgroup G).subtype (I.subgroupOf (U : Subgroup G))).symm.trans
176 hmap
177 change (U : Set G) ⊆
178 closure (((↑) : ↥(U : Subgroup G) → G) '' ((I.subgroupOf (U : Subgroup G)) :
179 Set ↥(U : Subgroup G)))
180 rw [himage]
181 simpa [Set.inter_comm, Set.inter_left_comm, Set.inter_assoc] using
182 hD_dense.open_subset_closure_inter U.isOpen'
183 let L : Subgroup (FreeGroup (Fin (n + 1))) := Subgroup.comap φ (U : Subgroup G)
184 letI : Finite (G ⧸ (U : Subgroup G)) := ProCGroups.openSubgroup_finiteQuotient (G := G) U
185 have hDindex :
186 (U : Subgroup G).relIndex D = (U : Subgroup G).index := by
187 change ((U : Subgroup G).subgroupOf D).index = (U : Subgroup G).index
188 have key :
189 ∀ x y : D,
190 QuotientGroup.leftRel ((U : Subgroup G).subgroupOf D) x y ↔
191 QuotientGroup.leftRel (U : Subgroup G) x y := by
192 intro x y
193 simp only [QuotientGroup.leftRel_apply, Subgroup.mem_subgroupOf, Subgroup.coe_mul, InvMemClass.coe_inv,
194 OpenSubgroup.mem_toSubgroup]
195 refine Nat.card_congr <|
196 Equiv.ofBijective
197 (Quotient.map' ((↑) : D → G) fun x y => (key x y).mp) ⟨?_, ?_⟩
198 · intro a b hab
199 revert hab
200 refine Quotient.inductionOn₂' a b ?_
201 intro x y hab
202 have hxy : QuotientGroup.leftRel (U : Subgroup G) x y := by
203 rw [Quotient.map'_mk'', Quotient.map'_mk''] at hab
204 exact Quotient.exact' hab
205 exact Quotient.sound' ((key x y).mpr hxy)
206 · refine Quotient.ind' fun x => ?_
207 let V : Set G := x • ((U : Subgroup G) : Set G)
208 have hVopen : IsOpen V := by
209 simpa [V] using U.isOpen'.smul x
210 have hVnonempty : V.Nonempty := by
211 refine ⟨x, ?_⟩
212 simpa [V] using mem_leftCoset x (show (1 : G) ∈ (U : Subgroup G) from U.one_mem)
213 rcases hD_dense.exists_mem_open hVopen hVnonempty with ⟨y, hyD, hyV⟩
214 refine ⟨(⟨y, hyD⟩ : D), ?_⟩
215 change QuotientGroup.mk y = QuotientGroup.mk x
216 apply QuotientGroup.eq.2
217 simpa [mul_inv_rev, inv_inv] using
218 (U : Subgroup G).inv_mem ((mem_leftCoset_iff x).1 (by simpa [V] using hyV))
219 have hLindex : L.index = (U : Subgroup G).index := by
220 calc
221 L.index = (U : Subgroup G).relIndex D := by
222 simpa [L, D] using (Subgroup.index_comap (H := (U : Subgroup G)) (f := φ))
223 _ = (U : Subgroup G).index := hDindex
224 have hLindex_ne_zero : L.index ≠ 0 := by
225 rw [hLindex]
226 exact Subgroup.index_ne_zero_of_finite (H := (U : Subgroup G))
227 haveI : Finite (FreeGroup (Fin (n + 1)) ⧸ L) :=
228 (Subgroup.index_ne_zero_iff_finite (H := L)).1 hLindex_ne_zero
229 obtain ⟨Y, ⟨eL⟩, hYcard⟩ :=
231 (X := Fin (n + 1)) (L := L)
232 have hquotCard :
233 Nat.card (FreeGroup (Fin (n + 1)) ⧸ L) = Nat.card (G ⧸ (U : Subgroup G)) := by
234 rw [← Subgroup.index_eq_card (H := L), hLindex, Subgroup.index_eq_card]
235 have hYcard' :
236 Nat.card Y = _root_.ReidemeisterSchreier.Schreier.rankTransform (n + 1) (Nat.card (G ⧸ (U : Subgroup G))) := by
237 simpa [hquotCard] using hYcard
238 have hYnonzero : Nat.card Y ≠ 0 := by
239 rw [hYcard', _root_.ReidemeisterSchreier.Schreier.rankTransform_succ]
240 simp only [Nat.add_comm, ne_eq, Nat.add_eq_zero_iff, mul_eq_zero, one_ne_zero, and_false, not_false_eq_true]
241 haveI : Finite Y := Nat.finite_of_card_ne_zero hYnonzero
242 letI : Fintype Y := Fintype.ofFinite Y
243 let φU : L →* ↥(U : Subgroup G) := {
244 toFun := fun x => ⟨φ x.1, x.2⟩
245 map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one, φ]
246 map_mul' := by
247 intro a b
248 ext
249 simp only [Subgroup.coe_mul, map_mul, φ]}
250 let κ : Y → ↥(U : Subgroup G) := fun y => φU (eL y)
251 have hLtop :
252 Subgroup.closure (Set.range fun y : Y => eL y) = ⊤ := by
253 have hset :
254 Set.range (fun y : Y => eL y) =
255 eL.repr.symm.toMonoidHom '' Set.range (FreeGroup.of : Y → FreeGroup Y) := by
256 ext z
257 constructor
258 · rintro ⟨y, rfl⟩
259 exact ⟨FreeGroup.of y, ⟨y, rfl⟩, by rfl⟩
260 · rintro ⟨x, hx, rfl⟩
261 rcases hx with ⟨y, rfl⟩
262 exact ⟨y, rfl⟩
263 calc
264 Subgroup.closure (Set.range fun y : Y => eL y)
265 =
266 Subgroup.closure
267 (eL.repr.symm.toMonoidHom '' Set.range (FreeGroup.of : Y → FreeGroup Y)) := by
268 rw [hset]
269 _ = ⊤ := by
270 rw [← MonoidHom.map_closure, FreeGroup.closure_range_of]
271 exact Subgroup.map_top_of_surjective
272 eL.repr.symm.toMonoidHom eL.repr.symm.surjective
273 have hφU_range : φU.range = I.subgroupOf (U : Subgroup G) := by
274 ext u
275 constructor
276 · rintro ⟨x, rfl⟩
277 change φ x.1 ∈ I
278 exact ⟨x.2, ⟨x.1, rfl⟩⟩
279 · intro hu
280 change (u : G) ∈ I at hu
281 rcases hu with ⟨huU, huD⟩
282 rcases huD with ⟨x, hx⟩
283 refine ⟨⟨x, ?_⟩, ?_⟩
284 · change φ x ∈ (U : Subgroup G)
285 exact hx.symm ▸ huU
286 · apply Subtype.ext
287 simp only [MonoidHom.coe_mk, OneHom.coe_mk, hx, Subtype.coe_eta, φU]
288 have hφU_dense :
289 Dense ((φU.range : Subgroup ↥(U : Subgroup G)) : Set ↥(U : Subgroup G)) := by
290 rw [hφU_range]
291 exact hIU_dense
292 have hκclosure :
293 Subgroup.closure (Set.range κ) = φU.range := by
294 have hmap :
295 (Subgroup.closure (Set.range fun y : Y => eL y)).map φU =
296 Subgroup.closure (φU '' Set.range (fun y : Y => eL y)) := by
297 simpa using
298 (MonoidHom.map_closure φU (Set.range fun y : Y => eL y))
299 have himage :
300 φU '' Set.range (fun y : Y => eL y) = Set.range κ := by
301 ext u
302 constructor
303 · rintro ⟨x, ⟨y, rfl⟩, rfl⟩
304 exact ⟨y, rfl⟩
305 · rintro ⟨y, rfl⟩
306 exact ⟨eL y, ⟨y, rfl⟩, rfl⟩
307 calc
308 Subgroup.closure (Set.range κ)
309 = Subgroup.closure (φU '' Set.range (fun y : Y => eL y)) := by
310 rw [← himage]
311 _ = (Subgroup.closure (Set.range fun y : Y => eL y)).map φU := by
312 symm
313 exact hmap
314 _ = (⊤ : Subgroup L).map φU := by rw [hLtop]
315 _ = φU.range := by rw [← MonoidHom.range_eq_map]
316 have hκgen :
317 Generation.TopologicallyGenerates (G := ↥(U : Subgroup G)) (Set.range κ) := by
318 exact (Generation.topologicallyGenerates_iff_dense
319 (G := ↥(U : Subgroup G)) (X := Set.range κ)).2 <|
320 by simpa [hκclosure] using hφU_dense
321 let s : Finset ↥(U : Subgroup G) := Finset.univ.image κ
322 have hs_card : s.card ≤ Nat.card Y := by
323 simpa [s, Nat.card_eq_fintype_card] using
324 (Finset.card_image_le (s := (Finset.univ : Finset Y)) (f := κ))
325 have hs_gen :
326 Generation.TopologicallyGenerates (G := ↥(U : Subgroup G))
327 (↑s : Set ↥(U : Subgroup G)) := by
328 simpa [s, Finset.coe_image] using hκgen
329 have hdU_nat : Generation.topologicalRank ↥(U : Subgroup G) ≤ Nat.card Y := by
331 (G := ↥(U : Subgroup G)) ⟨s, hs_card, hs_gen⟩
332 calc
333 Generation.topologicalRank ↥(U : Subgroup G) ≤ (Nat.card Y : Cardinal) := by
334 exact hdU_nat
335 _ = (_root_.ReidemeisterSchreier.Schreier.rankTransform (n + 1) (Nat.card (G ⧸ (U : Subgroup G))) : Cardinal) := by
336 exact_mod_cast hYcard'
338end Profinite
339end ReidemeisterSchreier