# mathlib3documentation

group_theory.free_group

# Free groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 `free_group` is the left adjoint to the forgetful functor from groups to types, see `algebra/category/Group/adjunctions`.

## Main definitions #

• `free_group`/`free_add_group`: 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`.
• `free_group.mk`/`free_add_group.mk`: the canonical quotient map `list (α × bool) → free_group α`.
• `free_group.of`/`free_add_group.of`: the canonical injection `α → free_group α`.
• `free_group.lift f`/`free_add_group.lift`: the canonical group homomorphism `free_group α →* G` given a group `G` and a function `f : α → G`.

## Main statements #

• `free_group.church_rosser`/`free_add_group.church_rosser`: The Church-Rosser theorem for word reduction (also known as Newman's diamond lemma).
• `free_group.free_group_unit_equiv_int`: 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 `free_group.red.step`: `w * x * x⁻¹ * v ~> w * v`, its reflexive transitive closure `free_group.red.trans` and prove that its join is an equivalence relation. Then we introduce `free_group α` as a quotient over `free_group.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 free_add_group.red.step {α : Type u} :
list × bool) list × bool) Prop

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

inductive free_group.red.step {α : Type u} :
list × bool) list × bool) Prop

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

def free_group.red {α : Type u} :
list × bool) list × bool) Prop

Reflexive-transitive closure of red.step

Equations
Instances for `free_group.red`
def free_add_group.red {α : Type u} :
list × bool) list × bool) Prop

Reflexive-transitive closure of red.step

Equations
@[refl]
theorem free_add_group.red.refl {α : Type u} {L : list × bool)} :
@[refl]
theorem free_group.red.refl {α : Type u} {L : list × bool)} :
@[trans]
theorem free_group.red.trans {α : Type u} {L₁ L₂ L₃ : list × bool)} :
L₂ L₃ L₃
@[trans]
theorem free_add_group.red.trans {α : Type u} {L₁ L₂ L₃ : list × bool)} :
L₂ L₃ L₃
theorem free_group.red.step.length {α : Type u} {L₁ L₂ : list × bool)} :
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₄`

theorem free_add_group.red.step.length {α : Type u} {L₁ L₂ : list × bool)} :
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₄`

