This file defines some extra lemmas for free groups, in particular about cyclically reduced words.

Main declarations

• FreeGroup.IsCyclicallyReduced: the predicate for cyclically reduced words

def FreeGroup.IsCyclicallyReduced {α : Type u} (L : List (α × Bool)) : Prop

Predicate asserting that the word L is cyclically reduced, i.e., it is reduced and furthermore the first and the last letter of the word do not cancel. The empty word is by convention also cyclically reduced.

Equations

• FreeGroup.IsCyclicallyReduced L = (FreeGroup.IsReduced L ∧ ∀ a ∈ L.getLast?, ∀ b ∈ L.head?, a.1 = b.1 → a.2 = b.2)

def FreeAddGroup.IsCyclicallyReduced {α : Type u} (L : List (α × Bool)) : Prop

Predicate asserting that the word L is cyclically reduced, i.e., it is reduced and furthermore the first and the last letter of the word do not cancel. The empty word is by convention also cyclically reduced.

Equations

• FreeAddGroup.IsCyclicallyReduced L = (FreeAddGroup.IsReduced L ∧ ∀ a ∈ L.getLast?, ∀ b ∈ L.head?, a.1 = b.1 → a.2 = b.2)

theorem FreeGroup.isCyclicallyReduced_iff {α : Type u} {L : List (α × Bool)} : IsCyclicallyReduced L ↔ IsReduced L ∧ ∀ a ∈ L.getLast?, ∀ b ∈ L.head?, a.1 = b.1 → a.2 = b.2

theorem FreeAddGroup.isCyclicallyReduced_iff {α : Type u} {L : List (α × Bool)} : IsCyclicallyReduced L ↔ IsReduced L ∧ ∀ a ∈ L.getLast?, ∀ b ∈ L.head?, a.1 = b.1 → a.2 = b.2

theorem FreeGroup.isCyclicallyReduced_cons_append_iff {α : Type u} {L : List (α × Bool)} {a b : α × Bool} : IsCyclicallyReduced (b :: L ++ [a]) ↔ IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)

theorem FreeAddGroup.isCyclicallyReduced_cons_append_iff {α : Type u} {L : List (α × Bool)} {a b : α × Bool} : IsCyclicallyReduced (b :: L ++ [a]) ↔ IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)

@[simp]

theorem FreeGroup.IsCyclicallyReduced.nil {α : Type u} : IsCyclicallyReduced []

@[simp]

theorem FreeAddGroup.IsCyclicallyReduced.nil {α : Type u} : IsCyclicallyReduced []

@[simp]

theorem FreeGroup.IsCyclicallyReduced.singleton {α : Type u} {x : α × Bool} : IsCyclicallyReduced [x]

@[simp]

theorem FreeAddGroup.IsCyclicallyReduced.singleton {α : Type u} {x : α × Bool} : IsCyclicallyReduced [x]

theorem FreeGroup.IsCyclicallyReduced.isReduced {α : Type u} {L : List (α × Bool)} (h : IsCyclicallyReduced L) : IsReduced L

theorem FreeAddGroup.IsCyclicallyReduced.isReduced {α : Type u} {L : List (α × Bool)} (h : IsCyclicallyReduced L) : IsReduced L

theorem FreeGroup.IsCyclicallyReduced.flatten_replicate {α : Type u} {L : List (α × Bool)} (n : ℕ) (h : IsCyclicallyReduced L) : IsCyclicallyReduced (List.replicate n L).flatten

theorem FreeAddGroup.IsCyclicallyReduced.flatten_replicate {α : Type u} {L : List (α × Bool)} (n : ℕ) (h : IsCyclicallyReduced L) : IsCyclicallyReduced (List.replicate n L).flatten

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

This function produces a subword of a word w by cancelling the first and last letters of w as long as possible. If w is reduced, the resulting word will be cyclically reduced.

Equations

• One or more equations did not get rendered due to their size.

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

