The maximal reduction of a word in a free group

Main declarations

• FreeGroup.reduce: the maximal reduction of a word in a free group
• FreeGroup.norm: the length of the maximal reduction of a word in a free group

def FreeGroup.reduce {α : Type u_1} [DecidableEq α] (L : List (α × Bool)) : List (α × Bool)

The maximal reduction of a word. It is computable iff α has decidable equality.

def FreeAddGroup.reduce {α : Type u_1} [DecidableEq α] (L : List (α × Bool)) : List (α × Bool)

The maximal reduction of a word. It is computable iff α has decidable equality.

@[simp]

theorem FreeGroup.reduce_nil {α : Type u_1} [DecidableEq α] : reduce [] = []

@[simp]

theorem FreeAddGroup.reduce_nil {α : Type u_1} [DecidableEq α] : reduce [] = []

theorem FreeGroup.reduce_singleton {α : Type u_1} [DecidableEq α] (s : α × Bool) : reduce [s] = [s]

theorem FreeAddGroup.reduce_singleton {α : Type u_1} [DecidableEq α] (s : α × Bool) : reduce [s] = [s]

@[simp]

theorem FreeGroup.reduce.cons {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] (x : α × Bool) : reduce (x :: L) = List.casesOn (reduce L) [x] fun (hd : α × Bool) (tl : List (α × Bool)) => if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl

@[simp]

theorem FreeAddGroup.reduce.cons {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] (x : α × Bool) : reduce (x :: L) = List.casesOn (reduce L) [x] fun (hd : α × Bool) (tl : List (α × Bool)) => if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl

@[simp]

theorem FreeGroup.reduce_replicate {α : Type u_1} [DecidableEq α] (n : ℕ) (x : α × Bool) : reduce (List.replicate n x) = List.replicate n x

@[simp]

theorem FreeAddGroup.reduce_replicate {α : Type u_1} [DecidableEq α] (n : ℕ) (x : α × Bool) : reduce (List.replicate n x) = List.replicate n x

theorem FreeGroup.reduce.red {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] : Red L (reduce L)

The first theorem that characterises the function reduce: a word reduces to its maximal reduction.

theorem FreeAddGroup.reduce.red {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] : Red L (reduce L)

The first theorem that characterises the function reduce: a word reduces to its maximal reduction.

theorem FreeGroup.reduce.not {α : Type u_1} [DecidableEq α] {p : Prop} {L₁ L₂ L₃ : List (α × Bool)} {x : α} {b : Bool} : reduce L₁ = L₂ ++ (x, b) :: (x, !b) :: L₃ → p

theorem FreeAddGroup.reduce.not {α : Type u_1} [DecidableEq α] {p : Prop} {L₁ L₂ L₃ : List (α × Bool)} {x : α} {b : Bool} : reduce L₁ = L₂ ++ (x, b) :: (x, !b) :: L₃ → p

theorem FreeGroup.reduce.min {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : Red (reduce L₁) L₂) : reduce L₁ = L₂

The second theorem that characterises the function reduce: the maximal reduction of a word only reduces to itself.

theorem FreeAddGroup.reduce.min {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : Red (reduce L₁) L₂) : reduce L₁ = L₂

The second theorem that characterises the function reduce: the maximal reduction of a word only reduces to itself.

@[simp]

theorem FreeGroup.reduce.idem {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] : reduce (reduce L) = reduce L

reduce is idempotent, i.e. the maximal reduction of the maximal reduction of a word is the maximal reduction of the word.

@[simp]

theorem FreeAddGroup.reduce.idem {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] : reduce (reduce L) = reduce L

reduce is idempotent, i.e. the maximal reduction of the maximal reduction of a word is the maximal reduction of the word.

theorem FreeGroup.reduce.Step.eq {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : Red.Step L₁ L₂) : reduce L₁ = reduce L₂

theorem FreeAddGroup.reduce.Step.eq {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : Red.Step L₁ L₂) : reduce L₁ = reduce L₂