@[simp]
theorem free_add_group.red.step.bnot_rev {α : Type u} {L₁ L₂ : list × bool)} {x : α} {b : bool} :
free_add_group.red.step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)
@[simp]
theorem free_group.red.step.bnot_rev {α : Type u} {L₁ L₂ : list × bool)} {x : α} {b : bool} :
free_group.red.step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)
@[simp]
theorem free_add_group.red.step.cons_bnot {α : Type u} {L : list × bool)} {x : α} {b : bool} :
free_add_group.red.step ((x, b) :: (x, !b) :: L) L
@[simp]
theorem free_group.red.step.cons_bnot {α : Type u} {L : list × bool)} {x : α} {b : bool} :
free_group.red.step ((x, b) :: (x, !b) :: L) L
@[simp]
theorem free_add_group.red.step.cons_bnot_rev {α : Type u} {L : list × bool)} {x : α} {b : bool} :
free_add_group.red.step ((x, !b) :: (x, b) :: L) L
@[simp]
theorem free_group.red.step.cons_bnot_rev {α : Type u} {L : list × bool)} {x : α} {b : bool} :
free_group.red.step ((x, !b) :: (x, b) :: L) L
theorem free_group.red.step.append_left {α : Type u} {L₁ L₂ L₃ : list × bool)} :
L₃ free_group.red.step (L₁ ++ L₂) (L₁ ++ L₃)
theorem free_add_group.red.step.append_left {α : Type u} {L₁ L₂ L₃ : list × bool)} :
free_add_group.red.step (L₁ ++ L₂) (L₁ ++ L₃)
theorem free_group.red.step.cons {α : Type u} {L₁ L₂ : list × bool)} {x : α × bool} (H : L₂) :
free_group.red.step (x :: L₁) (x :: L₂)
theorem free_add_group.red.step.cons {α : Type u} {L₁ L₂ : list × bool)} {x : α × bool} (H : L₂) :
free_add_group.red.step (x :: L₁) (x :: L₂)
theorem free_add_group.red.step.append_right {α : Type u} {L₁ L₂ L₃ : list × bool)} :
free_add_group.red.step (L₁ ++ L₃) (L₂ ++ L₃)
theorem free_group.red.step.append_right {α : Type u} {L₁ L₂ L₃ : list × bool)} :
L₂ free_group.red.step (L₁ ++ L₃) (L₂ ++ L₃)
theorem free_group.red.not_step_nil {α : Type u} {L : list × bool)} :
theorem free_add_group.red.not_step_nil {α : Type u} {L : list × bool)} :
theorem free_group.red.step.cons_left_iff {α : Type u} {L₁ L₂ : list × bool)} {a : α} {b : bool} :
free_group.red.step ((a, b) :: L₁) L₂ ( (L : list × bool)), L₂ = (a, b) :: L) L₁ = (a, !b) :: L₂
theorem free_add_group.red.step.cons_left_iff {α : Type u} {L₁ L₂ : list × bool)} {a : α} {b : bool} :
free_add_group.red.step ((a, b) :: L₁) L₂ ( (L : list × bool)), L₂ = (a, b) :: L) L₁ = (a, !b) :: L₂
theorem free_group.red.not_step_singleton {α : Type u} {L : list × bool)} {p : α × bool} :
theorem free_add_group.red.not_step_singleton {α : Type u} {L : list × bool)} {p : α × bool} :
theorem free_add_group.red.step.cons_cons_iff {α : Type u} {L₁ L₂ : list × bool)} {p : α × bool} :
free_add_group.red.step (p :: L₁) (p :: L₂)
theorem free_group.red.step.cons_cons_iff {α : Type u} {L₁ L₂ : list × bool)} {p : α × bool} :
free_group.red.step (p :: L₁) (p :: L₂) L₂
theorem free_add_group.red.step.append_left_iff {α : Type u} {L₁ L₂ : list × bool)} (L : list × bool)) :
free_add_group.red.step (L ++ L₁) (L ++ L₂)
theorem free_group.red.step.append_left_iff {α : Type u} {L₁ L₂ : list × bool)} (L : list × bool)) :
free_group.red.step (L ++ L₁) (L ++ L₂) L₂
theorem free_add_group.red.step.diamond_aux {α : Type u} {L₁ L₂ L₃ 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)), free_add_group.red.step (L₁ ++ L₂) L₅ free_add_group.red.step (L₃ ++ L₄) L₅)
theorem free_group.red.step.diamond_aux {α : Type u} {L₁ L₂ L₃ 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)), free_group.red.step (L₁ ++ L₂) L₅ free_group.red.step (L₃ ++ L₄) L₅)
theorem free_group.red.step.diamond {α : Type u} {L₁ L₂ L₃ L₄ : list × bool)} :
L₃ L₄ L₁ = L₂ (L₃ = L₄ (L₅ : list × bool)), L₅ L₅)
theorem free_add_group.red.step.diamond {α : Type u} {L₁ L₂ L₃ L₄ : list × bool)} :
L₁ = L₂ (L₃ = L₄ (L₅ : list × bool)), L₅)
theorem free_add_group.red.step.to_red {α : Type u} {L₁ L₂ : list × bool)} :
L₂
theorem free_group.red.step.to_red {α : Type u} {L₁ L₂ : list × bool)} :
L₂ L₂
theorem free_group.red.church_rosser {α : Type u} {L₁ L₂ L₃ : list × bool)} :
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 free_add_group.red.church_rosser {α : Type u} {L₁ L₂ L₃ : list × bool)} :
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 free_add_group.red.cons_cons {α : Type u} {L₁ L₂ : list × bool)} {p : α × bool} :
L₂ free_add_group.red (p :: L₁) (p :: L₂)
theorem free_group.red.cons_cons {α : Type u} {L₁ L₂ : list × bool)} {p : α × bool} :
L₂ free_group.red (p :: L₁) (p :: L₂)
theorem free_group.red.cons_cons_iff {α : Type u} {L₁ L₂ : list × bool)} (p : α × bool) :
free_group.red (p :: L₁) (p :: L₂) L₂
theorem free_add_group.red.cons_cons_iff {α : Type u} {L₁ L₂ : list × bool)} (p : α × bool) :
free_add_group.red (p :: L₁) (p :: L₂) L₂
theorem free_add_group.red.append_append_left_iff {α : Type u} {L₁ L₂ : list × bool)} (L : list × bool)) :
free_add_group.red (L ++ L₁) (L ++ L₂) L₂
theorem free_group.red.append_append_left_iff {α : Type u} {L₁ L₂ : list × bool)} (L : list × bool)) :
free_group.red (L ++ L₁) (L ++ L₂) L₂
theorem free_group.red.append_append {α : Type u} {L₁ L₂ L₃ L₄ : list × bool)} (h₁ : L₃) (h₂ : L₄) :
free_group.red (L₁ ++ L₂) (L₃ ++ L₄)
theorem free_add_group.red.append_append {α : Type u} {L₁ L₂ L₃ L₄ : list × bool)} (h₁ : L₃) (h₂ : L₄) :
free_add_group.red (L₁ ++ L₂) (L₃ ++ L₄)
theorem free_add_group.red.to_append_iff {α : Type u} {L L₁ L₂ : list × bool)} :
(L₁ ++ L₂) (L₃ L₄ : list × bool)), L = L₃ ++ L₄ L₁ L₂
theorem free_group.red.to_append_iff {α : Type u} {L L₁ L₂ : list × bool)} :
(L₁ ++ L₂) (L₃ L₄ : list × bool)), L = L₃ ++ L₄ L₁ L₂
theorem free_add_group.red.nil_iff {α : Type u} {L : list × bool)} :

The empty word `[]` only reduces to itself.

theorem free_group.red.nil_iff {α : Type u} {L : list × bool)} :

The empty word `[]` only reduces to itself.

theorem free_group.red.singleton_iff {α : Type u} {L₁ : list × bool)} {x : α × bool} :
L₁ L₁ = [x]

A letter only reduces to itself.

