Yamaguchi Lean 4 Library
ReidemeisterSchreier/Discrete/OpenSubgroups/Transversals.lean
ReidemeisterSchreier/Discrete/OpenSubgroups/Transversals/Source

ReidemeisterSchreier/Discrete/OpenSubgroups/Transversals.lean

1import Mathlib.GroupTheory.Schreier
2import ReidemeisterSchreier.Discrete.OpenSubgroups.Words.Basic
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ReidemeisterSchreier/Discrete/OpenSubgroups/Transversals.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Discrete open-subgroup Schreier API
15Schreier transversals, representatives, generators, prefix trees, bases, and rank formulas for finite-index subgroups of free groups.
16-/
18namespace ReidemeisterSchreier.Discrete.OpenSubgroups
20section RightSchreierTransversals
22open scoped Pointwise
23open FreeGroup
25/-- A right Schreier transversal is a right transversal containing every initial segment of each of
26its elements. -/
27def IsRightSchreierTransversal {X : Type u} [DecidableEq X]
28 (L : Subgroup (FreeGroup X)) (T : Set (FreeGroup X)) : Prop :=
29 Subgroup.IsComplement (L : Set (FreeGroup X)) T ∧
30 (1 : FreeGroup X) ∈ T ∧
31 ∀ ⦃t : FreeGroup X⦄, t ∈ T → freeGroupInitialSegments t ⊆ T
33/-- A right partial Schreier transversal is prefix-closed, contains `1`, and meets each right
34coset in at most one element. -/
35def IsRightPartialSchreierTransversal {X : Type u} [DecidableEq X]
36 (L : Subgroup (FreeGroup X)) (T : Set (FreeGroup X)) : Prop :=
37 (1 : FreeGroup X) ∈ T ∧
38 (∀ ⦃t : FreeGroup X⦄, t ∈ T → freeGroupInitialSegments t ⊆ T) ∧
39 ∀ ⦃a b : FreeGroup X⦄, a ∈ T → b ∈ T →
40 (Quotient.mk'' a : Quotient (QuotientGroup.rightRel L)) =
41 Quotient.mk'' b → a = b
43theorem IsRightSchreierTransversal.isComplement {X : Type u} [DecidableEq X]
44 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
45 (hT : IsRightSchreierTransversal (X := X) L T) :
46 Subgroup.IsComplement (L : Set (FreeGroup X)) T :=
47 hT.1
49theorem IsRightSchreierTransversal.one_mem {X : Type u} [DecidableEq X]
50 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
51 (hT : IsRightSchreierTransversal (X := X) L T) :
52 (1 : FreeGroup X) ∈ T :=
53 hT.2.1
55theorem IsRightSchreierTransversal.prefix_closed {X : Type u} [DecidableEq X]
56 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
57 (hT : IsRightSchreierTransversal (X := X) L T)
58 {t : FreeGroup X} (ht : t ∈ T) :
60 hT.2.2 ht
62theorem IsRightPartialSchreierTransversal.one_mem {X : Type u} [DecidableEq X]
63 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
65 (1 : FreeGroup X) ∈ T :=
66 hT.1
68theorem IsRightPartialSchreierTransversal.prefix_closed {X : Type u} [DecidableEq X]
69 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
71 {t : FreeGroup X} (ht : t ∈ T) :
73 hT.2.1 ht
75theorem IsRightPartialSchreierTransversal.eq_of_rightQuotient_eq
76 {X : Type u} [DecidableEq X]
77 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
79 {a b : FreeGroup X} (ha : a ∈ T) (hb : b ∈ T)
80 (hEq :
81 (Quotient.mk'' a : Quotient (QuotientGroup.rightRel L)) =
82 Quotient.mk'' b) :
83 a = b :=
84 hT.2.2 ha hb hEq
86theorem prefixParent_mem_of_partial {X : Type u} [DecidableEq X]
87 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
89 {t : FreeGroup X} (ht : t ∈ T) :
90 FreeGroup.prefixParent t ∈ T := by
91 exact hT.2.1 ht ⟨(FreeGroup.toWord t).length - 1, Nat.sub_le (FreeGroup.toWord t).length 1, by
92 simp only [prefixParent, List.dropLast_eq_take]⟩
94/-- A nonempty chain of right partial Schreier transversals has a union that is again a right
95partial Schreier transversal. This is the chain-upper-bound step used in the Zorn construction. -/
97 {X : Type u} [DecidableEq X]
98 {L : Subgroup (FreeGroup X)} {c : Set (Set (FreeGroup X))}
99 (hcn : c.Nonempty)
100 (hc :
101 ∀ ⦃s⦄, s ∈ c → ∀ ⦃t⦄, t ∈ c → s ≠ t → s ⊆ t ∨ t ⊆ s)
102 (hcPartial :
103 ∀ ⦃s⦄, s ∈ c → IsRightPartialSchreierTransversal (X := X) L s) :
104 IsRightPartialSchreierTransversal (X := X) L (⋃₀ c) := by
105 refine ⟨?_, ?_, ?_⟩
106 · rcases hcn with ⟨s, hs⟩
107 exact Set.mem_sUnion_of_mem ((hcPartial hs).1) hs
108 · intro t ht u hu
109 rcases Set.mem_sUnion.mp ht with ⟨s, hs, hts⟩
110 exact Set.mem_sUnion.mpr ⟨s, hs, (hcPartial hs).2.1 hts hu⟩
111 · intro a b ha hb hab
112 rcases Set.mem_sUnion.mp ha with ⟨s, hs, has⟩
113 rcases Set.mem_sUnion.mp hb with ⟨t, ht, hbt⟩
114 by_cases hst : s = t
115 · subst hst
116 exact (hcPartial ht).2.2 has hbt hab
117 · rcases hc hs ht hst with hst' | hts'
118 · exact (hcPartial ht).2.2 (hst' has) hbt hab
119 · exact (hcPartial hs).2.2 has (hts' hbt) hab
121/-- Every right partial Schreier transversal extends to a full right Schreier transversal. -/
122theorem exists_rightSchreierTransversal_of_partial {X : Type u} [DecidableEq X]
123 {L : Subgroup (FreeGroup X)} {T₀ : Set (FreeGroup X)}
124 (hT₀ : IsRightPartialSchreierTransversal (X := X) L T₀) :
125 ∃ T : Set (FreeGroup X), T₀ ⊆ T ∧ IsRightSchreierTransversal (X := X) L T := by
126 classical
127 let S : Set (Set (FreeGroup X)) :=
128 {T | T₀ ⊆ T ∧ IsRightPartialSchreierTransversal (X := X) L T}
129 have hT₀S : T₀ ∈ S := by
130 exact ⟨Set.Subset.rfl, hT₀⟩
131 obtain ⟨T, hTS, hTmax⟩ :=
132 zorn_subset_nonempty S
133 (fun c hcS hc hcn => by
134 refine ⟨⋃₀ c, ?_, ?_⟩
135 · refine ⟨?_, ?_⟩
136 · intro t ht
137 rcases hcn with ⟨s, hs⟩
138 exact Set.mem_sUnion_of_mem ((hcS hs).1 ht) hs
140 (X := X) (L := L) hcn (fun {s} hs {t} ht hst => hc hs ht hst)
141 (fun {s} hs => (hcS hs).2)
142 · intro s hs
143 exact Set.subset_sUnion_of_mem hs)
144 T₀ hT₀S
145 have hTpartial : IsRightPartialSchreierTransversal (X := X) L T := hTmax.prop.2
146 have hTcover :
147 ∀ g : FreeGroup X,
148 ∃ t ∈ T,
149 (Quotient.mk'' t : Quotient (QuotientGroup.rightRel L)) = Quotient.mk'' g := by
150 intro g
151 by_contra hnog
152 let Missing : FreeGroup X → Prop := fun w =>
153 ∀ t ∈ T,
154 (Quotient.mk'' t : Quotient (QuotientGroup.rightRel L)) ≠ Quotient.mk'' w
155 have hmissing : Missing g := by
156 intro t ht hEq
157 exact hnog ⟨t, ht, hEq⟩
158 let P : ℕ → Prop := fun n =>
159 ∃ w : FreeGroup X, Missing w ∧ (FreeGroup.toWord w).length = n
160 have hP : ∃ n, P n := ⟨(FreeGroup.toWord g).length, g, hmissing, rfl⟩
161 let n := Nat.find hP
162 obtain ⟨w, hwmiss, hwlen⟩ := Nat.find_spec hP
163 have hmin : ∀ u : FreeGroup X, Missing u → n ≤ (FreeGroup.toWord u).length := by
164 intro u hu
165 exact Nat.find_min' hP ⟨u, hu, rfl⟩
166 have hw1 : w ≠ 1 := by
167 intro hw1
168 exact hwmiss 1 hTpartial.1 (by simp only [hw1])
169 have hwword : FreeGroup.toWord w ≠ [] := by
170 exact mt (FreeGroup.toWord_eq_nil_iff.mp) hw1
171 let y : X × Bool := (FreeGroup.toWord w).getLast hwword
172 let u : FreeGroup X := FreeGroup.prefixParent w
173 have huWitness :
174 ∃ t ∈ T,
175 (Quotient.mk'' t : Quotient (QuotientGroup.rightRel L)) = Quotient.mk'' u := by
176 by_contra hu
177 have humiss : Missing u := by
178 intro t ht hEq
179 exact hu ⟨t, ht, hEq⟩
180 have hlt : (FreeGroup.toWord u).length < n := by
181 simpa [u, n, hwlen] using
182 Internal.FreeGroupWord.FreeGroup.toWord_length_prefixParent_lt (t := w) hw1
183 exact (Nat.not_lt_of_ge (hmin u humiss)) hlt
184 obtain ⟨t, htT, htq⟩ := huWitness
185 let z : FreeGroup X := t * FreeGroup.mk [y]
186 have hzq :
187 (Quotient.mk'' z : Quotient (QuotientGroup.rightRel L)) = Quotient.mk'' w := by
188 apply Quotient.sound'
189 have hrel : QuotientGroup.rightRel L t u := Quotient.exact' htq
190 rw [QuotientGroup.rightRel_apply] at hrel ⊢
191 have hwrep :
192 u * FreeGroup.mk [y] = w := by
193 exact Internal.FreeGroupWord.FreeGroup.prefixParent_mul_mk_singleton_of_last
194 w y hwword (by rfl)
195 have hzw : w * z⁻¹ = u * t⁻¹ := by
196 have hcancelWord :
197 FreeGroup.mk [y] * FreeGroup.mk (FreeGroup.invRev [y]) = (1 : FreeGroup X) := by
198 rw [← FreeGroup.inv_mk (L := [y])]
199 exact mul_inv_cancel (FreeGroup.mk [y])
200 have hcancelWord' :
201 FreeGroup.mk (y :: FreeGroup.invRev [y]) = (1 : FreeGroup X) := by
202 simpa using hcancelWord
203 have htail :
204 FreeGroup.mk [y] * (FreeGroup.mk (FreeGroup.invRev [y]) * t⁻¹) =
205 FreeGroup.mk (y :: FreeGroup.invRev [y]) * t⁻¹ := by
206 calc
207 FreeGroup.mk [y] * (FreeGroup.mk (FreeGroup.invRev [y]) * t⁻¹)
208 = (FreeGroup.mk [y] * FreeGroup.mk (FreeGroup.invRev [y])) * t⁻¹ := by
209 rw [mul_assoc]
210 _ = FreeGroup.mk (y :: FreeGroup.invRev [y]) * t⁻¹ := by
211 rw [FreeGroup.mul_mk]
212 rfl
213 calc
214 w * z⁻¹ = (u * FreeGroup.mk [y]) * z⁻¹ := by rw [hwrep]
215 _ = (u * FreeGroup.mk [y]) * (t * FreeGroup.mk [y])⁻¹ := by rfl
216 _ = (u * FreeGroup.mk [y]) * (FreeGroup.mk (FreeGroup.invRev [y]) * t⁻¹) := by
217 simp only [mul_inv_rev, FreeGroup.inv_mk]
218 _ = u * (FreeGroup.mk [y] * (FreeGroup.mk (FreeGroup.invRev [y]) * t⁻¹)) := by
219 rw [← mul_assoc, ← mul_assoc, mul_assoc]
220 _ = u * (FreeGroup.mk (y :: FreeGroup.invRev [y]) * t⁻¹) := by
221 exact congrArg (fun x => u * x) htail
222 _ = u * (1 * t⁻¹) := by rw [hcancelWord']
223 _ = u * t⁻¹ := by simp only [one_mul]
224 simpa [hzw] using hrel
225 by_cases hcancel :
226 ∃ hw' : FreeGroup.toWord t ≠ [],
227 (FreeGroup.toWord t).getLast hw' = (y.1, !y.2)
228 · rcases hcancel with ⟨hw', hlast'⟩
229 have hzEqPrefix : z = FreeGroup.prefixParent t := by
230 simpa [z, FreeGroup.prefixParent] using
231 Internal.FreeGroupWord.FreeGroup.mul_mk_singleton_eq_mk_dropLast_of_cancels
232 t y hw' hlast'
233 have hzT : z ∈ T := by
234 simpa [hzEqPrefix] using prefixParent_mem_of_partial (X := X) (L := L) hTpartial htT
235 exact hwmiss z hzT hzq
236 · have hzWord : FreeGroup.toWord z = FreeGroup.toWord t ++ [y] :=
237 Internal.FreeGroupWord.FreeGroup.toWord_mul_mk_singleton_of_not_cancels t y hcancel
238 let U : Set (FreeGroup X) := Set.insert z T
239 have hzPrefix : freeGroupInitialSegments z ⊆ U := by
240 intro v hv
241 rcases hv with ⟨m, hm, rfl⟩
242 have hlenz : (FreeGroup.toWord z).length = (FreeGroup.toWord t).length + 1 := by
243 rw [hzWord]
244 simp only [List.length_append, List.length_cons, List.length_nil, zero_add]
245 have hm' : m ≤ (FreeGroup.toWord t).length + 1 := by
246 simpa [hlenz] using hm
247 rcases Nat.eq_or_lt_of_le hm' with hmEq | hmLt
248 · left
249 have hmz : m = (FreeGroup.toWord z).length := by
250 simpa [hlenz] using hmEq
251 have htake : List.take m (FreeGroup.toWord z) = FreeGroup.toWord z := by
252 rw [hmz, List.take_length]
253 rw [htake]
254 exact FreeGroup.mk_toWord (x := z)
255 · right
256 have hmle : m ≤ (FreeGroup.toWord t).length := Nat.lt_succ_iff.mp hmLt
257 have htake : List.take m (FreeGroup.toWord z) = List.take m (FreeGroup.toWord t) := by
258 rw [hzWord, List.take_append_of_le_length hmle]
259 rw [htake]
260 exact hTpartial.2.1 htT ⟨m, hmle, rfl⟩
261 have hUin : U ∈ S := by
262 refine ⟨?_, ?_⟩
263 · intro s hs
264 exact Or.inr (hTmax.prop.1 hs)
265 · refine ⟨Or.inr hTpartial.1, ?_, ?_⟩
266 · intro s hs
267 rcases hs with rfl | hsT
268 · exact hzPrefix
269 · intro v hv
270 exact Or.inr (hTpartial.2.1 hsT hv)
271 · intro a b ha hb hab
272 rcases ha with rfl | haT
273 · rcases hb with rfl | hbT
274 · rfl
275 · exfalso
276 exact hwmiss b hbT (hab.symm.trans hzq)
277 · rcases hb with rfl | hbT
278 · exfalso
279 exact hwmiss a haT (hab.trans hzq)
280 · exact hTpartial.2.2 haT hbT hab
281 have hTU : T = U := hTmax.eq_of_subset hUin (by intro s hs; exact Or.inr hs)
282 have hzT : z ∈ T := by
283 have hzU : z ∈ U := by
284 change z ∈ Set.insert z T
285 exact Set.mem_insert z T
286 exact hTU.symm ▸ hzU
287 exact hwmiss z hzT hzq
288 refine ⟨T, hTmax.prop.1, ?_⟩
289 refine ⟨?_, hTpartial.1, hTpartial.2.1⟩
290 rw [Subgroup.isComplement_iff_existsUnique_mul_inv_mem]
291 intro g
292 rcases hTcover g with ⟨t, htT, htq⟩
293 refine ⟨⟨t, htT⟩, ?_, ?_⟩
294 · have hrel : QuotientGroup.rightRel L t g := Quotient.exact' htq
295 simpa [QuotientGroup.rightRel_apply] using hrel
296 · intro t' hmem
297 apply Subtype.ext
298 apply hTpartial.2.2 t'.2 htT
299 calc
300 (Quotient.mk'' (t' : FreeGroup X) :
301 Quotient (QuotientGroup.rightRel L)) =
302 Quotient.mk'' g := by
303 apply Quotient.sound'
304 rw [QuotientGroup.rightRel_apply]
305 simpa using hmem
306 _ = Quotient.mk'' t := htq.symm
308/-- Every subgroup of a free group admits a right Schreier transversal. -/
309theorem exists_rightSchreierTransversal {X : Type u} [DecidableEq X]
310 (L : Subgroup (FreeGroup X)) :
311 ∃ T : Set (FreeGroup X), IsRightSchreierTransversal (X := X) L T := by
312 let T₀ : Set (FreeGroup X) := {(1 : FreeGroup X)}
313 have hT₀ : IsRightPartialSchreierTransversal (X := X) L T₀ := by
314 refine ⟨by simp only [Set.mem_singleton_iff, T₀], ?_, ?_⟩
315 · intro t ht u hu
316 have ht1 : t = 1 := by
317 simpa [T₀] using ht
318 subst t
319 rcases hu with ⟨n, hn, hu⟩
320 have hn0 : n = 0 := Nat.eq_zero_of_le_zero (by simpa using hn)
321 subst hn0
322 simpa using hu
323 · intro a b ha hb _
324 have ha1 : a = 1 := by
325 simpa [T₀] using ha
326 have hb1 : b = 1 := by
327 simpa [T₀] using hb
328 subst a
329 subst b
330 rfl
331 rcases exists_rightSchreierTransversal_of_partial (X := X) (L := L) hT₀ with ⟨T, _, hT⟩
332 exact ⟨T, hT⟩
335 {L : Subgroup (FreeGroup X)} (x : X) {m n : ℕ} (hmn : m ≤ n)
336 (hEq :
337 (Quotient.mk'' ((FreeGroup.of x) ^ m) : Quotient (QuotientGroup.rightRel L)) =
338 Quotient.mk'' ((FreeGroup.of x) ^ n)) :
339 (FreeGroup.of x) ^ (n - m) ∈ L := by
340 have hrel : QuotientGroup.rightRel L ((FreeGroup.of x) ^ m) ((FreeGroup.of x) ^ n) :=
341 Quotient.exact' hEq
342 rw [QuotientGroup.rightRel_apply] at hrel
343 have hcalc :
344 (FreeGroup.of x) ^ n * (((FreeGroup.of x) ^ m)⁻¹) =
345 (FreeGroup.of x) ^ (n - m) := by
346 calc
347 (FreeGroup.of x) ^ n * (((FreeGroup.of x) ^ m)⁻¹)
348 = (FreeGroup.of x) ^ ((n - m) + m) * (((FreeGroup.of x) ^ m)⁻¹) := by
349 rw [Nat.sub_add_cancel hmn]
350 _ = (((FreeGroup.of x) ^ (n - m)) * (FreeGroup.of x) ^ m) *
351 (((FreeGroup.of x) ^ m)⁻¹) := by
352 rw [pow_add]
353 _ = (FreeGroup.of x) ^ (n - m) := by simp only [mul_assoc, mul_inv_cancel, mul_one]
354 exact hcalc ▸ hrel
357 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} (x : X) {N : ℕ}
358 (hN : 0 < N)
359 (hmin : ∀ m : ℕ, 0 < m → m < N → (FreeGroup.of x) ^ m ∉ L) :
361 (Set.range fun i : Fin N => (FreeGroup.of x) ^ (i : ℕ)) := by
362 refine ⟨?_, ?_, ?_⟩
363 · exact ⟨⟨0, hN⟩, by simp only [pow_zero]⟩
364 · intro t ht u hu
365 rcases ht with ⟨i, rfl⟩
366 rcases hu with ⟨m, hm, rfl⟩
367 have hm' : m ≤ (i : ℕ) := by
368 simpa [FreeGroup.toWord_of_pow, List.length_replicate] using hm
369 refine ⟨⟨m, lt_of_le_of_lt hm' i.2⟩, ?_⟩
370 rw [FreeGroup.toWord_of_pow, List.take_replicate, min_eq_left hm',
371 ← FreeGroup.toWord_of_pow, FreeGroup.mk_toWord]
372 · intro a b ha hb hEq
373 rcases ha with ⟨i, rfl⟩
374 rcases hb with ⟨j, rfl⟩
375 have hij : (i : ℕ) = j := by
376 by_contra hij
377 rcases lt_or_gt_of_ne hij with hijlt | hjilt
378 · have hmem : (FreeGroup.of x) ^ ((j : ℕ) - i) ∈ L :=
380 (Nat.le_of_lt hijlt) hEq
381 exact hmin ((j : ℕ) - i) (Nat.sub_pos_of_lt hijlt)
382 (lt_of_le_of_lt (Nat.sub_le _ _) j.2) hmem
383 · have hmem : (FreeGroup.of x) ^ ((i : ℕ) - j) ∈ L :=
385 (Nat.le_of_lt hjilt) hEq.symm
386 exact hmin ((i : ℕ) - j) (Nat.sub_pos_of_lt hjilt)
387 (lt_of_le_of_lt (Nat.sub_le _ _) i.2) hmem
388 have hij' : i = j := Fin.ext hij
389 subst hij'
390 rfl
392/-- Right multiplication on right cosets, expressed as a left action via
393`g • [t] = [t * g⁻¹]`. This is the action naturally compatible with Schreier generators of the
394form `t x (\widetilde{t x})⁻¹`. -/
395instance rightCosetLeftMulActionByInverse {X : Type u} (L : Subgroup (FreeGroup X)) :
396 MulAction (FreeGroup X) (Quotient (QuotientGroup.rightRel L)) where
397 smul g :=
398 Quotient.map' (fun a => a * g⁻¹) fun a b hab => by
399 rw [QuotientGroup.rightRel_apply] at hab ⊢
400 simpa [mul_assoc] using hab
401 one_smul q := by
402 refine Quotient.inductionOn' q ?_
403 intro a
404 apply Quotient.sound'
405 rw [QuotientGroup.rightRel_apply]
406 simp only [inv_one, mul_one, mul_inv_cancel, one_mem]
407 mul_smul g h q := by
408 refine Quotient.inductionOn' q ?_
409 intro a
410 apply Quotient.sound'
411 rw [QuotientGroup.rightRel_apply]
412 simp only [mul_assoc, mul_inv_rev, inv_inv, inv_mul_cancel_left, mul_inv_cancel, one_mem]
414@[simp] theorem rightCosetLeftMulActionByInverse_mk_smul {X : Type u}
415 (L : Subgroup (FreeGroup X)) (g a : FreeGroup X) :
416 g • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel L)) =
417 Quotient.mk'' (a * g⁻¹) :=
418 rfl
420end RightSchreierTransversals
422end ReidemeisterSchreier.Discrete.OpenSubgroups