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₃

abbrev FreeAddGroup.Red.Step.length.match_1 {α : Type u_1} (motive : (x x_1 : List (α × Bool)) → FreeAddGroup.Red.Step x x_1 → Prop) : ∀ (x x_1 : List (α × Bool)) (x_2 : FreeAddGroup.Red.Step x x_1), (∀ (L1 L2 : List (α × Bool)) (x : α) (b : Bool), motive (L1 ++ (x, b) :: (x, !b) :: L2) (L1 ++ L2) (_ : FreeAddGroup.Red.Step (L1 ++ (x, b) :: (x, !b) :: L2) (L1 ++ L2))) → motive x x_1 x_2

Equations

• (_ : motive x✝¹ x✝ x) = (_ : motive x✝¹ x✝ x)

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

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₂ → List.length L₂ + 2 = List.length L₁

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

abbrev FreeAddGroup.Red.Step.append_left.match_1 {α : Type u_1} (motive : List (α × Bool) → (x x_1 : List (α × Bool)) → FreeAddGroup.Red.Step x x_1 → Prop) : ∀ (x x_1 x_2 : List (α × Bool)) (x_3 : FreeAddGroup.Red.Step x_1 x_2), (∀ (x L₁ L₂ : List (α × Bool)) (x_4 : α) (b : Bool), motive x (L₁ ++ (x_4, b) :: (x_4, !b) :: L₂) (L₁ ++ L₂) (_ : FreeAddGroup.Red.Step (L₁ ++ (x_4, b) :: (x_4, !b) :: L₂) (L₁ ++ L₂))) → motive x x_1 x_2 x_3

Equations

• (_ : motive x✝² x✝¹ x✝ x) = (_ : motive x✝² x✝¹ x✝ x)

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₂)

abbrev FreeAddGroup.Red.Step.append_right.match_1 {α : Type u_1} (motive : (x x_1 : List (α × Bool)) → List (α × Bool) → FreeAddGroup.Red.Step x x_1 → Prop) : ∀ (x x_1 x_2 : List (α × Bool)) (x_3 : FreeAddGroup.Red.Step x x_1), (∀ (x L₁ L₂ : List (α × Bool)) (x_4 : α) (b : Bool), motive (L₁ ++ (x_4, b) :: (x_4, !b) :: L₂) (L₁ ++ L₂) x (_ : FreeAddGroup.Red.Step (L₁ ++ (x_4, b) :: (x_4, !b) :: L₂) (L₁ ++ L₂))) → motive x x_1 x_2 x_3

Equations

• (_ : motive x✝² x✝¹ x✝ x) = (_ : motive x✝² x✝¹ x✝ x)

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₂