theorem free_add_group.red.singleton_iff {α : Type u} {L₁ : list × bool)} {x : α × bool} :
L₁ L₁ = [x]

A letter only reduces to itself.

theorem free_group.red.cons_nil_iff_singleton {α : Type u} {L : list × bool)} {x : α} {b : bool} :
free_group.red ((x, b) :: L) list.nil [(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 free_add_group.red.cons_nil_iff_singleton {α : Type u} {L : list × bool)} {x : α} {b : bool} :
free_add_group.red ((x, b) :: L) list.nil [(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 free_add_group.red.red_iff_irreducible {α : Type u} {L : list × bool)} {x1 : α} {b1 : bool} {x2 : α} {b2 : bool} (h : (x1, b1) (x2, b2)) :
free_add_group.red [(x1, !b1), (x2, b2)] L L = [(x1, !b1), (x2, b2)]
theorem free_group.red.red_iff_irreducible {α : Type u} {L : list × bool)} {x1 : α} {b1 : bool} {x2 : α} {b2 : bool} (h : (x1, b1) (x2, b2)) :
free_group.red [(x1, !b1), (x2, b2)] L L = [(x1, !b1), (x2, b2)]
theorem free_group.red.inv_of_red_of_ne {α : Type u} {L₁ L₂ : list × bool)} {x1 : α} {b1 : bool} {x2 : α} {b2 : bool} (H1 : (x1, b1) (x2, b2)) (H2 : free_group.red ((x1, b1) :: L₁) ((x2, b2) :: 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 free_add_group.red.neg_of_red_of_ne {α : Type u} {L₁ L₂ : list × bool)} {x1 : α} {b1 : bool} {x2 : α} {b2 : bool} (H1 : (x1, b1) (x2, b2)) (H2 : free_add_group.red ((x1, b1) :: L₁) ((x2, b2) :: 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 free_add_group.red.step.sublist {α : Type u} {L₁ L₂ : list × bool)} (H : L₂) :
L₂ <+ L₁
theorem free_group.red.step.sublist {α : Type u} {L₁ L₂ : list × bool)} (H : L₂) :
L₂ <+ L₁
@[protected]
theorem free_add_group.red.sublist {α : Type u} {L₁ L₂ : list × bool)} :
L₂ L₂ <+ L₁

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

@[protected]
theorem free_group.red.sublist {α : Type u} {L₁ L₂ : list × bool)} :
L₂ L₂ <+ L₁

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

theorem free_add_group.red.length_le {α : Type u} {L₁ L₂ : list × bool)} (h : L₂) :
L₂.length L₁.length
theorem free_group.red.length_le {α : Type u} {L₁ L₂ : list × bool)} (h : L₂) :
L₂.length L₁.length
theorem free_group.red.sizeof_of_step {α : Type u} {L₁ L₂ : list × bool)} :
L₂ L₂.sizeof < L₁.sizeof
theorem free_add_group.red.sizeof_of_step {α : Type u} {L₁ L₂ : list × bool)} :
L₂.sizeof < L₁.sizeof
theorem free_group.red.length {α : Type u} {L₁ L₂ : list × bool)} (h : L₂) :
(n : ), L₁.length = L₂.length + 2 * n
theorem free_add_group.red.length {α : Type u} {L₁ L₂ : list × bool)} (h : L₂) :
(n : ), L₁.length = L₂.length + 2 * n
theorem free_add_group.red.antisymm {α : Type u} {L₁ L₂ : list × bool)} (h₁₂ : L₂) (h₂₁ : L₁) :
L₁ = L₂
theorem free_group.red.antisymm {α : Type u} {L₁ L₂ : list × bool)} (h₁₂ : L₂) (h₂₁ : L₁) :
L₁ = L₂
theorem free_group.join_red_of_step {α : Type u} {L₁ L₂ : list × bool)} (h : L₂) :
theorem free_add_group.join_red_of_step {α : Type u} {L₁ L₂ : list × bool)} (h : L₂) :
theorem free_add_group.eqv_gen_step_iff_join_red {α : Type u} {L₁ L₂ : list × bool)} :
theorem free_group.eqv_gen_step_iff_join_red {α : Type u} {L₁ L₂ : list × bool)} :
def free_group (α : 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
Instances for `free_group`
def free_add_group (α : 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
Instances for `free_add_group`
def free_group.mk {α : Type u} (L : list × bool)) :

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

Equations
def free_add_group.mk {α : Type u} (L : list × bool)) :

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

