This file defines some extra lemmas for free groups, in particular about cyclically reduced words. We show that free groups are (strongly) torsion-free in the sense of IsMulTorsionFree, i.e., taking powers by every non-zero element n : ℕ is injective.

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)} (h : IsCyclicallyReduced L) (n : ℕ) : IsCyclicallyReduced (List.replicate n L).flatten

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

theorem FreeGroup.IsReduced.append_flatten_replicate_append {α : Type u} {L₁ L₂ L₃ : List (α × Bool)} (h₁ : IsCyclicallyReduced L₂) (h₂ : IsReduced (L₁ ++ L₂ ++ L₃)) {n : ℕ} (hn : n ≠ 0) : IsReduced (L₁ ++ (List.replicate n L₂).flatten ++ L₃)

theorem FreeAddGroup.IsReduced.append_flatten_replicate_append {α : Type u} {L₁ L₂ L₃ : List (α × Bool)} (h₁ : IsCyclicallyReduced L₂) (h₂ : IsReduced (L₁ ++ L₂ ++ L₃)) {n : ℕ} (hn : n ≠ 0) : IsReduced (L₁ ++ (List.replicate n L₂).flatten ++ L₃)

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

This function produces a subword of a word L by cancelling the first and last letters of L as long as possible. If L 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 L by cancelling the first and last letters of L as long as possible. If L 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} {L : List (α × Bool)} [DecidableEq α] (h : IsReduced L) : IsCyclicallyReduced (reduceCyclically L)

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

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

Partner function to reduceCyclically. See reduceCyclically.conj_conjugator_reduceCyclically.

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

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 α] (L : List (α × Bool)) : conjugator L ++ reduceCyclically L ++ invRev (conjugator L) = L

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

theorem FreeGroup.reduceCyclically.reduce_flatten_replicate_succ {α : Type u} {L : List (α × Bool)} [DecidableEq α] (h : IsReduced L) (n : ℕ) : reduce (List.replicate (n + 1) L).flatten = conjugator L ++ (List.replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)

theorem FreeAddGroup.reduceCyclically.reduce_flatten_replicate_succ {α : Type u} {L : List (α × Bool)} [DecidableEq α] (h : IsReduced L) (n : ℕ) : reduce (List.replicate (n + 1) L).flatten = conjugator L ++ (List.replicate (n + 1) (reduceCyclically L)).flatten ++ negRev (conjugator L)

theorem FreeGroup.reduceCyclically.reduce_flatten_replicate {α : Type u} {L : List (α × Bool)} [DecidableEq α] (h : IsReduced L) (n : ℕ) : reduce (List.replicate n L).flatten = if n = 0 then [] else conjugator L ++ (List.replicate n (reduceCyclically L)).flatten ++ invRev (conjugator L)

theorem FreeAddGroup.reduceCyclically.reduce_flatten_replicate {α : Type u} {L : List (α × Bool)} [DecidableEq α] (h : IsReduced L) (n : ℕ) : reduce (List.replicate n L).flatten = if n = 0 then [] else conjugator L ++ (List.replicate n (reduceCyclically L)).flatten ++ negRev (conjugator L)

instance FreeGroup.instIsMulTorsionFree {α : Type u} : IsMulTorsionFree (FreeGroup α)

Free groups are torsion-free, i.e., taking powers is injective. Our proof idea is as follows: if x ^ n = y ^ n, then also x ^ (2 * n) = y ^ (2 * n). We then compare the reduced words representing the powers in terms of the cyclic reductions of x.toWord and y.toWord using reduce_flatten_replicate. We conclude that the cyclic reductions of x.toWord and y.toWord must have the same length, and in fact they have to agree.

instance FreeAddGroup.instIsAddTorsionFree {α : Type u} : IsAddTorsionFree (FreeAddGroup α)

Free additive groups are torsion free, i.e., scalar multiplication by every non-zero element n : ℕ is injective. See the instance for free groups for an overview over the proof.