Free groups

This file defines free groups over a type. Furthermore, it is shown that the free group construction is an instance of a monad. For the result that FreeGroup is the left adjoint to the forgetful functor from groups to types, see Algebra/Category/Group/Adjunctions.

Main definitions

• FreeGroup/FreeAddGroup: the free group (resp. free additive group) associated to a type α defined as the words over a : α × Bool modulo the relation a * x * x⁻¹ * b = a * b.
• FreeGroup.mk/FreeAddGroup.mk: the canonical quotient map List (α × Bool) → FreeGroup α.
• FreeGroup.of/FreeAddGroup.of: the canonical injection α → FreeGroup α.
• FreeGroup.lift f/FreeAddGroup.lift: the canonical group homomorphism FreeGroup α →* G given a group G and a function f : α → G.

Main statements

• FreeGroup.Red.church_rosser/FreeAddGroup.Red.church_rosser: The Church-Rosser theorem for word reduction (also known as Newman's diamond lemma).
• FreeGroup.freeGroupUnitEquivInt: The free group over the one-point type is isomorphic to the integers.
• The free group construction is an instance of a monad.

Implementation details

First we introduce the one step reduction relation FreeGroup.Red.Step: w * x * x⁻¹ * v ~> w * v, its reflexive transitive closure FreeGroup.Red.trans and prove that its join is an equivalence relation. Then we introduce FreeGroup α as a quotient over FreeGroup.Red.Step.

For the additive version we introduce the same relation under a different name so that we can distinguish the quotient types more easily.

Tags

free group, Newman's diamond lemma, Church-Rosser theorem

inductive FreeAddGroup.Red.Step {α : Type u} : List (α × Bool) → List (α × Bool) → Prop

Reduction step for the additive free group relation: w + x + (-x) + v ~> w + v

• not: ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool}, FreeAddGroup.Red.Step (L₁ ++ (x, b) :: (x, !b) :: L₂) (L₁ ++ L₂)

inductive FreeGroup.Red.Step {α : Type u} : List (α × Bool) → List (α × Bool) → Prop

Reduction step for the multiplicative free group relation: w * x * x⁻¹ * v ~> w * v

• not: ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool}, FreeGroup.Red.Step (L₁ ++ (x, b) :: (x, !b) :: L₂) (L₁ ++ L₂)

def FreeAddGroup.Red {α : Type u} : List (α × Bool) → List (α × Bool) → Prop

Reflexive-transitive closure of Red.Step

Equations

• FreeAddGroup.Red = Relation.ReflTransGen FreeAddGroup.Red.Step

def FreeGroup.Red {α : Type u} : List (α × Bool) → List (α × Bool) → Prop

Reflexive-transitive closure of Red.Step

Equations

• FreeGroup.Red = Relation.ReflTransGen FreeGroup.Red.Step

theorem FreeAddGroup.Red.refl {α : Type u} {L : List (α × Bool)} : FreeAddGroup.Red L L

theorem FreeGroup.Red.refl {α : Type u} {L : List (α × Bool)} : FreeGroup.Red L L

theorem FreeAddGroup.Red.trans {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} : FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red L₂ L₃ → FreeAddGroup.Red L₁ L₃

theorem FreeGroup.Red.trans {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} : FreeGroup.Red L₁ L₂ → FreeGroup.Red L₂ L₃ → FreeGroup.Red L₁ L₃