abbrev FreeAddGroup.Red.not_step_singleton.match_1 {α : Type u_1} (motive : α × Bool → Prop) : ∀ (x : α × Bool), (∀ (a : α) (b : Bool), motive (a, b)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

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₂

abbrev FreeAddGroup.Red.Step.append_left_iff.match_1 {α : Type u_1} (motive : List (α × Bool) → Prop) : ∀ (x : List (α × Bool)), (Unit → motive []) → (∀ (p : α × Bool) (l : List (α × Bool)), motive (p :: l)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

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₂

abbrev FreeAddGroup.Red.Step.diamond_aux.match_1 {α : Type u_1} (tl : List (α × Bool)) : ∀ (x tl2 x_1 : List (α × Bool)) (motive : (tl ++ x = tl2 ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step (tl ++ x) L₅ ∧ FreeAddGroup.Red.Step (tl2 ++ x_1) L₅) → Prop) (x_2 : tl ++ x = tl2 ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step (tl ++ x) L₅ ∧ FreeAddGroup.Red.Step (tl2 ++ x_1) L₅), (∀ (H3 : tl ++ x = tl2 ++ x_1), motive (_ : tl ++ x = tl2 ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step (tl ++ x) L₅ ∧ FreeAddGroup.Red.Step (tl2 ++ x_1) L₅)) → (∀ (L₅ : List (α × Bool)) (H3 : FreeAddGroup.Red.Step (tl ++ x) L₅) (H4 : FreeAddGroup.Red.Step (tl2 ++ x_1) L₅), motive (_ : tl ++ x = tl2 ++ x_1 ∨ ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step (tl ++ x) L₅ ∧ FreeAddGroup.Red.Step (tl2 ++ x_1) L₅)) → motive x_2

Equations

• (_ : motive x) = (_ : motive x)

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₅

abbrev FreeAddGroup.Red.Step.diamond_aux.match_2 {α : Type u_1} (x3 : α) (b3 : Bool) (tl : List (α × Bool)) : ∀ (x : List (α × Bool)) (x4 : α) (b4 : Bool) (tl2 x_1 : List (α × Bool)) (x_2 : α) (x_3 : Bool) (x_4 : α) (x_5 : Bool) (motive : (x3, b3) = (x4, b4) ∧ List.append tl ((x_2, x_3) :: (x_2, !x_3) :: x) = List.append tl2 ((x_4, x_5) :: (x_4, !x_5) :: x_1) → Prop) (x_6 : (x3, b3) = (x4, b4) ∧ List.append tl ((x_2, x_3) :: (x_2, !x_3) :: x) = List.append tl2 ((x_4, x_5) :: (x_4, !x_5) :: x_1)), (∀ (H1 : (x3, b3) = (x4, b4)) (H2 : List.append tl ((x_2, x_3) :: (x_2, !x_3) :: x) = List.append tl2 ((x_4, x_5) :: (x_4, !x_5) :: x_1)), motive (_ : (x3, b3) = (x4, b4) ∧ List.append tl ((x_2, x_3) :: (x_2, !x_3) :: x) = List.append tl2 ((x_4, x_5) :: (x_4, !x_5) :: x_1))) → motive x_6

Equations

• (_ : motive x) = (_ : motive x)

abbrev FreeAddGroup.Red.Step.diamond_aux.match_3 {α : Type u_1} (motive : (x x_1 x_2 x_3 : List (α × Bool)) → (x_4 : α) → (x_5 : Bool) → (x_6 : α) → (x_7 : Bool) → x ++ (x_4, x_5) :: (x_4, !x_5) :: x_1 = x_2 ++ (x_6, x_7) :: (x_6, !x_7) :: x_3 → Prop) : ∀ (x x_1 x_2 x_3 : List (α × Bool)) (x_4 : α) (x_5 : Bool) (x_6 : α) (x_7 : Bool) (x_8 : x ++ (x_4, x_5) :: (x_4, !x_5) :: x_1 = x_2 ++ (x_6, x_7) :: (x_6, !x_7) :: x_3), (∀ (x x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α) (x_13 : Bool) (H : [] ++ (x_10, x_11) :: (x_10, !x_11) :: x = [] ++ (x_12, x_13) :: (x_12, !x_13) :: x_9), motive [] x [] x_9 x_10 x_11 x_12 x_13 H) → (∀ (x : List (α × Bool)) (x3 : α) (b3 : Bool) (x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α) (x_13 : Bool) (H : [] ++ (x_10, x_11) :: (x_10, !x_11) :: x = [(x3, b3)] ++ (x_12, x_13) :: (x_12, !x_13) :: x_9), motive [] x [(x3, b3)] x_9 x_10 x_11 x_12 x_13 H) → (∀ (x3 : α) (b3 : Bool) (x x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α) (x_13 : Bool) (H : [(x3, b3)] ++ (x_10, x_11) :: (x_10, !x_11) :: x = [] ++ (x_12, x_13) :: (x_12, !x_13) :: x_9), motive [(x3, b3)] x [] x_9 x_10 x_11 x_12 x_13 H) → (∀ (x : List (α × Bool)) (x3 : α) (b3 : Bool) (x4 : α) (b4 : Bool) (tl x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α) (x_13 : Bool) (H : [] ++ (x_10, x_11) :: (x_10, !x_11) :: x = (x3, b3) :: (x4, b4) :: tl ++ (x_12, x_13) :: (x_12, !x_13) :: x_9), motive [] x ((x3, b3) :: (x4, b4) :: tl) x_9 x_10 x_11 x_12 x_13 H) → (∀ (x3 : α) (b3 : Bool) (x4 : α) (b4 : Bool) (tl x x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α) (x_13 : Bool) (H : (x3, b3) :: (x4, b4) :: tl ++ (x_10, x_11) :: (x_10, !x_11) :: x = [] ++ (x_12, x_13) :: (x_12, !x_13) :: x_9), motive ((x3, b3) :: (x4, b4) :: tl) x [] x_9 x_10 x_11 x_12 x_13 H) → (∀ (x3 : α) (b3 : Bool) (tl x : List (α × Bool)) (x4 : α) (b4 : Bool) (tl2 x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α) (x_13 : Bool) (H : (x3, b3) :: tl ++ (x_10, x_11) :: (x_10, !x_11) :: x = (x4, b4) :: tl2 ++ (x_12, x_13) :: (x_12, !x_13) :: x_9), motive ((x3, b3) :: tl) x ((x4, b4) :: tl2) x_9 x_10 x_11 x_12 x_13 H) → motive x x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8

Equations

• (_ : motive x✝⁷ x✝⁶ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ x) = (_ : motive x✝⁷ x✝⁶ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ x)

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₅

abbrev FreeAddGroup.Red.Step.diamond.match_1 {α : Type u_1} (motive : (x x_1 x_2 x_3 : List (α × Bool)) → FreeAddGroup.Red.Step x x_2 → FreeAddGroup.Red.Step x_1 x_3 → x = x_1 → Prop) : ∀ (x x_1 x_2 x_3 : List (α × Bool)) (x_4 : FreeAddGroup.Red.Step x x_2) (x_5 : FreeAddGroup.Red.Step x_1 x_3) (x_6 : x = x_1), (∀ (L₁ L₂ : List (α × Bool)) (x : α) (b : Bool) (L₁_1 L₂_1 : List (α × Bool)) (x_7 : α) (b_1 : Bool) (H : L₁ ++ (x, b) :: (x, !b) :: L₂ = L₁_1 ++ (x_7, b_1) :: (x_7, !b_1) :: L₂_1), motive (L₁ ++ (x, b) :: (x, !b) :: L₂) (L₁_1 ++ (x_7, b_1) :: (x_7, !b_1) :: L₂_1) (L₁ ++ L₂) (L₁_1 ++ L₂_1) (_ : FreeAddGroup.Red.Step (L₁ ++ (x, b) :: (x, !b) :: L₂) (L₁ ++ L₂)) (_ : FreeAddGroup.Red.Step (L₁_1 ++ (x_7, b_1) :: (x_7, !b_1) :: L₂_1) (L₁_1 ++ L₂_1)) H) → motive x x_1 x_2 x_3 x_4 x_5 x_6

Equations

• (_ : motive x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ x) = (_ : motive x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ x)

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.

abbrev FreeAddGroup.Red.church_rosser.match_1 {α : Type u_1} (a : List (α × Bool)) (motive : (b c : List (α × Bool)) → (b = c ∨ ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step b L₅ ∧ FreeAddGroup.Red.Step c L₅) → FreeAddGroup.Red.Step a b → FreeAddGroup.Red.Step a c → Prop) : ∀ (b c : List (α × Bool)) (x : b = c ∨ ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step b L₅ ∧ FreeAddGroup.Red.Step c L₅) (hab : FreeAddGroup.Red.Step a b) (hac : FreeAddGroup.Red.Step a c), (∀ (b : List (α × Bool)) (hab hac : FreeAddGroup.Red.Step a b), motive b b (_ : b = b ∨ ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step b L₅ ∧ FreeAddGroup.Red.Step b L₅) hab hac) → (∀ (b c d : List (α × Bool)) (hbd : FreeAddGroup.Red.Step b d) (hcd : FreeAddGroup.Red.Step c d) (hab : FreeAddGroup.Red.Step a b) (hac : FreeAddGroup.Red.Step a c), motive b c (_ : b = c ∨ ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step b L₅ ∧ FreeAddGroup.Red.Step c L₅) hab hac) → motive b c x hab hac

Equations

• (_ : motive b c x hab hac) = (_ : motive b c x hab hac)

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₄)

abbrev FreeAddGroup.Red.to_append_iff.match_1 {α : Type u_1} {L : List (α × Bool)} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (motive : (∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ FreeAddGroup.Red L₃ L₁ ∧ FreeAddGroup.Red L₄ L₂) → Prop) : ∀ (x : ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ FreeAddGroup.Red L₃ L₁ ∧ FreeAddGroup.Red L₄ L₂), (∀ (L₃ L₄ : List (α × Bool)) (Eq : L = L₃ ++ L₄) (h₃ : FreeAddGroup.Red L₃ L₁) (h₄ : FreeAddGroup.Red L₄ L₂), motive (_ : ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ FreeAddGroup.Red L₃ L₁ ∧ FreeAddGroup.Red L₄ L₂)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

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.

abbrev FreeAddGroup.Red.cons_nil_iff_singleton.match_1 {α : Type u_1} {L : List (α × Bool)} {x : α} {b : Bool} (motive : Relation.Join FreeAddGroup.Red [(x, !b)] L → Prop) : ∀ (x_1 : Relation.Join FreeAddGroup.Red [(x, !b)] L), (∀ (L' : List (α × Bool)) (h₁ : FreeAddGroup.Red [(x, !b)] L') (h₂ : FreeAddGroup.Red L L'), motive (_ : ∃ (c : List (α × Bool)), FreeAddGroup.Red [(x, !b)] c ∧ FreeAddGroup.Red L c)) → motive x_1

Equations

• (_ : motive x) = (_ : motive 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₂) : List.Sublist L₂ L₁

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

theorem FreeAddGroup.Red.sublist {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} : FreeAddGroup.Red L₁ L₂ → List.Sublist L₂ 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₂ → List.Sublist L₂ 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₂) : List.length L₂ ≤ List.length L₁

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

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 : ℕ), List.length L₁ = List.length L₂ + 2 * n

theorem FreeGroup.Red.length {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeGroup.Red L₁ L₂) : ∃ (n : ℕ), List.length L₁ = List.length L₂ + 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)} : 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)} : 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.instZeroFreeAddGroup {α : Type u} : Zero (FreeAddGroup α)

