Reduced words in free groups

Elementary facts about reduced words complementing Mathlib.GroupTheory.FreeGroup.Reduce: the formal inverse of a one-letter word, uniqueness of reduced representatives, reducedness of formal inverses, and reducedness of words w u w⁻¹ in which no letter cancels at either join.

The last section controls cancellation under left multiplication: if the reduced word of g does not begin with the formal inverse of x₂, then the reduced word of (x₁ ++ x₂) * g still begins with x₁ whenever x₁ ++ x₂ is reduced. This is the prefix calculus behind ping-pong arguments on reduced words, such as the big powers property of free groups.

Finally, the reduced word of g⁻¹ * f arises from those of g and f by cancelling their longest common prefix, so ‖g⁻¹ * f‖ + 2 * commonPrefixLength g f = ‖g‖ + ‖f‖ for the word length ‖·‖. Thus the Gromov product of word length is the common prefix length of reduced words.

theorem FreeGroup.inv_mk_singleton {α : Type u_1} (w : α × Bool) : (mk [w])⁻¹ = mk [(w.1, !w.2)]

The inverse of a one-letter word is the inverse letter.

theorem FreeGroup.IsReduced.eq_of_mk_eq {α : Type u_1} {u v : List (α × Bool)} (hu : IsReduced u) (hv : IsReduced v) (h : mk u = mk v) : u = v

Reduced words representing the same element of a free group are equal.

theorem FreeGroup.IsReduced.invRev {α : Type u_1} {w : List (α × Bool)} (hw : IsReduced w) : IsReduced (FreeGroup.invRev w)

The formal inverse of a reduced word is reduced.

@[simp]

theorem FreeGroup.isReduced_invRev {α : Type u_1} {w : List (α × Bool)} : IsReduced (invRev w) ↔ IsReduced w

A formal inverse is reduced exactly when the original word is.

theorem FreeGroup.IsReduced.append_append_invRev {α : Type u_1} {w u : List (α × Bool)} (hw : IsReduced w) (hu : IsReduced u) (hu₀ : u ≠ []) (hhead : ∀ a ∈ w.getLast?, (a.1, !a.2) ∉ u.head?) (hlast : ∀ a ∈ w.getLast?, a ∉ u.getLast?) : IsReduced (w ++ u ++ FreeGroup.invRev w)

If w and the nonempty word u are reduced, the last letter of w does not cancel against the first letter of u, and the last letter of u does not cancel against the first letter of invRev w, then w ++ u ++ invRev w is reduced.

theorem FreeGroup.IsReduced.invRev_ne_self {α : Type u_1} {w : List (α × Bool)} (hw : IsReduced w) (hw₀ : w ≠ []) : FreeGroup.invRev w ≠ w

A nonempty reduced word is never its own formal inverse: otherwise it would represent an element of order at most two of the torsion-free group FreeGroup α.

theorem FreeGroup.toWord_mk_mul_of_invRev_prefix {α : Type u_1} [DecidableEq α] {x : List (α × Bool)} {g : FreeGroup α} (h : invRev x <+: g.toWord) : (mk x * g).toWord = List.drop x.length g.toWord

If the reduced word of g begins with the formal inverse of x, then left multiplication by x cancels that prefix.

theorem FreeGroup.ne_inv_of_isReduced_cons_cons {α : Type u_1} {a b : α × Bool} {l : List (α × Bool)} (h : IsReduced (a :: b :: l)) : b ≠ (a.1, !a.2)

In a reduced word, a letter is never followed by its inverse.

theorem FreeGroup.toWord_mk_singleton_mul_of_head?_ne {α : Type u_1} [DecidableEq α] {a : α × Bool} {g : FreeGroup α} (h : g.toWord.head? ≠ some (a.1, !a.2)) : (mk [a] * g).toWord = a :: g.toWord

Left multiplication by a letter that does not cancel prepends it to the reduced word.

theorem FreeGroup.head?_toWord_mk_mul {α : Type u_1} [DecidableEq α] {x : List (α × Bool)} {g : FreeGroup α} (hx : IsReduced x) (h : ¬invRev x <+: g.toWord) : (mk x * g).toWord.head? = x.head?

If x is reduced and the reduced word of g does not begin with the formal inverse of x, then the first letter of x survives in the reduced word of x * g.

theorem FreeGroup.prefix_toWord_mk_append_mul {α : Type u_1} [DecidableEq α] {x₁ x₂ : List (α × Bool)} {g : FreeGroup α} (hx : IsReduced (x₁ ++ x₂)) (h : ¬invRev x₂ <+: g.toWord) : x₁ <+: (mk (x₁ ++ x₂) * g).toWord

If x₁ ++ x₂ is reduced and the reduced word of g does not begin with the formal inverse of x₂, then the reduced word of (x₁ ++ x₂) * g begins with x₁: the cancellation between the two factors stops inside x₂.

theorem FreeGroup.length_toWord_inv_mk_mul_mk {α : Type u_1} [DecidableEq α] {u v : List (α × Bool)} (hu : IsReduced u) (hv : IsReduced v) : ((mk u)⁻¹ * mk v).toWord.length + 2 * u.commonPrefixLength v = u.length + v.length

For reduced words u and v, the reduced word of (mk u)⁻¹ * mk v has length u.length + v.length - 2 * commonPrefixLength u v. Intuitively, this reduced word arises from invRev u ++ v by cancelling the longest common prefix of u and v.

theorem FreeGroup.norm_inv_mul_add_two_mul_commonPrefixLength {α : Type u_1} [DecidableEq α] (g f : FreeGroup α) : (g⁻¹ * f).norm + 2 * g.toWord.commonPrefixLength f.toWord = g.norm + f.norm

The word length of g⁻¹ * f is the sum of the word lengths of g and f minus twice the length of the longest common prefix of their reduced words.

theorem FreeGroup.induction_on_reduced {α : Type u_1} [DecidableEq α] {motive : FreeGroup α → Prop} (g : FreeGroup α) (one : motive 1) (mul_mk_singleton : ∀ (g : FreeGroup α) (x : α × Bool), (g * mk [x]).toWord = g.toWord ++ [x] → motive g → motive (g * mk [x])) : motive g

Induction along reduced words: a property of 1 that passes from g to g * mk [x] whenever the reduced word of g * mk [x] is that of g followed by x holds for every element of the free group.