Equations
@[simp]
theorem free_add_group.quot_mk_eq_mk {α : Type u} {L : list × bool)} :
@[simp]
theorem free_group.quot_mk_eq_mk {α : Type u} {L : list × bool)} :
@[simp]
theorem free_group.quot_lift_mk {α : Type u} {L : list × bool)} (β : Type v) (f : list × bool) β) (H : (L₁ L₂ : list × bool)), L₂ f L₁ = f L₂) :
quot.lift f H = f L
@[simp]
theorem free_add_group.quot_lift_mk {α : Type u} {L : list × bool)} (β : Type v) (f : list × bool) β) (H : (L₁ L₂ : list × bool)), f L₁ = f L₂) :
quot.lift f H = f L
@[simp]
theorem free_group.quot_lift_on_mk {α : Type u} {L : list × bool)} (β : Type v) (f : list × bool) β) (H : (L₁ L₂ : list × bool)), L₂ f L₁ = f L₂) :
H = f L
@[simp]
theorem free_add_group.quot_lift_on_mk {α : Type u} {L : list × bool)} (β : Type v) (f : list × bool) β) (H : (L₁ L₂ : list × bool)), f L₁ = f L₂) :
H = f L
@[simp]
theorem free_add_group.quot_map_mk {α : Type u} {L : list × bool)} (β : Type v) (f : list × bool) list × bool)) (H : f) :
@[simp]
theorem free_group.quot_map_mk {α : Type u} {L : list × bool)} (β : Type v) (f : list × bool) list × bool)) (H : f) :
H = free_group.mk (f L)
@[protected, instance]
def free_group.has_one {α : Type u} :
Equations
@[protected, instance]
def free_add_group.has_zero {α : Type u} :
Equations
theorem free_add_group.zero_eq_mk {α : Type u} :
theorem free_group.one_eq_mk {α : Type u} :
@[protected, instance]
def free_add_group.inhabited {α : Type u} :
Equations
@[protected, instance]
def free_group.inhabited {α : Type u} :
Equations
@[protected, instance]
Equations
@[protected, instance]
def free_group.has_mul {α : Type u} :
Equations
@[simp]
theorem free_group.mul_mk {α : Type u} {L₁ L₂ : list × bool)} :
= free_group.mk (L₁ ++ L₂)
@[simp]
theorem free_add_group.add_mk {α : Type u} {L₁ L₂ : list × bool)} :
def free_group.inv_rev {α : Type u} (w : list × bool)) :
list × bool)

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

Equations
def free_add_group.neg_rev {α : Type u} (w : list × bool)) :
list × bool)

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

Equations
@[simp]
theorem free_group.inv_rev_length {α : Type u} {L₁ : list × bool)} :
@[simp]
theorem free_add_group.neg_rev_length {α : Type u} {L₁ : list × bool)} :
= L₁.length
@[simp]
theorem free_add_group.neg_rev_neg_rev {α : Type u} {L₁ : list × bool)} :
@[simp]
theorem free_group.inv_rev_inv_rev {α : Type u} {L₁ : list × bool)} :
@[simp]
theorem free_group.inv_rev_empty {α : Type u} :
@[simp]
theorem free_add_group.neg_rev_empty {α : Type u} :
@[protected, instance]
def free_add_group.has_neg {α : Type u} :
Equations
@[protected, instance]
def free_group.has_inv {α : Type u} :
Equations
@[simp]
theorem free_group.inv_mk {α : Type u} {L : list × bool)} :
@[simp]
theorem free_add_group.neg_mk {α : Type u} {L : list × bool)} :
theorem free_add_group.red.step.neg_rev {α : Type u} {L₁ L₂ : list × bool)} (h : L₂) :
theorem free_group.red.step.inv_rev {α : Type u} {L₁ L₂ : list × bool)} (h : L₂) :
theorem free_group.red.inv_rev {α : Type u} {L₁ L₂ : list × bool)} (h : L₂) :
theorem free_add_group.red.neg_rev {α : Type u} {L₁ L₂ : list × bool)} (h : L₂) :
@[simp]
theorem free_add_group.red.step_neg_rev_iff {α : Type u} {L₁ L₂ : list × bool)} :
@[simp]
theorem free_group.red.step_inv_rev_iff {α : Type u} {L₁ L₂ : list × bool)} :
@[simp]
theorem free_group.red_inv_rev_iff {α : Type u} {L₁ L₂ : list × bool)} :
L₂
@[simp]
theorem free_add_group.red_neg_rev_iff {α : Type u} {L₁ L₂ : list × bool)} :
@[protected, instance]
def free_group.group {α : Type u} :
Equations
@[protected, instance]
Equations
def free_group.of {α : Type u} (x : α) :

`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
def free_add_group.of {α : Type u} (x : α) :

`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
theorem free_add_group.red.exact {α : Type u} {L₁ L₂ : list × bool)} :
theorem free_group.red.exact {α : Type u} {L₁ L₂ : list × bool)} :
theorem free_add_group.of_injective {α : Type u} :

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

theorem free_group.of_injective {α : Type u} :

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

def free_add_group.lift.aux {α : Type u} {β : Type v} [add_group β] (f : α β) :
list × bool) β

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

Equations
def free_group.lift.aux {α : Type u} {β : Type v} [group β] (f : α β) :
list × bool) β

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

Equations
theorem free_add_group.red.step.lift {α : Type u} {L₁ L₂ : list × bool)} {β : Type v} [add_group β] {f : α β} (H : L₂) :
theorem free_group.red.step.lift {α : Type u} {L₁ L₂ : list × bool)} {β : Type v} [group β] {f : α β} (H : L₂) :
=
@[simp]
theorem free_group.lift_symm_apply {α : Type u} {β : Type v} [group β] (g : →* β) (ᾰ : α) :
def free_group.lift {α : Type u} {β : Type v} [group β] :
β) →* β)

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