This function produces a subword of a word w by cancelling the first and last letters of w as long as possible. If w is reduced, the resulting word will be cyclically reduced.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FreeGroup.reduceCyclically.nil {α : Type u} [DecidableEq α] : reduceCyclically [] = []

@[simp]

theorem FreeAddGroup.reduceCyclically.nil {α : Type u} [DecidableEq α] : reduceCyclically [] = []

@[simp]

theorem FreeGroup.reduceCyclically.singleton {α : Type u} [DecidableEq α] {a : α × Bool} : reduceCyclically [a] = [a]

@[simp]

theorem FreeAddGroup.reduceCyclically.singleton {α : Type u} [DecidableEq α] {a : α × Bool} : reduceCyclically [a] = [a]

theorem FreeGroup.reduceCyclically.cons_append {α : Type u} [DecidableEq α] {a b : α × Bool} (l : List (α × Bool)) : reduceCyclically (a :: (l ++ [b])) = if b.1 = a.1 ∧ (!b.2) = a.2 then reduceCyclically l else a :: l ++ [b]

theorem FreeAddGroup.reduceCyclically.cons_append {α : Type u} [DecidableEq α] {a b : α × Bool} (l : List (α × Bool)) : reduceCyclically (a :: (l ++ [b])) = if b.1 = a.1 ∧ (!b.2) = a.2 then reduceCyclically l else a :: l ++ [b]

theorem FreeGroup.reduceCyclically.isCyclicallyReduced {α : Type u} [DecidableEq α] (w : List (α × Bool)) (h : IsReduced w) : IsCyclicallyReduced (reduceCyclically w)

theorem FreeAddGroup.reduceCyclically.isCyclicallyReduced {α : Type u} [DecidableEq α] (w : List (α × Bool)) (h : IsReduced w) : IsCyclicallyReduced (reduceCyclically w)

def FreeGroup.reduceCyclically.conjugator {α : Type u} [DecidableEq α] : List (α × Bool) → List (α × Bool)

Partner function to reduceCyclically. See reduceCyclically.conjugation.

Equations

• One or more equations did not get rendered due to their size.

def FreeAddGroup.reduceCyclically.conjugator {α : Type u} [DecidableEq α] : List (α × Bool) → List (α × Bool)

Partner function to reduceCyclically. See reduceCyclically.conjugation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FreeGroup.reduceCyclically.conjugator.nil {α : Type u} [DecidableEq α] : conjugator [] = []

@[simp]

theorem FreeAddGroup.reduceCyclically.conjugator.nil {α : Type u} [DecidableEq α] : conjugator [] = []

@[simp]

theorem FreeGroup.reduceCyclically.conjugator.singleton {α : Type u} [DecidableEq α] {a : α × Bool} : conjugator [a] = []

@[simp]

theorem FreeAddGroup.reduceCyclically.conjugator.singleton {α : Type u} [DecidableEq α] {a : α × Bool} : conjugator [a] = []

theorem FreeGroup.reduceCyclically.conjugator.cons_append {α : Type u} [DecidableEq α] {a b : α × Bool} (l : List (α × Bool)) : conjugator (a :: (l ++ [b])) = if b.1 = a.1 ∧ (!b.2) = a.2 then a :: conjugator l else []

theorem FreeAddGroup.reduceCyclically.conjugator.cons_append {α : Type u} [DecidableEq α] {a b : α × Bool} (l : List (α × Bool)) : conjugator (a :: (l ++ [b])) = if b.1 = a.1 ∧ (!b.2) = a.2 then a :: conjugator l else []

theorem FreeGroup.reduceCyclically.conj_conjugator_reduceCyclically {α : Type u} [DecidableEq α] (w : List (α × Bool)) : conjugator w ++ reduceCyclically w ++ invRev (conjugator w) = w

theorem FreeAddGroup.reduceCyclically.conj_conjugator_reduceCyclically {α : Type u} [DecidableEq α] (w : List (α × Bool)) : conjugator w ++ reduceCyclically w ++ negRev (conjugator w) = w