Documentation

Mathlib.GroupTheory.FreeGroup.Reduce

The maximal reduction of a word in a free group #

Main declarations #

source
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.

Equations
  • One or more equations did not get rendered due to their size.
source
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.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem FreeGroup.reduce_nil {α : Type u_1} [DecidableEq α] :
reduce [] = []
source
@[simp]
theorem FreeAddGroup.reduce_nil {α : Type u_1} [DecidableEq α] :
reduce [] = []
source
theorem FreeGroup.reduce_singleton {α : Type u_1} [DecidableEq α] (s : α × Bool) :
reduce [s] = [s]
source
theorem FreeAddGroup.reduce_singleton {α : Type u_1} [DecidableEq α] (s : α × Bool) :
reduce [s] = [s]
source
@[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
source
@[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
source
@[simp]
theorem FreeGroup.reduce_replicate {α : Type u_1} [DecidableEq α] (n : ℕ) (x : α × Bool) :
reduce (List.replicate n x) = List.replicate n x
source
@[simp]
theorem FreeAddGroup.reduce_replicate {α : Type u_1} [DecidableEq α] (n : ℕ) (x : α × Bool) :
reduce (List.replicate n x) = List.replicate n x
source
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.

source
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.

source
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
source
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
source
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.

source
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.

source
@[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.

source
@[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.

source
theorem FreeGroup.reduce.Step.eq {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : Red.Step L₁ L₂) :
reduce L₁ = reduce L₂
source
theorem FreeAddGroup.reduce.Step.eq {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : Red.Step L₁ L₂) :
reduce L₁ = reduce L₂
source
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.

source
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.

source
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.

source
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.

source
theorem FreeGroup.Red.reduce_right {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (h : Red L₁ L₂) :
Red L₁ (reduce L₂)
source
theorem FreeAddGroup.Red.reduce_right {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (h : Red L₁ L₂) :
Red L₁ (reduce L₂)
source
theorem FreeGroup.Red.reduce_left {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (h : Red L₁ L₂) :
Red L₂ (reduce L₁)
source
theorem FreeAddGroup.Red.reduce_left {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (h : Red L₁ L₂) :
Red L₂ (reduce L₁)
source
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.

source
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.

source
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.

source
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.

source
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.

source
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.

source
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₁.

source
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₁.

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

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

Equations
source
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.

Equations
source
theorem FreeGroup.mk_toWord {α : Type u_1} [DecidableEq α] {x : FreeGroup α} :
mk x.toWord = x
source
theorem FreeAddGroup.mk_toWord {α : Type u_1} [DecidableEq α] {x : FreeAddGroup α} :
mk x.toWord = x
source
theorem FreeGroup.toWord_injective {α : Type u_1} [DecidableEq α] :
Function.Injective toWord
source
theorem FreeAddGroup.toWord_injective {α : Type u_1} [DecidableEq α] :
Function.Injective toWord
source
@[simp]
theorem FreeGroup.toWord_inj {α : Type u_1} [DecidableEq α] {x y : FreeGroup α} :
x.toWord = y.toWord ↔ x = y
source
@[simp]
theorem FreeAddGroup.toWord_inj {α : Type u_1} [DecidableEq α] {x y : FreeAddGroup α} :
x.toWord = y.toWord ↔ x = y
source
@[simp]
theorem FreeGroup.toWord_mk {α : Type u_1} {L₁ : List (α × Bool)} [DecidableEq α] :
(mk L₁).toWord = reduce L₁
source
@[simp]
theorem FreeAddGroup.toWord_mk {α : Type u_1} {L₁ : List (α × Bool)} [DecidableEq α] :
(mk L₁).toWord = reduce L₁
source
@[simp]
theorem FreeGroup.toWord_of {α : Type u_1} [DecidableEq α] (a : α) :
(of a).toWord = [(a, true)]
source
@[simp]
theorem FreeAddGroup.toWord_of {α : Type u_1} [DecidableEq α] (a : α) :
(of a).toWord = [(a, true)]
source
@[simp]
theorem FreeGroup.reduce_toWord {α : Type u_1} [DecidableEq α] (x : FreeGroup α) :
reduce x.toWord = x.toWord
source
@[simp]
theorem FreeAddGroup.reduce_toWord {α : Type u_1} [DecidableEq α] (x : FreeAddGroup α) :
reduce x.toWord = x.toWord
source
@[simp]
theorem FreeGroup.toWord_one {α : Type u_1} [DecidableEq α] :
toWord 1 = []
source
@[simp]
theorem FreeAddGroup.toWord_zero {α : Type u_1} [DecidableEq α] :
toWord 0 = []
source
theorem FreeGroup.toWord_mul {α : Type u_1} [DecidableEq α] (x y : FreeGroup α) :
(x * y).toWord = reduce (x.toWord ++ y.toWord)
source
theorem FreeAddGroup.toWord_add {α : Type u_1} [DecidableEq α] (x y : FreeAddGroup α) :
(x + y).toWord = reduce (x.toWord ++ y.toWord)
source
theorem FreeGroup.toWord_pow {α : Type u_1} [DecidableEq α] (x : FreeGroup α) (n : ℕ) :
(x ^ n).toWord = reduce (List.replicate n x.toWord).flatten
source
theorem FreeAddGroup.toWord_nsmul {α : Type u_1} [DecidableEq α] (x : FreeAddGroup α) (n : ℕ) :
(n • x).toWord = reduce (List.replicate n x.toWord).flatten
source
@[simp]
theorem FreeGroup.toWord_of_pow {α : Type u_1} [DecidableEq α] (a : α) (n : ℕ) :
(of a ^ n).toWord = List.replicate n (a, true)
source
@[simp]
theorem FreeAddGroup.toWord_of_nsmul {α : Type u_1} [DecidableEq α] (a : α) (n : ℕ) :
(n • of a).toWord = List.replicate n (a, true)
source
@[simp]
theorem FreeGroup.toWord_eq_nil_iff {α : Type u_1} [DecidableEq α] {x : FreeGroup α} :
x.toWord = [] ↔ x = 1
source
@[simp]
theorem FreeAddGroup.toWord_eq_nil_iff {α : Type u_1} [DecidableEq α] {x : FreeAddGroup α} :
x.toWord = [] ↔ x = 0
source
theorem FreeGroup.reduce_invRev {α : Type u_1} [DecidableEq α] {w : List (α × Bool)} :
reduce (invRev w) = invRev (reduce w)
source
theorem FreeAddGroup.reduce_negRev {α : Type u_1} [DecidableEq α] {w : List (α × Bool)} :
reduce (negRev w) = negRev (reduce w)
source
@[simp]
theorem FreeGroup.toWord_inv {α : Type u_1} [DecidableEq α] (x : FreeGroup α) :
x⁻¹.toWord = invRev x.toWord
source
@[simp]
theorem FreeAddGroup.toWord_neg {α : Type u_1} [DecidableEq α] (x : FreeAddGroup α) :
(-x).toWord = negRev x.toWord
source
theorem FreeGroup.reduce_append_reduce_reduce {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] :
reduce (reduce L₁ ++ reduce L₂) = reduce (L₁ ++ L₂)
source
theorem FreeAddGroup.reduce_append_reduce_reduce {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] :
reduce (reduce L₁ ++ reduce L₂) = reduce (L₁ ++ L₂)
source
theorem FreeGroup.reduce_cons_reduce {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] (a : α × Bool) :
reduce (a :: reduce L) = reduce (a :: L)
source
theorem FreeAddGroup.reduce_cons_reduce {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] (a : α × Bool) :
reduce (a :: reduce L) = reduce (a :: L)
source
theorem FreeGroup.reduce_invRev_left_cancel {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] :
reduce (invRev L ++ L) = []
source
theorem FreeAddGroup.reduce_negRev_left_cancel {α : Type u_1} {L : List (α × Bool)} [DecidableEq α] :
reduce (negRev L ++ L) = []
source
theorem FreeGroup.toWord_mul_sublist {α : Type u_1} [DecidableEq α] (x y : FreeGroup α) :
(x * y).toWord.Sublist (x.toWord ++ y.toWord)
source
theorem FreeAddGroup.toWord_add_sublist {α : Type u_1} [DecidableEq α] (x y : FreeAddGroup α) :
(x + y).toWord.Sublist (x.toWord ++ y.toWord)
source
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).

Equations
source
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).

Equations
source
instance FreeGroup.instDecidableEq {α : Type u_1} [DecidableEq α] :
DecidableEq (FreeGroup α)
Equations
source
instance FreeAddGroup.instDecidableEq {α : Type u_1} [DecidableEq α] :
DecidableEq (FreeAddGroup α)
Equations
source
instance FreeGroup.Red.decidableRel {α : Type u_1} [DecidableEq α] :
DecidableRel Red
Equations
source
def FreeGroup.Red.enum {α : Type u_1} [DecidableEq α] (L₁ : List (α × Bool)) :
List (List (α × Bool))

A list containing every word that w₁ reduces to.

Equations
source
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₂
source
theorem FreeGroup.Red.enum.complete {α : Type u_1} {L₁ L₂ : List (α × Bool)} [DecidableEq α] (H : Red L₁ L₂) :
L₂ ∈ enum L₁
source
instance FreeGroup.instFintypeSubtypeListProdBoolRed {α : Type u_1} [DecidableEq α] (L₁ : List (α × Bool)) :
Fintype { L₂ : List (α × Bool) // Red L₁ L₂ }
Equations
source
@[simp]
theorem FreeGroup.one_ne_of {α : Type u_1} (a : α) :
1 ≠ of a
source
@[simp]
theorem FreeAddGroup.zero_ne_of {α : Type u_1} (a : α) :
0 ≠ of a
source
@[simp]
theorem FreeGroup.of_ne_one {α : Type u_1} (a : α) :
of a ≠ 1
source
@[simp]
theorem FreeAddGroup.of_ne_zero {α : Type u_1} (a : α) :
of a ≠ 0
source
instance FreeGroup.instNontrivialOfNonempty {α : Type u_1} [Nonempty α] :
Nontrivial (FreeGroup α)
source
instance FreeAddGroup.instNontrivialOfNonempty {α : Type u_1} [Nonempty α] :
Nontrivial (FreeAddGroup α)
source
def FreeGroup.norm {α : Type u_1} [DecidableEq α] (x : FreeGroup α) :
ℕ

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

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

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

Equations
source
@[simp]
theorem FreeGroup.norm_inv_eq {α : Type u_1} [DecidableEq α] {x : FreeGroup α} :
x⁻¹.norm = x.norm
source
@[simp]
theorem FreeAddGroup.norm_neg_eq {α : Type u_1} [DecidableEq α] {x : FreeAddGroup α} :
(-x).norm = x.norm
source
@[simp]
theorem FreeGroup.norm_eq_zero {α : Type u_1} [DecidableEq α] {x : FreeGroup α} :
x.norm = 0 ↔ x = 1
source
@[simp]
theorem FreeAddGroup.norm_eq_zero {α : Type u_1} [DecidableEq α] {x : FreeAddGroup α} :
x.norm = 0 ↔ x = 0
source
@[simp]
theorem FreeGroup.norm_one {α : Type u_1} [DecidableEq α] :
norm 1 = 0
source
@[simp]
theorem FreeAddGroup.norm_zero {α : Type u_1} [DecidableEq α] :
norm 0 = 0
source
@[simp]
theorem FreeGroup.norm_of {α : Type u_1} [DecidableEq α] (a : α) :
(of a).norm = 1
source
@[simp]
theorem FreeAddGroup.norm_of {α : Type u_1} [DecidableEq α] (a : α) :
(of a).norm = 1
source
theorem FreeGroup.norm_mk_le {α : Type u_1} {L₁ : List (α × Bool)} [DecidableEq α] :
(mk L₁).norm ≤ L₁.length
source
theorem FreeAddGroup.norm_mk_le {α : Type u_1} {L₁ : List (α × Bool)} [DecidableEq α] :
(mk L₁).norm ≤ L₁.length
source
theorem FreeGroup.norm_mul_le {α : Type u_1} [DecidableEq α] (x y : FreeGroup α) :
(x * y).norm ≤ x.norm + y.norm
source
theorem FreeAddGroup.norm_add_le {α : Type u_1} [DecidableEq α] (x y : FreeAddGroup α) :
(x + y).norm ≤ x.norm + y.norm
source
@[simp]
theorem FreeGroup.norm_of_pow {α : Type u_1} [DecidableEq α] (a : α) (n : ℕ) :
(of a ^ n).norm = n
source
@[simp]
theorem FreeAddGroup.norm_of_nsmul {α : Type u_1} [DecidableEq α] (a : α) (n : ℕ) :
(n • of a).norm = n
source
theorem FreeGroup.norm_surjective {α : Type u_1} [DecidableEq α] [Nonempty α] :
Function.Surjective norm
source
theorem FreeAddGroup.norm_surjective {α : Type u_1} [DecidableEq α] [Nonempty α] :
Function.Surjective norm