ReidemeisterSchreier.FreeGroup.PrefixParent
This module develops Reidemeister--Schreier rewriting, Schreier generators, finite quotient transversals, and presentation transformations.
import
- Mathlib.GroupTheory.FreeGroup.Reduce
abbrev SignedLetter (X : Type u) := X × BoolA signed generator letter in the word model of a free group.
def inv {X : Type u} (y : SignedLetter X) : SignedLetter X :=
(y.1, !y.2)The inverse signed letter.
@[simp] theorem inv_fst {X : Type u} (y : SignedLetter X) : y.inv.1 = y.1The prefix-parent identity follows from the reduced-word decomposition into a prefix and a last letter.
Show proof
rflProof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□@[simp] theorem inv_snd {X : Type u} (y : SignedLetter X) : y.inv.2 = !y.2The prefix-parent identity follows from the reduced-word decomposition into a prefix and a last letter.
Show proof
rflProof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□@[simp] theorem inv_inv {X : Type u} (y : SignedLetter X) : y.inv.inv = yThe prefix-parent identity follows from the reduced-word decomposition into a prefix and a last letter.
Show proof
by
cases y
simp only [inv, Bool.not_not]Proof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□theorem FreeGroup.invRev_eq_getLast_append_dropLast {X : Type u}
(w : List (X × Bool)) (hw : w ≠ []) :
FreeGroup.invRev w =
[((w.getLast hw).1, ! (w.getLast hw).2)] ++ FreeGroup.invRev w.dropLastThe prefix-parent identity follows from the reduced-word decomposition into a prefix and a last letter.
Show proof
by
refine (congrArg FreeGroup.invRev (List.dropLast_append_getLast hw)).symm.trans ?_
simp only [FreeGroup.invRev, List.map_append, List.map_dropLast, List.map_cons, List.map_nil,
List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append, List.cons_append]Proof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□def FreeGroup.lastLetter? {X : Type u} [DecidableEq X] (g : FreeGroup X) :
Option (SignedLetter X) :=
(FreeGroup.toWord g).getLast?The last signed letter of the reduced word representing \(g\), if it is nonempty.
theorem FreeGroup.lastLetter?_eq_some_iff {X : Type u} [DecidableEq X]
{g : FreeGroup X} {y : SignedLetter X} :
FreeGroup.lastLetter? g = some y ↔
∃ hw : FreeGroup.toWord g ≠ [], (FreeGroup.toWord g).getLast hw = yA reduced word has the specified last letter exactly when its last-letter option is that value.
Show proof
by
constructor
· intro h
have hy : y ∈ (FreeGroup.toWord g).getLast? := by
simpa [FreeGroup.lastLetter?, h]
rcases List.mem_getLast?_eq_getLast hy with ⟨hw, hyw⟩
exact ⟨hw, hyw.symm⟩
· rintro ⟨hw, hlast⟩
rw [FreeGroup.lastLetter?, List.getLast?_eq_getLast_of_ne_nil hw, hlast]Proof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□theorem FreeGroup.toWord_mul_of_of_not_cancels {X : Type u} [DecidableEq X]
(t : FreeGroup X) (x : X)
(hcancel : ¬ ∃ hw : FreeGroup.toWord t ≠ [], (FreeGroup.toWord t).getLast hw = (x, false)) :
FreeGroup.toWord (t * FreeGroup.of x) = FreeGroup.toWord t ++ [(x, true)]The prefix-parent identity follows from the reduced-word decomposition into a prefix and a last letter.
Show proof
by
rw [FreeGroup.toWord_mul, FreeGroup.toWord_of]
have hred : FreeGroup.IsReduced (FreeGroup.toWord t ++ [(x, true)]) := by
refine List.IsChain.append (FreeGroup.isReduced_toWord (x := t)) ?_ ?_
· simp only [List.IsChain.singleton]
· intro a ha b hb hab
have hb' : (x, true) = b := by simpa using hb
cases hb'
rcases List.mem_getLast?_eq_getLast ha with ⟨hw, rfl⟩
have hne : (FreeGroup.toWord t).getLast hw ≠ (x, false) := by
intro hlast
exact hcancel ⟨hw, hlast⟩
dsimp at hab hne ⊢
cases h2 : ((FreeGroup.toWord t).getLast hw).2 with
| false =>
exfalso
apply hne
apply Prod.ext
· exact hab
· simpa using h2
| true => rfl
exact hred.reduce_eqProof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□theorem FreeGroup.mul_of_of_eq_mk_dropLast_of_cancels {X : Type u} [DecidableEq X]
(t : FreeGroup X) (x : X) (hw : FreeGroup.toWord t ≠ [])
(hlast : (FreeGroup.toWord t).getLast hw = (x, false)) :
t * FreeGroup.of x = FreeGroup.mk ((FreeGroup.toWord t).dropLast)The prefix-parent identity follows from the reduced-word decomposition into a prefix and a last letter.
Show proof
by
rw [← FreeGroup.mk_toWord (x := t)]
simp only [FreeGroup.toWord_mk, FreeGroup.reduce_toWord]
rw [FreeGroup.of, FreeGroup.mul_mk]
have ht :
FreeGroup.toWord t =
(FreeGroup.toWord t).dropLast ++ [(FreeGroup.toWord t).getLast hw] := by
simpa using (List.dropLast_append_getLast hw).symm
rw [ht, hlast]
simp only [List.append_assoc, List.cons_append, List.nil_append, ne_eq, List.cons_ne_self,
not_false_eq_true, List.dropLast_append_of_ne_nil, List.dropLast_singleton, List.append_nil]
exact Quot.sound (show FreeGroup.Red.Step
((FreeGroup.toWord t).dropLast ++ (x, false) :: (x, true) :: [])
((FreeGroup.toWord t).dropLast) from by
simpa using (show FreeGroup.Red.Step
((FreeGroup.toWord t).dropLast ++ (x, false) :: (x, true) :: [])
((FreeGroup.toWord t).dropLast ++ []) from by constructor))Proof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□theorem FreeGroup.toWord_mul_of_of_cancels {X : Type u} [DecidableEq X]
(t : FreeGroup X) (x : X) (hw : FreeGroup.toWord t ≠ [])
(hlast : (FreeGroup.toWord t).getLast hw = (x, false)) :
FreeGroup.toWord (t * FreeGroup.of x) = (FreeGroup.toWord t).dropLastThe prefix-parent identity follows from the reduced-word decomposition into a prefix and a last letter.
Show proof
by
rw [FreeGroup.mul_of_of_eq_mk_dropLast_of_cancels t x hw hlast, FreeGroup.toWord_mk]
have hred : FreeGroup.IsReduced ((FreeGroup.toWord t).dropLast) := by
exact (FreeGroup.isReduced_toWord (x := t)).dropLast
simpa using hred.reduce_eqProof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□theorem FreeGroup.toWord_mul_mk_singleton_of_not_cancels {X : Type u} [DecidableEq X]
(t : FreeGroup X) (y : X × Bool)
(hcancel :
¬ ∃ hw : FreeGroup.toWord t ≠ [],
(FreeGroup.toWord t).getLast hw = (y.1, !y.2)) :
FreeGroup.toWord (t * FreeGroup.mk [y]) = FreeGroup.toWord t ++ [y]Appending a reduced signed letter to a reduced word stays reduced unless the last letter is its inverse.
Show proof
by
rw [FreeGroup.toWord_mul, FreeGroup.toWord_mk]
have hred : FreeGroup.IsReduced (FreeGroup.toWord t ++ [y]) := by
refine List.IsChain.append (FreeGroup.isReduced_toWord (x := t)) ?_ ?_
· simp only [List.IsChain.singleton]
· intro a ha b hb hab
have hb' : y = b := by simpa using hb
cases hb'
rcases List.mem_getLast?_eq_getLast ha with ⟨hw, rfl⟩
have hne : (FreeGroup.toWord t).getLast hw ≠ (y.1, !y.2) := by
intro hlast
exact hcancel ⟨hw, hlast⟩
dsimp at hab hne ⊢
cases h2 : ((FreeGroup.toWord t).getLast hw).2 with
| false =>
cases y with
| mk x b =>
cases b with
| false => rfl
| true =>
exfalso
apply hne
apply Prod.ext
· exact hab
· simpa using h2
| true =>
cases y with
| mk x b =>
cases b with
| false =>
exfalso
apply hne
apply Prod.ext
· exact hab
· simp only [h2, Bool.not_false]
| true => rfl
exact hred.reduce_eqProof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□theorem FreeGroup.mul_mk_singleton_eq_mk_dropLast_of_cancels {X : Type u} [DecidableEq X]
(t : FreeGroup X) (y : X × Bool) (hw : FreeGroup.toWord t ≠ [])
(hlast : (FreeGroup.toWord t).getLast hw = (y.1, !y.2)) :
t * FreeGroup.mk [y] = FreeGroup.mk ((FreeGroup.toWord t).dropLast)Cancelling a reduced signed letter on the right amounts to deleting the last letter in the word model.
Show proof
by
rw [← FreeGroup.mk_toWord (x := t)]
simp only [FreeGroup.toWord_mk, FreeGroup.reduce_toWord]
have ht :
FreeGroup.toWord t =
(FreeGroup.toWord t).dropLast ++ [(FreeGroup.toWord t).getLast hw] := by
simpa using (List.dropLast_append_getLast hw).symm
rw [ht, hlast]
simp only [FreeGroup.mul_mk, List.append_assoc, List.cons_append, List.nil_append, ne_eq,
List.cons_ne_self, not_false_eq_true, List.dropLast_append_of_ne_nil,
List.dropLast_singleton, List.append_nil]
exact Quot.sound
(show FreeGroup.Red.Step
((FreeGroup.toWord t).dropLast ++ (y.1, !y.2) :: y :: [])
((FreeGroup.toWord t).dropLast) from by
simpa using
(show FreeGroup.Red.Step
((FreeGroup.toWord t).dropLast ++ (y.1, !y.2) :: y :: [])
((FreeGroup.toWord t).dropLast ++ []) from
FreeGroup.Red.Step.not_rev))Proof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□theorem FreeGroup.toWord_mul_mk_singleton_of_cancels {X : Type u} [DecidableEq X]
(t : FreeGroup X) (y : X × Bool) (hw : FreeGroup.toWord t ≠ [])
(hlast : (FreeGroup.toWord t).getLast hw = (y.1, !y.2)) :
FreeGroup.toWord (t * FreeGroup.mk [y]) = (FreeGroup.toWord t).dropLastThe to word multiplication coset representative formula singleton of cancels sends a singleton basis element to the singleton basis element supported at the induced quotient image, with the prescribed coefficient in the Reidemeister--Schreier rewriting system.
Show proof
by
rw [FreeGroup.mul_mk_singleton_eq_mk_dropLast_of_cancels t y hw hlast, FreeGroup.toWord_mk]
have hred : FreeGroup.IsReduced ((FreeGroup.toWord t).dropLast) := by
exact (FreeGroup.isReduced_toWord (x := t)).dropLast
simpa using hred.reduce_eqProof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□theorem FreeGroup.toWord_mul_singleton {X : Type u} [DecidableEq X]
(t : FreeGroup X) (y : SignedLetter X) :
FreeGroup.toWord (t * FreeGroup.mk [y]) =
if FreeGroup.lastLetter? t = some y.inv then
(FreeGroup.toWord t).dropLast
else
FreeGroup.toWord t ++ [y]Unified signed-letter multiplication rule for reduced words.
Show proof
by
by_cases hlast? : FreeGroup.lastLetter? t = some y.inv
· rw [if_pos hlast?]
rcases (FreeGroup.lastLetter?_eq_some_iff (g := t) (y := y.inv)).1 hlast? with
⟨hw, hlast⟩
simpa [SignedLetter.inv] using
FreeGroup.toWord_mul_mk_singleton_of_cancels t y hw hlast
· rw [if_neg hlast?]
have hcancel :
¬ ∃ hw : FreeGroup.toWord t ≠ [],
(FreeGroup.toWord t).getLast hw = (y.1, !y.2) := by
intro h
exact hlast?
((FreeGroup.lastLetter?_eq_some_iff (g := t) (y := y.inv)).2 (by
simpa [SignedLetter.inv] using h))
exact FreeGroup.toWord_mul_mk_singleton_of_not_cancels t y hcancelProof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□theorem FreeGroup.toWord_mul_of {X : Type u} [DecidableEq X]
(t : FreeGroup X) (x : X) :
FreeGroup.toWord (t * FreeGroup.of x) =
if FreeGroup.lastLetter? t = some ((x, false) : SignedLetter X) then
(FreeGroup.toWord t).dropLast
else
FreeGroup.toWord t ++ [(x, true)]Positive generators are the positive signed-letter specialization of the word-multiplication formula for free groups.
Show proof
by
simpa [FreeGroup.of, SignedLetter.inv] using
(FreeGroup.toWord_mul_singleton t ((x, true) : SignedLetter X))Proof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□def FreeGroup.prefixParent {X : Type u} [DecidableEq X] (t : FreeGroup X) : FreeGroup X :=
FreeGroup.mk ((FreeGroup.toWord t).dropLast)The predecessor of a reduced word, obtained by deleting its last letter.
theorem FreeGroup.mul_mk_singleton_eq_ite_prefixParent {X : Type u} [DecidableEq X]
(t : FreeGroup X) (y : X × Bool) :
t * FreeGroup.mk [y] =
if _ : ∃ hw : FreeGroup.toWord t ≠ [],
(FreeGroup.toWord t).getLast hw = (y.1, !y.2)
then FreeGroup.prefixParent t
else FreeGroup.mk (FreeGroup.toWord t ++ [y])Multiplication by a signed singleton either deletes the inverse last letter or appends the singleton to the reduced word.
Show proof
by
by_cases h : ∃ hw : FreeGroup.toWord t ≠ [],
(FreeGroup.toWord t).getLast hw = (y.1, !y.2)
· rcases h with ⟨hw, hlast⟩
rw [dif_pos ⟨hw, hlast⟩]
exact FreeGroup.mul_mk_singleton_eq_mk_dropLast_of_cancels t y hw hlast
· rw [dif_neg h]
calc
t * FreeGroup.mk [y] =
FreeGroup.mk (FreeGroup.toWord (t * FreeGroup.mk [y])) := by
exact (FreeGroup.mk_toWord (x := t * FreeGroup.mk [y])).symm
_ = FreeGroup.mk (FreeGroup.toWord t ++ [y]) := by
rw [FreeGroup.toWord_mul_mk_singleton_of_not_cancels t y h]Proof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□@[simp] theorem FreeGroup.toWord_prefixParent {X : Type u} [DecidableEq X] (t : FreeGroup X) :
FreeGroup.toWord (FreeGroup.prefixParent t) = (FreeGroup.toWord t).dropLastThe prefix-parent identity follows from the reduced-word decomposition into a prefix and a last letter.
Show proof
by
rw [FreeGroup.prefixParent, FreeGroup.toWord_mk]
have hred : FreeGroup.IsReduced ((FreeGroup.toWord t).dropLast) := by
exact (FreeGroup.isReduced_toWord (x := t)).dropLast
exact hred.reduce_eqProof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□theorem FreeGroup.toWord_length_prefixParent_lt {X : Type u} [DecidableEq X]
{t : FreeGroup X} (ht : t ≠ 1) :
(FreeGroup.toWord (FreeGroup.prefixParent t)).length < (FreeGroup.toWord t).lengthThe prefix-parent identity follows from the reduced-word decomposition into a prefix and a last letter.
Show proof
by
rw [FreeGroup.toWord_prefixParent, List.length_dropLast]
have hnonempty : FreeGroup.toWord t ≠ [] := by
exact mt (FreeGroup.toWord_eq_nil_iff.mp) ht
have hlen : 0 < (FreeGroup.toWord t).length := List.length_pos_iff_ne_nil.mpr hnonempty
simpa using Nat.pred_lt (Nat.ne_of_gt hlen)Proof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□theorem FreeGroup.length_prefixParent_eq_pred {X : Type u} [DecidableEq X]
(t : FreeGroup X) :
(FreeGroup.toWord (FreeGroup.prefixParent t)).length =
(FreeGroup.toWord t).length - 1The prefix-parent identity follows from the reduced-word decomposition into a prefix and a last letter.
Show proof
by
rw [FreeGroup.toWord_prefixParent, List.length_dropLast]Proof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□theorem FreeGroup.prefixParent_mul_of_of_last_pos {X : Type u} [DecidableEq X]
(t : FreeGroup X) (x : X) (hw : FreeGroup.toWord t ≠ [])
(hlast : (FreeGroup.toWord t).getLast hw = (x, true)) :
FreeGroup.prefixParent t * FreeGroup.of x = tThe prefix-parent identity follows from the reduced-word decomposition into a prefix and a last letter.
Show proof
by
apply FreeGroup.toWord_injective
rw [FreeGroup.toWord_mul, FreeGroup.toWord_of]
have ht : FreeGroup.toWord t =
(FreeGroup.toWord t).dropLast ++ [(FreeGroup.toWord t).getLast hw] := by
simpa using (List.dropLast_append_getLast hw).symm
have hword : FreeGroup.toWord (FreeGroup.prefixParent t) ++ [(x, true)] = FreeGroup.toWord t := by
calc
FreeGroup.toWord (FreeGroup.prefixParent t) ++ [(x, true)]
= (FreeGroup.toWord t).dropLast ++ [(x, true)] := by rw [FreeGroup.toWord_prefixParent]
_ = FreeGroup.toWord t := by
have ht' := ht.symm
rw [hlast] at ht'
exact ht'
have hred : FreeGroup.IsReduced (FreeGroup.toWord (FreeGroup.prefixParent t) ++ [(x, true)]) := by
rw [hword]
exact FreeGroup.isReduced_toWord (x := t)
exact hred.reduce_eq.trans hwordProof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□theorem FreeGroup.prefixParent_mul_mk_singleton_of_last {X : Type u} [DecidableEq X]
(t : FreeGroup X) (y : X × Bool) (hw : FreeGroup.toWord t ≠ [])
(hlast : (FreeGroup.toWord t).getLast hw = y) :
FreeGroup.prefixParent t * FreeGroup.mk [y] = tThe prefix-parent multiplication formula for the last singleton sends a singleton basis element to the singleton supported at the induced quotient image, with the prescribed coefficient in the Reidemeister--Schreier rewriting system.
Show proof
by
apply FreeGroup.toWord_injective
rw [FreeGroup.toWord_mul, FreeGroup.toWord_prefixParent, FreeGroup.toWord_mk]
have ht :
FreeGroup.toWord t =
(FreeGroup.toWord t).dropLast ++ [(FreeGroup.toWord t).getLast hw] := by
simpa using (List.dropLast_append_getLast hw).symm
have hword : (FreeGroup.toWord t).dropLast ++ [y] = FreeGroup.toWord t := by
have ht' := ht.symm
rw [hlast] at ht'
exact ht'
have hred : FreeGroup.IsReduced ((FreeGroup.toWord t).dropLast ++ [y]) := by
rw [hword]
exact FreeGroup.isReduced_toWord (x := t)
exact hred.reduce_eq.trans hwordProof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□theorem FreeGroup.prefixParent_mul_lastLetter {X : Type u} [DecidableEq X]
{t : FreeGroup X} {y : SignedLetter X}
(h : FreeGroup.lastLetter? t = some y) :
FreeGroup.prefixParent t * FreeGroup.mk [y] = tThe prefix-parent identity follows from the reduced-word decomposition into a prefix and a last letter.
Show proof
by
rcases (FreeGroup.lastLetter?_eq_some_iff (g := t) (y := y)).1 h with
⟨hw, hlast⟩
exact FreeGroup.prefixParent_mul_mk_singleton_of_last t y hw hlastProof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□structure FreeGroup.PrefixParentEdge {X : Type u} [DecidableEq X] (t : FreeGroup X) where
parent : FreeGroup X
letter : SignedLetter X
parent_eq : parent = FreeGroup.prefixParent t
rebuild : parent * FreeGroup.mk [letter] = tThe parent edge data obtained by deleting the last signed letter of a nontrivial word.
def FreeGroup.prefixParentEdgeOfNeOne {X : Type u} [DecidableEq X]
{t : FreeGroup X} (ht : t ≠ 1) : FreeGroup.PrefixParentEdge t := by
have hw : FreeGroup.toWord t ≠ [] := by
exact mt (FreeGroup.toWord_eq_nil_iff.mp) ht
refine
{ parent := FreeGroup.prefixParent t
letter := (FreeGroup.toWord t).getLast hw
parent_eq := rfl
rebuild := ?_ }
exact Internal.FreeGroupWord.FreeGroup.prefixParent_mul_mk_singleton_of_last t
((FreeGroup.toWord t).getLast hw) hw rflA nontrivial reduced word has a canonical parent edge.
@[simp] theorem FreeGroup.prefixParentEdgeOfNeOne_parent {X : Type u} [DecidableEq X]
{t : FreeGroup X} (ht : t ≠ 1) :
(FreeGroup.prefixParentEdgeOfNeOne (X := X) ht).parent =
FreeGroup.prefixParent tThe prefix-parent identity follows from the reduced-word decomposition into a prefix and a last letter.
Show proof
rflProof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□theorem FreeGroup.prefixParentEdgeOfNeOne_lastLetter? {X : Type u} [DecidableEq X]
{t : FreeGroup X} (ht : t ≠ 1) :
FreeGroup.lastLetter? t =
some (FreeGroup.prefixParentEdgeOfNeOne (X := X) ht).letterThe prefix-parent identity follows from the reduced-word decomposition into a prefix and a last letter.
Show proof
by
have hw : FreeGroup.toWord t ≠ [] := by
exact mt (FreeGroup.toWord_eq_nil_iff.mp) ht
simp only [lastLetter?, List.getLast?_eq_getLast_of_ne_nil hw, prefixParentEdgeOfNeOne]Proof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□theorem FreeGroup.exists_prefixParent_mul_lastLetter_of_ne_one
{X : Type u} [DecidableEq X] {t : FreeGroup X} (ht : t ≠ 1) :
∃ y : SignedLetter X,
FreeGroup.lastLetter? t = some y ∧
FreeGroup.prefixParent t * FreeGroup.mk [y] = tNontrivial words decompose as parent times their last signed letter.
Show proof
by
have hw : FreeGroup.toWord t ≠ [] := by
exact mt (FreeGroup.toWord_eq_nil_iff.mp) ht
refine ⟨(FreeGroup.toWord t).getLast hw, ?_, ?_⟩
· rw [FreeGroup.lastLetter?, List.getLast?_eq_getLast_of_ne_nil hw]
· exact Internal.FreeGroupWord.FreeGroup.prefixParent_mul_mk_singleton_of_last t
((FreeGroup.toWord t).getLast hw) hw rflProof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□theorem FreeGroup.lastLetter_cases_of_ne_one {X : Type u} [DecidableEq X]
{t : FreeGroup X} (ht : t ≠ 1) :
∃ x : X,
(∃ hw : FreeGroup.toWord t ≠ [],
(FreeGroup.toWord t).getLast hw = (x, true) ∧
FreeGroup.prefixParent t * FreeGroup.of x = t) ∨
(∃ hw : FreeGroup.toWord t ≠ [],
(FreeGroup.toWord t).getLast hw = (x, false) ∧
t * FreeGroup.of x = FreeGroup.prefixParent t)The prefix-parent identity follows from the reduced-word decomposition into a prefix and a last letter.
Show proof
by
have hw : FreeGroup.toWord t ≠ [] := by
exact mt (FreeGroup.toWord_eq_nil_iff.mp) ht
rcases hlast : (FreeGroup.toWord t).getLast hw with ⟨x, b⟩
cases b with
| false =>
refine ⟨x, Or.inr ⟨hw, hlast, ?_⟩⟩
simpa [FreeGroup.prefixParent] using
Internal.FreeGroupWord.FreeGroup.mul_of_of_eq_mk_dropLast_of_cancels t x hw hlast
| true =>
refine ⟨x, Or.inl ⟨hw, hlast, ?_⟩⟩
exact Internal.FreeGroupWord.FreeGroup.prefixParent_mul_of_of_last_pos t x hw hlastProof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□theorem FreeGroup.mul_of_eq_prefixParent_of_cancels {X : Type u} [DecidableEq X]
(t : FreeGroup X) (x : X) (hw : FreeGroup.toWord t ≠ [])
(hlast : (FreeGroup.toWord t).getLast hw = (x, false)) :
t * FreeGroup.of x = FreeGroup.prefixParent tThe prefix-parent identity follows from the reduced-word decomposition into a prefix and a last letter.
Show proof
by
simpa [FreeGroup.prefixParent] using
FreeGroup.mul_of_of_eq_mk_dropLast_of_cancels t x hw hlastProof. Proceed by induction on the reduced free-group word. A nontrivial word has a last signed letter and a prefix obtained by removing it; multiplying the prefix by that last letter reconstructs the original word. Prefix and parent-edge assertions then follow from the reduced-word decomposition and the uniqueness of the final-letter split.
□