Equations
@[simp]
theorem free_add_group.lift_symm_apply {α : Type u} {β : Type v} [add_group β] (g : →+ β) (ᾰ : α) :
=
def free_add_group.lift {α : Type u} {β : Type v} [add_group β] :
β) →+ β)

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
@[simp]
theorem free_add_group.lift.mk {α : Type u} {L : list × bool)} {β : Type v} [add_group β] {f : α β} :
= (list.map (λ (x : α × bool), cond x.snd (f x.fst) (-f x.fst)) L).sum
@[simp]
theorem free_group.lift.mk {α : Type u} {L : list × bool)} {β : Type v} [group β] {f : α β} :
= (list.map (λ (x : α × bool), cond x.snd (f x.fst) (f x.fst)⁻¹) L).prod
@[simp]
theorem free_group.lift.of {α : Type u} {β : Type v} [group β] {f : α β} {x : α} :
= f x
@[simp]
theorem free_add_group.lift.of {α : Type u} {β : Type v} [add_group β] {f : α β} {x : α} :
= f x
theorem free_add_group.lift.unique {α : Type u} {β : Type v} [add_group β] {f : α β} (g : →+ β) (hg : (x : α), g = f x) {x : free_add_group α} :
g x =
theorem free_group.lift.unique {α : Type u} {β : Type v} [group β] {f : α β} (g : →* β) (hg : (x : α), g = f x) {x : free_group α} :
g x = x
@[ext]
theorem free_group.ext_hom {α : Type u} {G : Type u_1} [group G] (f g : →* G) (h : (a : α), f = g ) :
f = g

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

@[ext]
theorem free_add_group.ext_hom {α : Type u} {G : Type u_1} [add_group G] (f g : →+ G) (h : (a : α), f = g ) :
f = g

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

theorem free_group.lift.of_eq {α : Type u} (x : free_group α) :
theorem free_group.lift.range_le {α : Type u} {β : Type v} [group β] {f : α β} {s : subgroup β} (H : s) :
s
theorem free_add_group.lift.range_le {α : Type u} {β : Type v} [add_group β] {f : α β} {s : add_subgroup β} (H : s) :
theorem free_add_group.lift.range_eq_closure {α : Type u} {β : Type v} [add_group β] {f : α β} :
theorem free_group.lift.range_eq_closure {α : Type u} {β : Type v} [group β] {f : α β} :
def free_group.map {α : Type u} {β : Type v} (f : α β) :

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

Equations
def free_add_group.map {α : Type u} {β : Type v} (f : α β) :

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

Equations
@[simp]
theorem free_group.map.mk {α : Type u} {L : list × bool)} {β : Type v} {f : α β} :
= free_group.mk (list.map (λ (x : α × bool), (f x.fst, x.snd)) L)
@[simp]
theorem free_add_group.map.mk {α : Type u} {L : list × bool)} {β : Type v} {f : α β} :
= free_add_group.mk (list.map (λ (x : α × bool), (f x.fst, x.snd)) L)
@[simp]
= x
@[simp]
theorem free_group.map.id {α : Type u} (x : free_group α) :
= x
@[simp]
theorem free_group.map.id' {α : Type u} (x : free_group α) :
(free_group.map (λ (z : α), z)) x = x
@[simp]
(free_add_group.map (λ (z : α), z)) x = x
theorem free_group.map.comp {α : Type u} {β : Type v} {γ : Type w} (f : α β) (g : β γ) (x : free_group α) :
( x) = (free_group.map (g f)) x
theorem free_add_group.map.comp {α : Type u} {β : Type v} {γ : Type w} (f : α β) (g : β γ) (x : free_add_group α) :
@[simp]
theorem free_add_group.map.of {α : Type u} {β : Type v} {f : α β} {x : α} :
@[simp]
theorem free_group.map.of {α : Type u} {β : Type v} {f : α β} {x : α} :
theorem free_group.map.unique {α : Type u} {β : Type v} {f : α β} (g : →* ) (hg : (x : α), g = free_group.of (f x)) {x : free_group α} :
g x = x
theorem free_add_group.map.unique {α : Type u} {β : Type v} {f : α β} (g : →+ ) (hg : (x : α), g = free_add_group.of (f x)) {x : free_add_group α} :
g x = x
theorem free_group.map_eq_lift {α : Type u} {β : Type v} {f : α β} {x : free_group α} :
x = x
theorem free_add_group.map_eq_lift {α : Type u} {β : Type v} {f : α β} {x : free_add_group α} :
x =
@[simp]
theorem free_group.free_group_congr_apply {α : Type u_1} {β : Type u_2} (e : α β) (ᾰ : free_group α) :
=
@[simp]
theorem free_add_group.free_add_group_congr_apply {α : Type u_1} {β : Type u_2} (e : α β) (ᾰ : free_add_group α) :
def free_group.free_group_congr {α : Type u_1} {β : Type u_2} (e : α β) :

Equivalent types give rise to multiplicatively equivalent free groups.

The converse can be found in `group_theory.free_abelian_group_finsupp`, as `equiv.of_free_group_equiv`

Equations
def free_add_group.free_add_group_congr {α : Type u_1} {β : Type u_2} (e : α β) :

