mathlib documentation

group_theory.free_group

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

Main definitions #

Main statements #

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.

Tags #

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

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

Reduction step: w * x * x⁻¹ * v ~> w * v

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

Reflexive-transitive closure of red.step

Equations
source
theorem free_group.red.refl {α : Type u} {L : list (α × bool)} :
free_group.red L L
source
theorem free_group.red.trans {α : Type u} {L₁ L₂ L₃ : list (α × bool)} :
free_group.red L₁ L₂ → free_group.red L₂ L₃ → free_group.red L₁ L₃
source
theorem free_group.red.step.length {α : Type u} {L₁ L₂ : list (α × bool)} :
free_group.red.step L₁ L₂ → L₂.length + 2 = L₁.length

Predicate asserting that 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₄

source
@[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₂)
source
@[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
source
@[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
source
theorem free_group.red.step.append_left {α : Type u} {L₁ L₂ L₃ : list (α × bool)} :
free_group.red.step L₂ L₃ → free_group.red.step (L₁ ++ L₂) (L₁ ++ L₃)
source
theorem free_group.red.step.cons {α : Type u} {L₁ L₂ : list (α × bool)} {x : α × bool} (H : free_group.red.step L₁ L₂) :
free_group.red.step (x :: L₁) (x :: L₂)
source
theorem free_group.red.step.append_right {α : Type u} {L₁ L₂ L₃ : list (α × bool)} :
free_group.red.step L₁ L₂ → free_group.red.step (L₁ ++ L₃) (L₂ ++ L₃)
source
theorem free_group.red.not_step_nil {α : Type u} {L : list (α × bool)} :
¬free_group.red.step list.nil L
source
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)), free_group.red.step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂
source
theorem free_group.red.not_step_singleton {α : Type u} {L : list (α × bool)} {p : α × bool} :
¬free_group.red.step [p] L
source
theorem free_group.red.step.cons_cons_iff {α : Type u} {L₁ L₂ : list (α × bool)} {p : α × bool} :
free_group.red.step (p :: L₁) (p :: L₂) ↔ free_group.red.step L₁ L₂
source
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₂) ↔ free_group.red.step L₁ L₂
source
theorem free_group.red.step.diamond {α : Type u} {L₁ L₂ L₃ L₄ : list (α × bool)} :
free_group.red.step L₁ L₃ → free_group.red.step L₂ L₄ → L₁ = L₂ → (L₃ = L₄ ∨ ∃ (L₅ : list (α × bool)), free_group.red.step L₃ L₅ ∧ free_group.red.step L₄ L₅)
source
theorem free_group.red.step.to_red {α : Type u} {L₁ L₂ : list (α × bool)} :
free_group.red.step L₁ L₂ → free_group.red L₁ L₂
source
theorem free_group.red.church_rosser {α : Type u} {L₁ L₂ L₃ : list (α × bool)} :
free_group.red L₁ L₂ → free_group.red L₁ L₃ → relation.join free_group.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.

source
theorem free_group.red.cons_cons {α : Type u} {L₁ L₂ : list (α × bool)} {p : α × bool} :
free_group.red L₁ L₂ → free_group.red (p :: L₁) (p :: L₂)
source
theorem free_group.red.cons_cons_iff {α : Type u} {L₁ L₂ : list (α × bool)} (p : α × bool) :
free_group.red (p :: L₁) (p :: L₂) ↔ free_group.red L₁ L₂
source
theorem free_group.red.append_append_left_iff {α : Type u} {L₁ L₂ : list (α × bool)} (L : list (α × bool)) :
free_group.red (L ++ L₁) (L ++ L₂) ↔ free_group.red L₁ L₂
source
theorem free_group.red.append_append {α : Type u} {L₁ L₂ L₃ L₄ : list (α × bool)} (h₁ : free_group.red L₁ L₃) (h₂ : free_group.red L₂ L₄) :
free_group.red (L₁ ++ L₂) (L₃ ++ L₄)
source
theorem free_group.red.to_append_iff {α : Type u} {L L₁ L₂ : list (α × bool)} :
free_group.red L (L₁ ++ L₂) ↔ ∃ (L₃ L₄ : list (α × bool)), L = L₃ ++ L₄ ∧ free_group.red L₃ L₁ ∧ free_group.red L₄ L₂
source
theorem free_group.red.nil_iff {α : Type u} {L : list (α × bool)} :
free_group.red list.nil L ↔ L = list.nil

