This module develops the signed-letter view of reduced free-group words, including cancellation at the last letter and the prefix-parent operation used to build Schreier prefix trees.
A signed generator letter in the word model of a free group.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreierabbrev Internal.SignedLetter (X : Type u)The inverse signed letter.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.SignedLetterdef inv {X : Type u} (y : Internal.SignedLetter X) : Internal.SignedLetter XInverting a signed letter preserves its underlying generator.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.SignedLettertheorem inv_fst {X : Type u} (y : Internal.SignedLetter X) : y.inv.1 = y.1Inverting a signed letter reverses its orientation.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.SignedLettertheorem inv_snd {X : Type u} (y : Internal.SignedLetter X) : y.inv.2 = !y.2Inversion of signed letters is involutive.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.SignedLettertheorem inv_inv {X : Type u} (y : Internal.SignedLetter X) : y.inv.inv = yThe inverse-reversal of a nonempty word starts with the inverse of its last letter.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.FreeGroupWordtheorem 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 last signed letter of the reduced word representing \(g\), if it is nonempty.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreierdef FreeGroup.lastLetter? {X : Type u} [DecidableEq X] (g : FreeGroup X) :
Option (Internal.SignedLetter X)A reduced word has the specified last letter exactly when its last-letter option is that value.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.FreeGroupWordtheorem FreeGroup.lastLetter?_eq_some_iff {X : Type u} [DecidableEq X]
{g : FreeGroup X} {y : Internal.SignedLetter X} :
FreeGroup.lastLetter? g = some y ↔
∃ hw : FreeGroup.toWord g ≠ [], (FreeGroup.toWord g).getLast hw = yMultiplication by a positive generator appends its letter when no cancellation occurs.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.FreeGroupWordtheorem 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)]If the last letter is the inverse of a generator, multiplying by that generator removes it.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.FreeGroupWordtheorem 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)In the cancelling case, the reduced word of the product is the original word without its last letter.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.FreeGroupWordtheorem 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).dropLastAppending a reduced signed letter to a reduced word stays reduced unless the last letter is its inverse.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.FreeGroupWordtheorem 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]Cancelling a reduced signed letter on the right amounts to deleting the last letter in the word model.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.FreeGroupWordtheorem 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)The 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.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.FreeGroupWordtheorem 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).dropLastUnified signed-letter multiplication rule for reduced words.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.FreeGroupWordtheorem FreeGroup.toWord_mul_singleton {X : Type u} [DecidableEq X]
(t : FreeGroup X) (y : Internal.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] := by
by_cases hlast? : FreeGroup.lastLetter? t = some y.inv
· rw [ite_eq_left hlast?]
rcases (FreeGroup.lastLetter?_eq_some_iff (g := t) (y := y.inv)).1 hlast? with
⟨hw, hlast⟩
simpa [Internal.SignedLetter.inv] using
FreeGroup.toWord_mul_mk_singleton_of_cancels t y hw hlast
· rw [ite_eq_right 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 [Internal.SignedLetter.inv] using h))
exact FreeGroup.toWord_mul_mk_singleton_of_not_cancels t y hcancelPositive generators are the positive signed-letter specialization of the word-multiplication formula for free groups.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.FreeGroupWordtheorem 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) : Internal.SignedLetter X) then
(FreeGroup.toWord t).dropLast
else
FreeGroup.toWord t ++ [(x, true)] := by
simpa [FreeGroup.of, Internal.SignedLetter.inv] using
(FreeGroup.toWord_mul_singleton t ((x, true) : Internal.SignedLetter X))The predecessor of a reduced word, obtained by deleting its last letter.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreierdef FreeGroup.prefixParent {X : Type u} [DecidableEq X] (t : FreeGroup X) : FreeGroup XMultiplication by a signed singleton either deletes the inverse last letter or appends the singleton to the reduced word.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.FreeGroupWordtheorem 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]) := by
by_cases h : ∃ hw : FreeGroup.toWord t ≠ [],
(FreeGroup.toWord t).getLast hw = (y.1, !y.2)
· rcases h with ⟨hw, hlast⟩
rw [dite_eq_left ⟨hw, hlast⟩]
exact FreeGroup.mul_mk_singleton_eq_mk_dropLast_of_cancels t y hw hlast
· rw [dite_eq_right 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]The reduced word of the prefix parent is obtained by dropping the final letter.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.FreeGroupWordtheorem FreeGroup.toWord_prefixParent {X : Type u} [DecidableEq X] (t : FreeGroup X) :
FreeGroup.toWord (FreeGroup.prefixParent t) = (FreeGroup.toWord t).dropLastTaking the prefix parent strictly shortens a nontrivial reduced word.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.FreeGroupWordtheorem 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 reduced-word length of the prefix parent is the predecessor of the original length.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.FreeGroupWordtheorem FreeGroup.length_prefixParent_eq_pred {X : Type u} [DecidableEq X]
(t : FreeGroup X) :
(FreeGroup.toWord (FreeGroup.prefixParent t)).length =
(FreeGroup.toWord t).length - 1A word ending in a positive generator is reconstructed from its prefix parent by that generator.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.FreeGroupWordtheorem 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 = tMultiplying the prefix parent by the final signed letter reconstructs the original word.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.FreeGroupWordtheorem 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] = tA last-letter option supplies the signed letter that reconstructs the word from its prefix parent.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.FreeGroupWordtheorem FreeGroup.prefixParent_mul_lastLetter {X : Type u} [DecidableEq X]
{t : FreeGroup X} {y : Internal.SignedLetter X}
(h : FreeGroup.lastLetter? t = some y) :
FreeGroup.prefixParent t * FreeGroup.mk [y] = tThe parent edge data obtained by deleting the last signed letter of a nontrivial word.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreierstructure FreeGroup.PrefixParentEdge {X : Type u} [DecidableEq X] (t : FreeGroup X) where
/-- The free-group element represented by the reduced word with its last letter removed. -/
parent : FreeGroup X
/-- The last signed letter removed from the reduced word. -/
letter : Internal.SignedLetter X
/-- The stored parent agrees with the canonical prefix-parent operation. -/
parent_eq : parent = FreeGroup.prefixParent t
/-- Multiplying the parent by the last letter reconstructs the original element. -/
rebuild : parent * FreeGroup.mk [letter] = tA nontrivial reduced word has a canonical parent edge.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreierdef FreeGroup.prefixParentEdgeOfNeOne {X : Type u} [DecidableEq X]
{t : FreeGroup X} (ht : t ≠ 1) : FreeGroup.PrefixParentEdge tThe canonical edge of a nontrivial word stores its prefix parent.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreiertheorem FreeGroup.prefixParentEdgeOfNeOne_parent {X : Type u} [DecidableEq X]
{t : FreeGroup X} (ht : t ≠ 1) :
(FreeGroup.prefixParentEdgeOfNeOne (X := X) ht).parent =
FreeGroup.prefixParent tThe letter stored by the canonical parent edge is the word's last letter.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreiertheorem FreeGroup.prefixParentEdgeOfNeOne_lastLetter? {X : Type u} [DecidableEq X]
{t : FreeGroup X} (ht : t ≠ 1) :
FreeGroup.lastLetter? t =
some (FreeGroup.prefixParentEdgeOfNeOne (X := X) ht).letterNontrivial words decompose as parent times their last signed letter.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreiertheorem FreeGroup.exists_prefixParent_mul_lastLetter_of_ne_one
{X : Type u} [DecidableEq X] {t : FreeGroup X} (ht : t ≠ 1) :
∃ y : Internal.SignedLetter X,
FreeGroup.lastLetter? t = some y ∧
FreeGroup.prefixParent t * FreeGroup.mk [y] = tThe last letter of a nontrivial word is either positive or negative, with the corresponding parent formula.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreiertheorem 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)Multiplication by a generator cancelling the final negative letter gives the prefix parent.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ReidemeisterSchreier
namespace Internal.FreeGroupWordtheorem 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 t