Equations
@[simp]
@[simp]
@[simp]
theorem free_add_group.free_add_group_congr_symm {α : Type u_1} {β : Type u_2} (e : α β) :
@[simp]
theorem free_group.free_group_congr_symm {α : Type u_1} {β : Type u_2} (e : α β) :
theorem free_group.free_group_congr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α β) (f : β γ) :
theorem free_add_group.free_add_group_congr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α β) (f : β γ) :
def free_group.prod {α : Type u} [group α] :
→* α

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 `free_group.sum`.

Equations

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

Equations
@[simp]
theorem free_group.prod_mk {α : Type u} {L : list × bool)} [group α] :
= (list.map (λ (x : α × bool), cond x.snd x.fst (x.fst)⁻¹) L).prod
@[simp]
theorem free_add_group.sum_mk {α : Type u} {L : list × bool)} [add_group α] :
= (list.map (λ (x : α × bool), cond x.snd x.fst (-x.fst)) L).sum
@[simp]
theorem free_add_group.sum.of {α : Type u} [add_group α] {x : α} :
@[simp]
theorem free_group.prod.of {α : Type u} [group α] {x : α} :
theorem free_group.prod.unique {α : Type u} [group α] (g : →* α) (hg : (x : α), g = x) {x : free_group α} :
g x =
theorem free_add_group.sum.unique {α : Type u} [add_group α] (g : →+ α) (hg : (x : α), g = x) {x : free_add_group α} :
theorem free_add_group.lift_eq_sum_map {α : Type u} {β : Type v} [add_group β] {f : α β} {x : free_add_group α} :
=
theorem free_group.lift_eq_prod_map {α : Type u} {β : Type v} [group β] {f : α β} {x : free_group α} :
def free_group.sum {α : Type u} [add_group α] (x : free_group α) :
α

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
@[simp]
theorem free_group.sum_mk {α : Type u} {L : list × bool)} [add_group α] :
.sum = (list.map (λ (x : α × bool), cond x.snd x.fst (-x.fst)) L).sum
@[simp]
theorem free_group.sum.of {α : Type u} [add_group α] {x : α} :
.sum = x
@[simp]
theorem free_group.sum.map_mul {α : Type u} [add_group α] {x y : free_group α} :
(x * y).sum = x.sum + y.sum
@[simp]
theorem free_group.sum.map_one {α : Type u} [add_group α] :
1.sum = 0
@[simp]
theorem free_group.sum.map_inv {α : Type u} [add_group α] {x : free_group α} :

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

Equations

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

Equations

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

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]
theorem free_group.induction_on {α : Type u} {C : Prop} (z : free_group α) (C1 : C 1) (Cp : (x : α), C ) (Ci : (x : α), C C ⁻¹) (Cm : (x y : , C x C y C (x * y)) :
C z
@[protected]
theorem free_add_group.induction_on {α : Type u} {C : Prop} (z : free_add_group α) (C1 : C 0) (Cp : (x : α), C ) (Ci : (x : α), C C (-) (Cm : (x y : , C x C y C (x + y)) :
C z
@[simp]
theorem free_group.map_pure {α β : Type u} (f : α β) (x : α) :
@[simp]
theorem free_add_group.map_pure {α β : Type u} (f : α β) (x : α) :
@[simp]
theorem free_add_group.map_zero {α β : Type u} (f : α β) :
f <\$> 0 = 0
@[simp]
theorem free_group.map_one {α β : Type u} (f : α β) :
f <\$> 1 = 1
@[simp]
theorem free_add_group.map_add {α β : Type u} (f : α β) (x y : free_add_group α) :
f <\$> (x + y) = f <\$> x + f <\$> y
@[simp]
theorem free_group.map_mul {α β : Type u} (f : α β) (x y : free_group α) :
f <\$> (x * y) = f <\$> x * f <\$> y
@[simp]
theorem free_add_group.map_neg {α β : Type u} (f : α β) (x : free_add_group α) :
f <\$> -x = -f <\$> x
@[simp]
theorem free_group.map_inv {α β : Type u} (f : α β) (x : free_group α) :
f <\$> x⁻¹ = (f <\$> x)⁻¹
@[simp]
theorem free_group.pure_bind {α β : Type u} (f : α ) (x : α) :
= f x
@[simp]
theorem free_add_group.pure_bind {α β : Type u} (f : α ) (x : α) :
= f x
@[simp]
theorem free_group.one_bind {α β : Type u} (f : α ) :
1 >>= f = 1
@[simp]
theorem free_add_group.zero_bind {α β : Type u} (f : α ) :
0 >>= f = 0
@[simp]
theorem free_group.mul_bind {α β : Type u} (f : α ) (x y : free_group α) :
x * y >>= f = (x >>= f) * (y >>= f)
@[simp]
theorem free_add_group.add_bind {α β : Type u} (f : α ) (x y : free_add_group α) :
x + y >>= f = (x >>= f) + (y >>= f)
@[simp]
theorem free_add_group.neg_bind {α β : Type u} (f : α ) (x : free_add_group α) :
-x >>= f = -(x >>= f)
@[simp]
theorem free_group.inv_bind {α β : Type u} (f : α ) (x : free_group α) :
x⁻¹ >>= f = (x >>= f)⁻¹
@[protected, instance]
@[protected, instance]
def free_group.reduce {α : Type u} [decidable_eq α] (L : list × bool)) :
list × bool)

The maximal reduction of a word. It is computable iff `α` has decidable equality.

Equations
def free_add_group.reduce {α : Type u} [decidable_eq α] (L : list × bool)) :
list × bool)