The empty word [] only reduces to itself.

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

A letter only reduces to itself.

source
theorem free_group.red.cons_nil_iff_singleton {α : Type u} {L : list (α × bool)} {x : α} {b : bool} :
free_group.red ((x, b) :: L) list.nil ↔ free_group.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⁻¹

source
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)]
source
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₂)) :
free_group.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₂.

source
theorem free_group.red.step.sublist {α : Type u} {L₁ L₂ : list (α × bool)} (H : free_group.red.step L₁ L₂) :
L₂ <+ L₁
source
theorem free_group.red.sublist {α : Type u} {L₁ L₂ : list (α × bool)} :
free_group.red L₁ L₂ → L₂ <+ L₁

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

source
theorem free_group.red.sizeof_of_step {α : Type u} {L₁ L₂ : list (α × bool)} :
free_group.red.step L₁ L₂ → L₂.sizeof < L₁.sizeof
source
theorem free_group.red.length {α : Type u} {L₁ L₂ : list (α × bool)} (h : free_group.red L₁ L₂) :
∃ (n : ℕ), L₁.length = L₂.length + 2 * n
source
theorem free_group.red.antisymm {α : Type u} {L₁ L₂ : list (α × bool)} (h₁₂ : free_group.red L₁ L₂) :
free_group.red L₂ L₁ → L₁ = L₂
source
theorem free_group.equivalence_join_red {α : Type u} :
equivalence (relation.join free_group.red)
source
theorem free_group.join_red_of_step {α : Type u} {L₁ L₂ : list (α × bool)} (h : free_group.red.step L₁ L₂) :
relation.join free_group.red L₁ L₂
source
theorem free_group.eqv_gen_step_iff_join_red {α : Type u} {L₁ L₂ : list (α × bool)} :
eqv_gen free_group.red.step L₁ L₂ ↔ relation.join free_group.red L₁ L₂
source
def free_group (α : 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
source
def free_group.mk {α : Type u} (L : list (α × bool)) :
free_group α

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

Equations
source
@[simp]
theorem free_group.quot_mk_eq_mk {α : Type u} {L : list (α × bool)} :
quot.mk free_group.red.step L = free_group.mk L
source
@[simp]
theorem free_group.quot_lift_mk {α : Type u} {L : list (α × bool)} (β : Type v) (f : list (α × bool) → β) (H : ∀ (L₁ L₂ : list (α × bool)), free_group.red.step L₁ L₂ → f L₁ = f L₂) :
quot.lift f H (free_group.mk L) = f L
source
@[simp]
theorem free_group.quot_lift_on_mk {α : Type u} {L : list (α × bool)} (β : Type v) (f : list (α × bool) → β) (H : ∀ (L₁ L₂ : list (α × bool)), free_group.red.step L₁ L₂ → f L₁ = f L₂) :
quot.lift_on (free_group.mk L) f H = f L
source
@[simp]
theorem free_group.quot_map_mk {α : Type u} {L : list (α × bool)} (β : Type v) (f : list (α × bool) → list (β × bool)) (H : (free_group.red.step ⇒ free_group.red.step) f f) :
quot.map f H (free_group.mk L) = free_group.mk (f L)
source
@[protected, instance]
def free_group.has_one {α : Type u} :
has_one (free_group α)
Equations
source
theorem free_group.one_eq_mk {α : Type u} :
1 = free_group.mk list.nil
source
@[protected, instance]
def free_group.inhabited {α : Type u} :
inhabited (free_group α)
Equations
source
@[protected, instance]
def free_group.has_mul {α : Type u} :
has_mul (free_group α)
Equations
source
@[simp]
theorem free_group.mul_mk {α : Type u} {L₁ L₂ : list (α × bool)} :
(free_group.mk L₁) * free_group.mk L₂ = free_group.mk (L₁ ++ L₂)
source
@[protected, instance]
def free_group.has_inv {α : Type u} :
has_inv (free_group α)
Equations
source
@[simp]
theorem free_group.inv_mk {α : Type u} {L : list (α × bool)} :
(free_group.mk L)⁻¹ = free_group.mk (list.map (λ (x : α × bool), (x.fst, !x.snd)) L).reverse
source
@[protected, instance]
def free_group.group {α : Type u} :
group (free_group α)
Equations
source
def free_group.of {α : Type u} (x : α) :
free_group α

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
source
theorem free_group.red.exact {α : Type u} {L₁ L₂ : list (α × bool)} :
free_group.mk L₁ = free_group.mk L₂ ↔ relation.join free_group.red L₁ L₂
source
theorem free_group.of_injective {α : Type u} :
function.injective free_group.of

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

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

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

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

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

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

source
theorem free_group.lift.of_eq {α : Type u} (x : free_group α) :
⇑(⇑free_group.lift free_group.of) x = x
source
theorem free_group.lift.range_le {α : Type u} {β : Type v} [group β] {f : α → β} {s : subgroup β} (H : set.range f ⊆ ↑s) :
(⇑free_group.lift f).range ≤ s
source
theorem free_group.lift.range_eq_closure {α : Type u} {β : Type v} [group β] {f : α → β} :
(⇑free_group.lift f).range = subgroup.closure (set.range f)
source
def free_group.map {α : Type u} {β : Type v} (f : α → β) :
free_group α →* free_group β

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

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

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
source
@[simp]
theorem free_group.free_group_congr_refl {α : Type u} :
free_group.free_group_congr (equiv.refl α) = mul_equiv.refl (free_group α)
source
@[simp]
theorem free_group.free_group_congr_symm {α : Type u_1} {β : Type u_2} (e : α ≃ β) :
(free_group.free_group_congr e).symm = free_group.free_group_congr e.symm
source
theorem free_group.free_group_congr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (f : β ≃ γ) :
(free_group.free_group_congr e).trans (free_group.free_group_congr f) = free_group.free_group_congr (e.trans f)
source
def free_group.prod {α : Type u} [group α] :
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 multiplicative version of sum.

Equations
source
@[simp]
theorem free_group.prod_mk {α : Type u} {L : list (α × bool)} [group α] :
⇑free_group.prod (free_group.mk L) = (list.map (λ (x : α × bool), cond x.snd x.fst (x.fst)⁻¹) L).prod
source
@[simp]
theorem free_group.prod.of {α : Type u} [group α] {x : α} :
⇑free_group.prod (free_group.of x) = x
source
theorem free_group.prod.unique {α : Type u} [group α] (g : free_group α →* α) (hg : ∀ (x : α), ⇑g (free_group.of x) = x) {x : free_group α} :
⇑g x = ⇑free_group.prod x
source
theorem free_group.lift_eq_prod_map {α : Type u} {β : Type v} [group β] {f : α → β} {x : free_group α} :
⇑(⇑free_group.lift f) x = ⇑free_group.prod (⇑(free_group.map f) x)
source
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
source
@[simp]
theorem free_group.sum_mk {α : Type u} {L : list (α × bool)} [add_group α] :
(free_group.mk L).sum = (list.map (λ (x : α × bool), cond x.snd x.fst (-x.fst)) L).sum
source
@[simp]
theorem free_group.sum.of {α : Type u} [add_group α] {x : α} :
(free_group.of x).sum = x
source
@[simp]
theorem free_group.sum.map_mul {α : Type u} [add_group α] {x y : free_group α} :
(x * y).sum = x.sum + y.sum
source
@[simp]
theorem free_group.sum.map_one {α : Type u} [add_group α] :
1.sum = 0
source
@[simp]
theorem free_group.sum.map_inv {α : Type u} [add_group α] {x : free_group α} :
x⁻¹.sum = -x.sum
source
def free_group.free_group_empty_equiv_unit  :
free_group empty ≃ unit

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

Equations
source
def free_group.free_group_unit_equiv_int  :
free_group unit ≃ ℤ

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

Equations
source
@[protected, instance]
def free_group.monad  :
monad free_group
Equations
source
@[protected]
theorem free_group.induction_on {α : Type u} {C : free_group α → Prop} (z : free_group α) (C1 : C 1) (Cp : ∀ (x : α), C (pure x)) (Ci : ∀ (x : α), C (pure x) → C (pure x)⁻¹) (Cm : ∀ (x y : free_group α), C x → C y → C (x * y)) :
C z
source
@[simp]
theorem free_group.map_pure {α β : Type u} (f : α → β) (x : α) :
f <$> pure x = pure (f x)
source
@[simp]
theorem free_group.map_one {α β : Type u} (f : α → β) :
f <$> 1 = 1
source
@[simp]
theorem free_group.map_mul {α β : Type u} (f : α → β) (x y : free_group α) :
f <$> x * y = (f <$> x) * f <$> y
source
@[simp]
theorem free_group.map_inv {α β : Type u} (f : α → β) (x : free_group α) :
f <$> x⁻¹ = (f <$> x)⁻¹
source
@[simp]
theorem free_group.pure_bind {α β : Type u} (f : α → free_group β) (x : α) :
pure x >>= f = f x
source
@[simp]
theorem free_group.one_bind {α β : Type u} (f : α → free_group β) :
1 >>= f = 1
source
@[simp]
theorem free_group.mul_bind {α β : Type u} (f : α → free_group β) (x y : free_group α) :
x * y >>= f = (x >>= f) * (y >>= f)
source
@[simp]
theorem free_group.inv_bind {α β : Type u} (f : α → free_group β) (x : free_group α) :
x⁻¹ >>= f = (x >>= f)⁻¹
source
@[protected, instance]
def free_group.is_lawful_monad  :
is_lawful_monad free_group
source
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
source
@[simp]
theorem free_group.reduce.cons {α : Type u} {L : list (α × bool)} [decidable_eq α] (x : α × bool) :
free_group.reduce (x :: L) = (free_group.reduce L).cases_on [x] (λ (hd : α × bool) (tl : list (α × bool)), ite (x.fst = hd.fst ∧ x.snd = !hd.snd) tl (x :: hd :: tl))
source
theorem free_group.reduce.red {α : Type u} {L : list (α × bool)} [decidable_eq α] :
free_group.red L (free_group.reduce L)

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

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

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

source
theorem free_group.reduce.idem {α : Type u} {L : list (α × bool)} [decidable_eq α] :
free_group.reduce (free_group.reduce L) = free_group.reduce L

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

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

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

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

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

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

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

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

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

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

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

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

Equations
source
theorem free_group.to_word.mk {α : Type u} [decidable_eq α] {x : free_group α} :
free_group.mk x.to_word = x
source
theorem free_group.to_word.inj {α : Type u} [decidable_eq α] (x y : free_group α) :
x.to_word = y.to_word → x = y
source
def free_group.reduce.church_rosser {α : Type u} {L₁ L₂ L₃ : list (α × bool)} [decidable_eq α] (H12 : free_group.red L₁ L₂) (H13 : free_group.red L₁ L₃) :
{L₄ // free_group.red L₂ L₄ ∧ free_group.red L₃ L₄}

Constructive Church-Rosser theorem (compare church_rosser).

Equations
source
@[protected, instance]
def free_group.decidable_eq {α : Type u} [decidable_eq α] :
decidable_eq (free_group α)
Equations
source
@[protected, instance]
def free_group.red.decidable_rel {α : Type u} [decidable_eq α] :
decidable_rel free_group.red
Equations
source
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
source
theorem free_group.red.enum.sound {α : Type u} {L₁ L₂ : list (α × bool)} [decidable_eq α] (H : L₂ ∈ free_group.red.enum L₁) :
free_group.red L₁ L₂
source
theorem free_group.red.enum.complete {α : Type u} {L₁ L₂ : list (α × bool)} [decidable_eq α] (H : free_group.red L₁ L₂) :
L₂ ∈ free_group.red.enum L₁
source
@[protected, instance]
def free_group.subtype.fintype {α : Type u} {L₁ : list (α × bool)} [decidable_eq α] :
fintype {L₂ // free_group.red L₁ L₂}
Equations