theorem FreeGroup.reduce.eq_of_red {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : Red L₁ L₂) : reduce L₁ = reduce L₂

If a word reduces to another word, then they have a common maximal reduction.

theorem FreeAddGroup.reduce.eq_of_red {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : Red L₁ L₂) : reduce L₁ = reduce L₂

If a word reduces to another word, then they have a common maximal reduction.

theorem FreeGroup.red.reduce_eq {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : Red L₁ L₂) : reduce L₁ = reduce L₂

Alias of FreeGroup.reduce.eq_of_red.

---

If a word reduces to another word, then they have a common maximal reduction.

theorem FreeGroup.freeAddGroup.red.reduce_eq {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : FreeAddGroup.Red L₁ L₂) : FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂

Alias of FreeAddGroup.reduce.eq_of_red.

---

If a word reduces to another word, then they have a common maximal reduction.

theorem FreeGroup.Red.reduce_right {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (h : Red L₁ L₂) : Red L₁ (reduce L₂)

theorem FreeAddGroup.Red.reduce_right {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (h : Red L₁ L₂) : Red L₁ (reduce L₂)

theorem FreeGroup.Red.reduce_left {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (h : Red L₁ L₂) : Red L₂ (reduce L₁)

theorem FreeAddGroup.Red.reduce_left {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (h : Red L₁ L₂) : Red L₂ (reduce L₁)

theorem FreeGroup.reduce.sound {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : mk L₁ = mk L₂) : reduce L₁ = reduce L₂

If two words correspond to the same element in the free group, then they have a common maximal reduction. This is the proof that the function that sends an element of the free group to its maximal reduction is well-defined.

theorem FreeAddGroup.reduce.sound {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : mk L₁ = mk L₂) : reduce L₁ = reduce L₂

If two words correspond to the same element in the additive free group, then they have a common maximal reduction. This is the proof that the function that sends an element of the free group to its maximal reduction is well-defined.

theorem FreeGroup.reduce.exact {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : reduce L₁ = reduce L₂) : mk L₁ = mk L₂

If two words have a common maximal reduction, then they correspond to the same element in the free group.

theorem FreeAddGroup.reduce.exact {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : reduce L₁ = reduce L₂) : mk L₁ = mk L₂

If two words have a common maximal reduction, then they correspond to the same element in the additive free group.

theorem FreeGroup.reduce.self {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] : mk (reduce L) = mk L

A word and its maximal reduction correspond to the same element of the free group.

theorem FreeAddGroup.reduce.self {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] : mk (reduce L) = mk L

A word and its maximal reduction correspond to the same element of the additive free group.

theorem FreeGroup.reduce.rev {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : Red L₁ L₂) : Red L₂ (reduce L₁)

If words w₁ w₂ are such that w₁ reduces to w₂, then w₂ reduces to the maximal reduction of w₁.

theorem FreeAddGroup.reduce.rev {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : Red L₁ L₂) : Red L₂ (reduce L₁)

If words w₁ w₂ are such that w₁ reduces to w₂, then w₂ reduces to the maximal reduction of w₁.

def FreeGroup.toWord {α : Type u_1} [DecidableEq α] : FreeGroup α → List (α × Bool)

The function that sends an element of the free group to its maximal reduction.

def FreeAddGroup.toWord {α : Type u_1} [DecidableEq α] : FreeAddGroup α → List (α × Bool)

The function that sends an element of the additive free group to its maximal reduction.

theorem FreeGroup.mk_toWord {α : Type u_1} [DecidableEq α] {x : FreeGroup α} : mk x.toWord = x

theorem FreeAddGroup.mk_toWord {α : Type u_1} [DecidableEq α] {x : FreeAddGroup α} : mk x.toWord = x

theorem FreeGroup.toWord_injective {α : Type u_1} [DecidableEq α] : Function.Injective toWord

theorem FreeAddGroup.toWord_injective {α : Type u_1} [DecidableEq α] : Function.Injective toWord

@[simp]

theorem FreeGroup.toWord_inj {α : Type u_1} [DecidableEq α] {x y : FreeGroup α} : x.toWord = y.toWord ↔ x = y

@[simp]

theorem FreeAddGroup.toWord_inj {α : Type u_1} [DecidableEq α] {x y : FreeAddGroup α} : x.toWord = y.toWord ↔ x = y

@[simp]

theorem FreeGroup.toWord_mk {α : Type u_1} {L₁ : List (α × Bool)} [DecidableEq α] : (mk L₁).toWord = reduce L₁

@[simp]

theorem FreeAddGroup.toWord_mk {α : Type u_1} {L₁ : List (α × Bool)} [DecidableEq α] : (mk L₁).toWord = reduce L₁

@[simp]

theorem FreeGroup.toWord_of {α : Type u_1} [DecidableEq α] (a : α) : (of a).toWord = [(a, true)]

@[simp]

theorem FreeAddGroup.toWord_of {α : Type u_1} [DecidableEq α] (a : α) : (of a).toWord = [(a, true)]

@[simp]

theorem FreeGroup.reduce_toWord {α : Type u_1} [DecidableEq α] (x : FreeGroup α) : reduce x.toWord = x.toWord

@[simp]

theorem FreeAddGroup.reduce_toWord {α : Type u_1} [DecidableEq α] (x : FreeAddGroup α) : reduce x.toWord = x.toWord

@[simp]

theorem FreeGroup.toWord_one {α : Type u_1} [DecidableEq α] : toWord 1 = []

@[simp]

theorem FreeAddGroup.toWord_zero {α : Type u_1} [DecidableEq α] : toWord 0 = []

theorem FreeGroup.toWord_mul {α : Type u_1} [DecidableEq α] (x y : FreeGroup α) : (x * y).toWord = reduce (x.toWord ++ y.toWord)

theorem FreeAddGroup.toWord_add {α : Type u_1} [DecidableEq α] (x y : FreeAddGroup α) : (x + y).toWord = reduce (x.toWord ++ y.toWord)

theorem FreeGroup.toWord_pow {α : Type u_1} [DecidableEq α] (x : FreeGroup α) (n : ℕ) : (x ^ n).toWord = reduce (List.replicate n x.toWord).flatten

theorem FreeAddGroup.toWord_nsmul {α : Type u_1} [DecidableEq α] (x : FreeAddGroup α) (n : ℕ) : (n • x).toWord = reduce (List.replicate n x.toWord).flatten

@[simp]

theorem FreeGroup.toWord_of_pow {α : Type u_1} [DecidableEq α] (a : α) (n : ℕ) : (of a ^ n).toWord = List.replicate n (a, true)

@[simp]

theorem FreeAddGroup.toWord_of_nsmul {α : Type u_1} [DecidableEq α] (a : α) (n : ℕ) : (n • of a).toWord = List.replicate n (a, true)

@[simp]

theorem FreeGroup.toWord_eq_nil_iff {α : Type u_1} [DecidableEq α] {x : FreeGroup α} : x.toWord = [] ↔ x = 1

@[simp]

theorem FreeAddGroup.toWord_eq_nil_iff {α : Type u_1} [DecidableEq α] {x : FreeAddGroup α} : x.toWord = [] ↔ x = 0

theorem FreeGroup.reduce_invRev {α : Type u_1} [DecidableEq α] {w : List (α × Bool)} : reduce (invRev w) = invRev (reduce w)

theorem FreeAddGroup.reduce_negRev {α : Type u_1} [DecidableEq α] {w : List (α × Bool)} : reduce (negRev w) = negRev (reduce w)

@[simp]

theorem FreeGroup.toWord_inv {α : Type u_1} [DecidableEq α] (x : FreeGroup α) : x⁻¹.toWord = invRev x.toWord

@[simp]

theorem FreeAddGroup.toWord_neg {α : Type u_1} [DecidableEq α] (x : FreeAddGroup α) : (-x).toWord = negRev x.toWord

theorem FreeGroup.reduce_append_reduce_reduce {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] : reduce (reduce L₁ ++ reduce L₂) = reduce (L₁ ++ L₂)

theorem FreeAddGroup.reduce_append_reduce_reduce {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] : reduce (reduce L₁ ++ reduce L₂) = reduce (L₁ ++ L₂)

theorem FreeGroup.reduce_cons_reduce {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] (a : α × Bool) : reduce (a :: reduce L) = reduce (a :: L)

theorem FreeAddGroup.reduce_cons_reduce {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] (a : α × Bool) : reduce (a :: reduce L) = reduce (a :: L)

theorem FreeGroup.reduce_invRev_left_cancel {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] : reduce (invRev L ++ L) = []

theorem FreeAddGroup.reduce_negRev_left_cancel {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] : reduce (negRev L ++ L) = []

theorem FreeGroup.toWord_mul_sublist {α : Type u_1} [DecidableEq α] (x y : FreeGroup α) : (x * y).toWord.Sublist (x.toWord ++ y.toWord)

theorem FreeAddGroup.toWord_add_sublist {α : Type u_1} [DecidableEq α] (x y : FreeAddGroup α) : (x + y).toWord.Sublist (x.toWord ++ y.toWord)

def FreeGroup.reduce.churchRosser {α : Type u_1} {L₁ L₂ L₃ : List (α × Bool)} [DecidableEq α] (H12 : Red L₁ L₂) (H13 : Red L₁ L₃) : { L₄ : List (α × Bool) // Red L₂ L₄ ∧ Red L₃ L₄ }

Constructive Church-Rosser theorem (compare FreeGroup.Red.church_rosser).

def FreeAddGroup.reduce.churchRosser {α : Type u_1} {L₁ L₂ L₃ : List (α × Bool)} [DecidableEq α] (H12 : Red L₁ L₂) (H13 : Red L₁ L₃) : { L₄ : List (α × Bool) // Red L₂ L₄ ∧ Red L₃ L₄ }

Constructive Church-Rosser theorem (compare FreeAddGroup.Red.church_rosser).

instance FreeGroup.instDecidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (FreeGroup α)

instance FreeAddGroup.instDecidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (FreeAddGroup α)

instance FreeGroup.Red.decidableRel {α : Type u_1} [DecidableEq α] : DecidableRel Red

def FreeGroup.Red.enum {α : Type u_1} [DecidableEq α] (L₁ : List (α × Bool)) : List (List (α × Bool))

A list containing every word that w₁ reduces to.

theorem FreeGroup.Red.enum.sound {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : L₂ ∈ List.filter (fun (b : List (α × Bool)) => decide (Red L₁ b)) L₁.sublists) : Red L₁ L₂

theorem FreeGroup.Red.enum.complete {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : Red L₁ L₂) : L₂ ∈ enum L₁

instance FreeGroup.instFintypeSubtypeListProdBoolRed {α : Type u_1} [DecidableEq α] (L₁ : List (α × Bool)) : Fintype { L₂ : List (α × Bool) // Red L₁ L₂ }

theorem FreeGroup.IsReduced.reduce_eq {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] (h : IsReduced L) : reduce L = L

theorem FreeAddGroup.IsReduced.reduce_eq {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] (h : IsReduced L) : reduce L = L

theorem FreeGroup.IsReduced.of_reduce_eq {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] (h : reduce L = L) : IsReduced L

theorem FreeAddGroup.IsReduced.of_reduce_eq {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] (h : reduce L = L) : IsReduced L

theorem FreeGroup.isReduced_iff_reduce_eq {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] : IsReduced L ↔ reduce L = L

theorem FreeAddGroup.isReduced_iff_reduce_eq {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] : IsReduced L ↔ reduce L = L

theorem FreeGroup.isReduced_toWord {α : Type u_1} [DecidableEq α] {x : FreeGroup α} : IsReduced x.toWord

theorem FreeAddGroup.isReduced_toWord {α : Type u_1} [DecidableEq α] {x : FreeAddGroup α} : IsReduced x.toWord

@[simp]

theorem FreeGroup.one_ne_of {α : Type u_1} (a : α) : 1 ≠ of a

@[simp]

theorem FreeAddGroup.zero_ne_of {α : Type u_1} (a : α) : 0 ≠ of a

@[simp]

theorem FreeGroup.of_ne_one {α : Type u_1} (a : α) : of a ≠ 1

@[simp]

theorem FreeAddGroup.of_ne_zero {α : Type u_1} (a : α) : of a ≠ 0

instance FreeGroup.instNontrivialOfNonempty {α : Type u_1} [Nonempty α] : Nontrivial (FreeGroup α)

instance FreeAddGroup.instNontrivialOfNonempty {α : Type u_1} [Nonempty α] : Nontrivial (FreeAddGroup α)

def FreeGroup.norm {α : Type u_1} [DecidableEq α] (x : FreeGroup α) : ℕ

The length of reduced words provides a norm on a free group.

def FreeAddGroup.norm {α : Type u_1} [DecidableEq α] (x : FreeAddGroup α) : ℕ

The length of reduced words provides a norm on an additive free group.

@[simp]

theorem FreeGroup.norm_inv_eq {α : Type u_1} [DecidableEq α] {x : FreeGroup α} : x⁻¹.norm = x.norm

@[simp]

theorem FreeAddGroup.norm_neg_eq {α : Type u_1} [DecidableEq α] {x : FreeAddGroup α} : (-x).norm = x.norm

@[simp]

theorem FreeGroup.norm_eq_zero {α : Type u_1} [DecidableEq α] {x : FreeGroup α} : x.norm = 0 ↔ x = 1

@[simp]

theorem FreeAddGroup.norm_eq_zero {α : Type u_1} [DecidableEq α] {x : FreeAddGroup α} : x.norm = 0 ↔ x = 0

@[simp]

theorem FreeGroup.norm_one {α : Type u_1} [DecidableEq α] : norm 1 = 0

@[simp]

theorem FreeAddGroup.norm_zero {α : Type u_1} [DecidableEq α] : norm 0 = 0

@[simp]

theorem FreeGroup.norm_of {α : Type u_1} [DecidableEq α] (a : α) : (of a).norm = 1

@[simp]

theorem FreeAddGroup.norm_of {α : Type u_1} [DecidableEq α] (a : α) : (of a).norm = 1

theorem FreeGroup.norm_mk_le {α : Type u_1} {L₁ : List (α × Bool)} [DecidableEq α] : (mk L₁).norm ≤ L₁.length

theorem FreeAddGroup.norm_mk_le {α : Type u_1} {L₁ : List (α × Bool)} [DecidableEq α] : (mk L₁).norm ≤ L₁.length

theorem FreeGroup.norm_mul_le {α : Type u_1} [DecidableEq α] (x y : FreeGroup α) : (x * y).norm ≤ x.norm + y.norm

theorem FreeAddGroup.norm_add_le {α : Type u_1} [DecidableEq α] (x y : FreeAddGroup α) : (x + y).norm ≤ x.norm + y.norm

@[simp]

theorem FreeGroup.norm_of_pow {α : Type u_1} [DecidableEq α] (a : α) (n : ℕ) : (of a ^ n).norm = n

@[simp]

theorem FreeAddGroup.norm_of_nsmul {α : Type u_1} [DecidableEq α] (a : α) (n : ℕ) : (n • of a).norm = n

theorem FreeGroup.norm_surjective {α : Type u_1} [DecidableEq α] [Nonempty α] : Function.Surjective norm

theorem FreeAddGroup.norm_surjective {α : Type u_1} [DecidableEq α] [Nonempty α] : Function.Surjective norm