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

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.

Instances For

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.

Instances For

source

@[simp]

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

FreeGroup.reduce [] = []

source

@[simp]

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

FreeAddGroup.reduce [] = []

source

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

FreeGroup.reduce [s] = [s]

source

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

FreeAddGroup.reduce [s] = [s]

source

@[simp]

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

FreeGroup.reduce (x :: L) = List.casesOn (FreeGroup.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) :

FreeAddGroup.reduce (x :: L) = List.casesOn (FreeAddGroup.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) :

FreeGroup.reduce (List.replicate n x) = List.replicate n x

source

@[simp]

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

FreeAddGroup.reduce (List.replicate n x) = List.replicate n x

source

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

FreeGroup.Red L (FreeGroup.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 α] :

FreeAddGroup.Red L (FreeAddGroup.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} :

FreeGroup.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} :

FreeAddGroup.reduce L₁ = L₂ ++ (x, b) :: (x, !b) :: L₃ → p

source

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

FreeGroup.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 : FreeAddGroup.Red (FreeAddGroup.reduce L₁) L₂) :

FreeAddGroup.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 α] :

FreeGroup.reduce (FreeGroup.reduce L) = FreeGroup.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 α] :

FreeAddGroup.reduce (FreeAddGroup.reduce L) = FreeAddGroup.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 : FreeGroup.Red.Step L₁ L₂) :

FreeGroup.reduce L₁ = FreeGroup.reduce L₂

source

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

FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂

source

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

FreeGroup.reduce L₁ = FreeGroup.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 : FreeAddGroup.Red L₁ L₂) :

FreeAddGroup.reduce L₁ = FreeAddGroup.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 : FreeGroup.Red L₁ L₂) :

FreeGroup.reduce L₁ = FreeGroup.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 : FreeGroup.Red L₁ L₂) :

FreeGroup.Red L₁ (FreeGroup.reduce L₂)

source

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

FreeAddGroup.Red L₁ (FreeAddGroup.reduce L₂)

source

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

FreeGroup.Red L₂ (FreeGroup.reduce L₁)

source

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

FreeAddGroup.Red L₂ (FreeAddGroup.reduce L₁)

source

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

FreeGroup.reduce L₁ = FreeGroup.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 : FreeAddGroup.mk L₁ = FreeAddGroup.mk L₂) :

FreeAddGroup.reduce L₁ = FreeAddGroup.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 : FreeGroup.reduce L₁ = FreeGroup.reduce L₂) :

FreeGroup.mk L₁ = FreeGroup.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 : FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂) :

FreeAddGroup.mk L₁ = FreeAddGroup.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 α] :

FreeGroup.mk (FreeGroup.reduce L) = FreeGroup.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 α] :

FreeAddGroup.mk (FreeAddGroup.reduce L) = FreeAddGroup.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 : FreeGroup.Red L₁ L₂) :

FreeGroup.Red L₂ (FreeGroup.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 : FreeAddGroup.Red L₁ L₂) :

FreeAddGroup.Red L₂ (FreeAddGroup.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

FreeGroup.toWord = Quot.lift FreeGroup.reduce ⋯

Instances For

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

FreeAddGroup.toWord = Quot.lift FreeAddGroup.reduce ⋯

Instances For

source

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

FreeGroup.mk x.toWord = x

source

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

FreeAddGroup.mk x.toWord = x

source

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

Function.Injective FreeGroup.toWord

source

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

Function.Injective FreeAddGroup.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 α] :

(FreeGroup.mk L₁).toWord = FreeGroup.reduce L₁

source

@[simp]

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

(FreeAddGroup.mk L₁).toWord = FreeAddGroup.reduce L₁

source

@[simp]

theorem FreeGroup.toWord_of {α : Type u_1} [DecidableEq α] (a : α) :

(FreeGroup.of a).toWord = [(a, true)]

source

@[simp]

theorem FreeAddGroup.toWord_of {α : Type u_1} [DecidableEq α] (a : α) :

(FreeAddGroup.of a).toWord = [(a, true)]

source

@[simp]

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

FreeGroup.reduce x.toWord = x.toWord

source

@[simp]

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

FreeAddGroup.reduce x.toWord = x.toWord

source

@[simp]

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

FreeGroup.toWord 1 = []

source

@[simp]

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

FreeAddGroup.toWord 0 = []

source

@[simp]

theorem FreeGroup.toWord_of_pow {α : Type u_1} [DecidableEq α] (a : α) (n : ℕ) :

