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

ReidemeisterSchreier/Profinite/OpenSubgroups/SchreierTransversals.lean

1import ProCGroups.FreeProC.Basic
2import ProCGroups.WreathProducts
3import ReidemeisterSchreier.Profinite.OpenSubgroups.RightQuotient
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ReidemeisterSchreier/Profinite/OpenSubgroups/SchreierTransversals.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.ProC
27open ProCGroups.FreeProC
28open ProCGroups.WreathProducts
30universe u v
32section LeftQuotientSections
34variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
36/-- The normalized continuous section of the left quotient by an open subgroup. -/
37noncomputable abbrev openSubgroupLeftSchreierSection (H : OpenSubgroup F) :
38 F ⧸ (H : Subgroup F) → F :=
41omit [IsTopologicalGroup F] in
42theorem openSubgroupLeftSchreierSection_rightInverse (H : OpenSubgroup F) :
43 Function.RightInverse (openSubgroupLeftSchreierSection (F := F) H)
44 (QuotientGroup.mk (s := (H : Subgroup F))) := by
47 (G := F) (U := (H : Subgroup F)))
49theorem continuous_openSubgroupLeftSchreierSection (H : OpenSubgroup F) :
50 Continuous (openSubgroupLeftSchreierSection (F := F) H) := by
53 (G := F) (U := (H : Subgroup F)) H.isOpen')
55omit [IsTopologicalGroup F] in
57 (H : OpenSubgroup F) (q : F ⧸ (H : Subgroup F)) :
58 QuotientGroup.mk (s := (H : Subgroup F))
59 (openSubgroupLeftSchreierSection (F := F) H q) = q :=
62omit [IsTopologicalGroup F] in
64 (H : OpenSubgroup F) :
66 (QuotientGroup.mk (s := (H : Subgroup F)) (1 : F)) = 1 := by
69/-- For a normal open subgroup, right and left cosets can be identified by the same
70representative. -/
72 (H : OpenSubgroup F) [Subgroup.Normal (H : Subgroup F)] :
73 OpenSubgroupRightQuotient H ≃ F ⧸ (H : Subgroup F) where
74 toFun :=
75 Quotient.map' id fun a b hab => by
76 rw [QuotientGroup.leftRel_apply]
77 exact Subgroup.Normal.mem_comm (show Subgroup.Normal (H : Subgroup F) by infer_instance)
78 (QuotientGroup.rightRel_apply.mp hab)
79 invFun :=
80 Quotient.map' id fun a b hab => by
81 rw [QuotientGroup.rightRel_apply]
82 exact Subgroup.Normal.mem_comm (show Subgroup.Normal (H : Subgroup F) by infer_instance)
83 (QuotientGroup.leftRel_apply.mp hab)
84 left_inv := by
85 intro q
86 refine Quotient.inductionOn' q ?_
87 intro g
88 rfl
89 right_inv := by
90 intro q
91 refine Quotient.inductionOn' q ?_
92 intro g
93 rfl
95omit [IsTopologicalGroup F] in
96/-- Under normality, the left Schreier section also represents the corresponding right coset. -/
98 (H : OpenSubgroup F) [Subgroup.Normal (H : Subgroup F)]
100 Quotient.mk'' (openSubgroupLeftSchreierSection (F := F) H
103 change e.symm (QuotientGroup.mk (s := (H : Subgroup F))
104 (openSubgroupLeftSchreierSection (F := F) H (e q))) = q
105 exact (Equiv.symm_apply_eq e).2 (openSubgroupLeftSchreierSection_mk (F := F) H (e q))
107end LeftQuotientSections
109section AbstractSchreierSections
111variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
112variable {X : Type v}
113variable (H : OpenSubgroup F)
115/-- The two cocycle orientations used by left- and right-coset Schreier generators. -/
116inductive SchreierOrientation where
117 | left
118 | right
119deriving DecidableEq
123/-- The oriented Schreier cocycle associated to a section and a next-coset operation. -/
124def cocycle {Q : Type u} (o : SchreierOrientation)
125 (sec : Q → F) (next : Q → X → Q) (ι : X → F) (q : Q) (x : X) : F :=
126 match o with
127 | left => (sec (next q x))⁻¹ * sec q * ι x
128 | right => sec q * ι x * (sec (next q x))⁻¹
132/-- A section-level Schreier generator package. It abstracts over the quotient type, the
133left/right cocycle orientation, and the next-coset operation, so the common generator-set,
134continuity, closure, and cardinality API can be stated once. -/
135structure SchreierSection where
136 Q : Type u
137 orientation : SchreierOrientation
138 sectionMap : Q → F
139 next : (X → F) → Q → X → Q
140 cocycle_mem :
141 ∀ (ι : X → F) (q : Q) (x : X),
142 orientation.cocycle sectionMap (next ι) ι q x ∈ (H : Subgroup F)
146variable {H}
148/-- The subgroup-valued generator attached to an abstract Schreier section. -/
149noncomputable def generator (S : SchreierSection (F := F) (X := X) H)
150 (ι : X → F) (q : S.Q) (x : X) : ↥(H : Subgroup F) :=
151 ⟨S.orientation.cocycle S.sectionMap (S.next ι) ι q x, S.cocycle_mem ι q x⟩
153omit [IsTopologicalGroup F] in
154@[simp] theorem generator_coe (S : SchreierSection (F := F) (X := X) H)
155 (ι : X → F) (q : S.Q) (x : X) :
156 ((S.generator ι q x : ↥(H : Subgroup F)) : F) =
157 S.orientation.cocycle S.sectionMap (S.next ι) ι q x :=
158 rfl
160/-- Nontrivial generator values of an abstract Schreier section. -/
161def generatorSet (S : SchreierSection (F := F) (X := X) H)
162 (ι : X → F) : Set ↥(H : Subgroup F) :=
163 {z | ∃ q : S.Q, ∃ x : X, z = S.generator ι q x ∧ z ≠ 1}
165/-- Nontrivial section Schreier pairs. -/
166def NontrivialPairs (S : SchreierSection (F := F) (X := X) H)
167 (ι : X → F) : Type (max u v) :=
168 {p : S.Q × X // S.generator ι p.1 p.2 ≠ 1}
170omit [IsTopologicalGroup F] in
172 (S : SchreierSection (F := F) (X := X) H) (ι : X → F)
173 [Finite X] [Finite S.Q] :
174 Finite (S.NontrivialPairs ι) :=
175 Finite.of_injective (fun p : S.NontrivialPairs ι => p.1) (by
176 intro a b h
177 exact Subtype.ext h)
179omit [IsTopologicalGroup F] in
180/-- The tautological map from nontrivial abstract Schreier pairs to the generator value set. -/
182 (S : SchreierSection (F := F) (X := X) H) (ι : X → F) :
183 S.NontrivialPairs ι → ↥(S.generatorSet ι) := fun p =>
184 ⟨S.generator ι p.1.1 p.1.2, ⟨p.1.1, p.1.2, rfl, p.2⟩⟩
186omit [IsTopologicalGroup F] in
188 (S : SchreierSection (F := F) (X := X) H) (ι : X → F) :
189 Function.Surjective (S.nontrivialPairsToGeneratorSet ι) := by
190 intro z
191 rcases z.2 with ⟨q, x, hz, hz_ne⟩
192 refine ⟨⟨(q, x), ?_⟩, ?_⟩
193 · simpa [hz] using hz_ne
194 · apply Subtype.ext
195 exact hz.symm
197omit [IsTopologicalGroup F] in
199 (S : SchreierSection (F := F) (X := X) H) (ι : X → F)
200 [Finite X] [Finite S.Q] :
201 Nat.card (S.generatorSet ι) ≤ Nat.card (S.NontrivialPairs ι) :=
202 Nat.card_le_card_of_surjective (S.nontrivialPairsToGeneratorSet ι)
203 (S.surjective_nontrivialPairsToGeneratorSet ι)
205omit [IsTopologicalGroup F] in
207 (S : SchreierSection (F := F) (X := X) H) (ι : X → F)
208 [Finite X] [Finite S.Q] :
209 Nat.card (S.NontrivialPairs ι) ≤ Nat.card S.Q * Nat.card X := by
210 have hle : Nat.card (S.NontrivialPairs ι) ≤ Nat.card (S.Q × X) :=
211 Nat.card_le_card_of_injective (fun p : S.NontrivialPairs ι => p.1) (by
212 intro a b h
213 exact Subtype.ext h)
214 simpa [Nat.card_prod] using hle
216omit [IsTopologicalGroup F] in
218 (S : SchreierSection (F := F) (X := X) H) (ι : X → F)
219 [Finite X] [Finite S.Q] :
220 Nat.card (S.generatorSet ι) ≤ Nat.card S.Q * Nat.card X :=
221 (S.natCard_generatorSet_le_nontrivialPairs ι).trans (S.natCard_nontrivialPairs_le ι)
223omit [IsTopologicalGroup F] in
225 (S : SchreierSection (F := F) (X := X) H) (ι : X → F) :
226 Subgroup.closure (S.generatorSet ι) =
227 Subgroup.closure (Set.range fun p : S.Q × X => S.generator ι p.1 p.2) := by
228 simpa [generatorSet] using
230 (G := ↥(H : Subgroup F))
231 (fun p : S.Q × X => S.generator ι p.1 p.2))
234 (S : SchreierSection (F := F) (X := X) H) (ι : X → F) :
236 (S.generatorSet ι) ↔
238 (Set.range fun p : S.Q × X => S.generator ι p.1 p.2) := by
241 S.subgroupClosure_generatorSet_eq_closure_range ι]
243omit [IsTopologicalGroup F] in
245 (S : SchreierSection (F := F) (X := X) H)
246 (hleft : S.orientation = SchreierOrientation.left)
247 (ι : X → F) (q : S.Q) (x : X) :
248 S.generator ι q x = 1 ↔ S.sectionMap (S.next ι q x) = S.sectionMap q * ι x := by
249 constructor
250 · intro h
251 have hval := congrArg Subtype.val h
252 change S.orientation.cocycle S.sectionMap (S.next ι) ι q x = 1 at hval
253 exact inv_mul_eq_one.mp (by
254 simpa [SchreierOrientation.cocycle, hleft, mul_assoc] using hval)
255 · intro hrep
256 apply Subtype.ext
257 simp only [generator, SchreierOrientation.cocycle, hleft, hrep, mul_inv_rev, mul_assoc, inv_mul_cancel,
258 mul_one, OneMemClass.coe_one]
260omit [IsTopologicalGroup F] in
262 (S : SchreierSection (F := F) (X := X) H)
263 (hright : S.orientation = SchreierOrientation.right)
264 (ι : X → F) (q : S.Q) (x : X) :
265 S.generator ι q x = 1 ↔ S.sectionMap (S.next ι q x) = S.sectionMap q * ι x := by
266 constructor
267 · intro h
268 have hval := congrArg Subtype.val h
269 change S.orientation.cocycle S.sectionMap (S.next ι) ι q x = 1 at hval
270 exact (mul_inv_eq_one.mp
271 (by simpa [SchreierOrientation.cocycle, hright, mul_assoc] using hval)).symm
272 · intro hrep
273 apply Subtype.ext
274 simp only [generator, SchreierOrientation.cocycle, hright, hrep, mul_inv_rev, mul_assoc, mul_inv_cancel_left,
275 mul_inv_cancel, OneMemClass.coe_one]
277omit [IsTopologicalGroup F] in
279 (S : SchreierSection (F := F) (X := X) H)
280 (ι : X → F) (q : S.Q) (x : X)
281 (hnext : S.sectionMap (S.next ι q x) = 1)
282 (hmem : S.sectionMap q * ι x ∈ (H : Subgroup F)) :
283 S.generator ι q x = ⟨S.sectionMap q * ι x, hmem⟩ := by
284 apply Subtype.ext
285 cases hside : S.orientation with
286 | left =>
287 simp only [generator, SchreierOrientation.cocycle, hside, hnext, inv_one, one_mul]
288 | right =>
289 simp only [generator, SchreierOrientation.cocycle, hside, hnext, inv_one, mul_one]
292 (S : SchreierSection (F := F) (X := X) H)
293 [TopologicalSpace S.Q] [TopologicalSpace X]
294 (ι : X → F)
295 (hsection : Continuous S.sectionMap)
296 (hnext : Continuous (fun p : S.Q × X => S.next ι p.1 p.2))
297 (hι : Continuous ι) :
298 Continuous (fun p : S.Q × X => S.generator ι p.1 p.2) := by
299 refine Continuous.subtype_mk ?_ ?_
300 cases hside : S.orientation with
301 | left =>
302 have hcont :
303 Continuous (fun p : S.Q × X =>
304 (S.sectionMap (S.next ι p.1 p.2))⁻¹ * (S.sectionMap p.1 * ι p.2)) :=
305 ((hsection.comp hnext).inv).mul
306 ((hsection.comp continuous_fst).mul (hι.comp continuous_snd))
307 simpa [generator, SchreierOrientation.cocycle, hside, mul_assoc] using hcont
308 | right =>
309 have hcont :
310 Continuous (fun p : S.Q × X =>
311 (S.sectionMap p.1 * ι p.2) * (S.sectionMap (S.next ι p.1 p.2))⁻¹) :=
312 ((hsection.comp continuous_fst).mul (hι.comp continuous_snd)).mul
313 ((hsection.comp hnext).inv)
314 simpa [generator, SchreierOrientation.cocycle, hside, mul_assoc] using hcont
318end AbstractSchreierSections
320section LeftSchreierGenerators
322variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
323variable (H : OpenSubgroup F)
324variable {X : Type v}
325variable (σ : F ⧸ (H : Subgroup F) → F)
326variable (hσ : Function.RightInverse σ (QuotientGroup.mk (s := (H : Subgroup F))))
327variable (ι : X → F)
329/-- Raw Schreier section cocycle for a section, a next-coset operation, and ambient generators. -/
330def sectionCocycle {Q : Type u} (σ : Q → F) (next : Q → X → Q) (ι : X → F) :
331 Q → X → F :=
332 fun q x => (σ (next q x))⁻¹ * σ q * ι x
334/-- The next left coset obtained from a chosen representative and a generator. -/
335def leftSchreierNextCoset (q : F ⧸ (H : Subgroup F)) (x : X) : F ⧸ (H : Subgroup F) :=
336 QuotientGroup.mk (s := (H : Subgroup F)) (σ q * ι x)
338/-- Left-coset Schreier generator attached to a section of the quotient by an open subgroup. -/
339noncomputable def leftSchreierGenerator
340 (hσ : Function.RightInverse σ (QuotientGroup.mk (s := (H : Subgroup F))))
341 (q : F ⧸ (H : Subgroup F)) (x : X) :
342 ↥(H : Subgroup F) := by
343 let qx := leftSchreierNextCoset (F := F) H σ ι q x
344 refine ⟨sectionCocycle (F := F) (X := X) σ
345 (leftSchreierNextCoset (F := F) H σ ι) ι q x, ?_⟩
346 have hqx :
347 QuotientGroup.mk (s := (H : Subgroup F)) (σ qx) =
348 QuotientGroup.mk (s := (H : Subgroup F)) (σ q * ι x) := by
349 simpa [qx, leftSchreierNextCoset] using hσ qx
350 simpa [sectionCocycle, mul_assoc] using (QuotientGroup.eq.1 hqx)
352/-- The left-coset Schreier data as an instance of the abstract section API. -/
353noncomputable def leftSchreierSection :
354 SchreierSection (F := F) (X := X) H where
355 Q := F ⧸ (H : Subgroup F)
356 orientation := SchreierOrientation.left
357 sectionMap := σ
358 next := fun ι q x => leftSchreierNextCoset (F := F) H σ ι q x
359 cocycle_mem := by
360 intro ι q x
361 exact (leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) q x).property
363omit [IsTopologicalGroup F] in
365 (q : F ⧸ (H : Subgroup F)) (x : X) :
366 (leftSchreierSection (F := F) (H := H) (σ := σ) (hσ := hσ) :
367 SchreierSection (F := F) (X := X) H).generator ι q x =
368 leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) q x := by
369 apply Subtype.ext
370 rfl
372/-- The normalized left quotient section as abstract Schreier section data. -/
373noncomputable def chosenLeftSchreierSection :
374 SchreierSection (F := F) (X := X) H :=
375 leftSchreierSection (F := F) (H := H)
379omit [IsTopologicalGroup F] in
381 (hσ : Function.RightInverse σ (QuotientGroup.mk (s := (H : Subgroup F))))
382 {q : F ⧸ (H : Subgroup F)} {x : X}
383 (hx : ι x ∈ (H : Subgroup F)) :
384 leftSchreierNextCoset (F := F) H σ ι q x = q := by
385 have hEq :
386 QuotientGroup.mk (s := (H : Subgroup F)) (σ q) =
387 QuotientGroup.mk (s := (H : Subgroup F)) (σ q * ι x) := by
388 exact QuotientGroup.eq.2 (by simpa using hx)
389 calc
390 leftSchreierNextCoset (F := F) H σ ι q x
391 = QuotientGroup.mk (s := (H : Subgroup F)) (σ q * ι x) := rfl
392 _ = QuotientGroup.mk (s := (H : Subgroup F)) (σ q) := hEq.symm
393 _ = q := hσ q
395omit [IsTopologicalGroup F] in
397 {q : F ⧸ (H : Subgroup F)} {x : X}
398 (hx : σ q * ι x ∈ (H : Subgroup F)) :
399 leftSchreierNextCoset (F := F) H σ ι q x =
400 QuotientGroup.mk (s := (H : Subgroup F)) (1 : F) := by
401 apply QuotientGroup.eq.2
402 simpa using (H : Subgroup F).inv_mem hx
404omit [IsTopologicalGroup F] in
406 {q : F ⧸ (H : Subgroup F)} {x : X}
407 (hx : ι x ∈ (H : Subgroup F)) :
408 leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) q x = ⟨ι x, hx⟩ := by
409 apply Subtype.ext
410 have hnext :
411 leftSchreierNextCoset (F := F) H σ ι q x = q :=
412 leftSchreierNextCoset_eq_of_mem (F := F) (H := H) (σ := σ) (ι := ι) hσ hx
413 simp only [leftSchreierGenerator, sectionCocycle, hnext, inv_mul_cancel, one_mul]
415omit [IsTopologicalGroup F] in
417 {q : F ⧸ (H : Subgroup F)} {x : X}
418 (hx : ι x = 1) :
419 leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) q x = 1 := by
420 have hx' : ι x ∈ (H : Subgroup F) := by
421 rw [hx]
422 exact (H : Subgroup F).one_mem
423 rw [leftSchreierGenerator_eq_of_mem (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) hx']
424 simp only [hx, Subgroup.mk_eq_one]
426omit [IsTopologicalGroup F] in
428 {H : OpenSubgroup F}
429 {σ : F ⧸ (H : Subgroup F) → F}
430 (hσ : Function.RightInverse σ (QuotientGroup.mk (s := (H : Subgroup F))))
431 {ι : X → F}
432 {q : F ⧸ (H : Subgroup F)} {x : X} :
433 leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) q x = 1 ↔
434 σ (leftSchreierNextCoset (F := F) H σ ι q x) = σ q * ι x := by
435 simpa using
436 ((leftSchreierSection (F := F) (H := H) (σ := σ) (hσ := hσ) :
438 rfl ι q x)
440omit [IsTopologicalGroup F] in
442 {q : F ⧸ (H : Subgroup F)} {x : X}
443 (hrep : σ (leftSchreierNextCoset (F := F) H σ ι q x) = σ q * ι x) :
444 leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) q x = 1 :=
446 (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι)
447 (q := q) (x := x)).2 hrep
449omit [IsTopologicalGroup F] in
451 (hσ1 : σ (QuotientGroup.mk (s := (H : Subgroup F)) (1 : F)) = 1)
452 {q : F ⧸ (H : Subgroup F)} {x : X}
453 (hx : σ q * ι x ∈ (H : Subgroup F)) :
454 leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) q x =
455 ⟨σ q * ι x, hx⟩ := by
456 have hnext : leftSchreierNextCoset (F := F) H σ ι q x =
457 QuotientGroup.mk (s := (H : Subgroup F)) (1 : F) := by
458 apply QuotientGroup.eq.2
459 simpa [mul_inv_rev] using (H : Subgroup F).inv_mem hx
460 have hsectionNext :
461 σ (leftSchreierNextCoset (F := F) H σ ι q x) = 1 := by
462 simpa [hnext] using hσ1
463 simpa using
464 ((leftSchreierSection (F := F) (H := H) (σ := σ) (hσ := hσ) :
466 ι q x hsectionNext hx)
468section Topological
470variable [TopologicalSpace X]
473 (hσcont : Continuous σ) (hιcont : Continuous ι) :
474 Continuous (fun p : (F ⧸ (H : Subgroup F)) × X =>
475 leftSchreierNextCoset (F := F) H σ ι p.1 p.2) := by
477 (QuotientGroup.continuous_mk.comp
478 ((hσcont.comp continuous_fst).mul (hιcont.comp continuous_snd)))
481 (hσcont : Continuous σ) (hιcont : Continuous ι) :
482 Continuous (fun p : (F ⧸ (H : Subgroup F)) × X =>
483 leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) p.1 p.2) := by
484 letI : TopologicalSpace
485 (leftSchreierSection (F := F) (H := H) (σ := σ) (hσ := hσ) :
486 SchreierSection (F := F) (X := X) H).Q :=
487 inferInstanceAs (TopologicalSpace (F ⧸ (H : Subgroup F)))
488 simpa using
489 ((leftSchreierSection (F := F) (H := H) (σ := σ) (hσ := hσ) :
491 ι hσcont
492 (continuous_leftSchreierNextCoset (F := F) (H := H) (σ := σ) (ι := ι)
493 hσcont hιcont)
494 hιcont)
496end Topological
498section FiniteCardinality
500omit [IsTopologicalGroup F] in
502 [Finite X] [Finite (F ⧸ (H : Subgroup F))] :
503 Nat.card
504 (Set.range fun p : (F ⧸ (H : Subgroup F)) × X =>
505 leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) p.1 p.2) ≤
506 Nat.card (F ⧸ (H : Subgroup F)) * Nat.card X := by
507 simpa [Nat.card_prod] using
508 (Finite.card_range_le
509 (fun p : (F ⧸ (H : Subgroup F)) × X =>
510 leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) p.1 p.2))
512end FiniteCardinality
514/-- The nontrivial left-coset Schreier generators attached to a section. -/
515def leftSchreierGeneratorSet : Set ↥(H : Subgroup F) :=
516 {z | ∃ q : F ⧸ (H : Subgroup F), ∃ x : X,
517 z = leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) q x ∧
518 z ≠ 1}
520/-- Nontrivial left Schreier pairs for a chosen section. -/
521def leftNontrivialSchreierPairs : Type (max u v) :=
522 {p : (F ⧸ (H : Subgroup F)) × X //
523 leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) p.1 p.2 ≠ 1}
525omit [IsTopologicalGroup F] in
527 [Finite X] [Finite (F ⧸ (H : Subgroup F))] :
528 Finite (leftNontrivialSchreierPairs (F := F) H σ hσ ι) :=
529 Finite.of_injective
530 (fun p : leftNontrivialSchreierPairs (F := F) H σ hσ ι => p.1)
531 (by
532 intro a b h
533 exact Subtype.ext h)
535omit [IsTopologicalGroup F] in
537 [Finite X] [Finite (F ⧸ (H : Subgroup F))] :
538 Nat.card (leftNontrivialSchreierPairs (F := F) H σ hσ ι) ≤
539 Nat.card (F ⧸ (H : Subgroup F)) * Nat.card X := by
540 have hle :
541 Nat.card (leftNontrivialSchreierPairs (F := F) H σ hσ ι) ≤
542 Nat.card ((F ⧸ (H : Subgroup F)) × X) := by
543 exact Nat.card_le_card_of_injective
544 (fun p : leftNontrivialSchreierPairs (F := F) H σ hσ ι => p.1)
545 (by
546 intro a b h
547 exact Subtype.ext h)
548 simpa [Nat.card_prod] using hle
550omit [IsTopologicalGroup F] in
551/-- The tautological map from nontrivial left Schreier pairs to the nontrivial generator set. -/
553 leftNontrivialSchreierPairs (F := F) H σ hσ ι →
554 ↥(leftSchreierGeneratorSet (F := F) H σ hσ ι) := fun p =>
555 ⟨leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) p.1.1 p.1.2,
556 ⟨p.1.1, p.1.2, rfl, p.2⟩⟩
558omit [IsTopologicalGroup F] in
560 (p : leftNontrivialSchreierPairs (F := F) H σ hσ ι) :
562 ↥(leftSchreierGeneratorSet (F := F) H σ hσ ι)) : ↥(H : Subgroup F)) =
563 leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι)
564 p.1.1 p.1.2 :=
565 rfl
567omit [IsTopologicalGroup F] in
569 Function.Surjective
570 (leftNontrivialSchreierPairsToGeneratorSet (F := F) H σ hσ ι) := by
571 intro z
572 rcases z.2 with ⟨q, x, hz, hz_ne⟩
573 refine ⟨⟨(q, x), ?_⟩, ?_⟩
574 · simpa [hz] using hz_ne
575 · apply Subtype.ext
576 exact hz.symm
578omit [IsTopologicalGroup F] in
580 [Finite X] [Finite (F ⧸ (H : Subgroup F))] :
581 Nat.card (leftSchreierGeneratorSet (F := F) H σ hσ ι) ≤
582 Nat.card (leftNontrivialSchreierPairs (F := F) H σ hσ ι) := by
583 exact Nat.card_le_card_of_surjective
586 (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι))
588omit [IsTopologicalGroup F] in
590 {H : OpenSubgroup F}
591 {σ : F ⧸ (H : Subgroup F) → F}
592 {hσ : Function.RightInverse σ (QuotientGroup.mk (s := (H : Subgroup F)))}
593 {ι : X → F} {z : ↥(H : Subgroup F)} :
594 z ∈ leftSchreierGeneratorSet (F := F) H σ hσ ι ↔
595 ∃ q : F ⧸ (H : Subgroup F), ∃ x : X,
596 z = leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) q x ∧
597 z ≠ 1 :=
598 Iff.rfl
600omit [IsTopologicalGroup F] in
602 leftSchreierGeneratorSet (F := F) H σ hσ ι ⊆
603 Set.range (fun p : (F ⧸ (H : Subgroup F)) × X =>
604 leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) p.1 p.2) := by
605 intro z hz
606 rcases hz with ⟨q, x, rfl, _⟩
607 exact ⟨(q, x), rfl⟩
609omit [IsTopologicalGroup F] in
611 Subgroup.closure (leftSchreierGeneratorSet (F := F) H σ hσ ι) =
612 Subgroup.closure (Set.range fun p : (F ⧸ (H : Subgroup F)) × X =>
613 leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) p.1 p.2) := by
614 simpa [leftSchreierGeneratorSet, SchreierSection.generatorSet] using
615 ((leftSchreierSection (F := F) (H := H) (σ := σ) (hσ := hσ) :
619 {H : OpenSubgroup F}
620 {σ : F ⧸ (H : Subgroup F) → F}
621 {hσ : Function.RightInverse σ (QuotientGroup.mk (s := (H : Subgroup F)))}
622 {ι : X → F} :
624 (leftSchreierGeneratorSet (F := F) H σ hσ ι) ↔
626 (Set.range fun p : (F ⧸ (H : Subgroup F)) × X =>
627 leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) p.1 p.2) := by
628 simpa [leftSchreierGeneratorSet, SchreierSection.generatorSet] using
629 ((leftSchreierSection (F := F) (H := H) (σ := σ) (hσ := hσ) :
632omit [IsTopologicalGroup F] in
634 [Finite X] [Finite (F ⧸ (H : Subgroup F))] :
635 Nat.card (leftSchreierGeneratorSet (F := F) H σ hσ ι) ≤
636 Nat.card (F ⧸ (H : Subgroup F)) * Nat.card X := by
637 letI : Finite
638 (leftSchreierSection (F := F) (H := H) (σ := σ) (hσ := hσ) :
639 SchreierSection (F := F) (X := X) H).Q :=
640 inferInstanceAs (Finite (F ⧸ (H : Subgroup F)))
641 simpa [leftSchreierGeneratorSet, SchreierSection.generatorSet] using
642 ((leftSchreierSection (F := F) (H := H) (σ := σ) (hσ := hσ) :
645end LeftSchreierGenerators
647section RightSchreierGenerators
649variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
650variable (H : OpenSubgroup F)
651variable {X : Type v}
652variable (τ : OpenSubgroupRightQuotient H → F)
653variable (hτ : ∀ q, Quotient.mk'' (τ q) = q)
654variable (ι : X → F)
657 MulAction F (OpenSubgroupRightQuotient H) :=
658 rightCosetMulAction (H : Subgroup F)
660/-- The next right coset obtained from a chosen representative and a generator. -/
663 (ι x)⁻¹ • q
665omit [IsTopologicalGroup F] in
667 {x : X} (hx : ι x ∈ (H : Subgroup F)) :
668 rightSchreierNextCoset (F := F) H ι (openSubgroupRightCoset H (1 : F)) x =
669 openSubgroupRightCoset H (1 : F) := by
670 calc
671 rightSchreierNextCoset (F := F) H ι (openSubgroupRightCoset H (1 : F)) x =
672 (ι x)⁻¹ • (Quotient.mk'' (1 : F) : OpenSubgroupRightQuotient H) := rfl
673 _ = Quotient.mk'' ((1 : F) * ι x) := by
674 rw [rightCosetMulAction_inv_mk_smul (H := (H : Subgroup F))]
675 _ = openSubgroupRightCoset H (1 : F) := by
677 (by simpa using hx)
679omit [IsTopologicalGroup F] in
681 (hτ : ∀ q, Quotient.mk'' (τ q) = q)
683 (hx : τ q * ι x ∈ (H : Subgroup F)) :
684 rightSchreierNextCoset (F := F) H ι q x = openSubgroupRightCoset H (1 : F) := by
685 calc
686 rightSchreierNextCoset (F := F) H ι q x =
687 (ι x)⁻¹ • (Quotient.mk'' (τ q) : OpenSubgroupRightQuotient H) := by
688 simp only [rightSchreierNextCoset, hτ q]
689 _ = Quotient.mk'' (τ q * ι x) := by
690 rw [rightCosetMulAction_inv_mk_smul (H := (H : Subgroup F))]
691 _ = openSubgroupRightCoset H (1 : F) :=
694/-- Right-coset Schreier generator `t_q x t_{qx}^{-1}`. -/
695noncomputable def rightSchreierGenerator (q : OpenSubgroupRightQuotient H) (x : X) :
696 ↥(H : Subgroup F) :=
697 rightQuotientSectionCocycle (H := (H : Subgroup F)) τ hτ (ι x) q
699/-- The right-coset Schreier data as an instance of the abstract section API. -/
700noncomputable def rightSchreierSection :
701 SchreierSection (F := F) (X := X) H where
703 orientation := SchreierOrientation.right
704 sectionMap := τ
705 next := fun ι q x => rightSchreierNextCoset (F := F) H ι q x
706 cocycle_mem := by
707 intro ι q x
708 exact (rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) q x).property
710omit [IsTopologicalGroup F] in
712 (q : OpenSubgroupRightQuotient H) (x : X) :
713 (rightSchreierSection (F := F) (H := H) (τ := τ) (hτ := hτ) :
714 SchreierSection (F := F) (X := X) H).generator ι q x =
715 rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) q x := by
716 apply Subtype.ext
717 rfl
719/-- The normalized right quotient section as abstract Schreier section data. -/
720noncomputable def chosenRightSchreierSection :
721 SchreierSection (F := F) (X := X) H :=
722 rightSchreierSection (F := F) (H := H)
726omit [IsTopologicalGroup F] in
729 (hx : ι x = 1) :
730 rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) q x = 1 := by
731 apply Subtype.ext
732 simp only [rightSchreierGenerator, rightQuotientSectionCocycle, hx, mul_one, inv_one, one_smul,
733 mul_inv_cancel, OneMemClass.coe_one]
735omit [IsTopologicalGroup F] in
737 {H : OpenSubgroup F}
739 (hτ : ∀ q, Quotient.mk'' (τ q) = q)
740 {ι : X → F}
741 {q : OpenSubgroupRightQuotient H} {x : X} :
742 rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) q x = 1 ↔
743 τ ((ι x)⁻¹ • q) = τ q * ι x := by
744 simpa using
745 ((rightSchreierSection (F := F) (H := H) (τ := τ) (hτ := hτ) :
747 rfl ι q x)
749omit [IsTopologicalGroup F] in
751 {H : OpenSubgroup F}
753 (hτ : ∀ q, Quotient.mk'' (τ q) = q)
754 {ι : X → F}
755 {q : OpenSubgroupRightQuotient H} {x : X} :
756 rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) q x = 1 ↔
757 τ (rightSchreierNextCoset (F := F) H ι q x) = τ q * ι x := by
760 (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι)
761 (q := q) (x := x))
763omit [IsTopologicalGroup F] in
766 (hrep : τ ((ι x)⁻¹ • q) = τ q * ι x) :
767 rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) q x = 1 :=
769 (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι)
770 (q := q) (x := x)).2 hrep
772omit [IsTopologicalGroup F] in
774 (hτ1 : τ (openSubgroupRightCoset H (1 : F)) = 1)
776 (hx : τ q * ι x ∈ (H : Subgroup F)) :
777 rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) q x =
778 ⟨τ q * ι x, hx⟩ := by
779 have hnext : (ι x)⁻¹ • q = openSubgroupRightCoset H (1 : F) := by
780 calc
781 (ι x)⁻¹ • q = (ι x)⁻¹ • (Quotient.mk'' (τ q) : OpenSubgroupRightQuotient H) := by
782 rw [hτ q]
783 _ = Quotient.mk'' (τ q * ι x) := by
784 rw [rightCosetMulAction_inv_mk_smul (H := (H : Subgroup F))]
785 _ = openSubgroupRightCoset H (1 : F) :=
787 have hsectionNext : τ ((ι x)⁻¹ • q) = 1 := by
788 simpa [hnext] using hτ1
789 simpa using
790 ((rightSchreierSection (F := F) (H := H) (τ := τ) (hτ := hτ) :
792 ι q x hsectionNext hx)
794omit [IsTopologicalGroup F] in
796 (hτ1 : τ (openSubgroupRightCoset H (1 : F)) = 1)
797 {x : X} (hx : ι x ∈ (H : Subgroup F)) :
798 rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι)
799 (openSubgroupRightCoset H (1 : F)) x =
800 ⟨ι x, hx⟩ := by
801 have hx' : τ (openSubgroupRightCoset H (1 : F)) * ι x ∈ (H : Subgroup F) := by
802 simpa [hτ1] using hx
803 simpa [hτ1] using
805 (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι)
806 hτ1 (q := openSubgroupRightCoset H (1 : F)) (x := x) hx')
808section Topological
810variable [TopologicalSpace X]
811variable [TopologicalSpace (OpenSubgroupRightQuotient H)]
812variable [DiscreteTopology (OpenSubgroupRightQuotient H)]
815 (hιcont : Continuous ι) :
816 Continuous (fun p : OpenSubgroupRightQuotient H × X =>
817 rightSchreierNextCoset (F := F) H ι p.1 p.2) := by
818 letI : MulAction F (OpenSubgroupRightQuotient H) :=
819 rightCosetMulAction (H : Subgroup F)
820 refine (continuous_prod_of_discrete_left).2 ?_
821 intro q
822 have hqcont :
823 Continuous fun x : X => ((ι x)⁻¹ • q : OpenSubgroupRightQuotient H) := by
824 rw [continuous_discrete_rng]
825 intro q'
826 classical
827 let a : F := q.out
828 let b : F := q'.out
829 have hpre :
830 (fun x : X => ((ι x)⁻¹ • q : OpenSubgroupRightQuotient H)) ⁻¹' ({q'} :
832 (fun x : X => b * (ι x)⁻¹ * a⁻¹) ⁻¹' ((H : Subgroup F) : Set F) := by
833 ext x
834 constructor
835 · intro hx
836 have hEq :
837 (Quotient.mk'' (a * ι x) : OpenSubgroupRightQuotient H) = Quotient.mk'' b := by
838 calc
839 (Quotient.mk'' (a * ι x) : OpenSubgroupRightQuotient H)
840 = (ι x)⁻¹ • (Quotient.mk'' a : OpenSubgroupRightQuotient H) := by
841 rw [rightCosetMulAction_inv_mk_smul (H := (H : Subgroup F)) (ι x) a]
842 _ = (ι x)⁻¹ • q := by rw [Quotient.out_eq' q]
843 _ = q' := hx
844 _ = Quotient.mk'' b := (Quotient.out_eq' q').symm
845 have hrel :
846 QuotientGroup.rightRel (H : Subgroup F) (a * ι x) b := Quotient.eq''.mp hEq
847 simpa [a, b, mul_inv_rev, mul_assoc] using (QuotientGroup.rightRel_apply.mp hrel)
848 · intro hx
849 have hrel :
850 QuotientGroup.rightRel (H : Subgroup F) (a * ι x) b := by
851 rw [QuotientGroup.rightRel_apply]
852 simpa only [a, b, mul_inv_rev, mul_assoc] using hx
853 calc
854 ((ι x)⁻¹ • q : OpenSubgroupRightQuotient H)
855 = (ι x)⁻¹ • (Quotient.mk'' a : OpenSubgroupRightQuotient H) := by
856 rw [Quotient.out_eq' q]
857 _ = Quotient.mk'' (a * ι x) := by
858 rw [rightCosetMulAction_inv_mk_smul (H := (H : Subgroup F)) (ι x) a]
859 _ = Quotient.mk'' b := Quotient.eq''.mpr hrel
860 _ = q' := Quotient.out_eq' q'
861 rw [show
862 (fun x : X => ((ι x)⁻¹ • q : OpenSubgroupRightQuotient H)) ⁻¹' ({q'} :
864 (fun x : X => b * (ι x)⁻¹ * a⁻¹) ⁻¹' ((H : Subgroup F) : Set F) by
865 simpa using hpre]
866 exact H.isOpen'.preimage ((continuous_const.mul (hιcont.inv)).mul continuous_const)
867 simpa [rightSchreierNextCoset] using hqcont
870 (hτcont : Continuous τ) (hιcont : Continuous ι) :
871 Continuous (fun p : OpenSubgroupRightQuotient H × X =>
872 rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) p.1 p.2) := by
873 letI : TopologicalSpace
874 (rightSchreierSection (F := F) (H := H) (τ := τ) (hτ := hτ) :
875 SchreierSection (F := F) (X := X) H).Q :=
876 inferInstanceAs (TopologicalSpace (OpenSubgroupRightQuotient H))
877 simpa using
878 ((rightSchreierSection (F := F) (H := H) (τ := τ) (hτ := hτ) :
880 ι hτcont
881 (continuous_rightSchreierNextCoset (F := F) (H := H) (ι := ι) hιcont)
882 hιcont)
884end Topological
888 [CompactSpace F] [Finite X] :
889 Nat.card
890 (Set.range fun p : OpenSubgroupRightQuotient H × X =>
891 rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) p.1 p.2) ≤
892 Nat.card (OpenSubgroupRightQuotient H) * Nat.card X := by
893 simpa [Nat.card_prod] using
894 (Finite.card_range_le
895 (fun p : OpenSubgroupRightQuotient H × X =>
896 rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) p.1 p.2))
899/-- The nontrivial right-coset Schreier generators attached to a section. -/
900def rightSchreierGeneratorSet : Set ↥(H : Subgroup F) :=
901 {z | ∃ q : OpenSubgroupRightQuotient H, ∃ x : X,
902 z = rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) q x ∧
903 z ≠ 1}
905/-- Nontrivial right Schreier pairs for a chosen section. -/
906def rightNontrivialSchreierPairs : Type (max u v) :=
908 rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) p.1 p.2 ≠ 1}
910omit [IsTopologicalGroup F] in
912 [Finite X] [Finite (OpenSubgroupRightQuotient H)] :
913 Finite (rightNontrivialSchreierPairs (F := F) H τ hτ ι) :=
914 Finite.of_injective
915 (fun p : rightNontrivialSchreierPairs (F := F) H τ hτ ι => p.1)
916 (by
917 intro a b h
918 exact Subtype.ext h)
920omit [IsTopologicalGroup F] in
922 [Finite X] [Finite (OpenSubgroupRightQuotient H)] :
923 Nat.card (rightNontrivialSchreierPairs (F := F) H τ hτ ι) ≤
924 Nat.card (OpenSubgroupRightQuotient H) * Nat.card X := by
925 have hle :
926 Nat.card (rightNontrivialSchreierPairs (F := F) H τ hτ ι) ≤
927 Nat.card (OpenSubgroupRightQuotient H × X) := by
928 exact Nat.card_le_card_of_injective
929 (fun p : rightNontrivialSchreierPairs (F := F) H τ hτ ι => p.1)
930 (by
931 intro a b h
932 exact Subtype.ext h)
933 simpa [Nat.card_prod] using hle
935omit [IsTopologicalGroup F] in
936/-- The tautological map from nontrivial right Schreier pairs to the nontrivial generator set. -/
938 rightNontrivialSchreierPairs (F := F) H τ hτ ι →
939 ↥(rightSchreierGeneratorSet (F := F) H τ hτ ι) := fun p =>
940 ⟨rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) p.1.1 p.1.2,
941 ⟨p.1.1, p.1.2, rfl, p.2⟩⟩
943omit [IsTopologicalGroup F] in
945 (p : rightNontrivialSchreierPairs (F := F) H τ hτ ι) :
947 ↥(rightSchreierGeneratorSet (F := F) H τ hτ ι)) : ↥(H : Subgroup F)) =
948 rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι)
949 p.1.1 p.1.2 :=
950 rfl
952omit [IsTopologicalGroup F] in
954 Function.Surjective
955 (rightNontrivialSchreierPairsToGeneratorSet (F := F) H τ hτ ι) := by
956 intro z
957 rcases z.2 with ⟨q, x, hz, hz_ne⟩
958 refine ⟨⟨(q, x), ?_⟩, ?_⟩
959 · simpa [hz] using hz_ne
960 · apply Subtype.ext
961 exact hz.symm
963omit [IsTopologicalGroup F] in
965 [Finite X] [Finite (OpenSubgroupRightQuotient H)] :
966 Nat.card (rightSchreierGeneratorSet (F := F) H τ hτ ι) ≤
967 Nat.card (rightNontrivialSchreierPairs (F := F) H τ hτ ι) := by
968 exact Nat.card_le_card_of_surjective
971 (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι))
973omit [IsTopologicalGroup F] in
975 {H : OpenSubgroup F}
977 {hτ : ∀ q, Quotient.mk'' (τ q) = q}
978 {ι : X → F} {z : ↥(H : Subgroup F)} :
979 z ∈ rightSchreierGeneratorSet (F := F) H τ hτ ι ↔
980 ∃ q : OpenSubgroupRightQuotient H, ∃ x : X,
981 z = rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) q x ∧
982 z ≠ 1 :=
983 Iff.rfl
985omit [IsTopologicalGroup F] in
987 rightSchreierGeneratorSet (F := F) H τ hτ ι ⊆
988 Set.range (fun p : OpenSubgroupRightQuotient H × X =>
989 rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) p.1 p.2) := by
990 intro z hz
991 rcases hz with ⟨q, x, rfl, _⟩
992 exact ⟨(q, x), rfl⟩
994omit [IsTopologicalGroup F] in
996 Subgroup.closure (rightSchreierGeneratorSet (F := F) H τ hτ ι) =
997 Subgroup.closure (Set.range fun p : OpenSubgroupRightQuotient H × X =>
998 rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) p.1 p.2) := by
999 simpa [rightSchreierGeneratorSet, SchreierSection.generatorSet] using
1000 ((rightSchreierSection (F := F) (H := H) (τ := τ) (hτ := hτ) :
1004 {H : OpenSubgroup F}
1006 {hτ : ∀ q, Quotient.mk'' (τ q) = q}
1007 {ι : X → F} :
1009 (rightSchreierGeneratorSet (F := F) H τ hτ ι) ↔
1011 (Set.range fun p : OpenSubgroupRightQuotient H × X =>
1012 rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) p.1 p.2) := by
1013 simpa [rightSchreierGeneratorSet, SchreierSection.generatorSet] using
1014 ((rightSchreierSection (F := F) (H := H) (τ := τ) (hτ := hτ) :
1018 [CompactSpace F] [Finite X] :
1019 Nat.card (rightSchreierGeneratorSet (F := F) H τ hτ ι) ≤
1020 Nat.card (OpenSubgroupRightQuotient H) * Nat.card X := by
1021 letI : Finite
1022 (rightSchreierSection (F := F) (H := H) (τ := τ) (hτ := hτ) :
1023 SchreierSection (F := F) (X := X) H).Q :=
1024 inferInstanceAs (Finite (OpenSubgroupRightQuotient H))
1025 simpa [rightSchreierGeneratorSet, SchreierSection.generatorSet, rightSchreierSection,
1026 Nat.card_eq_fintype_card] using
1027 ((rightSchreierSection (F := F) (H := H) (τ := τ) (hτ := hτ) :
1030omit [IsTopologicalGroup F] in
1031/-- The basepoint projection induced by a wreath-product homomorphism evaluates a right Schreier
1032generator by the corresponding left coordinate. -/
1034 {A : Type*} [Group A]
1036 (hψ :
1037 (SemidirectProduct.rightHom :
1039 MonoidHom.id F)
1040 (hτpure :
1043 (openSubgroupRightCoset H (1 : F)) (τ q) = 1)
1046 (rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) q x) =
1047 wreathLeftCoordinate ψ q (ι x) := by
1049 (H : Subgroup F) τ hτ ψ hψ hτpure (ι x) q
1051end RightSchreierGenerators
1053end Profinite
1054end ReidemeisterSchreier