Source: ProCGroups.ReidemeisterSchreier.FreeGroup.PrefixParent
1import Mathlib.GroupTheory.FreeGroup.Reduce
3/-!
4# Reidemeister Schreier / Free Group / Prefix Parent
6This module develops the signed-letter view of reduced free-group words,
7including cancellation at the last letter and the prefix-parent operation
8used to build Schreier prefix trees.
9-/
11namespace ReidemeisterSchreier
13/-- A signed generator letter in the word model of a free group. -/
14abbrev Internal.SignedLetter (X : Type u) := X × Bool
16namespace Internal.SignedLetter
18/-- The inverse signed letter. -/
19def inv {X : Type u} (y : Internal.SignedLetter X) : Internal.SignedLetter X :=
20 (y.1, !y.2)
22/-- Inverting a signed letter preserves its underlying generator. -/
23@[simp] theorem inv_fst {X : Type u} (y : Internal.SignedLetter X) : y.inv.1 = y.1 := rfl
24/-- Inverting a signed letter reverses its orientation. -/
25@[simp] theorem inv_snd {X : Type u} (y : Internal.SignedLetter X) : y.inv.2 = !y.2 := rfl
26/-- Inversion of signed letters is involutive. -/
27@[simp] theorem inv_inv {X : Type u} (y : Internal.SignedLetter X) : y.inv.inv = y := by
28 cases y
29 simp only [inv, Bool.not_not]
31end Internal.SignedLetter
33namespace Internal.FreeGroupWord
35/-- The inverse-reversal of a nonempty word starts with the inverse of its last letter. -/
36theorem FreeGroup.invRev_eq_getLast_append_dropLast {X : Type u}
37 (w : List (X × Bool)) (hw : w ≠ []) :
38 FreeGroup.invRev w =
39 [((w.getLast hw).1, ! (w.getLast hw).2)] ++ FreeGroup.invRev w.dropLast := by
40 refine (congrArg FreeGroup.invRev (List.dropLast_append_getLast hw)).symm.trans ?_
41 simp only [FreeGroup.invRev, List.map_append, List.map_dropLast, List.map_cons, List.map_nil,
42 List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append, List.cons_append]
44end Internal.FreeGroupWord
46/-- The last signed letter of the reduced word representing \(g\), if it is nonempty. -/
47def FreeGroup.lastLetter? {X : Type u} [DecidableEq X] (g : FreeGroup X) :
48 Option (Internal.SignedLetter X) :=
49 (FreeGroup.toWord g).getLast?
51namespace Internal.FreeGroupWord
53/--
54A reduced word has the specified last letter exactly when its last-letter option is that value.
55-/
56theorem FreeGroup.lastLetter?_eq_some_iff {X : Type u} [DecidableEq X]
57 {g : FreeGroup X} {y : Internal.SignedLetter X} :
58 FreeGroup.lastLetter? g = some y ↔
59 ∃ hw : FreeGroup.toWord g ≠ [], (FreeGroup.toWord g).getLast hw = y := by
60 constructor
61 · intro h
62 have hy : y ∈ (FreeGroup.toWord g).getLast? := by
63 simpa [FreeGroup.lastLetter?, h]
64 rcases List.mem_getLast?_eq_getLast hy with ⟨hw, hyw⟩
65 exact ⟨hw, hyw.symm⟩
66 · rintro ⟨hw, hlast⟩
67 rw [FreeGroup.lastLetter?, List.getLast?_eq_getLast_of_ne_nil hw, hlast]
69/-- Multiplication by a positive generator appends its letter when no cancellation occurs. -/
70theorem FreeGroup.toWord_mul_of_of_not_cancels {X : Type u} [DecidableEq X]
71 (t : FreeGroup X) (x : X)
72 (hcancel : ¬ ∃ hw : FreeGroup.toWord t ≠ [], (FreeGroup.toWord t).getLast hw = (x, false)) :
73 FreeGroup.toWord (t * FreeGroup.of x) = FreeGroup.toWord t ++ [(x, true)] := by
74 rw [FreeGroup.toWord_mul, FreeGroup.toWord_of]
75 have hred : FreeGroup.IsReduced (FreeGroup.toWord t ++ [(x, true)]) := by
76 refine List.IsChain.append (FreeGroup.isReduced_toWord (x := t)) ?_ ?_
77 · simp only [List.IsChain.singleton]
78 · intro a ha b hb hab
79 have hb' : (x, true) = b := by simpa using hb
80 cases hb'
81 rcases List.mem_getLast?_eq_getLast ha with ⟨hw, rfl⟩
82 have hne : (FreeGroup.toWord t).getLast hw ≠ (x, false) := by
83 intro hlast
84 exact hcancel ⟨hw, hlast⟩
85 dsimp at hab hne ⊢
86 cases h2 : ((FreeGroup.toWord t).getLast hw).2 with
87 | false =>
88 exfalso
89 apply hne
90 apply Prod.ext
91 · exact hab
92 · simpa using h2
93 | true => rfl
94 exact hred.reduce_eq
96/-- If the last letter is the inverse of a generator, multiplying by that generator removes it. -/
97theorem FreeGroup.mul_of_of_eq_mk_dropLast_of_cancels {X : Type u} [DecidableEq X]
98 (t : FreeGroup X) (x : X) (hw : FreeGroup.toWord t ≠ [])
99 (hlast : (FreeGroup.toWord t).getLast hw = (x, false)) :
100 t * FreeGroup.of x = FreeGroup.mk ((FreeGroup.toWord t).dropLast) := by
101 rw [← FreeGroup.mk_toWord (x := t)]
102 simp only [FreeGroup.toWord_mk, FreeGroup.reduce_toWord]
103 rw [FreeGroup.of, FreeGroup.mul_mk]
104 have ht :
105 FreeGroup.toWord t =
106 (FreeGroup.toWord t).dropLast ++ [(FreeGroup.toWord t).getLast hw] := by
107 simpa using (List.dropLast_append_getLast hw).symm
108 rw [ht, hlast]
109 simp only [List.append_assoc, List.cons_append, List.nil_append, ne_eq, List.cons_ne_self,
110 not_false_eq_true, List.dropLast_append_of_ne_nil, List.dropLast_singleton, List.append_nil]
111 exact Quot.sound (show FreeGroup.Red.Step
112 ((FreeGroup.toWord t).dropLast ++ (x, false) :: (x, true) :: [])
113 ((FreeGroup.toWord t).dropLast) from by
114 simpa using (show FreeGroup.Red.Step
115 ((FreeGroup.toWord t).dropLast ++ (x, false) :: (x, true) :: [])
116 ((FreeGroup.toWord t).dropLast ++ []) from by constructor))
118/-- In the cancelling case, the reduced word of the product is the original word without its last letter. -/
119theorem FreeGroup.toWord_mul_of_of_cancels {X : Type u} [DecidableEq X]
120 (t : FreeGroup X) (x : X) (hw : FreeGroup.toWord t ≠ [])
121 (hlast : (FreeGroup.toWord t).getLast hw = (x, false)) :
122 FreeGroup.toWord (t * FreeGroup.of x) = (FreeGroup.toWord t).dropLast := by
123 rw [FreeGroup.mul_of_of_eq_mk_dropLast_of_cancels t x hw hlast, FreeGroup.toWord_mk]
124 have hred : FreeGroup.IsReduced ((FreeGroup.toWord t).dropLast) := by
125 exact (FreeGroup.isReduced_toWord (x := t)).dropLast
126 simpa using hred.reduce_eq
128/--
129Appending a reduced signed letter to a reduced word stays reduced unless the last letter is its
130inverse.
131-/
132theorem FreeGroup.toWord_mul_mk_singleton_of_not_cancels {X : Type u} [DecidableEq X]
133 (t : FreeGroup X) (y : X × Bool)
134 (hcancel :
135 ¬ ∃ hw : FreeGroup.toWord t ≠ [],
136 (FreeGroup.toWord t).getLast hw = (y.1, !y.2)) :
137 FreeGroup.toWord (t * FreeGroup.mk [y]) = FreeGroup.toWord t ++ [y] := by
138 rw [FreeGroup.toWord_mul, FreeGroup.toWord_mk]
139 have hred : FreeGroup.IsReduced (FreeGroup.toWord t ++ [y]) := by
140 refine List.IsChain.append (FreeGroup.isReduced_toWord (x := t)) ?_ ?_
141 · simp only [List.IsChain.singleton]
142 · intro a ha b hb hab
143 have hb' : y = b := by simpa using hb
144 cases hb'
145 rcases List.mem_getLast?_eq_getLast ha with ⟨hw, rfl⟩
146 have hne : (FreeGroup.toWord t).getLast hw ≠ (y.1, !y.2) := by
147 intro hlast
148 exact hcancel ⟨hw, hlast⟩
149 dsimp at hab hne ⊢
150 cases h2 : ((FreeGroup.toWord t).getLast hw).2 with
151 | false =>
152 cases y with
153 | mk x b =>
154 cases b with
155 | false => rfl
156 | true =>
157 exfalso
158 apply hne
159 apply Prod.ext
160 · exact hab
161 · simpa using h2
162 | true =>
163 cases y with
164 | mk x b =>
165 cases b with
166 | false =>
167 exfalso
168 apply hne
169 apply Prod.ext
170 · exact hab
171 · simp only [h2, Bool.not_false]
172 | true => rfl
173 exact hred.reduce_eq
175/--
176Cancelling a reduced signed letter on the right amounts to deleting the last letter in the word
177model.
178-/
179theorem FreeGroup.mul_mk_singleton_eq_mk_dropLast_of_cancels {X : Type u} [DecidableEq X]
180 (t : FreeGroup X) (y : X × Bool) (hw : FreeGroup.toWord t ≠ [])
181 (hlast : (FreeGroup.toWord t).getLast hw = (y.1, !y.2)) :
182 t * FreeGroup.mk [y] = FreeGroup.mk ((FreeGroup.toWord t).dropLast) := by
183 rw [← FreeGroup.mk_toWord (x := t)]
184 simp only [FreeGroup.toWord_mk, FreeGroup.reduce_toWord]
185 have ht :
186 FreeGroup.toWord t =
187 (FreeGroup.toWord t).dropLast ++ [(FreeGroup.toWord t).getLast hw] := by
188 simpa using (List.dropLast_append_getLast hw).symm
189 rw [ht, hlast]
190 simp only [FreeGroup.mul_mk, List.append_assoc, List.cons_append, List.nil_append, ne_eq,
191 List.cons_ne_self, not_false_eq_true, List.dropLast_append_of_ne_nil,
192 List.dropLast_singleton, List.append_nil]
193 exact Quot.sound
194 (show FreeGroup.Red.Step
195 ((FreeGroup.toWord t).dropLast ++ (y.1, !y.2) :: y :: [])
196 ((FreeGroup.toWord t).dropLast) from by
197 simpa using
198 (show FreeGroup.Red.Step
199 ((FreeGroup.toWord t).dropLast ++ (y.1, !y.2) :: y :: [])
200 ((FreeGroup.toWord t).dropLast ++ []) from
201 FreeGroup.Red.Step.not_rev))
203/--
204The to word multiplication coset representative formula singleton of cancels sends a singleton
205basis element to the singleton basis element supported at the induced quotient image, with the
206prescribed coefficient in the Reidemeister--Schreier rewriting system.
207-/
208theorem FreeGroup.toWord_mul_mk_singleton_of_cancels {X : Type u} [DecidableEq X]
209 (t : FreeGroup X) (y : X × Bool) (hw : FreeGroup.toWord t ≠ [])
210 (hlast : (FreeGroup.toWord t).getLast hw = (y.1, !y.2)) :
211 FreeGroup.toWord (t * FreeGroup.mk [y]) = (FreeGroup.toWord t).dropLast := by
212 rw [FreeGroup.mul_mk_singleton_eq_mk_dropLast_of_cancels t y hw hlast, FreeGroup.toWord_mk]
213 have hred : FreeGroup.IsReduced ((FreeGroup.toWord t).dropLast) := by
214 exact (FreeGroup.isReduced_toWord (x := t)).dropLast
215 simpa using hred.reduce_eq
217/-- Unified signed-letter multiplication rule for reduced words. -/
218theorem FreeGroup.toWord_mul_singleton {X : Type u} [DecidableEq X]
219 (t : FreeGroup X) (y : Internal.SignedLetter X) :
220 FreeGroup.toWord (t * FreeGroup.mk [y]) =
221 if FreeGroup.lastLetter? t = some y.inv then
222 (FreeGroup.toWord t).dropLast
223 else
224 FreeGroup.toWord t ++ [y] := by
225 by_cases hlast? : FreeGroup.lastLetter? t = some y.inv
226 · rw [if_pos hlast?]
227 rcases (FreeGroup.lastLetter?_eq_some_iff (g := t) (y := y.inv)).1 hlast? with
228 ⟨hw, hlast⟩
229 simpa [Internal.SignedLetter.inv] using
230 FreeGroup.toWord_mul_mk_singleton_of_cancels t y hw hlast
231 · rw [if_neg hlast?]
232 have hcancel :
233 ¬ ∃ hw : FreeGroup.toWord t ≠ [],
234 (FreeGroup.toWord t).getLast hw = (y.1, !y.2) := by
235 intro h
236 exact hlast?
237 ((FreeGroup.lastLetter?_eq_some_iff (g := t) (y := y.inv)).2 (by
238 simpa [Internal.SignedLetter.inv] using h))
239 exact FreeGroup.toWord_mul_mk_singleton_of_not_cancels t y hcancel
241/--
242Positive generators are the positive signed-letter specialization of the word-multiplication
243formula for free groups.
244-/
245theorem FreeGroup.toWord_mul_of {X : Type u} [DecidableEq X]
246 (t : FreeGroup X) (x : X) :
247 FreeGroup.toWord (t * FreeGroup.of x) =
248 if FreeGroup.lastLetter? t = some ((x, false) : Internal.SignedLetter X) then
249 (FreeGroup.toWord t).dropLast
250 else
251 FreeGroup.toWord t ++ [(x, true)] := by
252 simpa [FreeGroup.of, Internal.SignedLetter.inv] using
253 (FreeGroup.toWord_mul_singleton t ((x, true) : Internal.SignedLetter X))
255end Internal.FreeGroupWord
257/-- The predecessor of a reduced word, obtained by deleting its last letter. -/
258def FreeGroup.prefixParent {X : Type u} [DecidableEq X] (t : FreeGroup X) : FreeGroup X :=
259 FreeGroup.mk ((FreeGroup.toWord t).dropLast)
261namespace Internal.FreeGroupWord
263/--
264Multiplication by a signed singleton either deletes the inverse last letter or appends the
265singleton to the reduced word.
266-/
267theorem FreeGroup.mul_mk_singleton_eq_ite_prefixParent {X : Type u} [DecidableEq X]
268 (t : FreeGroup X) (y : X × Bool) :
269 t * FreeGroup.mk [y] =
270 if _ : ∃ hw : FreeGroup.toWord t ≠ [],
271 (FreeGroup.toWord t).getLast hw = (y.1, !y.2)
272 then FreeGroup.prefixParent t
273 else FreeGroup.mk (FreeGroup.toWord t ++ [y]) := by
274 by_cases h : ∃ hw : FreeGroup.toWord t ≠ [],
275 (FreeGroup.toWord t).getLast hw = (y.1, !y.2)
276 · rcases h with ⟨hw, hlast⟩
277 rw [dif_pos ⟨hw, hlast⟩]
278 exact FreeGroup.mul_mk_singleton_eq_mk_dropLast_of_cancels t y hw hlast
279 · rw [dif_neg h]
280 calc
281 t * FreeGroup.mk [y] =
282 FreeGroup.mk (FreeGroup.toWord (t * FreeGroup.mk [y])) := by
283 exact (FreeGroup.mk_toWord (x := t * FreeGroup.mk [y])).symm
284 _ = FreeGroup.mk (FreeGroup.toWord t ++ [y]) := by
285 rw [FreeGroup.toWord_mul_mk_singleton_of_not_cancels t y h]
287/-- The reduced word of the prefix parent is obtained by dropping the final letter. -/
288@[simp] theorem FreeGroup.toWord_prefixParent {X : Type u} [DecidableEq X] (t : FreeGroup X) :
289 FreeGroup.toWord (FreeGroup.prefixParent t) = (FreeGroup.toWord t).dropLast := by
290 rw [FreeGroup.prefixParent, FreeGroup.toWord_mk]
291 have hred : FreeGroup.IsReduced ((FreeGroup.toWord t).dropLast) := by
292 exact (FreeGroup.isReduced_toWord (x := t)).dropLast
293 exact hred.reduce_eq
295/-- Taking the prefix parent strictly shortens a nontrivial reduced word. -/
296theorem FreeGroup.toWord_length_prefixParent_lt {X : Type u} [DecidableEq X]
297 {t : FreeGroup X} (ht : t ≠ 1) :
298 (FreeGroup.toWord (FreeGroup.prefixParent t)).length < (FreeGroup.toWord t).length := by
299 rw [FreeGroup.toWord_prefixParent, List.length_dropLast]
300 have hnonempty : FreeGroup.toWord t ≠ [] := by
301 exact mt (FreeGroup.toWord_eq_nil_iff.mp) ht
302 have hlen : 0 < (FreeGroup.toWord t).length := List.length_pos_iff_ne_nil.mpr hnonempty
303 simpa using Nat.pred_lt (Nat.ne_of_gt hlen)
305/-- The reduced-word length of the prefix parent is the predecessor of the original length. -/
306theorem FreeGroup.length_prefixParent_eq_pred {X : Type u} [DecidableEq X]
307 (t : FreeGroup X) :
308 (FreeGroup.toWord (FreeGroup.prefixParent t)).length =
309 (FreeGroup.toWord t).length - 1 := by
310 rw [FreeGroup.toWord_prefixParent, List.length_dropLast]
312/-- A word ending in a positive generator is reconstructed from its prefix parent by that generator. -/
313theorem FreeGroup.prefixParent_mul_of_of_last_pos {X : Type u} [DecidableEq X]
314 (t : FreeGroup X) (x : X) (hw : FreeGroup.toWord t ≠ [])
315 (hlast : (FreeGroup.toWord t).getLast hw = (x, true)) :
316 FreeGroup.prefixParent t * FreeGroup.of x = t := by
317 apply FreeGroup.toWord_injective
318 rw [FreeGroup.toWord_mul, FreeGroup.toWord_of]
319 have ht : FreeGroup.toWord t =
320 (FreeGroup.toWord t).dropLast ++ [(FreeGroup.toWord t).getLast hw] := by
321 simpa using (List.dropLast_append_getLast hw).symm
322 have hword : FreeGroup.toWord (FreeGroup.prefixParent t) ++ [(x, true)] = FreeGroup.toWord t := by
323 calc
324 FreeGroup.toWord (FreeGroup.prefixParent t) ++ [(x, true)]
325 = (FreeGroup.toWord t).dropLast ++ [(x, true)] := by rw [FreeGroup.toWord_prefixParent]
326 _ = FreeGroup.toWord t := by
327 have ht' := ht.symm
328 rw [hlast] at ht'
329 exact ht'
330 have hred : FreeGroup.IsReduced (FreeGroup.toWord (FreeGroup.prefixParent t) ++ [(x, true)]) := by
331 rw [hword]
332 exact FreeGroup.isReduced_toWord (x := t)
333 exact hred.reduce_eq.trans hword
335/-- Multiplying the prefix parent by the final signed letter reconstructs the original word. -/
336theorem FreeGroup.prefixParent_mul_mk_singleton_of_last {X : Type u} [DecidableEq X]
337 (t : FreeGroup X) (y : X × Bool) (hw : FreeGroup.toWord t ≠ [])
338 (hlast : (FreeGroup.toWord t).getLast hw = y) :
339 FreeGroup.prefixParent t * FreeGroup.mk [y] = t := by
340 apply FreeGroup.toWord_injective
341 rw [FreeGroup.toWord_mul, FreeGroup.toWord_prefixParent, FreeGroup.toWord_mk]
342 have ht :
343 FreeGroup.toWord t =
344 (FreeGroup.toWord t).dropLast ++ [(FreeGroup.toWord t).getLast hw] := by
345 simpa using (List.dropLast_append_getLast hw).symm
346 have hword : (FreeGroup.toWord t).dropLast ++ [y] = FreeGroup.toWord t := by
347 have ht' := ht.symm
348 rw [hlast] at ht'
349 exact ht'
350 have hred : FreeGroup.IsReduced ((FreeGroup.toWord t).dropLast ++ [y]) := by
351 rw [hword]
352 exact FreeGroup.isReduced_toWord (x := t)
353 exact hred.reduce_eq.trans hword
355/-- A last-letter option supplies the signed letter that reconstructs the word from its prefix parent. -/
356theorem FreeGroup.prefixParent_mul_lastLetter {X : Type u} [DecidableEq X]
357 {t : FreeGroup X} {y : Internal.SignedLetter X}
358 (h : FreeGroup.lastLetter? t = some y) :
359 FreeGroup.prefixParent t * FreeGroup.mk [y] = t := by
360 rcases (FreeGroup.lastLetter?_eq_some_iff (g := t) (y := y)).1 h with
361 ⟨hw, hlast⟩
362 exact FreeGroup.prefixParent_mul_mk_singleton_of_last t y hw hlast
364end Internal.FreeGroupWord
366/-- The parent edge data obtained by deleting the last signed letter of a nontrivial word. -/
367structure FreeGroup.PrefixParentEdge {X : Type u} [DecidableEq X] (t : FreeGroup X) where
368 /-- The free-group element represented by the reduced word with its last letter removed. -/
369 parent : FreeGroup X
370 /-- The last signed letter removed from the reduced word. -/
371 letter : Internal.SignedLetter X
372 /-- The stored parent agrees with the canonical prefix-parent operation. -/
373 parent_eq : parent = FreeGroup.prefixParent t
374 /-- Multiplying the parent by the last letter reconstructs the original element. -/
375 rebuild : parent * FreeGroup.mk [letter] = t
377/-- A nontrivial reduced word has a canonical parent edge. -/
378def FreeGroup.prefixParentEdgeOfNeOne {X : Type u} [DecidableEq X]
379 {t : FreeGroup X} (ht : t ≠ 1) : FreeGroup.PrefixParentEdge t := by
380 have hw : FreeGroup.toWord t ≠ [] := by
381 exact mt (FreeGroup.toWord_eq_nil_iff.mp) ht
382 refine
383 { parent := FreeGroup.prefixParent t
384 letter := (FreeGroup.toWord t).getLast hw
385 parent_eq := rfl
386 rebuild := ?_ }
387 exact Internal.FreeGroupWord.FreeGroup.prefixParent_mul_mk_singleton_of_last t
388 ((FreeGroup.toWord t).getLast hw) hw rfl
390/-- The canonical edge of a nontrivial word stores its prefix parent. -/
391@[simp] theorem FreeGroup.prefixParentEdgeOfNeOne_parent {X : Type u} [DecidableEq X]
392 {t : FreeGroup X} (ht : t ≠ 1) :
393 (FreeGroup.prefixParentEdgeOfNeOne (X := X) ht).parent =
394 FreeGroup.prefixParent t :=
395 rfl
397/-- The letter stored by the canonical parent edge is the word's last letter. -/
398theorem FreeGroup.prefixParentEdgeOfNeOne_lastLetter? {X : Type u} [DecidableEq X]
399 {t : FreeGroup X} (ht : t ≠ 1) :
400 FreeGroup.lastLetter? t =
401 some (FreeGroup.prefixParentEdgeOfNeOne (X := X) ht).letter := by
402 have hw : FreeGroup.toWord t ≠ [] := by
403 exact mt (FreeGroup.toWord_eq_nil_iff.mp) ht
404 simp only [lastLetter?, List.getLast?_eq_getLast_of_ne_nil hw, prefixParentEdgeOfNeOne]
406/-- Nontrivial words decompose as parent times their last signed letter. -/
407theorem FreeGroup.exists_prefixParent_mul_lastLetter_of_ne_one
408 {X : Type u} [DecidableEq X] {t : FreeGroup X} (ht : t ≠ 1) :
409 ∃ y : Internal.SignedLetter X,
410 FreeGroup.lastLetter? t = some y ∧
411 FreeGroup.prefixParent t * FreeGroup.mk [y] = t := by
412 have hw : FreeGroup.toWord t ≠ [] := by
413 exact mt (FreeGroup.toWord_eq_nil_iff.mp) ht
414 refine ⟨(FreeGroup.toWord t).getLast hw, ?_, ?_⟩
415 · rw [FreeGroup.lastLetter?, List.getLast?_eq_getLast_of_ne_nil hw]
416 · exact Internal.FreeGroupWord.FreeGroup.prefixParent_mul_mk_singleton_of_last t
417 ((FreeGroup.toWord t).getLast hw) hw rfl
419/-- The last letter of a nontrivial word is either positive or negative, with the corresponding parent formula. -/
420theorem FreeGroup.lastLetter_cases_of_ne_one {X : Type u} [DecidableEq X]
421 {t : FreeGroup X} (ht : t ≠ 1) :
422 ∃ x : X,
423 (∃ hw : FreeGroup.toWord t ≠ [],
424 (FreeGroup.toWord t).getLast hw = (x, true) ∧
425 FreeGroup.prefixParent t * FreeGroup.of x = t) ∨
426 (∃ hw : FreeGroup.toWord t ≠ [],
427 (FreeGroup.toWord t).getLast hw = (x, false) ∧
428 t * FreeGroup.of x = FreeGroup.prefixParent t) := by
429 have hw : FreeGroup.toWord t ≠ [] := by
430 exact mt (FreeGroup.toWord_eq_nil_iff.mp) ht
431 rcases hlast : (FreeGroup.toWord t).getLast hw with ⟨x, b⟩
432 cases b with
433 | false =>
434 refine ⟨x, Or.inr ⟨hw, hlast, ?_⟩⟩
435 simpa [FreeGroup.prefixParent] using
436 Internal.FreeGroupWord.FreeGroup.mul_of_of_eq_mk_dropLast_of_cancels t x hw hlast
437 | true =>
438 refine ⟨x, Or.inl ⟨hw, hlast, ?_⟩⟩
439 exact Internal.FreeGroupWord.FreeGroup.prefixParent_mul_of_of_last_pos t x hw hlast
441namespace Internal.FreeGroupWord
443/-- Multiplication by a generator cancelling the final negative letter gives the prefix parent. -/
444theorem FreeGroup.mul_of_eq_prefixParent_of_cancels {X : Type u} [DecidableEq X]
445 (t : FreeGroup X) (x : X) (hw : FreeGroup.toWord t ≠ [])
446 (hlast : (FreeGroup.toWord t).getLast hw = (x, false)) :
447 t * FreeGroup.of x = FreeGroup.prefixParent t := by
448 simpa [FreeGroup.prefixParent] using
449 FreeGroup.mul_of_of_eq_mk_dropLast_of_cancels t x hw hlast
451end Internal.FreeGroupWord
453end ReidemeisterSchreier