theorem FreeAddGroup.Red.Step.length {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : FreeAddGroup.Red.Step L₁ L₂ → L₂.length + 2 = L₁.length

Predicate asserting that the word w₁ can be reduced to w₂ in one step, i.e. there are words w₃ w₄ and letter x such that w₁ = w₃ + x + (-x) + w₄ and w₂ = w₃w₄

theorem FreeGroup.Red.Step.length {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : FreeGroup.Red.Step L₁ L₂ → L₂.length + 2 = L₁.length

Predicate asserting that the word w₁ can be reduced to w₂ in one step, i.e. there are words w₃ w₄ and letter x such that w₁ = w₃xx⁻¹w₄ and w₂ = w₃w₄

@[simp]

theorem FreeAddGroup.Red.Step.not_rev {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {x : α} {b : Bool} : FreeAddGroup.Red.Step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)

@[simp]

theorem FreeGroup.Red.Step.not_rev {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {x : α} {b : Bool} : FreeGroup.Red.Step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)

@[simp]

theorem FreeAddGroup.Red.Step.cons_not {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool} : FreeAddGroup.Red.Step ((x, b) :: (x, !b) :: L) L

@[simp]

theorem FreeGroup.Red.Step.cons_not {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool} : FreeGroup.Red.Step ((x, b) :: (x, !b) :: L) L

@[simp]

theorem FreeAddGroup.Red.Step.cons_not_rev {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool} : FreeAddGroup.Red.Step ((x, !b) :: (x, b) :: L) L

@[simp]

theorem FreeGroup.Red.Step.cons_not_rev {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool} : FreeGroup.Red.Step ((x, !b) :: (x, b) :: L) L

theorem FreeAddGroup.Red.Step.append_left {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} : FreeAddGroup.Red.Step L₂ L₃ → FreeAddGroup.Red.Step (L₁ ++ L₂) (L₁ ++ L₃)

theorem FreeGroup.Red.Step.append_left {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} : FreeGroup.Red.Step L₂ L₃ → FreeGroup.Red.Step (L₁ ++ L₂) (L₁ ++ L₃)

theorem FreeAddGroup.Red.Step.cons {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {x : α × Bool} (H : FreeAddGroup.Red.Step L₁ L₂) : FreeAddGroup.Red.Step (x :: L₁) (x :: L₂)

theorem FreeGroup.Red.Step.cons {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {x : α × Bool} (H : FreeGroup.Red.Step L₁ L₂) : FreeGroup.Red.Step (x :: L₁) (x :: L₂)

theorem FreeAddGroup.Red.Step.append_right {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} : FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Red.Step (L₁ ++ L₃) (L₂ ++ L₃)

theorem FreeGroup.Red.Step.append_right {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} : FreeGroup.Red.Step L₁ L₂ → FreeGroup.Red.Step (L₁ ++ L₃) (L₂ ++ L₃)

theorem FreeAddGroup.Red.not_step_nil {α : Type u} {L : List (α × Bool)} : ¬FreeAddGroup.Red.Step [] L

theorem FreeGroup.Red.not_step_nil {α : Type u} {L : List (α × Bool)} : ¬FreeGroup.Red.Step [] L

theorem FreeAddGroup.Red.Step.cons_left_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {a : α} {b : Bool} : FreeAddGroup.Red.Step ((a, b) :: L₁) L₂ ↔ (∃ (L : List (α × Bool)), FreeAddGroup.Red.Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂

theorem FreeGroup.Red.Step.cons_left_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {a : α} {b : Bool} : FreeGroup.Red.Step ((a, b) :: L₁) L₂ ↔ (∃ (L : List (α × Bool)), FreeGroup.Red.Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂

theorem FreeAddGroup.Red.not_step_singleton {α : Type u} {L : List (α × Bool)} {p : α × Bool} : ¬FreeAddGroup.Red.Step [p] L

theorem FreeGroup.Red.not_step_singleton {α : Type u} {L : List (α × Bool)} {p : α × Bool} : ¬FreeGroup.Red.Step [p] L

theorem FreeAddGroup.Red.Step.cons_cons_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {p : α × Bool} : FreeAddGroup.Red.Step (p :: L₁) (p :: L₂) ↔ FreeAddGroup.Red.Step L₁ L₂

theorem FreeGroup.Red.Step.cons_cons_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {p : α × Bool} : FreeGroup.Red.Step (p :: L₁) (p :: L₂) ↔ FreeGroup.Red.Step L₁ L₂

theorem FreeAddGroup.Red.Step.append_left_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (L : List (α × Bool)) : FreeAddGroup.Red.Step (L ++ L₁) (L ++ L₂) ↔ FreeAddGroup.Red.Step L₁ L₂

theorem FreeGroup.Red.Step.append_left_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (L : List (α × Bool)) : FreeGroup.Red.Step (L ++ L₁) (L ++ L₂) ↔ FreeGroup.Red.Step L₁ L₂

theorem FreeAddGroup.Red.Step.diamond_aux {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} {L₄ : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool} : L₁ ++ (x1, b1) :: (x1, !b1) :: L₂ = L₃ ++ (x2, b2) :: (x2, !b2) :: L₄ → L₁ ++ L₂ = L₃ ++ L₄ ∨ ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step (L₁ ++ L₂) L₅ ∧ FreeAddGroup.Red.Step (L₃ ++ L₄) L₅

theorem FreeGroup.Red.Step.diamond_aux {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} {L₄ : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool} : L₁ ++ (x1, b1) :: (x1, !b1) :: L₂ = L₃ ++ (x2, b2) :: (x2, !b2) :: L₄ → L₁ ++ L₂ = L₃ ++ L₄ ∨ ∃ (L₅ : List (α × Bool)), FreeGroup.Red.Step (L₁ ++ L₂) L₅ ∧ FreeGroup.Red.Step (L₃ ++ L₄) L₅

theorem FreeAddGroup.Red.Step.diamond {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} {L₄ : List (α × Bool)} : FreeAddGroup.Red.Step L₁ L₃ → FreeAddGroup.Red.Step L₂ L₄ → L₁ = L₂ → L₃ = L₄ ∨ ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step L₃ L₅ ∧ FreeAddGroup.Red.Step L₄ L₅

theorem FreeGroup.Red.Step.diamond {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} {L₄ : List (α × Bool)} : FreeGroup.Red.Step L₁ L₃ → FreeGroup.Red.Step L₂ L₄ → L₁ = L₂ → L₃ = L₄ ∨ ∃ (L₅ : List (α × Bool)), FreeGroup.Red.Step L₃ L₅ ∧ FreeGroup.Red.Step L₄ L₅

theorem FreeAddGroup.Red.Step.to_red {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Red L₁ L₂

theorem FreeGroup.Red.Step.to_red {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : FreeGroup.Red.Step L₁ L₂ → FreeGroup.Red L₁ L₂

theorem FreeAddGroup.Red.church_rosser {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} : FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red L₁ L₃ → Relation.Join FreeAddGroup.Red L₂ L₃

Church-Rosser theorem for word reduction: If w1 w2 w3 are words such that w1 reduces to w2 and w3 respectively, then there is a word w4 such that w2 and w3 reduce to w4 respectively. This is also known as Newman's diamond lemma.

theorem FreeGroup.Red.church_rosser {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} : FreeGroup.Red L₁ L₂ → FreeGroup.Red L₁ L₃ → Relation.Join FreeGroup.Red L₂ L₃

Church-Rosser theorem for word reduction: If w1 w2 w3 are words such that w1 reduces to w2 and w3 respectively, then there is a word w4 such that w2 and w3 reduce to w4 respectively. This is also known as Newman's diamond lemma.

theorem FreeAddGroup.Red.cons_cons {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {p : α × Bool} : FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red (p :: L₁) (p :: L₂)

theorem FreeGroup.Red.cons_cons {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {p : α × Bool} : FreeGroup.Red L₁ L₂ → FreeGroup.Red (p :: L₁) (p :: L₂)

theorem FreeAddGroup.Red.cons_cons_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (p : α × Bool) : FreeAddGroup.Red (p :: L₁) (p :: L₂) ↔ FreeAddGroup.Red L₁ L₂

theorem FreeGroup.Red.cons_cons_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (p : α × Bool) : FreeGroup.Red (p :: L₁) (p :: L₂) ↔ FreeGroup.Red L₁ L₂

theorem FreeAddGroup.Red.append_append_left_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (L : List (α × Bool)) : FreeAddGroup.Red (L ++ L₁) (L ++ L₂) ↔ FreeAddGroup.Red L₁ L₂

theorem FreeGroup.Red.append_append_left_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (L : List (α × Bool)) : FreeGroup.Red (L ++ L₁) (L ++ L₂) ↔ FreeGroup.Red L₁ L₂

theorem FreeAddGroup.Red.append_append {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} {L₄ : List (α × Bool)} (h₁ : FreeAddGroup.Red L₁ L₃) (h₂ : FreeAddGroup.Red L₂ L₄) : FreeAddGroup.Red (L₁ ++ L₂) (L₃ ++ L₄)

theorem FreeGroup.Red.append_append {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} {L₄ : List (α × Bool)} (h₁ : FreeGroup.Red L₁ L₃) (h₂ : FreeGroup.Red L₂ L₄) : FreeGroup.Red (L₁ ++ L₂) (L₃ ++ L₄)

theorem FreeAddGroup.Red.to_append_iff {α : Type u} {L : List (α × Bool)} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : FreeAddGroup.Red L (L₁ ++ L₂) ↔ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ FreeAddGroup.Red L₃ L₁ ∧ FreeAddGroup.Red L₄ L₂

theorem FreeGroup.Red.to_append_iff {α : Type u} {L : List (α × Bool)} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : FreeGroup.Red L (L₁ ++ L₂) ↔ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ FreeGroup.Red L₃ L₁ ∧ FreeGroup.Red L₄ L₂

theorem FreeAddGroup.Red.nil_iff {α : Type u} {L : List (α × Bool)} : FreeAddGroup.Red [] L ↔ L = []

The empty word [] only reduces to itself.

theorem FreeGroup.Red.nil_iff {α : Type u} {L : List (α × Bool)} : FreeGroup.Red [] L ↔ L = []

The empty word [] only reduces to itself.

theorem FreeAddGroup.Red.singleton_iff {α : Type u} {L₁ : List (α × Bool)} {x : α × Bool} : FreeAddGroup.Red [x] L₁ ↔ L₁ = [x]

A letter only reduces to itself.

theorem FreeGroup.Red.singleton_iff {α : Type u} {L₁ : List (α × Bool)} {x : α × Bool} : FreeGroup.Red [x] L₁ ↔ L₁ = [x]

A letter only reduces to itself.

theorem FreeAddGroup.Red.cons_nil_iff_singleton {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool} : FreeAddGroup.Red ((x, b) :: L) [] ↔ FreeAddGroup.Red L [(x, !b)]

If x is a letter and w is a word such that x + w reduces to the empty word, then w reduces to -x.

theorem FreeGroup.Red.cons_nil_iff_singleton {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool} : FreeGroup.Red ((x, b) :: L) [] ↔ FreeGroup.Red L [(x, !b)]

If x is a letter and w is a word such that xw reduces to the empty word, then w reduces to x⁻¹

theorem FreeAddGroup.Red.red_iff_irreducible {α : Type u} {L : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool} (h : (x1, b1) ≠ (x2, b2)) : FreeAddGroup.Red [(x1, !b1), (x2, b2)] L ↔ L = [(x1, !b1), (x2, b2)]

theorem FreeGroup.Red.red_iff_irreducible {α : Type u} {L : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool} (h : (x1, b1) ≠ (x2, b2)) : FreeGroup.Red [(x1, !b1), (x2, b2)] L ↔ L = [(x1, !b1), (x2, b2)]

theorem FreeAddGroup.Red.neg_of_red_of_ne {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool} (H1 : (x1, b1) ≠ (x2, b2)) (H2 : FreeAddGroup.Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)) : FreeAddGroup.Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)

If x and y are distinct letters and w₁ w₂ are words such that x + w₁ reduces to y + w₂, then w₁ reduces to -x + y + w₂.

theorem FreeGroup.Red.inv_of_red_of_ne {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool} (H1 : (x1, b1) ≠ (x2, b2)) (H2 : FreeGroup.Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)) : FreeGroup.Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)

If x and y are distinct letters and w₁ w₂ are words such that xw₁ reduces to yw₂, then w₁ reduces to x⁻¹yw₂.

theorem FreeAddGroup.Red.Step.sublist {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (H : FreeAddGroup.Red.Step L₁ L₂) : L₂.Sublist L₁

theorem FreeGroup.Red.Step.sublist {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (H : FreeGroup.Red.Step L₁ L₂) : L₂.Sublist L₁

theorem FreeAddGroup.Red.sublist {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : FreeAddGroup.Red L₁ L₂ → L₂.Sublist L₁

If w₁ w₂ are words such that w₁ reduces to w₂, then w₂ is a sublist of w₁.

theorem FreeGroup.Red.sublist {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : FreeGroup.Red L₁ L₂ → L₂.Sublist L₁

If w₁ w₂ are words such that w₁ reduces to w₂, then w₂ is a sublist of w₁.

theorem FreeAddGroup.Red.length_le {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeAddGroup.Red L₁ L₂) : L₂.length ≤ L₁.length

theorem FreeGroup.Red.length_le {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeGroup.Red L₁ L₂) : L₂.length ≤ L₁.length

theorem FreeAddGroup.Red.sizeof_of_step {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : FreeAddGroup.Red.Step L₁ L₂ → sizeOf L₂ < sizeOf L₁

theorem FreeGroup.Red.sizeof_of_step {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : FreeGroup.Red.Step L₁ L₂ → sizeOf L₂ < sizeOf L₁

theorem FreeAddGroup.Red.length {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeAddGroup.Red L₁ L₂) : ∃ (n : ℕ), L₁.length = L₂.length + 2 * n

theorem FreeGroup.Red.length {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeGroup.Red L₁ L₂) : ∃ (n : ℕ), L₁.length = L₂.length + 2 * n

theorem FreeAddGroup.Red.antisymm {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h₁₂ : FreeAddGroup.Red L₁ L₂) (h₂₁ : FreeAddGroup.Red L₂ L₁) : L₁ = L₂

theorem FreeGroup.Red.antisymm {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h₁₂ : FreeGroup.Red L₁ L₂) (h₂₁ : FreeGroup.Red L₂ L₁) : L₁ = L₂

theorem FreeAddGroup.equivalence_join_red {α : Type u} : Equivalence (Relation.Join FreeAddGroup.Red)

theorem FreeGroup.equivalence_join_red {α : Type u} : Equivalence (Relation.Join FreeGroup.Red)

theorem FreeAddGroup.join_red_of_step {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeAddGroup.Red.Step L₁ L₂) : Relation.Join FreeAddGroup.Red L₁ L₂

theorem FreeGroup.join_red_of_step {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeGroup.Red.Step L₁ L₂) : Relation.Join FreeGroup.Red L₁ L₂

theorem FreeAddGroup.eqvGen_step_iff_join_red {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : Relation.EqvGen FreeAddGroup.Red.Step L₁ L₂ ↔ Relation.Join FreeAddGroup.Red L₁ L₂

theorem FreeGroup.eqvGen_step_iff_join_red {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : Relation.EqvGen FreeGroup.Red.Step L₁ L₂ ↔ Relation.Join FreeGroup.Red L₁ L₂

def FreeAddGroup (α : Type u) : Type u

The free additive group over a type, i.e. the words formed by the elements of the type and their formal inverses, quotient by one step reduction.

Equations

• FreeAddGroup α = Quot FreeAddGroup.Red.Step

def FreeGroup (α : Type u) : Type u

The free group over a type, i.e. the words formed by the elements of the type and their formal inverses, quotient by one step reduction.

Equations

• FreeGroup α = Quot FreeGroup.Red.Step

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

The canonical map from list (α × bool) to the free additive group on α.

Equations

• FreeAddGroup.mk L = Quot.mk FreeAddGroup.Red.Step L

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

The canonical map from List (α × Bool) to the free group on α.

Equations

• FreeGroup.mk L = Quot.mk FreeGroup.Red.Step L

@[simp]

theorem FreeAddGroup.quot_mk_eq_mk {α : Type u} {L : List (α × Bool)} : Quot.mk FreeAddGroup.Red.Step L = FreeAddGroup.mk L

@[simp]

theorem FreeGroup.quot_mk_eq_mk {α : Type u} {L : List (α × Bool)} : Quot.mk FreeGroup.Red.Step L = FreeGroup.mk L

@[simp]

theorem FreeAddGroup.quot_lift_mk {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool) → β) (H : ∀ (L₁ L₂ : List (α × Bool)), FreeAddGroup.Red.Step L₁ L₂ → f L₁ = f L₂) : Quot.lift f H (FreeAddGroup.mk L) = f L

@[simp]

theorem FreeGroup.quot_lift_mk {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool) → β) (H : ∀ (L₁ L₂ : List (α × Bool)), FreeGroup.Red.Step L₁ L₂ → f L₁ = f L₂) : Quot.lift f H (FreeGroup.mk L) = f L

@[simp]

theorem FreeAddGroup.quot_liftOn_mk {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool) → β) (H : ∀ (L₁ L₂ : List (α × Bool)), FreeAddGroup.Red.Step L₁ L₂ → f L₁ = f L₂) : Quot.liftOn (FreeAddGroup.mk L) f H = f L

@[simp]

theorem FreeGroup.quot_liftOn_mk {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool) → β) (H : ∀ (L₁ L₂ : List (α × Bool)), FreeGroup.Red.Step L₁ L₂ → f L₁ = f L₂) : Quot.liftOn (FreeGroup.mk L) f H = f L

@[simp]

theorem FreeAddGroup.quot_map_mk {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool) → List (β × Bool)) (H : (FreeAddGroup.Red.Step ⇒ FreeAddGroup.Red.Step) f f) : Quot.map f H (FreeAddGroup.mk L) = FreeAddGroup.mk (f L)

@[simp]

theorem FreeGroup.quot_map_mk {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool) → List (β × Bool)) (H : (FreeGroup.Red.Step ⇒ FreeGroup.Red.Step) f f) : Quot.map f H (FreeGroup.mk L) = FreeGroup.mk (f L)

instance FreeAddGroup.instZero {α : Type u} : Zero (FreeAddGroup α)

Equations

• FreeAddGroup.instZero = { zero := FreeAddGroup.mk [] }

instance FreeGroup.instOne {α : Type u} : One (FreeGroup α)

Equations

• FreeGroup.instOne = { one := FreeGroup.mk [] }

theorem FreeAddGroup.zero_eq_mk {α : Type u} : 0 = FreeAddGroup.mk []

theorem FreeGroup.one_eq_mk {α : Type u} : 1 = FreeGroup.mk []

instance FreeAddGroup.instInhabited {α : Type u} : Inhabited (FreeAddGroup α)

Equations

• FreeAddGroup.instInhabited = { default := 0 }

instance FreeGroup.instInhabited {α : Type u} : Inhabited (FreeGroup α)

Equations

• FreeGroup.instInhabited = { default := 1 }

instance FreeAddGroup.instUniqueOfIsEmpty {α : Type u} [IsEmpty α] : Unique (FreeAddGroup α)

Equations

• FreeAddGroup.instUniqueOfIsEmpty = id inferInstance

instance FreeGroup.instUniqueOfIsEmpty {α : Type u} [IsEmpty α] : Unique (FreeGroup α)

Equations

• FreeGroup.instUniqueOfIsEmpty = id inferInstance

instance FreeAddGroup.instAdd {α : Type u} : Add (FreeAddGroup α)

Equations

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

theorem FreeAddGroup.instAdd.proof_1 {α : Type u_1} (L₁ : List (α × Bool)) (_L₂ : List (α × Bool)) (_L₃ : List (α × Bool)) (H : FreeAddGroup.Red.Step _L₂ _L₃) : Quot.mk FreeAddGroup.Red.Step (L₁ ++ _L₂) = Quot.mk FreeAddGroup.Red.Step (L₁ ++ _L₃)

theorem FreeAddGroup.instAdd.proof_2 {α : Type u_1} (y : FreeAddGroup α) (_L₁ : List (α × Bool)) (_L₂ : List (α × Bool)) (H : FreeAddGroup.Red.Step _L₁ _L₂) : (fun (L₁ : List (α × Bool)) => Quot.liftOn y (fun (L₂ : List (α × Bool)) => FreeAddGroup.mk (L₁ ++ L₂)) ⋯) _L₁ = (fun (L₁ : List (α × Bool)) => Quot.liftOn y (fun (L₂ : List (α × Bool)) => FreeAddGroup.mk (L₁ ++ L₂)) ⋯) _L₂

instance FreeGroup.instMul {α : Type u} : Mul (FreeGroup α)

Equations

• FreeGroup.instMul = { mul := fun (x y : FreeGroup α) => Quot.liftOn x (fun (L₁ : List (α × Bool)) => Quot.liftOn y (fun (L₂ : List (α × Bool)) => FreeGroup.mk (L₁ ++ L₂)) ⋯) ⋯ }

@[simp]

theorem FreeAddGroup.add_mk {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : FreeAddGroup.mk L₁ + FreeAddGroup.mk L₂ = FreeAddGroup.mk (L₁ ++ L₂)

@[simp]

theorem FreeGroup.mul_mk {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : FreeGroup.mk L₁ * FreeGroup.mk L₂ = FreeGroup.mk (L₁ ++ L₂)

def FreeAddGroup.negRev {α : Type u} (w : List (α × Bool)) : List (α × Bool)

Transform a word representing a free group element into a word representing its negative.

Equations

• FreeAddGroup.negRev w = (List.map (fun (g : α × Bool) => (g.1, !g.2)) w).reverse

def FreeGroup.invRev {α : Type u} (w : List (α × Bool)) : List (α × Bool)

Transform a word representing a free group element into a word representing its inverse.

Equations

• FreeGroup.invRev w = (List.map (fun (g : α × Bool) => (g.1, !g.2)) w).reverse

@[simp]

theorem FreeAddGroup.negRev_length {α : Type u} {L₁ : List (α × Bool)} : (FreeAddGroup.negRev L₁).length = L₁.length

@[simp]

theorem FreeGroup.invRev_length {α : Type u} {L₁ : List (α × Bool)} : (FreeGroup.invRev L₁).length = L₁.length

@[simp]

theorem FreeAddGroup.negRev_negRev {α : Type u} {L₁ : List (α × Bool)} : FreeAddGroup.negRev (FreeAddGroup.negRev L₁) = L₁

@[simp]

theorem FreeGroup.invRev_invRev {α : Type u} {L₁ : List (α × Bool)} : FreeGroup.invRev (FreeGroup.invRev L₁) = L₁

@[simp]

theorem FreeAddGroup.negRev_empty {α : Type u} : FreeAddGroup.negRev [] = []

@[simp]

theorem FreeGroup.invRev_empty {α : Type u} : FreeGroup.invRev [] = []

theorem FreeAddGroup.negRev_involutive {α : Type u} : Function.Involutive FreeAddGroup.negRev

theorem FreeGroup.invRev_involutive {α : Type u} : Function.Involutive FreeGroup.invRev

theorem FreeAddGroup.negRev_injective {α : Type u} : Function.Injective FreeAddGroup.negRev

theorem FreeGroup.invRev_injective {α : Type u} : Function.Injective FreeGroup.invRev

theorem FreeAddGroup.negRev_surjective {α : Type u} : Function.Surjective FreeAddGroup.negRev

theorem FreeGroup.invRev_surjective {α : Type u} : Function.Surjective FreeGroup.invRev

theorem FreeAddGroup.negRev_bijective {α : Type u} : Function.Bijective FreeAddGroup.negRev

theorem FreeGroup.invRev_bijective {α : Type u} : Function.Bijective FreeGroup.invRev

instance FreeAddGroup.instNeg {α : Type u} : Neg (FreeAddGroup α)

Equations

• FreeAddGroup.instNeg = { neg := Quot.map FreeAddGroup.negRev ⋯ }

theorem FreeAddGroup.instNeg.proof_1 {α : Type u_1} ⦃a : List (α × Bool)⦄ ⦃b : List (α × Bool)⦄ (h : FreeAddGroup.Red.Step a b) : FreeAddGroup.Red.Step (FreeAddGroup.negRev a) (FreeAddGroup.negRev b)

instance FreeGroup.instInv {α : Type u} : Inv (FreeGroup α)

Equations

• FreeGroup.instInv = { inv := Quot.map FreeGroup.invRev ⋯ }

@[simp]

theorem FreeAddGroup.neg_mk {α : Type u} {L : List (α × Bool)} : -FreeAddGroup.mk L = FreeAddGroup.mk (FreeAddGroup.negRev L)

@[simp]

theorem FreeGroup.inv_mk {α : Type u} {L : List (α × Bool)} : (FreeGroup.mk L)⁻¹ = FreeGroup.mk (FreeGroup.invRev L)

theorem FreeAddGroup.Red.Step.negRev {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeAddGroup.Red.Step L₁ L₂) : FreeAddGroup.Red.Step (FreeAddGroup.negRev L₁) (FreeAddGroup.negRev L₂)

theorem FreeGroup.Red.Step.invRev {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeGroup.Red.Step L₁ L₂) : FreeGroup.Red.Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)

theorem FreeAddGroup.Red.negRev {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeAddGroup.Red L₁ L₂) : FreeAddGroup.Red (FreeAddGroup.negRev L₁) (FreeAddGroup.negRev L₂)

theorem FreeGroup.Red.invRev {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeGroup.Red L₁ L₂) : FreeGroup.Red (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)

@[simp]

theorem FreeAddGroup.Red.step_negRev_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : FreeAddGroup.Red.Step (FreeAddGroup.negRev L₁) (FreeAddGroup.negRev L₂) ↔ FreeAddGroup.Red.Step L₁ L₂

@[simp]

theorem FreeGroup.Red.step_invRev_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : FreeGroup.Red.Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂) ↔ FreeGroup.Red.Step L₁ L₂

@[simp]

theorem FreeAddGroup.red_negRev_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : FreeAddGroup.Red (FreeAddGroup.negRev L₁) (FreeAddGroup.negRev L₂) ↔ FreeAddGroup.Red L₁ L₂

@[simp]

theorem FreeGroup.red_invRev_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : FreeGroup.Red (FreeGroup.invRev L₁) (FreeGroup.invRev L₂) ↔ FreeGroup.Red L₁ L₂

theorem FreeAddGroup.instAddGroup.proof_5 {α : Type u_1} : ∀ (n : ℕ) (x : FreeAddGroup α), nsmulRecAuto (n + 1) x = nsmulRecAuto (n + 1) x

theorem FreeAddGroup.instAddGroup.proof_6 {α : Type u_1} : ∀ (a b : FreeAddGroup α), a - b = a - b

theorem FreeAddGroup.instAddGroup.proof_3 {α : Type u_1} : ∀ (a : FreeAddGroup α), a + 0 = a

theorem FreeAddGroup.instAddGroup.proof_9 {α : Type u_1} : ∀ (n : ℕ) (a : FreeAddGroup α), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a

theorem FreeAddGroup.instAddGroup.proof_2 {α : Type u_1} : ∀ (a : FreeAddGroup α), 0 + a = a

theorem FreeAddGroup.instAddGroup.proof_4 {α : Type u_1} : ∀ (x : FreeAddGroup α), nsmulRecAuto 0 x = nsmulRecAuto 0 x

instance FreeAddGroup.instAddGroup {α : Type u} : AddGroup (FreeAddGroup α)

Equations

• FreeAddGroup.instAddGroup = AddGroup.mk ⋯

theorem FreeAddGroup.instAddGroup.proof_1 {α : Type u_1} : ∀ (a b c : FreeAddGroup α), a + b + c = a + (b + c)

theorem FreeAddGroup.instAddGroup.proof_7 {α : Type u_1} : ∀ (a : FreeAddGroup α), zsmulRec 0 a = zsmulRec 0 a

theorem FreeAddGroup.instAddGroup.proof_8 {α : Type u_1} : ∀ (n : ℕ) (a : FreeAddGroup α), zsmulRec (↑n.succ) a = zsmulRec (↑n.succ) a

theorem FreeAddGroup.instAddGroup.proof_10 {α : Type u_1} : ∀ (a : FreeAddGroup α), -a + a = 0

instance FreeGroup.instGroup {α : Type u} : Group (FreeGroup α)

Equations

• FreeGroup.instGroup = Group.mk ⋯

@[simp]

theorem FreeAddGroup.nsmul_mk {α : Type u} {L : List (α × Bool)} (n : ℕ) : n • FreeAddGroup.mk L = FreeAddGroup.mk (List.replicate n L).join

@[simp]

theorem FreeGroup.pow_mk {α : Type u} {L : List (α × Bool)} (n : ℕ) : FreeGroup.mk L ^ n = FreeGroup.mk (List.replicate n L).join

def FreeAddGroup.of {α : Type u} (x : α) : FreeAddGroup α

of is the canonical injection from the type to the free group over that type by sending each element to the equivalence class of the letter that is the element.

Equations

• FreeAddGroup.of x = FreeAddGroup.mk [(x, true)]

def FreeGroup.of {α : Type u} (x : α) : FreeGroup α

of is the canonical injection from the type to the free group over that type by sending each element to the equivalence class of the letter that is the element.

Equations

• FreeGroup.of x = FreeGroup.mk [(x, true)]

theorem FreeAddGroup.Red.exact {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : FreeAddGroup.mk L₁ = FreeAddGroup.mk L₂ ↔ Relation.Join FreeAddGroup.Red L₁ L₂

theorem FreeGroup.Red.exact {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : FreeGroup.mk L₁ = FreeGroup.mk L₂ ↔ Relation.Join FreeGroup.Red L₁ L₂

theorem FreeAddGroup.of_injective {α : Type u} : Function.Injective FreeAddGroup.of

The canonical map from the type to the additive free group is an injection.

theorem FreeGroup.of_injective {α : Type u} : Function.Injective FreeGroup.of

The canonical map from the type to the free group is an injection.

def FreeAddGroup.Lift.aux {α : Type u} {β : Type v} [AddGroup β] (f : α → β) : List (α × Bool) → β

Given f : α → β with β an additive group, the canonical map list (α × bool) → β

Equations

• FreeAddGroup.Lift.aux f L = (List.map (fun (x : α × Bool) => bif x.2 then f x.1 else -f x.1) L).sum

def FreeGroup.Lift.aux {α : Type u} {β : Type v} [Group β] (f : α → β) : List (α × Bool) → β

Given f : α → β with β a group, the canonical map List (α × Bool) → β

Equations

• FreeGroup.Lift.aux f L = (List.map (fun (x : α × Bool) => bif x.2 then f x.1 else (f x.1)⁻¹) L).prod

theorem FreeAddGroup.Red.Step.lift {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {β : Type v} [AddGroup β] {f : α → β} (H : FreeAddGroup.Red.Step L₁ L₂) : FreeAddGroup.Lift.aux f L₁ = FreeAddGroup.Lift.aux f L₂

theorem FreeGroup.Red.Step.lift {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {β : Type v} [Group β] {f : α → β} (H : FreeGroup.Red.Step L₁ L₂) : FreeGroup.Lift.aux f L₁ = FreeGroup.Lift.aux f L₂

theorem FreeAddGroup.lift.proof_2 {α : Type u_1} {β : Type u_2} [AddGroup β] (f : α → β) : [fun (x : α) => (fun (x : α × Bool) => bif x.2 then f x.1 else -f x.1) (x, true)].sum = fun (x : α) => (fun (x : α × Bool) => bif x.2 then f x.1 else -f x.1) (x, true)

def FreeAddGroup.lift {α : Type u} {β : Type v} [AddGroup β] : (α → β) ≃ (FreeAddGroup α →+ β)

If β is an additive group, then any function from α to β extends uniquely to an additive group homomorphism from the free additive group over α to β

Equations

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

theorem FreeAddGroup.lift.proof_3 {α : Type u_1} {β : Type u_2} [AddGroup β] (g : FreeAddGroup α →+ β) : (fun (f : α → β) => AddMonoidHom.mk' (Quot.lift (FreeAddGroup.Lift.aux f) ⋯) ⋯) ((fun (g : FreeAddGroup α →+ β) => ⇑g ∘ FreeAddGroup.of) g) = g

theorem FreeAddGroup.lift.proof_1 {α : Type u_1} {β : Type u_2} [AddGroup β] (f : α → β) : ∀ (a b : FreeAddGroup α), Quot.lift (FreeAddGroup.Lift.aux f) ⋯ (a + b) = Quot.lift (FreeAddGroup.Lift.aux f) ⋯ a + Quot.lift (FreeAddGroup.Lift.aux f) ⋯ b

@[simp]

theorem FreeAddGroup.lift_symm_apply {α : Type u} {β : Type v} [AddGroup β] (g : FreeAddGroup α →+ β) : ∀ (a : α), FreeAddGroup.lift.symm g a = (⇑g ∘ FreeAddGroup.of) a

@[simp]

theorem FreeGroup.lift_symm_apply {α : Type u} {β : Type v} [Group β] (g : FreeGroup α →* β) : ∀ (a : α), FreeGroup.lift.symm g a = (⇑g ∘ FreeGroup.of) a

def FreeGroup.lift {α : Type u} {β : Type v} [Group β] : (α → β) ≃ (FreeGroup α →* β)

If β is a group, then any function from α to β extends uniquely to a group homomorphism from the free group over α to β

Equations

• FreeGroup.lift = { toFun := fun (f : α → β) => MonoidHom.mk' (Quot.lift (FreeGroup.Lift.aux f) ⋯) ⋯, invFun := fun (g : FreeGroup α →* β) => ⇑g ∘ FreeGroup.of, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem FreeAddGroup.lift.mk {α : Type u} {L : List (α × Bool)} {β : Type v} [AddGroup β] {f : α → β} : (FreeAddGroup.lift f) (FreeAddGroup.mk L) = (List.map (fun (x : α × Bool) => bif x.2 then f x.1 else -f x.1) L).sum

@[simp]

theorem FreeGroup.lift.mk {α : Type u} {L : List (α × Bool)} {β : Type v} [Group β] {f : α → β} : (FreeGroup.lift f) (FreeGroup.mk L) = (List.map (fun (x : α × Bool) => bif x.2 then f x.1 else (f x.1)⁻¹) L).prod

@[simp]

theorem FreeAddGroup.lift.of {α : Type u} {β : Type v} [AddGroup β] {f : α → β} {x : α} : (FreeAddGroup.lift f) (FreeAddGroup.of x) = f x

@[simp]

theorem FreeGroup.lift.of {α : Type u} {β : Type v} [Group β] {f : α → β} {x : α} : (FreeGroup.lift f) (FreeGroup.of x) = f x

theorem FreeAddGroup.lift.unique {α : Type u} {β : Type v} [AddGroup β] {f : α → β} (g : FreeAddGroup α →+ β) (hg : ∀ (x : α), g (FreeAddGroup.of x) = f x) {x : FreeAddGroup α} : g x = (FreeAddGroup.lift f) x

theorem FreeGroup.lift.unique {α : Type u} {β : Type v} [Group β] {f : α → β} (g : FreeGroup α →* β) (hg : ∀ (x : α), g (FreeGroup.of x) = f x) {x : FreeGroup α} : g x = (FreeGroup.lift f) x

theorem FreeAddGroup.ext_hom {α : Type u} {G : Type u_1} [AddGroup G] (f : FreeAddGroup α →+ G) (g : FreeAddGroup α →+ G) (h : ∀ (a : α), f (FreeAddGroup.of a) = g (FreeAddGroup.of a)) : f = g

Two homomorphisms out of a free additive group are equal if they are equal on generators. See note [partially-applied ext lemmas].

theorem FreeGroup.ext_hom_iff {α : Type u} {G : Type u_1} [Group G] {f : FreeGroup α →* G} {g : FreeGroup α →* G} : f = g ↔ ∀ (a : α), f (FreeGroup.of a) = g (FreeGroup.of a)

theorem FreeAddGroup.ext_hom_iff {α : Type u} {G : Type u_1} [AddGroup G] {f : FreeAddGroup α →+ G} {g : FreeAddGroup α →+ G} : f = g ↔ ∀ (a : α), f (FreeAddGroup.of a) = g (FreeAddGroup.of a)

theorem FreeGroup.ext_hom {α : Type u} {G : Type u_1} [Group G] (f : FreeGroup α →* G) (g : FreeGroup α →* G) (h : ∀ (a : α), f (FreeGroup.of a) = g (FreeGroup.of a)) : f = g

Two homomorphisms out of a free group are equal if they are equal on generators.

See note [partially-applied ext lemmas].

theorem FreeAddGroup.lift_of_eq_id (α : Type u_1) : FreeAddGroup.lift FreeAddGroup.of = AddMonoidHom.id (FreeAddGroup α)

theorem FreeGroup.lift_of_eq_id (α : Type u_1) : FreeGroup.lift FreeGroup.of = MonoidHom.id (FreeGroup α)

theorem FreeAddGroup.lift.of_eq {α : Type u} (x : FreeAddGroup α) : (FreeAddGroup.lift FreeAddGroup.of) x = x

theorem FreeGroup.lift.of_eq {α : Type u} (x : FreeGroup α) : (FreeGroup.lift FreeGroup.of) x = x

theorem FreeAddGroup.lift.range_le {α : Type u} {β : Type v} [AddGroup β] {f : α → β} {s : AddSubgroup β} (H : Set.range f ⊆ ↑s) : (FreeAddGroup.lift f).range ≤ s

theorem FreeGroup.lift.range_le {α : Type u} {β : Type v} [Group β] {f : α → β} {s : Subgroup β} (H : Set.range f ⊆ ↑s) : (FreeGroup.lift f).range ≤ s

theorem FreeAddGroup.lift.range_eq_closure {α : Type u} {β : Type v} [AddGroup β] {f : α → β} : (FreeAddGroup.lift f).range = AddSubgroup.closure (Set.range f)

theorem FreeGroup.lift.range_eq_closure {α : Type u} {β : Type v} [Group β] {f : α → β} : (FreeGroup.lift f).range = Subgroup.closure (Set.range f)

@[simp]

theorem FreeAddGroup.closure_range_of (α : Type u_1) : AddSubgroup.closure (Set.range FreeAddGroup.of) = ⊤

@[simp]

theorem FreeGroup.closure_range_of (α : Type u_1) : Subgroup.closure (Set.range FreeGroup.of) = ⊤

The generators of FreeGroup α generate FreeGroup α. That is, the subgroup closure of the set of generators equals ⊤.

theorem FreeAddGroup.map.proof_1 {α : Type u_1} {β : Type u_2} (f : α → β) (L₁ : List (α × Bool)) (L₂ : List (α × Bool)) (H : FreeAddGroup.Red.Step L₁ L₂) : FreeAddGroup.Red.Step (List.map (fun (x : α × Bool) => (f x.1, x.2)) L₁) (List.map (fun (x : α × Bool) => (f x.1, x.2)) L₂)

theorem FreeAddGroup.map.proof_2 {α : Type u_1} {β : Type u_2} (f : α → β) : ∀ (a b : FreeAddGroup α), Quot.map (List.map fun (x : α × Bool) => (f x.1, x.2)) ⋯ (a + b) = Quot.map (List.map fun (x : α × Bool) => (f x.1, x.2)) ⋯ a + Quot.map (List.map fun (x : α × Bool) => (f x.1, x.2)) ⋯ b

def FreeAddGroup.map {α : Type u} {β : Type v} (f : α → β) : FreeAddGroup α →+ FreeAddGroup β

Any function from α to β extends uniquely to an additive group homomorphism from the additive free group over α to the additive free group over β.

Equations

• FreeAddGroup.map f = AddMonoidHom.mk' (Quot.map (List.map fun (x : α × Bool) => (f x.1, x.2)) ⋯) ⋯

def FreeGroup.map {α : Type u} {β : Type v} (f : α → β) : FreeGroup α →* FreeGroup β

Any function from α to β extends uniquely to a group homomorphism from the free group over α to the free group over β.

Equations

• FreeGroup.map f = MonoidHom.mk' (Quot.map (List.map fun (x : α × Bool) => (f x.1, x.2)) ⋯) ⋯

@[simp]

theorem FreeAddGroup.map.mk {α : Type u} {L : List (α × Bool)} {β : Type v} {f : α → β} : (FreeAddGroup.map f) (FreeAddGroup.mk L) = FreeAddGroup.mk (List.map (fun (x : α × Bool) => (f x.1, x.2)) L)

@[simp]

theorem FreeGroup.map.mk {α : Type u} {L : List (α × Bool)} {β : Type v} {f : α → β} : (FreeGroup.map f) (FreeGroup.mk L) = FreeGroup.mk (List.map (fun (x : α × Bool) => (f x.1, x.2)) L)

@[simp]

theorem FreeAddGroup.map.id {α : Type u} (x : FreeAddGroup α) : (FreeAddGroup.map id) x = x

@[simp]

theorem FreeGroup.map.id {α : Type u} (x : FreeGroup α) : (FreeGroup.map id) x = x

@[simp]

theorem FreeAddGroup.map.id' {α : Type u} (x : FreeAddGroup α) : (FreeAddGroup.map fun (z : α) => z) x = x

@[simp]

theorem FreeGroup.map.id' {α : Type u} (x : FreeGroup α) : (FreeGroup.map fun (z : α) => z) x = x

theorem FreeAddGroup.map.comp {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) (x : FreeAddGroup α) : (FreeAddGroup.map g) ((FreeAddGroup.map f) x) = (FreeAddGroup.map (g ∘ f)) x

theorem FreeGroup.map.comp {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) (x : FreeGroup α) : (FreeGroup.map g) ((FreeGroup.map f) x) = (FreeGroup.map (g ∘ f)) x

@[simp]

theorem FreeAddGroup.map.of {α : Type u} {β : Type v} {f : α → β} {x : α} : (FreeAddGroup.map f) (FreeAddGroup.of x) = FreeAddGroup.of (f x)

@[simp]

theorem FreeGroup.map.of {α : Type u} {β : Type v} {f : α → β} {x : α} : (FreeGroup.map f) (FreeGroup.of x) = FreeGroup.of (f x)

theorem FreeAddGroup.map.unique {α : Type u} {β : Type v} {f : α → β} (g : FreeAddGroup α →+ FreeAddGroup β) (hg : ∀ (x : α), g (FreeAddGroup.of x) = FreeAddGroup.of (f x)) {x : FreeAddGroup α} : g x = (FreeAddGroup.map f) x

theorem FreeGroup.map.unique {α : Type u} {β : Type v} {f : α → β} (g : FreeGroup α →* FreeGroup β) (hg : ∀ (x : α), g (FreeGroup.of x) = FreeGroup.of (f x)) {x : FreeGroup α} : g x = (FreeGroup.map f) x

theorem FreeAddGroup.map_eq_lift {α : Type u} {β : Type v} {f : α → β} {x : FreeAddGroup α} : (FreeAddGroup.map f) x = (FreeAddGroup.lift (FreeAddGroup.of ∘ f)) x

theorem FreeGroup.map_eq_lift {α : Type u} {β : Type v} {f : α → β} {x : FreeGroup α} : (FreeGroup.map f) x = (FreeGroup.lift (FreeGroup.of ∘ f)) x

theorem FreeAddGroup.freeAddGroupCongr.proof_3 {α : Type u_1} {β : Type u_2} (e : α ≃ β) (a : FreeAddGroup α) (b : FreeAddGroup α) : (FreeAddGroup.map ⇑e) (a + b) = (FreeAddGroup.map ⇑e) a + (FreeAddGroup.map ⇑e) b

def FreeAddGroup.freeAddGroupCongr {α : Type u_1} {β : Type u_2} (e : α ≃ β) : FreeAddGroup α ≃+ FreeAddGroup β

Equivalent types give rise to additively equivalent additive free groups.

Equations

• FreeAddGroup.freeAddGroupCongr e = { toFun := ⇑(FreeAddGroup.map ⇑e), invFun := ⇑(FreeAddGroup.map ⇑e.symm), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

theorem FreeAddGroup.freeAddGroupCongr.proof_2 {α : Type u_2} {β : Type u_1} (e : α ≃ β) (x : FreeAddGroup β) : (FreeAddGroup.map ⇑e) ((FreeAddGroup.map ⇑e.symm) x) = x

theorem FreeAddGroup.freeAddGroupCongr.proof_1 {α : Type u_1} {β : Type u_2} (e : α ≃ β) (x : FreeAddGroup α) : (FreeAddGroup.map ⇑e.symm) ((FreeAddGroup.map ⇑e) x) = x

@[simp]

theorem FreeAddGroup.freeAddGroupCongr_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (a : FreeAddGroup α) : (FreeAddGroup.freeAddGroupCongr e) a = (FreeAddGroup.map ⇑e) a

@[simp]

theorem FreeGroup.freeGroupCongr_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (a : FreeGroup α) : (FreeGroup.freeGroupCongr e) a = (FreeGroup.map ⇑e) a

def FreeGroup.freeGroupCongr {α : Type u_1} {β : Type u_2} (e : α ≃ β) : FreeGroup α ≃* FreeGroup β

Equivalent types give rise to multiplicatively equivalent free groups.

The converse can be found in GroupTheory.FreeAbelianGroupFinsupp, as Equiv.of_freeGroupEquiv

Equations

• FreeGroup.freeGroupCongr e = { toFun := ⇑(FreeGroup.map ⇑e), invFun := ⇑(FreeGroup.map ⇑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem FreeAddGroup.freeAddGroupCongr_refl {α : Type u} : FreeAddGroup.freeAddGroupCongr (Equiv.refl α) = AddEquiv.refl (FreeAddGroup α)

@[simp]

theorem FreeGroup.freeGroupCongr_refl {α : Type u} : FreeGroup.freeGroupCongr (Equiv.refl α) = MulEquiv.refl (FreeGroup α)

@[simp]

theorem FreeAddGroup.freeAddGroupCongr_symm {α : Type u_1} {β : Type u_2} (e : α ≃ β) : (FreeAddGroup.freeAddGroupCongr e).symm = FreeAddGroup.freeAddGroupCongr e.symm

@[simp]

theorem FreeGroup.freeGroupCongr_symm {α : Type u_1} {β : Type u_2} (e : α ≃ β) : (FreeGroup.freeGroupCongr e).symm = FreeGroup.freeGroupCongr e.symm

theorem FreeAddGroup.freeAddGroupCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (f : β ≃ γ) : (FreeAddGroup.freeAddGroupCongr e).trans (FreeAddGroup.freeAddGroupCongr f) = FreeAddGroup.freeAddGroupCongr (e.trans f)

theorem FreeGroup.freeGroupCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (f : β ≃ γ) : (FreeGroup.freeGroupCongr e).trans (FreeGroup.freeGroupCongr f) = FreeGroup.freeGroupCongr (e.trans f)

def FreeAddGroup.sum {α : Type u} [AddGroup α] : FreeAddGroup α →+ α

If α is an additive group, then any function from α to α extends uniquely to an additive homomorphism from the additive free group over α to α.

Equations

• FreeAddGroup.sum = FreeAddGroup.lift id

def FreeGroup.prod {α : Type u} [Group α] : FreeGroup α →* α

If α is a group, then any function from α to α extends uniquely to a homomorphism from the free group over α to α. This is the multiplicative version of FreeGroup.sum.

Equations

• FreeGroup.prod = FreeGroup.lift id

@[simp]

theorem FreeAddGroup.sum_mk {α : Type u} {L : List (α × Bool)} [AddGroup α] : FreeAddGroup.sum (FreeAddGroup.mk L) = (List.map (fun (x : α × Bool) => bif x.2 then x.1 else -x.1) L).sum

@[simp]

theorem FreeGroup.prod_mk {α : Type u} {L : List (α × Bool)} [Group α] : FreeGroup.prod (FreeGroup.mk L) = (List.map (fun (x : α × Bool) => bif x.2 then x.1 else x.1⁻¹) L).prod

@[simp]

theorem FreeAddGroup.sum.of {α : Type u} [AddGroup α] {x : α} : FreeAddGroup.sum (FreeAddGroup.of x) = x

@[simp]

theorem FreeGroup.prod.of {α : Type u} [Group α] {x : α} : FreeGroup.prod (FreeGroup.of x) = x

theorem FreeAddGroup.sum.unique {α : Type u} [AddGroup α] (g : FreeAddGroup α →+ α) (hg : ∀ (x : α), g (FreeAddGroup.of x) = x) {x : FreeAddGroup α} : g x = FreeAddGroup.sum x

theorem FreeGroup.prod.unique {α : Type u} [Group α] (g : FreeGroup α →* α) (hg : ∀ (x : α), g (FreeGroup.of x) = x) {x : FreeGroup α} : g x = FreeGroup.prod x

theorem FreeAddGroup.lift_eq_sum_map {α : Type u} {β : Type v} [AddGroup β] {f : α → β} {x : FreeAddGroup α} : (FreeAddGroup.lift f) x = FreeAddGroup.sum ((FreeAddGroup.map f) x)

theorem FreeGroup.lift_eq_prod_map {α : Type u} {β : Type v} [Group β] {f : α → β} {x : FreeGroup α} : (FreeGroup.lift f) x = FreeGroup.prod ((FreeGroup.map f) x)

def FreeGroup.sum {α : Type u} [AddGroup α] (x : FreeGroup α) : α

If α is a group, then any function from α to α extends uniquely to a homomorphism from the free group over α to α. This is the additive version of Prod.

Equations

• x.sum = FreeGroup.prod x

@[simp]

theorem FreeGroup.sum_mk {α : Type u} {L : List (α × Bool)} [AddGroup α] : (FreeGroup.mk L).sum = (List.map (fun (x : α × Bool) => bif x.2 then x.1 else -x.1) L).sum

@[simp]

theorem FreeGroup.sum.of {α : Type u} [AddGroup α] {x : α} : (FreeGroup.of x).sum = x

@[simp]

theorem FreeGroup.sum.map_mul {α : Type u} [AddGroup α] {x : FreeGroup α} {y : FreeGroup α} : (x * y).sum = x.sum + y.sum

@[simp]

theorem FreeGroup.sum.map_one {α : Type u} [AddGroup α] : FreeGroup.sum 1 = 0

@[simp]

theorem FreeGroup.sum.map_inv {α : Type u} [AddGroup α] {x : FreeGroup α} : x⁻¹.sum = -x.sum

theorem FreeAddGroup.freeAddGroupEmptyEquivAddUnit.proof_1 : ∀ (x : FreeAddGroup Empty), (fun (x : Unit) => 0) ((fun (x : FreeAddGroup Empty) => ()) x) = x

def FreeAddGroup.freeAddGroupEmptyEquivAddUnit : FreeAddGroup Empty ≃ Unit

The bijection between the additive free group on the empty type, and a type with one element.

Equations

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

theorem FreeAddGroup.freeAddGroupEmptyEquivAddUnit.proof_2 : ∀ (x : Unit), (fun (x : FreeAddGroup Empty) => ()) ((fun (x : Unit) => 0) x) = x

def FreeGroup.freeGroupEmptyEquivUnit : FreeGroup Empty ≃ Unit

The bijection between the free group on the empty type, and a type with one element.

Equations

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

def FreeGroup.freeGroupUnitEquivInt : FreeGroup Unit ≃ ℤ

The bijection between the free group on a singleton, and the integers.

Equations

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

instance FreeAddGroup.instMonad : Monad FreeAddGroup

Equations

• FreeAddGroup.instMonad = Monad.mk

instance FreeGroup.instMonad : Monad FreeGroup

Equations

• FreeGroup.instMonad = Monad.mk

theorem FreeAddGroup.induction_on {α : Type u} {C : FreeAddGroup α → Prop} (z : FreeAddGroup α) (C1 : C 0) (Cp : ∀ (x : α), C (pure x)) (Ci : ∀ (x : α), C (pure x) → C (-pure x)) (Cm : ∀ (x y : FreeAddGroup α), C x → C y → C (x + y)) : C z

theorem FreeGroup.induction_on {α : Type u} {C : FreeGroup α → Prop} (z : FreeGroup α) (C1 : C 1) (Cp : ∀ (x : α), C (pure x)) (Ci : ∀ (x : α), C (pure x) → C (pure x)⁻¹) (Cm : ∀ (x y : FreeGroup α), C x → C y → C (x * y)) : C z

theorem FreeAddGroup.map_pure {α : Type u} {β : Type u} (f : α → β) (x : α) : f <$> pure x = pure (f x)

theorem FreeGroup.map_pure {α : Type u} {β : Type u} (f : α → β) (x : α) : f <$> pure x = pure (f x)

@[simp]

theorem FreeAddGroup.map_zero {α : Type u} {β : Type u} (f : α → β) : f <$> 0 = 0

@[simp]

theorem FreeGroup.map_one {α : Type u} {β : Type u} (f : α → β) : f <$> 1 = 1

@[simp]

theorem FreeAddGroup.map_add {α : Type u} {β : Type u} (f : α → β) (x : FreeAddGroup α) (y : FreeAddGroup α) : f <$> (x + y) = f <$> x + f <$> y

@[simp]

theorem FreeGroup.map_mul {α : Type u} {β : Type u} (f : α → β) (x : FreeGroup α) (y : FreeGroup α) : f <$> (x * y) = f <$> x * f <$> y

@[simp]

theorem FreeAddGroup.map_neg {α : Type u} {β : Type u} (f : α → β) (x : FreeAddGroup α) : f <$> (-x) = -f <$> x

@[simp]

theorem FreeGroup.map_inv {α : Type u} {β : Type u} (f : α → β) (x : FreeGroup α) : f <$> x⁻¹ = (f <$> x)⁻¹

theorem FreeAddGroup.pure_bind {α : Type u} {β : Type u} (f : α → FreeAddGroup β) (x : α) : pure x >>= f = f x

theorem FreeGroup.pure_bind {α : Type u} {β : Type u} (f : α → FreeGroup β) (x : α) : pure x >>= f = f x

@[simp]

theorem FreeAddGroup.zero_bind {α : Type u} {β : Type u} (f : α → FreeAddGroup β) : 0 >>= f = 0

@[simp]

theorem FreeGroup.one_bind {α : Type u} {β : Type u} (f : α → FreeGroup β) : 1 >>= f = 1

@[simp]

theorem FreeAddGroup.add_bind {α : Type u} {β : Type u} (f : α → FreeAddGroup β) (x : FreeAddGroup α) (y : FreeAddGroup α) : x + y >>= f = (x >>= f) + (y >>= f)

@[simp]

theorem FreeGroup.mul_bind {α : Type u} {β : Type u} (f : α → FreeGroup β) (x : FreeGroup α) (y : FreeGroup α) : x * y >>= f = (x >>= f) * (y >>= f)

@[simp]

theorem FreeAddGroup.neg_bind {α : Type u} {β : Type u} (f : α → FreeAddGroup β) (x : FreeAddGroup α) : -x >>= f = -(x >>= f)

@[simp]

theorem FreeGroup.inv_bind {α : Type u} {β : Type u} (f : α → FreeGroup β) (x : FreeGroup α) : x⁻¹ >>= f = (x >>= f)⁻¹

instance FreeAddGroup.instLawfulMonad : LawfulMonad FreeAddGroup

Equations

• FreeAddGroup.instLawfulMonad = ⋯

instance FreeGroup.instLawfulMonad : LawfulMonad FreeGroup

Equations

• FreeGroup.instLawfulMonad = ⋯

def FreeAddGroup.reduce {α : Type u} [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.

def FreeGroup.reduce {α : Type u} [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.

@[simp]

theorem FreeAddGroup.reduce.cons {α : Type u} {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

@[simp]

theorem FreeGroup.reduce.cons {α : Type u} {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

@[simp]

theorem FreeAddGroup.reduce_replicate {α : Type u} [DecidableEq α] (n : ℕ) (x : α × Bool) : FreeAddGroup.reduce (List.replicate n x) = List.replicate n x

@[simp]

theorem FreeGroup.reduce_replicate {α : Type u} [DecidableEq α] (n : ℕ) (x : α × Bool) : FreeGroup.reduce (List.replicate n x) = List.replicate n x

theorem FreeAddGroup.reduce.red {α : Type u} {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.

theorem FreeGroup.reduce.red {α : Type u} {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.

theorem FreeAddGroup.reduce.not {α : Type u} [DecidableEq α] {p : Prop} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} {x : α} {b : Bool} : FreeAddGroup.reduce L₁ = L₂ ++ (x, b) :: (x, !b) :: L₃ → p

theorem FreeGroup.reduce.not {α : Type u} [DecidableEq α] {p : Prop} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} {x : α} {b : Bool} : FreeGroup.reduce L₁ = L₂ ++ (x, b) :: (x, !b) :: L₃ → p

theorem FreeAddGroup.reduce.min {α : Type u} {L₁ : List (α × Bool)} {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.

theorem FreeGroup.reduce.min {α : Type u} {L₁ : List (α × Bool)} {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.

@[simp]

theorem FreeAddGroup.reduce.idem {α : Type u} {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.

@[simp]

theorem FreeGroup.reduce.idem {α : Type u} {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.

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

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

theorem FreeAddGroup.reduce.eq_of_red {α : Type u} {L₁ : List (α × Bool)} {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.

theorem FreeGroup.reduce.eq_of_red {α : Type u} {L₁ : List (α × Bool)} {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.

theorem FreeGroup.red.reduce_eq {α : Type u} {L₁ : List (α × Bool)} {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.

theorem FreeGroup.freeAddGroup.red.reduce_eq {α : Type u} {L₁ : List (α × Bool)} {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.

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

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

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

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

theorem FreeAddGroup.reduce.sound {α : Type u} {L₁ : List (α × Bool)} {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.

theorem FreeGroup.reduce.sound {α : Type u} {L₁ : List (α × Bool)} {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.

theorem FreeAddGroup.reduce.exact {α : Type u} {L₁ : List (α × Bool)} {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.

theorem FreeGroup.reduce.exact {α : Type u} {L₁ : List (α × Bool)} {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.

theorem FreeAddGroup.reduce.self {α : Type u} {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.

theorem FreeGroup.reduce.self {α : Type u} {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.

theorem FreeAddGroup.reduce.rev {α : Type u} {L₁ : List (α × Bool)} {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₁.

theorem FreeGroup.reduce.rev {α : Type u} {L₁ : List (α × Bool)} {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₁.

def FreeAddGroup.toWord {α : Type u} [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 ⋯

def FreeGroup.toWord {α : Type u} [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 ⋯

theorem FreeAddGroup.mk_toWord {α : Type u} [DecidableEq α] {x : FreeAddGroup α} : FreeAddGroup.mk x.toWord = x

theorem FreeGroup.mk_toWord {α : Type u} [DecidableEq α] {x : FreeGroup α} : FreeGroup.mk x.toWord = x

theorem FreeAddGroup.toWord_injective {α : Type u} [DecidableEq α] : Function.Injective FreeAddGroup.toWord

theorem FreeGroup.toWord_injective {α : Type u} [DecidableEq α] : Function.Injective FreeGroup.toWord

@[simp]

theorem FreeAddGroup.toWord_inj {α : Type u} [DecidableEq α] {x : FreeAddGroup α} {y : FreeAddGroup α} : x.toWord = y.toWord ↔ x = y

@[simp]

theorem FreeGroup.toWord_inj {α : Type u} [DecidableEq α] {x : FreeGroup α} {y : FreeGroup α} : x.toWord = y.toWord ↔ x = y

@[simp]

theorem FreeAddGroup.toWord_mk {α : Type u} {L₁ : List (α × Bool)} [DecidableEq α] : (FreeAddGroup.mk L₁).toWord = FreeAddGroup.reduce L₁

@[simp]

theorem FreeGroup.toWord_mk {α : Type u} {L₁ : List (α × Bool)} [DecidableEq α] : (FreeGroup.mk L₁).toWord = FreeGroup.reduce L₁

@[simp]

theorem FreeAddGroup.toWord_of {α : Type u} [DecidableEq α] (a : α) : (FreeAddGroup.of a).toWord = [(a, true)]

@[simp]

theorem FreeGroup.toWord_of {α : Type u} [DecidableEq α] (a : α) : (FreeGroup.of a).toWord = [(a, true)]

@[simp]

theorem FreeAddGroup.reduce_toWord {α : Type u} [DecidableEq α] (x : FreeAddGroup α) : FreeAddGroup.reduce x.toWord = x.toWord

@[simp]

theorem FreeGroup.reduce_toWord {α : Type u} [DecidableEq α] (x : FreeGroup α) : FreeGroup.reduce x.toWord = x.toWord

@[simp]

theorem FreeAddGroup.toWord_zero {α : Type u} [DecidableEq α] : FreeAddGroup.toWord 0 = []

@[simp]

theorem FreeGroup.toWord_one {α : Type u} [DecidableEq α] : FreeGroup.toWord 1 = []

@[simp]

theorem FreeAddGroup.toWord_of_nsmul {α : Type u} [DecidableEq α] (a : α) (n : ℕ) : (n • FreeAddGroup.of a).toWord = List.replicate n (a, true)

@[simp]

theorem FreeGroup.toWord_of_pow {α : Type u} [DecidableEq α] (a : α) (n : ℕ) : (FreeGroup.of a ^ n).toWord = List.replicate n (a, true)

@[simp]

theorem FreeAddGroup.toWord_eq_nil_iff {α : Type u} [DecidableEq α] {x : FreeAddGroup α} : x.toWord = [] ↔ x = 0

@[simp]

theorem FreeGroup.toWord_eq_nil_iff {α : Type u} [DecidableEq α] {x : FreeGroup α} : x.toWord = [] ↔ x = 1

theorem FreeAddGroup.reduce_negRev {α : Type u} [DecidableEq α] {w : List (α × Bool)} : FreeAddGroup.reduce (FreeAddGroup.negRev w) = FreeAddGroup.negRev (FreeAddGroup.reduce w)

theorem FreeGroup.reduce_invRev {α : Type u} [DecidableEq α] {w : List (α × Bool)} : FreeGroup.reduce (FreeGroup.invRev w) = FreeGroup.invRev (FreeGroup.reduce w)

theorem FreeAddGroup.toWord_neg {α : Type u} [DecidableEq α] {x : FreeAddGroup α} : (-x).toWord = FreeAddGroup.negRev x.toWord

theorem FreeGroup.toWord_inv {α : Type u} [DecidableEq α] {x : FreeGroup α} : x⁻¹.toWord = FreeGroup.invRev x.toWord

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

def FreeAddGroup.reduce.churchRosser {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {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₁, ⋯⟩

def FreeGroup.reduce.churchRosser {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {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₁, ⋯⟩

instance FreeAddGroup.instDecidableEq {α : Type u} [DecidableEq α] : DecidableEq (FreeAddGroup α)

Equations

• FreeAddGroup.instDecidableEq = ⋯.decidableEq

instance FreeGroup.instDecidableEq {α : Type u} [DecidableEq α] : DecidableEq (FreeGroup α)

Equations

• FreeGroup.instDecidableEq = ⋯.decidableEq

instance FreeGroup.Red.decidableRel {α : Type u} [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 ⋯

def FreeGroup.Red.enum {α : Type u} [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

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

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

instance FreeGroup.instFintypeSubtypeListProdBoolRed {α : Type u} {L₁ : List (α × Bool)} [DecidableEq α] : Fintype { L₂ : List (α × Bool) // FreeGroup.Red L₁ L₂ }

Equations

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

@[simp]

theorem FreeAddGroup.zero_ne_of {α : Type u} (a : α) : 0 ≠ FreeAddGroup.of a

@[simp]

theorem FreeGroup.one_ne_of {α : Type u} (a : α) : 1 ≠ FreeGroup.of a

@[simp]

theorem FreeAddGroup.of_ne_zero {α : Type u} (a : α) : FreeAddGroup.of a ≠ 0

@[simp]

theorem FreeGroup.of_ne_one {α : Type u} (a : α) : FreeGroup.of a ≠ 1

instance FreeAddGroup.instNontrivialOfNonempty {α : Type u} [Nonempty α] : Nontrivial (FreeAddGroup α)

Equations

• ⋯ = ⋯

instance FreeGroup.instNontrivialOfNonempty {α : Type u} [Nonempty α] : Nontrivial (FreeGroup α)

Equations

• ⋯ = ⋯

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

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

Equations

• x.norm = x.toWord.length

def FreeGroup.norm {α : Type u} [DecidableEq α] (x : FreeGroup α) : ℕ

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

Equations

• x.norm = x.toWord.length

@[simp]

theorem FreeAddGroup.norm_neg_eq {α : Type u} [DecidableEq α] {x : FreeAddGroup α} : (-x).norm = x.norm

@[simp]

theorem FreeGroup.norm_inv_eq {α : Type u} [DecidableEq α] {x : FreeGroup α} : x⁻¹.norm = x.norm

@[simp]

theorem FreeAddGroup.norm_eq_zero {α : Type u} [DecidableEq α] {x : FreeAddGroup α} : x.norm = 0 ↔ x = 0

@[simp]

theorem FreeGroup.norm_eq_zero {α : Type u} [DecidableEq α] {x : FreeGroup α} : x.norm = 0 ↔ x = 1

@[simp]

theorem FreeAddGroup.norm_zero {α : Type u} [DecidableEq α] : FreeAddGroup.norm 0 = 0

@[simp]

theorem FreeGroup.norm_one {α : Type u} [DecidableEq α] : FreeGroup.norm 1 = 0

@[simp]

theorem FreeAddGroup.norm_of {α : Type u} [DecidableEq α] (a : α) : (FreeAddGroup.of a).norm = 1

@[simp]

theorem FreeGroup.norm_of {α : Type u} [DecidableEq α] (a : α) : (FreeGroup.of a).norm = 1

theorem FreeAddGroup.norm_mk_le {α : Type u} {L₁ : List (α × Bool)} [DecidableEq α] : (FreeAddGroup.mk L₁).norm ≤ L₁.length

theorem FreeGroup.norm_mk_le {α : Type u} {L₁ : List (α × Bool)} [DecidableEq α] : (FreeGroup.mk L₁).norm ≤ L₁.length

theorem FreeAddGroup.norm_add_le {α : Type u} [DecidableEq α] (x : FreeAddGroup α) (y : FreeAddGroup α) : (x + y).norm ≤ x.norm + y.norm

theorem FreeGroup.norm_mul_le {α : Type u} [DecidableEq α] (x : FreeGroup α) (y : FreeGroup α) : (x * y).norm ≤ x.norm + y.norm

@[simp]

theorem FreeAddGroup.norm_of_nsmul {α : Type u} [DecidableEq α] (a : α) (n : ℕ) : (n • FreeAddGroup.of a).norm = n

@[simp]

theorem FreeGroup.norm_of_pow {α : Type u} [DecidableEq α] (a : α) (n : ℕ) : (FreeGroup.of a ^ n).norm = n

theorem FreeAddGroup.norm_surjective {α : Type u} [DecidableEq α] [Nonempty α] : Function.Surjective FreeAddGroup.norm

theorem FreeGroup.norm_surjective {α : Type u} [DecidableEq α] [Nonempty α] : Function.Surjective FreeGroup.norm