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

ReidemeisterSchreier/Profinite/OpenSubgroups/DenseFreeModel.lean

1import ProCGroups.WreathProducts
2import ReidemeisterSchreier.Discrete.OpenSubgroups.FreeBasis
3import ReidemeisterSchreier.Profinite.OpenSubgroups.FinitePermutationTargets
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ReidemeisterSchreier/Profinite/OpenSubgroups/DenseFreeModel.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.WreathProducts
27open ReidemeisterSchreier.Discrete.OpenSubgroups
29universe u v w
32section RightQuotientTransport
34open FreeGroup
36variable {F : Type u} [Group F]
37variable {P : Type v} [Group P]
38variable {Y : Type w}
41 (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
42 (K : Subgroup P) (hβ : π.comp βF = β)
43 {a b : FreeGroup Y}
44 (hab : QuotientGroup.rightRel (Subgroup.comap β K) a b) :
45 QuotientGroup.rightRel (Subgroup.comap π K) (βF a) (βF b) := by
46 have ha : π (βF a) = β a := by
47 simpa [MonoidHom.comp_apply] using congrArg (fun f : FreeGroup Y →* P => f a) hβ
48 have hb : π (βF b) = β b := by
49 simpa [MonoidHom.comp_apply] using congrArg (fun f : FreeGroup Y →* P => f b) hβ
50 rw [QuotientGroup.rightRel_apply] at hab ⊢
51 simpa [MonoidHom.map_mul, MonoidHom.map_inv, ha, hb] using hab
53/-- Transport right-coset classes along a homomorphism compatible with two subgroup preimages. -/
54noncomputable def mapRightQuotientOfComap :
55 (π : F →* P) → (βF : FreeGroup Y →* F) → (β : FreeGroup Y →* P) →
56 (K : Subgroup P) → (hβ : π.comp βF = β) →
57 Quotient (QuotientGroup.rightRel (Subgroup.comap β K)) →
58 Quotient (QuotientGroup.rightRel (Subgroup.comap π K))
59 | π, βF, β, K, hβ =>
60 Quotient.map' βF (fun _a _b hab => rightRel_map_of_comap π βF β K hβ hab)
63 (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
64 (K : Subgroup P) (hβ : π.comp βF = β)
65 (hβsurj : Function.Surjective β) :
66 Function.Surjective
67 (mapRightQuotientOfComap π βF β K hβ) := by
68 intro q
69 refine Quotient.inductionOn' q ?_
70 intro p
71 rcases hβsurj (π p) with ⟨w, hw⟩
72 refine ⟨Quotient.mk'' w, ?_⟩
73 change Quotient.mk'' (βF w) = Quotient.mk'' p
74 apply Quotient.sound'
75 have hw' : π (βF w) = π p := by
76 calc
77 π (βF w) = β w := by
78 simpa [MonoidHom.comp_apply] using congrArg (fun f : FreeGroup Y →* P => f w) hβ
79 _ = π p := hw
80 rw [QuotientGroup.rightRel_apply]
81 simp only [Subgroup.comap, Subgroup.mem_mk, Submonoid.mem_mk, Subsemigroup.mem_mk, mem_preimage,
82 MonoidHom.map_mul, MonoidHom.map_inv, hw', mul_inv_cancel, SetLike.mem_coe, one_mem]
85 (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
86 (K : Subgroup P) (hβ : π.comp βF = β) :
87 Function.Injective (mapRightQuotientOfComap π βF β K hβ) := by
88 intro a b hab
89 revert hab
90 refine Quotient.inductionOn₂' a b ?_
91 intro x y hxy
92 apply Quotient.sound'
93 have hrel :
94 QuotientGroup.rightRel (Subgroup.comap π K) (βF x) (βF y) := Quotient.exact' hxy
95 have hx : π (βF x) = β x := by
96 simpa [MonoidHom.comp_apply] using congrArg (fun f : FreeGroup Y →* P => f x) hβ
97 have hy : π (βF y) = β y := by
98 simpa [MonoidHom.comp_apply] using congrArg (fun f : FreeGroup Y →* P => f y) hβ
99 rw [QuotientGroup.rightRel_apply] at hrel ⊢
100 change π (βF y * (βF x)⁻¹) ∈ K at hrel
101 change β (y * x⁻¹) ∈ K
102 simpa [MonoidHom.map_mul, MonoidHom.map_inv, hx, hy] using hrel
104/-- If `β : FreeGroup Y → P` is surjective and `β = π ∘ βF`, then the right cosets of
105`β ⁻¹(K)` are canonically identified with the right cosets of `π ⁻¹(K)`. -/
107 (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
108 (K : Subgroup P) (hβ : π.comp βF = β)
109 (hβsurj : Function.Surjective β) :
110 Quotient (QuotientGroup.rightRel (Subgroup.comap β K)) ≃
111 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)) :=
112 Equiv.ofBijective
115 surjective_mapRightQuotientOfComap π βF β K hβ hβsurj⟩
118 (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
119 (K : Subgroup P) (hβ : π.comp βF = β)
120 (hβsurj : Function.Surjective β) (w : FreeGroup Y) :
121 rightQuotientEquivOfComap π βF β K hβ hβsurj
122 (Quotient.mk'' w) =
123 Quotient.mk'' (βF w) := by
124 simp only [rightQuotientEquivOfComap, mapRightQuotientOfComap, Equiv.ofBijective_apply, Quotient.map'_mk'']
126section SchreierSections
128variable [DecidableEq Y]
129variable {T : Set (FreeGroup Y)}
131/-- Transport a discrete Schreier transversal for `β ⁻¹(K)` to a right-coset section for
132`π ⁻¹(K)` in the ambient group `F`. -/
134 (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
135 (K : Subgroup P) (hβ : π.comp βF = β)
136 (hβsurj : Function.Surjective β)
137 (hT : IsRightSchreierTransversal (X := Y) (Subgroup.comap β K) T) :
138 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)) → F :=
139 fun q =>
140 βF <|
141 rightTransversalSection (H := Subgroup.comap β K) hT.1
142 ((rightQuotientEquivOfComap π βF β K hβ hβsurj).symm q)
145 (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
146 (K : Subgroup P) (hβ : π.comp βF = β)
147 (hβsurj : Function.Surjective β)
148 (hT : IsRightSchreierTransversal (X := Y) (Subgroup.comap β K) T)
149 (q : Quotient (QuotientGroup.rightRel (Subgroup.comap π K))) :
150 Quotient.mk'' (rightSchreierSectionOfComap π βF β K hβ hβsurj hT q) = q := by
151 let e := rightQuotientEquivOfComap π βF β K hβ hβsurj
152 let τT := rightTransversalSection (H := Subgroup.comap β K) hT.1
153 calc
154 Quotient.mk'' (rightSchreierSectionOfComap π βF β K hβ hβsurj hT q)
155 = e (Quotient.mk'' (τT (e.symm q))) := by
156 simpa [rightSchreierSectionOfComap, e, τT] using
157 (rightQuotientEquivOfComap_mk π βF β K hβ hβsurj (τT (e.symm q))).symm
158 _ = e (e.symm q) := by
159 rw [rightTransversalSection_spec (H := Subgroup.comap β K) hT.1]
160 _ = q := e.apply_symm_apply q
162/-- On a coset represented by an element of the chosen Schreier transversal, the transported
163section returns the image of that representative. -/
165 (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
166 (K : Subgroup P) (hβ : π.comp βF = β)
167 (hβsurj : Function.Surjective β)
168 (hT : IsRightSchreierTransversal (X := Y) (Subgroup.comap β K) T)
169 {t : FreeGroup Y} (ht : t ∈ T) :
170 rightSchreierSectionOfComap π βF β K hβ hβsurj hT
171 (Quotient.mk'' (βF t)) =
172 βF t := by
173 let e := rightQuotientEquivOfComap π βF β K hβ hβsurj
174 have heq :
175 e.symm (Quotient.mk'' (βF t)) = Quotient.mk'' t := by
176 apply e.injective
177 simp only [Equiv.apply_symm_apply, rightQuotientEquivOfComap_mk, e]
178 have hsec :
179 rightTransversalSection (H := Subgroup.comap β K) hT.1
180 (Quotient.mk'' t) = t := by
181 have hsub :
182 hT.1.rightQuotientEquiv (Quotient.mk'' t) = ⟨t, ht⟩ := by
183 have hq :
184 Quotient.mk'' t = hT.1.rightQuotientEquiv.symm ⟨t, ht⟩ := by
185 simpa using
186 (hT.1.mk''_rightQuotientEquiv (hT.1.rightQuotientEquiv.symm ⟨t, ht⟩)).symm
187 apply hT.1.rightQuotientEquiv.symm.injective
188 simpa using hq
189 simpa [rightTransversalSection] using congrArg Subtype.val hsub
192/-- The transported Schreier section is normalized at the trivial right coset. -/
194 (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
195 (K : Subgroup P) (hβ : π.comp βF = β)
196 (hβsurj : Function.Surjective β)
197 (hT : IsRightSchreierTransversal (X := Y) (Subgroup.comap β K) T) :
198 rightSchreierSectionOfComap π βF β K hβ hβsurj hT
199 (Quotient.mk'' (1 : F)) =
200 1 := by
201 have hβFone : βF (1 : FreeGroup Y) = 1 := by simp only [map_one]
202 rw [← hβFone]
203 exact rightSchreierSectionOfComap_eq_of_mem π βF β K hβ hβsurj hT hT.2.1
205end SchreierSections
207end RightQuotientTransport
209section DenseAbstractFreeModel
211open FreeGroup
213variable {X : Type u}
214variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
215variable {ι : X → F}
217/-- The abstract free-group lift of a topologically generating family has dense range. -/
219 (hgen : ProCGroups.Generation.TopologicallyGenerates (G := F) (Set.range ι)) :
220 DenseRange (FreeGroup.lift ι : FreeGroup X →* F) := by
221 let φ : FreeGroup X →* F := FreeGroup.lift ι
222 have hsub : Set.range ι ⊆ (φ.range : Set F) := by
223 rintro _ ⟨x, rfl⟩
224 exact ⟨FreeGroup.of x, by simp only [FreeGroup.lift_apply_of, φ]⟩
225 have hφgen :
226 ProCGroups.Generation.TopologicallyGenerates (G := F) (φ.range : Set F) :=
228 have hdense : Dense ((φ.range : Subgroup F) : Set F) := by
229 rw [← Subgroup.closure_eq φ.range]
231 (G := F) (X := (φ.range : Set F))).1 hφgen
232 simpa [DenseRange, MonoidHom.coe_range] using hdense
234/-- A dense abstract free-group lift topologically generates through the images of the free
235generators. -/
237 {Y : Type u}
238 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
239 {φ : FreeGroup Y →* H}
240 (hφ : DenseRange φ) :
242 (G := H) (Set.range fun y : Y => φ (FreeGroup.of y)) := by
243 let j : Y → H := fun y => φ (FreeGroup.of y)
244 have himage :
245 φ '' Set.range (FreeGroup.of : Y → FreeGroup Y) = Set.range j := by
246 simpa [j, Function.comp] using
247 (Set.range_comp φ (FreeGroup.of : Y → FreeGroup Y)).symm
248 have hclosure :
249 Subgroup.closure (Set.range j) = φ.range := by
250 calc
251 Subgroup.closure (Set.range j)
252 = Subgroup.map φ (Subgroup.closure (Set.range (FreeGroup.of : Y → FreeGroup Y))) := by
253 simpa [himage] using
254 (φ.map_closure (Set.range (FreeGroup.of : Y → FreeGroup Y))).symm
255 _ = φ.range := by
256 rw [FreeGroup.closure_range_of Y, MonoidHom.range_eq_map]
258 rw [SetLike.ext'_iff, Subgroup.topologicalClosure_coe, Subgroup.coe_top]
259 simpa [DenseRange, MonoidHom.coe_range, dense_iff_closure_eq] using hφ
261/-- Restricting a dense homomorphism to the preimage of an open subgroup still has dense range in
262that subgroup. -/
264 {G : Type u} [Group G]
265 {H : Type u} [Group H] [TopologicalSpace H]
266 {φ : G →* H} (hφ : DenseRange φ)
267 {U : Subgroup H} (hU : IsOpen (U : Set H)) :
268 DenseRange
269 ({ toFun := fun g : Subgroup.comap φ U => ⟨φ g.1, g.2⟩
270 map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
271 map_mul' := by
272 intro a b
273 ext
274 simp only [Subgroup.coe_mul, map_mul]} : Subgroup.comap φ U →* U) := by
275 let ψ : Subgroup.comap φ U →* U :=
276 { toFun := fun g => ⟨φ g.1, g.2⟩
277 map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
278 map_mul' := by
279 intro a b
280 ext
281 simp only [Subgroup.coe_mul, map_mul]}
282 have hdense : Dense (Set.range φ) := by
283 simpa [DenseRange] using hφ
284 have himage :
285 ((↑) : U → H) '' Set.range ψ = (U : Set H) ∩ Set.range φ := by
286 ext h
287 constructor
288 · rintro ⟨_, hu, rfl⟩
289 rcases hu with ⟨g, rfl⟩
290 exact ⟨g.2, ⟨g.1, rfl⟩⟩
291 · rintro ⟨hu, g, rfl⟩
292 exact ⟨⟨φ g, hu⟩, ⟨⟨g, hu⟩, rfl⟩, rfl⟩
293 have hsubset :
294 (U : Set H) ⊆ closure (((↑) : U → H) '' Set.range ψ) := by
295 rw [himage]
296 simpa [Set.inter_comm] using hdense.open_subset_closure_inter hU
297 have hDenseU : Dense (Set.range ψ : Set U) := by
298 exact (Subtype.dense_iff).2 hsubset
299 simpa [DenseRange] using hDenseU
301section FiniteTargets
303variable {P : Type u} [Group P] [TopologicalSpace P] [DiscreteTopology P] [Finite P]
305omit [TopologicalSpace F] [IsTopologicalGroup F] [Finite P] in
306/-- A homomorphism into a finite discrete group is surjective as soon as it has dense range. -/
308 {φ : F →* P} (hφ : DenseRange φ) :
309 Function.Surjective φ := by
310 have hclosed : IsClosed (Set.range φ) := isClosed_discrete _
311 have hclosure : closure (Set.range φ) = Set.univ := hφ.closure_range
312 have hrange : Set.range φ = Set.univ := by
313 rw [← hclosure]
314 exact (closure_eq_iff_isClosed.mpr hclosed).symm
315 intro p
316 have hp : p ∈ Set.range φ := by
317 simp only [hrange, mem_univ]
318 exact hp
320end FiniteTargets
322/-- The abstract subgroup of `FreeGroup X` lying over an open subgroup of a compact group via the
323dense free-group lift has the exact Schreier-transformed rank. -/
325 {X : Type u} [Finite X]
326 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F]
327 {ι : X → F}
328 (hgen : ProCGroups.Generation.TopologicallyGenerates (G := F) (Set.range ι))
329 (H : OpenSubgroup F) :
330 ∃ Y : Type u,
331 Nonempty (FreeGroupBasis Y (Subgroup.comap (FreeGroup.lift ι) (H : Subgroup F))) ∧
332 Nat.card Y = _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) := by
333 classical
334 let βF : FreeGroup X →* F := FreeGroup.lift ι
335 let L : Subgroup (FreeGroup X) := Subgroup.comap βF (H : Subgroup F)
336 let nQ : ℕ := Nat.card (F ⧸ (H : Subgroup F))
337 let P := openSubgroupIndexActionRange (G := F) H
338 (show Nat.card (F ⧸ (H : Subgroup F)) = nQ by rfl)
339 let ρ : F →ₜ* P :=
341 (show Nat.card (F ⧸ (H : Subgroup F)) = nQ by rfl)
342 let q0 : F ⧸ (H : Subgroup F) := QuotientGroup.mk (s := (H : Subgroup F)) (1 : F)
343 let K : Subgroup P := MulAction.stabilizer P q0
344 let β : FreeGroup X →* P := ρ.toMonoidHom.comp βF
345 letI : TopologicalSpace (FreeGroup X) := ⊥
346 letI : DiscreteTopology (FreeGroup X) := ⟨rfl⟩
347 letI : IsTopologicalGroup (FreeGroup X) := by infer_instance
348 have hcomap : Subgroup.comap ρ.toMonoidHom K = (H : Subgroup F) := by
349 ext g
350 constructor
351 · intro hg
352 change ρ g • q0 = q0 at hg
354 (show Nat.card (F ⧸ (H : Subgroup F)) = nQ by rfl) g] at hg
355 change (QuotientGroup.mk (s := (H : Subgroup F)) g : F ⧸ (H : Subgroup F)) =
356 QuotientGroup.mk (s := (H : Subgroup F)) (1 : F) at hg
357 simpa [QuotientGroup.eq] using hg
358 · intro hg
359 change ρ g • q0 = q0
361 (G := F) H (show Nat.card (F ⧸ (H : Subgroup F)) = nQ by rfl) hg
362 have hβFdense : DenseRange βF :=
364 have hρsurj : Function.Surjective ρ := by
365 intro p
366 rcases p.down.2 with ⟨g, hg⟩
367 refine ⟨g, ?_⟩
368 apply ULift.ext
369 apply Subtype.ext
370 exact hg
371 have hβdense : DenseRange β := by
372 simpa [β, MonoidHom.comp_apply] using
373 (Function.Surjective.denseRange hρsurj).comp hβFdense ρ.continuous_toFun
374 have hβsurj : Function.Surjective β :=
375 surjective_of_denseRange (F := FreeGroup X) (P := P) hβdense
376 let H0 : Subgroup F := Subgroup.comap ρ.toMonoidHom K
377 have hH0 : H0 = (H : Subgroup F) := by
378 simpa [H0] using hcomap
379 let eQ :
380 Quotient (QuotientGroup.rightRel (Subgroup.comap β K)) ≃
381 Quotient (QuotientGroup.rightRel H0) :=
382 rightQuotientEquivOfComap ρ.toMonoidHom βF β K rfl hβsurj
383 have hcomapL : Subgroup.comap β K = L := by
384 ext w
385 change β w ∈ K ↔ βF w ∈ (H : Subgroup F)
386 change βF w ∈ Subgroup.comap ρ.toMonoidHom K ↔ βF w ∈ (H : Subgroup F)
387 rw [hcomap]
388 let eQ0 :
389 Quotient (QuotientGroup.rightRel L) ≃
390 Quotient (QuotientGroup.rightRel H0) := by
391 simpa [hcomapL] using eQ
392 letI : Finite (F ⧸ (H : Subgroup F)) :=
394 letI : Finite (Quotient (QuotientGroup.rightRel (H : Subgroup F))) := by
395 exact
396 Finite.of_equiv (F ⧸ (H : Subgroup F))
397 (QuotientGroup.quotientRightRelEquivQuotientLeftRel (H : Subgroup F)).symm
398 have hRightEq :
399 Quotient (QuotientGroup.rightRel (H : Subgroup F)) =
400 Quotient (QuotientGroup.rightRel H0) := by
401 simpa using
402 congrArg (fun S : Subgroup F => Quotient (QuotientGroup.rightRel S)) hH0.symm
403 letI : Finite (Quotient (QuotientGroup.rightRel H0)) := by
404 exact Eq.ndrec
405 (motive := fun T => Finite T)
406 (inferInstance : Finite (Quotient (QuotientGroup.rightRel (H : Subgroup F))))
407 hRightEq
408 letI : Finite (Quotient (QuotientGroup.rightRel L)) :=
409 Finite.of_equiv
410 (Quotient (QuotientGroup.rightRel H0)) eQ0.symm
411 letI : Finite (FreeGroup X ⧸ L) :=
412 Finite.of_equiv
413 (Quotient (QuotientGroup.rightRel L))
414 (QuotientGroup.quotientRightRelEquivQuotientLeftRel L)
415 have hquotCard :
416 Nat.card (FreeGroup X ⧸ L) = Nat.card (F ⧸ (H : Subgroup F)) := by
417 calc
418 Nat.card (FreeGroup X ⧸ L)
419 = Nat.card (Quotient (QuotientGroup.rightRel L)) :=
420 Nat.card_congr (QuotientGroup.quotientRightRelEquivQuotientLeftRel L).symm
421 _ = Nat.card (Quotient (QuotientGroup.rightRel H0)) :=
422 Nat.card_congr eQ0
423 _ = Nat.card (Quotient (QuotientGroup.rightRel (H : Subgroup F))) := by
424 simpa using congrArg Nat.card hRightEq.symm
425 _ = Nat.card (F ⧸ (H : Subgroup F)) :=
426 Nat.card_congr (QuotientGroup.quotientRightRelEquivQuotientLeftRel (H : Subgroup F))
427 obtain ⟨Y, hYfree, hYcard⟩ :=
429 refine ⟨Y, hYfree, ?_⟩
430 simpa [hquotCard] using hYcard
432end DenseAbstractFreeModel
434end Profinite
435end ReidemeisterSchreier