Equations

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

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

Equations

• FreeGroup.instOneFreeGroup = { 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.instInhabitedFreeAddGroup {α : Type u} : Inhabited (FreeAddGroup α)

Equations

• FreeAddGroup.instInhabitedFreeAddGroup = { default := 0 }

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

Equations

• FreeGroup.instInhabitedFreeGroup = { default := 1 }

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

Equations

• FreeAddGroup.instUniqueFreeAddGroup = id inferInstance

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

Equations

• FreeGroup.instUniqueFreeGroup = id inferInstance

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

Equations

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

theorem FreeAddGroup.instAddFreeAddGroup.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.instAddFreeAddGroup.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₂ _L₃ : List (α × Bool)), FreeAddGroup.Red.Step _L₂ _L₃ → Quot.mk FreeAddGroup.Red.Step (L₁ ++ _L₂) = Quot.mk FreeAddGroup.Red.Step (L₁ ++ _L₃))) _L₁ = (fun (L₁ : List (α × Bool)) => Quot.liftOn y (fun (L₂ : List (α × Bool)) => FreeAddGroup.mk (L₁ ++ L₂)) (_ : ∀ (_L₂ _L₃ : List (α × Bool)), FreeAddGroup.Red.Step _L₂ _L₃ → Quot.mk FreeAddGroup.Red.Step (L₁ ++ _L₂) = Quot.mk FreeAddGroup.Red.Step (L₁ ++ _L₃))) _L₂

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

