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.

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.

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.

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.

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

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

Partner function to reduceCyclically. See reduceCyclically.conj_conjugator_reduceCyclically.

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