ReidemeisterSchreier/Discrete/OpenSubgroups/Generators.lean
1import ReidemeisterSchreier.Discrete.OpenSubgroups.Transversals
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ReidemeisterSchreier/Discrete/OpenSubgroups/Generators.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Schreier representatives and generators
14Defines Schreier representatives, nontrivial Schreier pairs, classical generator values, and pointed transversal constructions.
15-/
17namespace ReidemeisterSchreier.Discrete.OpenSubgroups
19section SchreierGenerators
21open scoped Pointwise
22open FreeGroup
24/-- The Schreier transversal itself carries the same right-coset action, transported along the
25equivalence with right cosets. -/
26noncomputable def schreierTransversalRightCosetAction {X : Type u} [DecidableEq X]
27 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
28 (hT : IsRightSchreierTransversal (X := X) L T) :
29 MulAction (FreeGroup X) T := by
30 letI : MulAction (FreeGroup X) (Quotient (QuotientGroup.rightRel L)) :=
32 let e : T ≃ Quotient (QuotientGroup.rightRel L) := hT.1.rightQuotientEquiv.symm
33 refine
34 { smul := fun g t => e.symm (g • e t)
35 one_smul := by
36 intro t
37 change e.symm (1 • e t) = t
38 rw [one_smul]
39 exact e.left_inv t
40 mul_smul := by
41 intro g h t
42 change e.symm ((g * h) • e t) = e.symm (g • e (e.symm (h • e t)))
43 rw [mul_smul, e.apply_symm_apply] }
45/-- The chosen representative of a right coset attached to a right Schreier transversal. -/
46noncomputable def schreierRepresentative {X : Type u} [DecidableEq X]
47 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
48 (hT : IsRightSchreierTransversal (X := X) L T) :
49 FreeGroup X → T :=
50 hT.1.toRightFun
52@[simp] theorem schreierRepresentative_eq_of_mem {X : Type u} [DecidableEq X]
53 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
54 (hT : IsRightSchreierTransversal (X := X) L T)
55 {t : FreeGroup X} (ht : t ∈ T) :
56 schreierRepresentative (X := X) hT t = ⟨t, ht⟩ := by
57 apply (Subgroup.isComplement_iff_existsUnique_mul_inv_mem.mp hT.1 t).unique
58 · exact hT.1.mul_inv_toRightFun_mem t
59 · simp only [mul_inv_cancel, SetLike.mem_coe, one_mem]
61@[simp] theorem schreierRepresentative_eq_one_of_mem {X : Type u} [DecidableEq X]
62 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
63 (hT : IsRightSchreierTransversal (X := X) L T)
64 {g : FreeGroup X} (hg : g ∈ L) :
65 schreierRepresentative (X := X) hT g = ⟨1, hT.2.1⟩ := by
66 apply (Subgroup.isComplement_iff_existsUnique_mul_inv_mem.mp hT.1 g).unique
67 · exact hT.1.mul_inv_toRightFun_mem g
68 · simpa using hg
70theorem schreierRepresentative_eq_of_mem_mul_inv_mem {X : Type u} [DecidableEq X]
71 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
72 (hT : IsRightSchreierTransversal (X := X) L T)
73 {g t : FreeGroup X} (ht : t ∈ T) (hgt : g * t⁻¹ ∈ L) :
74 schreierRepresentative (X := X) hT g = ⟨t, ht⟩ := by
75 apply (Subgroup.isComplement_iff_existsUnique_mul_inv_mem.mp hT.1 g).unique
76 · exact hT.1.mul_inv_toRightFun_mem g
77 · exact hgt
79theorem prefixParent_mem_of_mem {X : Type u} [DecidableEq X]
80 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
81 (hT : IsRightSchreierTransversal (X := X) L T)
82 {t : FreeGroup X} (ht : t ∈ T) :
83 FreeGroup.prefixParent t ∈ T := by
84 refine hT.2.2 ht ?_
85 refine ⟨(FreeGroup.toWord t).length - 1, Nat.sub_le (FreeGroup.toWord t).length 1, ?_⟩
86 simp only [prefixParent, List.dropLast_eq_take]
88theorem schreierTransversalRightCosetAction_smul {X : Type u} [DecidableEq X]
89 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
90 (hT : IsRightSchreierTransversal (X := X) L T)
91 (g : FreeGroup X) (t : T) :
92 letI := schreierTransversalRightCosetAction (X := X) hT
93 g • t = schreierRepresentative (X := X) hT ((t : FreeGroup X) * g⁻¹) := by
94 let e : T ≃ Quotient (QuotientGroup.rightRel L) := hT.1.rightQuotientEquiv.symm
95 have ht : e t = Quotient.mk'' (t : FreeGroup X) := by
96 simpa [e] using hT.1.mk''_rightQuotientEquiv (e t)
97 change
98 hT.1.rightQuotientEquiv (g • hT.1.rightQuotientEquiv.symm t) =
99 hT.1.rightQuotientEquiv (Quotient.mk'' ((t : FreeGroup X) * g⁻¹))
102/-- The Schreier expression attached to any word `t` and basis element `x`. -/
103noncomputable def schreierGenerator {X : Type u} [DecidableEq X]
104 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
105 (hT : IsRightSchreierTransversal (X := X) L T) (t : FreeGroup X) (x : X) : L := by
106 refine
107 ⟨t * FreeGroup.of x *
108 ((schreierRepresentative (X := X) hT (t * FreeGroup.of x) : T) : FreeGroup X)⁻¹, ?_⟩
109 exact hT.1.mul_inv_toRightFun_mem (t * FreeGroup.of x)
111/-- The canonical index type for the nontrivial Schreier generators attached to a right Schreier
112transversal. This pair-indexed type is the preferred basis index; the value-set
113`schreierGeneratorSet` records the same nontrivial generators by their subgroup values. -/
114abbrev NontrivialSchreierPair {X : Type u} [DecidableEq X]
115 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
116 (hT : IsRightSchreierTransversal (X := X) L T) : Type u :=
117 {p : T × X // schreierGenerator (X := X) hT ((p.1 : T) : FreeGroup X) p.2 ≠ 1}
119/-- The Schreier generator value represented by a nontrivial Schreier pair. -/
120noncomputable def nontrivialSchreierPairGenerator {X : Type u} [DecidableEq X]
121 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
122 (hT : IsRightSchreierTransversal (X := X) L T) :
123 NontrivialSchreierPair (X := X) hT → L :=
124 fun p => schreierGenerator (X := X) hT ((p.1.1 : T) : FreeGroup X) p.1.2
126@[simp] theorem nontrivialSchreierPairGenerator_apply {X : Type u} [DecidableEq X]
127 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
128 (hT : IsRightSchreierTransversal (X := X) L T)
129 (p : NontrivialSchreierPair (X := X) hT) :
130 nontrivialSchreierPairGenerator (X := X) hT p =
131 schreierGenerator (X := X) hT ((p.1.1 : T) : FreeGroup X) p.1.2 :=
132 rfl
134/-- The classical Schreier generator value set attached to a right Schreier transversal.
135Prefer `NontrivialSchreierPair` as the basis index; this set records only the resulting values. -/
136def schreierGeneratorSet {X : Type u} [DecidableEq X]
137 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
138 (hT : IsRightSchreierTransversal (X := X) L T) : Set L :=
139 {z | ∃ t ∈ T, ∃ x : X, z = schreierGenerator (X := X) hT t x ∧ z ≠ 1}
141@[simp] theorem mem_schreierGeneratorSet_iff {X : Type u} [DecidableEq X]
142 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
143 (hT : IsRightSchreierTransversal (X := X) L T) {z : L} :
144 z ∈ schreierGeneratorSet (X := X) hT ↔
145 ∃ t ∈ T, ∃ x : X, z = schreierGenerator (X := X) hT t x ∧ z ≠ 1 :=
146 Iff.rfl
149 {X : Type u} [DecidableEq X]
150 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
151 (hT : IsRightSchreierTransversal (X := X) L T)
152 {t : FreeGroup X} (ht : t ∈ T) (x : X)
153 (hne : schreierGenerator (X := X) hT t x ≠ 1) :
154 schreierGenerator (X := X) hT t x ∈ schreierGeneratorSet (X := X) hT :=
155 ⟨t, ht, x, rfl, hne⟩
158 {X : Type u} [DecidableEq X]
159 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
160 (hT : IsRightSchreierTransversal (X := X) L T)
161 (t : T) (x : X)
162 (hne : schreierGenerator (X := X) hT (t : FreeGroup X) x ≠ 1) :
163 schreierGenerator (X := X) hT (t : FreeGroup X) x ∈
164 schreierGeneratorSet (X := X) hT :=
166 (X := X) hT t.property x hne
168/-- The value-set API is precisely the range of the pair-indexed generator map. -/
170 {X : Type u} [DecidableEq X]
171 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
172 (hT : IsRightSchreierTransversal (X := X) L T) :
173 schreierGeneratorSet (X := X) hT =
174 Set.range (nontrivialSchreierPairGenerator (X := X) hT) := by
175 ext z
176 constructor
177 · intro hz
178 rcases hz with ⟨t, ht, x, hz, hne⟩
179 refine ⟨⟨(⟨t, ht⟩, x), ?_⟩, ?_⟩
180 · simpa [hz] using hne
181 · simp only [nontrivialSchreierPairGenerator, hz]
182 · rintro ⟨p, rfl⟩
184 (X := X) hT p.1.1 p.1.2 p.2
186@[simp] theorem schreierGenerator_eq_one_of_mem {X : Type u} [DecidableEq X]
187 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
188 (hT : IsRightSchreierTransversal (X := X) L T)
189 {t : FreeGroup X} {x : X}
190 (htx : t * FreeGroup.of x ∈ T) :
191 schreierGenerator (X := X) hT t x = 1 := by
192 apply Subtype.ext
193 simp only [schreierGenerator, schreierRepresentative_eq_of_mem (X := X) hT htx, mul_inv_rev, mul_assoc,
194 mul_inv_cancel_left, mul_inv_cancel, OneMemClass.coe_one]
196@[simp] theorem schreierGenerator_eq_of_mul_mem {X : Type u} [DecidableEq X]
197 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
198 (hT : IsRightSchreierTransversal (X := X) L T)
199 {t : FreeGroup X} {x : X}
200 (htx : t * FreeGroup.of x ∈ L) :
201 schreierGenerator (X := X) hT t x = ⟨t * FreeGroup.of x, htx⟩ := by
202 apply Subtype.ext
203 simp only [schreierGenerator, schreierRepresentative_eq_one_of_mem (X := X) hT htx, inv_one, mul_one]
205theorem schreierGenerator_eq_one_iff {X : Type u} [DecidableEq X]
206 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
207 {hT : IsRightSchreierTransversal (X := X) L T}
208 {t : FreeGroup X} {x : X} :
209 schreierGenerator (X := X) hT t x = 1 ↔
210 ((schreierRepresentative (X := X) hT (t * FreeGroup.of x) : T) : FreeGroup X) =
211 t * FreeGroup.of x := by
212 constructor
213 · intro h
214 have hval : t * FreeGroup.of x *
215 (((schreierRepresentative (X := X) hT (t * FreeGroup.of x) : T) : FreeGroup X))⁻¹ = 1 := by
216 exact congrArg Subtype.val h
217 have hmul := congrArg
218 (fun g : FreeGroup X =>
219 g * ((schreierRepresentative (X := X) hT (t * FreeGroup.of x) : T) : FreeGroup X)) hval
220 simpa [mul_assoc] using hmul.symm
221 · intro hrep
222 apply Subtype.ext
223 simp only [schreierGenerator, hrep, mul_inv_rev, mul_assoc, mul_inv_cancel_left, mul_inv_cancel,
224 OneMemClass.coe_one]
227/-- Pointed discrete Reidemeister-Schreier: if `x^N` is the first positive power of a free
231 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} (x : X) {N : ℕ}
232 (hN : 0 < N)
233 (hpow : (FreeGroup.of x) ^ N ∈ L)
234 (hmin : ∀ m : ℕ, 0 < m → m < N → (FreeGroup.of x) ^ m ∉ L) :
235 ∃ T : Set (FreeGroup X), ∃ hT : IsRightSchreierTransversal (X := X) L T,
236 (FreeGroup.of x) ^ (N - 1) ∈ T ∧
237 schreierGenerator (X := X) hT ((FreeGroup.of x) ^ (N - 1)) x =
238 ⟨(FreeGroup.of x) ^ N, hpow⟩ := by
239 let T₀ : Set (FreeGroup X) := Set.range fun i : Fin N => (FreeGroup.of x) ^ (i : ℕ)
240 have hT₀ : IsRightPartialSchreierTransversal (X := X) L T₀ :=
242 (X := X) (L := L) x hN hmin
243 rcases exists_rightSchreierTransversal_of_partial (X := X) (L := L) hT₀ with
244 ⟨T, hsub, hT⟩
245 have hpred : (FreeGroup.of x) ^ (N - 1) ∈ T := by
246 apply hsub
247 exact ⟨⟨N - 1, Nat.pred_lt (Nat.ne_of_gt hN)⟩, rfl⟩
248 have hmul :
249 (FreeGroup.of x) ^ (N - 1) * FreeGroup.of x = (FreeGroup.of x) ^ N := by
250 calc
251 (FreeGroup.of x) ^ (N - 1) * FreeGroup.of x = (FreeGroup.of x) ^ ((N - 1).succ) := by
252 rw [pow_succ]
253 _ = (FreeGroup.of x) ^ N := by
254 simpa using congrArg (fun n : ℕ => (FreeGroup.of x) ^ n) (Nat.succ_pred_eq_of_pos hN)
255 have hmul_mem : (FreeGroup.of x) ^ (N - 1) * FreeGroup.of x ∈ L := by
256 rw [hmul]
257 exact hpow
258 refine ⟨T, hT, hpred, ?_⟩
259 calc
260 schreierGenerator (X := X) hT ((FreeGroup.of x) ^ (N - 1)) x =
261 ⟨(FreeGroup.of x) ^ (N - 1) * FreeGroup.of x, hmul_mem⟩ := by
262 exact schreierGenerator_eq_of_mul_mem (X := X) hT hmul_mem
263 _ = ⟨(FreeGroup.of x) ^ N, hpow⟩ := by
264 apply Subtype.ext
265 exact hmul
267theorem schreierRepresentative_eq_prefixParent_of_cancels {X : Type u} [DecidableEq X]
268 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
269 (hT : IsRightSchreierTransversal (X := X) L T)
270 {t : FreeGroup X} {x : X}
271 (ht : t ∈ T) (hw : FreeGroup.toWord t ≠ [])
272 (hlast : (FreeGroup.toWord t).getLast hw = (x, false)) :
273 schreierRepresentative (X := X) hT (t * FreeGroup.of x) =
274 ⟨FreeGroup.prefixParent t, prefixParent_mem_of_mem (X := X) hT ht⟩ := by
275 rw [Internal.FreeGroupWord.FreeGroup.mul_of_eq_prefixParent_of_cancels t x hw hlast]
276 exact schreierRepresentative_eq_of_mem (X := X) hT (prefixParent_mem_of_mem (X := X) hT ht)
278theorem schreierRepresentative_eq_of_prefixParent_last_pos {X : Type u} [DecidableEq X]
279 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
280 (hT : IsRightSchreierTransversal (X := X) L T)
281 {t : FreeGroup X} (ht : t ∈ T) {x : X}
282 (hw : FreeGroup.toWord t ≠ [])
283 (hlast : (FreeGroup.toWord t).getLast hw = (x, true)) :
284 schreierRepresentative (X := X) hT (FreeGroup.prefixParent t * FreeGroup.of x) = ⟨t, ht⟩ := by
285 rw [Internal.FreeGroupWord.FreeGroup.prefixParent_mul_of_of_last_pos t x hw hlast]
286 exact schreierRepresentative_eq_of_mem (X := X) hT ht
288@[simp] theorem schreierGenerator_eq_one_of_cancels {X : Type u} [DecidableEq X]
289 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
290 (hT : IsRightSchreierTransversal (X := X) L T)
291 {t : FreeGroup X} {x : X}
292 (ht : t ∈ T) (hw : FreeGroup.toWord t ≠ [])
293 (hlast : (FreeGroup.toWord t).getLast hw = (x, false)) :
294 schreierGenerator (X := X) hT t x = 1 := by
295 apply schreierGenerator_eq_one_of_mem (X := X) hT
296 rw [Internal.FreeGroupWord.FreeGroup.mul_of_eq_prefixParent_of_cancels t x hw hlast]
297 exact prefixParent_mem_of_mem (X := X) hT ht
299@[simp] theorem schreierGenerator_eq_one_of_prefixParent_last_pos {X : Type u} [DecidableEq X]
300 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
301 (hT : IsRightSchreierTransversal (X := X) L T)
302 {t : FreeGroup X} (ht : t ∈ T) {x : X}
303 (hw : FreeGroup.toWord t ≠ [])
304 (hlast : (FreeGroup.toWord t).getLast hw = (x, true)) :
305 schreierGenerator (X := X) hT (FreeGroup.prefixParent t) x = 1 := by
306 apply schreierGenerator_eq_one_of_mem (X := X) hT
307 rw [Internal.FreeGroupWord.FreeGroup.prefixParent_mul_of_of_last_pos t x hw hlast]
308 exact ht
311end SchreierGenerators
313end ReidemeisterSchreier.Discrete.OpenSubgroups