The maximal reduction of a word. It is computable iff `α` has decidable equality.

Equations
@[simp]
theorem free_add_group.reduce.cons {α : Type u} {L : list × bool)} [decidable_eq α] (x : α × bool) :
free_add_group.reduce (x :: L) = .cases_on [x] (λ (hd : α × bool) (tl : list × bool)), ite (x.fst = hd.fst x.snd = !hd.snd) tl (x :: hd :: tl))
@[simp]
theorem free_group.reduce.cons {α : Type u} {L : list × bool)} [decidable_eq α] (x : α × bool) :
free_group.reduce (x :: L) = .cases_on [x] (λ (hd : α × bool) (tl : list × bool)), ite (x.fst = hd.fst x.snd = !hd.snd) tl (x :: hd :: tl))
theorem free_group.reduce.red {α : Type u} {L : list × bool)} [decidable_eq α] :

The first theorem that characterises the function `reduce`: a word reduces to its maximal reduction.

theorem free_add_group.reduce.red {α : Type u} {L : list × bool)} [decidable_eq α] :

The first theorem that characterises the function `reduce`: a word reduces to its maximal reduction.

theorem free_add_group.reduce.not {α : Type u} [decidable_eq α] {p : Prop} {L₁ L₂ L₃ : list × bool)} {x : α} {b : bool} :
= L₂ ++ (x, b) :: (x, !b) :: L₃ p
theorem free_group.reduce.not {α : Type u} [decidable_eq α] {p : Prop} {L₁ L₂ L₃ : list × bool)} {x : α} {b : bool} :
= L₂ ++ (x, b) :: (x, !b) :: L₃ p
theorem free_add_group.reduce.min {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (H : L₂) :

The second theorem that characterises the function `reduce`: the maximal reduction of a word only reduces to itself.

theorem free_group.reduce.min {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (H : L₂) :
= L₂

The second theorem that characterises the function `reduce`: the maximal reduction of a word only reduces to itself.

@[simp]
theorem free_group.reduce.idem {α : Type u} {L : list × bool)} [decidable_eq α] :

`reduce` is idempotent, i.e. the maximal reduction of the maximal reduction of a word is the maximal reduction of the word.

@[simp]
theorem free_add_group.reduce.idem {α : Type u} {L : list × bool)} [decidable_eq α] :

`reduce` is idempotent, i.e. the maximal reduction of the maximal reduction of a word is the maximal reduction of the word.