(FreeGroup.of a ^ n).toWord = List.replicate n (a, true)

source

@[simp]

theorem FreeAddGroup.toWord_of_nsmul {α : Type u_1} [DecidableEq α] (a : α) (n : ℕ) :

(n • FreeAddGroup.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)} :

FreeGroup.reduce (FreeGroup.invRev w) = FreeGroup.invRev (FreeGroup.reduce w)

source

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

FreeAddGroup.reduce (FreeAddGroup.negRev w) = FreeAddGroup.negRev (FreeAddGroup.reduce w)

source

@[simp]

theorem FreeGroup.toWord_inv {α : Type u_1} [DecidableEq α] (x : FreeGroup α) :

x⁻¹.toWord = FreeGroup.invRev x.toWord

source

@[simp]

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

(-x).toWord = FreeAddGroup.negRev x.toWord

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 : FreeGroup.Red L₁ L₂) (H13 : FreeGroup.Red L₁ L₃) :

{ L₄ : List (α × Bool) // FreeGroup.Red L₂ L₄ ∧ FreeGroup.Red L₃ L₄ }

Constructive Church-Rosser theorem (compare church_rosser).

Equations

FreeGroup.reduce.churchRosser H12 H13 = ⟨FreeGroup.reduce L₁, ⋯⟩

Instances For

source

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

{ L₄ : List (α × Bool) // FreeAddGroup.Red L₂ L₄ ∧ FreeAddGroup.Red L₃ L₄ }

Constructive Church-Rosser theorem (compare church_rosser).

Equations

FreeAddGroup.reduce.churchRosser H12 H13 = ⟨FreeAddGroup.reduce L₁, ⋯⟩

Instances For

source

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

DecidableEq (FreeGroup α)

Equations

FreeGroup.instDecidableEq = ⋯.decidableEq

source

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

DecidableEq (FreeAddGroup α)

Equations

FreeAddGroup.instDecidableEq = ⋯.decidableEq

source

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

DecidableRel FreeGroup.Red

Equations

One or more equations did not get rendered due to their size.
FreeGroup.Red.decidableRel [] [] = isTrue ⋯
FreeGroup.Red.decidableRel [] (_hd2 :: _tl2) = isFalse ⋯
FreeGroup.Red.decidableRel ((x_2, b) :: tl) [] = match FreeGroup.Red.decidableRel tl [(x_2, !b)] with | isTrue H => isTrue ⋯ | isFalse H => isFalse ⋯

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

FreeGroup.Red.enum L₁ = List.filter (fun (b : List (α × Bool)) => decide (FreeGroup.Red L₁ b)) L₁.sublists

Instances For

source

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

FreeGroup.Red L₁ L₂

source

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

L₂ ∈ FreeGroup.Red.enum L₁

source

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

Fintype { L₂ : List (α × Bool) // FreeGroup.Red L₁ L₂ }

Equations

FreeGroup.instFintypeSubtypeListProdBoolRed L₁ = Fintype.subtype (FreeGroup.Red.enum L₁).toFinset ⋯

source

@[simp]

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

1 ≠ FreeGroup.of a

source

@[simp]

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

0 ≠ FreeAddGroup.of a

source

@[simp]

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

FreeGroup.of a ≠ 1

source

@[simp]

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

FreeAddGroup.of a ≠ 0

source

theorem FreeGroup.instNontrivialOfNonempty {α : Type u_1} [Nonempty α] :

Nontrivial (FreeGroup α)

source

theorem 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

x.norm = x.toWord.length

Instances For

source

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

ℕ

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

Equations

x.norm = x.toWord.length

Instances For

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 α] :

FreeGroup.norm 1 = 0

source

@[simp]

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

FreeAddGroup.norm 0 = 0

source

@[simp]

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

(FreeGroup.of a).norm = 1

source

@[simp]

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

(FreeAddGroup.of a).norm = 1

source

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

(FreeGroup.mk L₁).norm ≤ L₁.length

source

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

(FreeAddGroup.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 : ℕ) :

(FreeGroup.of a ^ n).norm = n

source

@[simp]

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

(n • FreeAddGroup.of a).norm = n

source

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

Function.Surjective FreeGroup.norm

source

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

Function.Surjective FreeAddGroup.norm

Documentation

Mathlib.GroupTheory.FreeGroup.Reduce

The maximal reduction of a word in a free group #

Main declarations #