Equations

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

@[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.reverse (List.map (fun (g : α × Bool) => (g.1, !g.2)) w)

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.reverse (List.map (fun (g : α × Bool) => (g.1, !g.2)) w)

@[simp]

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

@[simp]

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

@[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.instNegFreeAddGroup {α : Type u} : Neg (FreeAddGroup α)

Equations

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

theorem FreeAddGroup.instNegFreeAddGroup.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.instInvFreeGroup {α : Type u} : Inv (FreeGroup α)

Equations

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

@[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.instAddGroupFreeAddGroup.proof_10 {α : Type u_1} : ∀ (a : FreeAddGroup α), -a + a = 0

theorem FreeAddGroup.instAddGroupFreeAddGroup.proof_8 {α : Type u_1} : ∀ (n : ℕ) (a : FreeAddGroup α), zsmulRec (Int.ofNat (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) a

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

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

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

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

Equations

• FreeAddGroup.instAddGroupFreeAddGroup = AddGroup.mk (_ : ∀ (a : FreeAddGroup α), -a + a = 0)

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

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

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

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

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

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

Equations

• FreeGroup.instGroupFreeGroup = Group.mk (_ : ∀ (a : FreeGroup α), a⁻¹ * a = 1)

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.

abbrev FreeAddGroup.of_injective.match_1 {α : Type u_1} : ∀ (x x_1 : α) (motive : Relation.Join FreeAddGroup.Red [(x, true)] [(x_1, true)] → Prop) (x_2 : Relation.Join FreeAddGroup.Red [(x, true)] [(x_1, true)]), (∀ (L₁ : List (α × Bool)) (hx : FreeAddGroup.Red [(x, true)] L₁) (hy : FreeAddGroup.Red [(x_1, true)] L₁), motive (_ : ∃ (c : List (α × Bool)), FreeAddGroup.Red [(x, true)] c ∧ FreeAddGroup.Red [(x_1, true)] c)) → motive x_2

Equations

• (_ : motive x) = (_ : motive x)

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.sum (List.map (fun (x : α × Bool) => bif x.2 then f x.1 else -f x.1) L)

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.prod (List.map (fun (x : α × Bool) => bif x.2 then f x.1 else (f x.1)⁻¹) L)

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_1 {α : Type u_1} {β : Type u_2} [AddGroup β] (f : α → β) : ∀ (a b : FreeAddGroup α), Quot.lift (FreeAddGroup.Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Lift.aux f L₁ = FreeAddGroup.Lift.aux f L₂) (a + b) = Quot.lift (FreeAddGroup.Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Lift.aux f L₁ = FreeAddGroup.Lift.aux f L₂) a + Quot.lift (FreeAddGroup.Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Lift.aux f L₁ = FreeAddGroup.Lift.aux f L₂) b

theorem FreeAddGroup.lift.proof_3 {α : Type u_2} {β : Type u_1} [AddGroup β] (g : FreeAddGroup α →+ β) : (fun (f : α → β) => AddMonoidHom.mk' (Quot.lift (FreeAddGroup.Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Lift.aux f L₁ = FreeAddGroup.Lift.aux f L₂)) (_ : ∀ (a b : FreeAddGroup α), Quot.lift (FreeAddGroup.Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Lift.aux f L₁ = FreeAddGroup.Lift.aux f L₂) (a + b) = Quot.lift (FreeAddGroup.Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Lift.aux f L₁ = FreeAddGroup.Lift.aux f L₂) a + Quot.lift (FreeAddGroup.Lift.aux f) (_ : ∀ (L₁ L₂ : List (α × Bool)), FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Lift.aux f L₁ = FreeAddGroup.Lift.aux f L₂) b)) ((fun (g : FreeAddGroup α →+ β) => ⇑g ∘ FreeAddGroup.of) g) = g

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_2 {α : Type u_1} {β : Type u_2} [AddGroup β] (f : α → β) : (0 + fun (x : α) => (fun (x : α × Bool) => bif x.2 then f x.1 else -f x.1) (x, true)) = fun (x : α) => (fun (x : α × Bool) => bif x.2 then f x.1 else -f x.1) (x, true)

@[simp]

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

@[simp]

theorem FreeAddGroup.lift_symm_apply {α : Type u} {β : Type v} [AddGroup β] (g : FreeAddGroup α →+ β) : ∀ (a : α), FreeAddGroup.lift.symm g a = (⇑g ∘ FreeAddGroup.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

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

@[simp]

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

@[simp]

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

@[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 {α : 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 {α : 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) : AddMonoidHom.range (FreeAddGroup.lift f) ≤ s

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

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

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

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

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

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)) (_ : ∀ (L₁ L₂ : List (α × Bool)), 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₂)) (a + b) = Quot.map (List.map fun (x : α × Bool) => (f x.1, x.2)) (_ : ∀ (L₁ L₂ : List (α × Bool)), 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₂)) a + Quot.map (List.map fun (x : α × Bool) => (f x.1, x.2)) (_ : ∀ (L₁ L₂ : List (α × Bool)), 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₂)) b

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

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

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

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

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 FreeGroup.freeGroupCongr_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (a : FreeGroup α) : (FreeGroup.freeGroupCongr e) a = (FreeGroup.map ⇑e) a

@[simp]

theorem FreeAddGroup.freeAddGroupCongr_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (a : FreeAddGroup α) : (FreeAddGroup.freeAddGroupCongr e) a = (FreeAddGroup.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

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

@[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 : α ≃ β) : AddEquiv.symm (FreeAddGroup.freeAddGroupCongr e) = FreeAddGroup.freeAddGroupCongr e.symm

@[simp]

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

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

theorem FreeGroup.freeGroupCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (f : β ≃ γ) : MulEquiv.trans (FreeGroup.freeGroupCongr e) (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.sum (List.map (fun (x : α × Bool) => bif x.2 then x.1 else -x.1) L)

@[simp]

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

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

• FreeGroup.sum x = FreeGroup.prod x

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FreeGroup.sum.map_inv {α : Type u} [AddGroup α] {x : FreeGroup α} : FreeGroup.sum x⁻¹ = -FreeGroup.sum 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.

abbrev FreeAddGroup.freeAddGroupEmptyEquivAddUnit.match_1 (motive : Unit → Prop) : ∀ (x : Unit), (Unit → motive PUnit.unit) → motive x

Equations

• (_ : motive x) = (_ : motive x)

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

theorem FreeAddGroup.freeAddGroupEmptyEquivAddUnit.proof_1 : ∀ (x : FreeAddGroup Empty), (fun (x : Unit) => 0) ((fun (x : FreeAddGroup Empty) => ()) 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.instMonadFreeAddGroup : Monad FreeAddGroup

Equations

• FreeAddGroup.instMonadFreeAddGroup = Monad.mk

instance FreeGroup.instMonadFreeGroup : Monad FreeGroup

Equations

• FreeGroup.instMonadFreeGroup = 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.instLawfulMonadFreeAddGroupInstMonadFreeAddGroup : LawfulMonad FreeAddGroup

Equations

• FreeAddGroup.instLawfulMonadFreeAddGroupInstMonadFreeAddGroup = (_ : LawfulMonad FreeAddGroup)

instance FreeGroup.instLawfulMonadFreeGroupInstMonadFreeGroup : LawfulMonad FreeGroup

Equations

• FreeGroup.instLawfulMonadFreeGroupInstMonadFreeGroup = (_ : LawfulMonad FreeGroup)

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

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.

abbrev FreeAddGroup.reduce.not.match_1 {α : Type u_1} (motive : List (α × Bool) → List (α × Bool) → List (α × Bool) → α → Bool → Prop) : ∀ (x x_1 x_2 : List (α × Bool)) (x_3 : α) (x_4 : Bool), (∀ (L2 L3 : List (α × Bool)) (x : α) (x_5 : Bool), motive [] L2 L3 x x_5) → (∀ (x : α) (b : Bool) (L1 L2 L3 : List (α × Bool)) (x' : α) (b' : Bool), motive ((x, b) :: L1) L2 L3 x' b') → motive x x_1 x_2 x_3 x_4

Equations

• (_ : motive x✝³ x✝² x✝¹ x✝ x) = (_ : motive x✝³ x✝² x✝¹ x✝ x)

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.

abbrev FreeAddGroup.reduce.Step.eq.match_1 {α : Type u_1} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (motive : Relation.Join FreeAddGroup.Red (FreeAddGroup.reduce L₁) (FreeAddGroup.reduce L₂) → Prop) : ∀ (x : Relation.Join FreeAddGroup.Red (FreeAddGroup.reduce L₁) (FreeAddGroup.reduce L₂)), (∀ (_L₃ : List (α × Bool)) (HR13 : FreeAddGroup.Red (FreeAddGroup.reduce L₁) _L₃) (HR23 : FreeAddGroup.Red (FreeAddGroup.reduce L₂) _L₃), motive (_ : ∃ (c : List (α × Bool)), FreeAddGroup.Red (FreeAddGroup.reduce L₁) c ∧ FreeAddGroup.Red (FreeAddGroup.reduce L₂) c)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

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.

abbrev FreeAddGroup.reduce.sound.match_1 {α : Type u_1} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (motive : Relation.Join FreeAddGroup.Red L₁ L₂ → Prop) : ∀ (x : Relation.Join FreeAddGroup.Red L₁ L₂), (∀ (_L₃ : List (α × Bool)) (H13 : FreeAddGroup.Red L₁ _L₃) (H23 : FreeAddGroup.Red L₂ _L₃), motive (_ : ∃ (c : List (α × Bool)), FreeAddGroup.Red L₁ c ∧ FreeAddGroup.Red L₂ c)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

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 (_ : ∀ (_L₁ _L₂ : List (α × Bool)), FreeAddGroup.Red.Step _L₁ _L₂ → FreeAddGroup.reduce _L₁ = FreeAddGroup.reduce _L₂)

theorem FreeAddGroup.toWord.proof_1 {α : Type u_1} [DecidableEq α] (_L₁ : List (α × Bool)) (_L₂ : List (α × Bool)) (H : FreeAddGroup.Red.Step _L₁ _L₂) : FreeAddGroup.reduce _L₁ = FreeAddGroup.reduce _L₂

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 (_ : ∀ (_L₁ _L₂ : List (α × Bool)), FreeGroup.Red.Step _L₁ _L₂ → FreeGroup.reduce _L₁ = FreeGroup.reduce _L₂)

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

theorem FreeGroup.mk_toWord {α : Type u} [DecidableEq α] {x : FreeGroup α} : FreeGroup.mk (FreeGroup.toWord x) = 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 α} : FreeAddGroup.toWord x = FreeAddGroup.toWord y ↔ x = y

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[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_eq_nil_iff {α : Type u} [DecidableEq α] {x : FreeAddGroup α} : FreeAddGroup.toWord x = [] ↔ x = 0

@[simp]

theorem FreeGroup.toWord_eq_nil_iff {α : Type u} [DecidableEq α] {x : FreeGroup α} : FreeGroup.toWord x = [] ↔ 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 α} : FreeAddGroup.toWord (-x) = FreeAddGroup.negRev (FreeAddGroup.toWord x)

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

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 = { val := FreeAddGroup.reduce L₁, property := (_ : FreeAddGroup.Red L₂ (FreeAddGroup.reduce L₁) ∧ FreeAddGroup.Red L₃ (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 = { val := FreeGroup.reduce L₁, property := (_ : FreeGroup.Red L₂ (FreeGroup.reduce L₁) ∧ FreeGroup.Red L₃ (FreeGroup.reduce L₁)) }

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

Equations

• FreeAddGroup.instDecidableEqFreeAddGroup = Function.Injective.decidableEq (_ : Function.Injective FreeAddGroup.toWord)

theorem FreeAddGroup.instDecidableEqFreeAddGroup.proof_1 {α : Type u_1} [DecidableEq α] : Function.Injective FreeAddGroup.toWord

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

Equations

• FreeGroup.instDecidableEqFreeGroup = Function.Injective.decidableEq (_ : Function.Injective FreeGroup.toWord)

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 [] [])
• FreeGroup.Red.decidableRel [] (_hd2 :: _tl2) = isFalse (_ : FreeGroup.Red [] (_hd2 :: _tl2) → List.noConfusionType False (_hd2 :: _tl2) [])

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)) (List.sublists L₁)

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)) (List.sublists L₁)) : 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

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

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

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

Equations

• FreeAddGroup.norm x = List.length (FreeAddGroup.toWord x)

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

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

Equations

• FreeGroup.norm x = List.length (FreeGroup.toWord x)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FreeGroup.norm_eq_zero {α : Type u} [DecidableEq α] {x : FreeGroup α} : FreeGroup.norm x = 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

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

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

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

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