theorem free_add_group.reduce.step.eq {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (H : L₂) :
theorem free_group.reduce.step.eq {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (H : L₂) :
theorem free_add_group.reduce.eq_of_red {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (H : L₂) :

If a word reduces to another word, then they have a common maximal reduction.

theorem free_group.reduce.eq_of_red {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (H : L₂) :

If a word reduces to another word, then they have a common maximal reduction.

theorem free_group.red.reduce_eq {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (H : L₂) :

Alias of `free_group.reduce.eq_of_red`.

theorem free_group.free_add_group.red.reduce_eq {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (H : L₂) :

Alias of `free_add_group.reduce.eq_of_red`.

theorem free_add_group.red.reduce_right {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (h : L₂) :
theorem free_group.red.reduce_right {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (h : L₂) :
theorem free_add_group.red.reduce_left {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (h : L₂) :
theorem free_group.red.reduce_left {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (h : L₂) :
theorem free_group.reduce.sound {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (H : = ) :

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 free_add_group.reduce.sound {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (H : = ) :

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 free_add_group.reduce.exact {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (H : = ) :

If two words have a common maximal reduction, then they correspond to the same element in the additive free group.

theorem free_group.reduce.exact {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (H : = ) :

If two words have a common maximal reduction, then they correspond to the same element in the free group.

theorem free_group.reduce.self {α : Type u} {L : list × bool)} [decidable_eq α] :

A word and its maximal reduction correspond to the same element of the free group.

theorem free_add_group.reduce.self {α : Type u} {L : list × bool)} [decidable_eq α] :

A word and its maximal reduction correspond to the same element of the additive free group.

theorem free_group.reduce.rev {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (H : L₂) :

If words `w₁ w₂` are such that `w₁` reduces to `w₂`, then `w₂` reduces to the maximal reduction of `w₁`.

theorem free_add_group.reduce.rev {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (H : L₂) :

If words `w₁ w₂` are such that `w₁` reduces to `w₂`, then `w₂` reduces to the maximal reduction of `w₁`.

def free_add_group.to_word {α : Type u} [decidable_eq α] :
list × bool)

The function that sends an element of the additive free group to its maximal reduction.

Equations
def free_group.to_word {α : Type u} [decidable_eq α] :
list × bool)

The function that sends an element of the free group to its maximal reduction.

Equations
theorem free_group.mk_to_word {α : Type u} [decidable_eq α] {x : free_group α} :
@[simp]
theorem free_group.to_word_inj {α : Type u} [decidable_eq α] {x y : free_group α} :
@[simp]
theorem free_add_group.to_word_inj {α : Type u} [decidable_eq α] {x y : free_add_group α} :
@[simp]
theorem free_add_group.to_word_mk {α : Type u} {L₁ : list × bool)} [decidable_eq α] :
@[simp]
theorem free_group.to_word_mk {α : Type u} {L₁ : list × bool)} [decidable_eq α] :
@[simp]
theorem free_group.reduce_to_word {α : Type u} [decidable_eq α] (x : free_group α) :
@[simp]
@[simp]
theorem free_add_group.to_word_zero {α : Type u} [decidable_eq α] :
@[simp]
theorem free_group.to_word_one {α : Type u} [decidable_eq α] :
@[simp]
theorem free_add_group.to_word_eq_nil_iff {α : Type u} [decidable_eq α] {x : free_add_group α} :
x = 0
@[simp]
theorem free_group.to_word_eq_nil_iff {α : Type u} [decidable_eq α] {x : free_group α} :
x = 1
theorem free_group.reduce_inv_rev {α : Type u} [decidable_eq α] {w : list × bool)} :
theorem free_add_group.reduce_neg_rev {α : Type u} [decidable_eq α] {w : list × bool)} :
theorem free_group.to_word_inv {α : Type u} [decidable_eq α] {x : free_group α} :
def free_group.reduce.church_rosser {α : Type u} {L₁ L₂ L₃ : list × bool)} [decidable_eq α] (H12 : L₂) (H13 : L₃) :
{L₄ // L₄ L₄}

Constructive Church-Rosser theorem (compare `church_rosser`).

Equations
def free_add_group.reduce.church_rosser {α : Type u} {L₁ L₂ L₃ : list × bool)} [decidable_eq α] (H12 : L₂) (H13 : L₃) :
{L₄ // L₄ L₄}

Constructive Church-Rosser theorem (compare `church_rosser`).

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
• free_group.red.decidable_rel ((x1, b1) :: tl1) ((x2, b2) :: tl2) = dite ((x1, b1) = (x2, b2)) (λ (h : (x1, b1) = (x2, b2)), free_group.red.decidable_rel._match_2 x1 b1 tl1 x2 b2 tl2 h tl2)) (λ (h : ¬(x1, b1) = (x2, b2)), free_group.red.decidable_rel._match_3 x1 b1 tl1 x2 b2 tl2 h ((x1, !b1) :: (x2, b2) :: tl2)))
• free_group.red.decidable_rel ((x, b) :: tl) list.nil = free_group.red.decidable_rel._match_1 x b tl [(x, !b)])
• = decidable.is_true free_group.red.decidable_rel._main._proof_1
• free_group.red.decidable_rel._match_2 x1 b1 tl1 x2 b2 tl2 h =
• free_group.red.decidable_rel._match_2 x1 b1 tl1 x2 b2 tl2 h =
• free_group.red.decidable_rel._match_3 x1 b1 tl1 x2 b2 tl2 h =
• free_group.red.decidable_rel._match_3 x1 b1 tl1 x2 b2 tl2 h =
• free_group.red.decidable_rel._match_1 x b tl =
• free_group.red.decidable_rel._match_1 x b tl =
def free_group.red.enum {α : Type u} [decidable_eq α] (L₁ : list × bool)) :
list (list × bool))

A list containing every word that `w₁` reduces to.

Equations
theorem free_group.red.enum.sound {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (H : L₂ ) :
L₂
theorem free_group.red.enum.complete {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] (H : L₂) :
L₂
@[protected, instance]
def free_group.subtype.fintype {α : Type u} {L₁ : list × bool)} [decidable_eq α] :
fintype {L₂ // L₂}
Equations
def free_add_group.norm {α : Type u} [decidable_eq α] (x : free_add_group α) :

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

Equations
def free_group.norm {α : Type u} [decidable_eq α] (x : free_group α) :

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

Equations
@[simp]
theorem free_group.norm_inv_eq {α : Type u} [decidable_eq α] {x : free_group α} :
@[simp]
theorem free_add_group.norm_neg_eq {α : Type u} [decidable_eq α] {x : free_add_group α} :
(-x).norm = x.norm
@[simp]
theorem free_add_group.norm_eq_zero {α : Type u} [decidable_eq α] {x : free_add_group α} :
x.norm = 0 x = 0
@[simp]
theorem free_group.norm_eq_zero {α : Type u} [decidable_eq α] {x : free_group α} :
x.norm = 0 x = 1
@[simp]
theorem free_group.norm_one {α : Type u} [decidable_eq α] :
1.norm = 0
@[simp]
theorem free_add_group.norm_zero {α : Type u} [decidable_eq α] :
0.norm = 0
theorem free_group.norm_mk_le {α : Type u} {L₁ : list × bool)} [decidable_eq α] :
theorem free_add_group.norm_mk_le {α : Type u} {L₁ : list × bool)} [decidable_eq α] :