mathlib docs: group_theory.free

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} :

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.

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)} :

free_group.red L₁ L₃ → 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} :

(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} :

(x1, b1) ≠ (x2, b2) → 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)} :

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)} :

free_group.red L₁ L₂ → (∃ (n : ℕ), L₁.length = L₂.length + 2 * n)

source

theorem free_group.red.antisymm {α : Type u} {L₁ L₂ : list (α × bool)} :

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)} :

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

free_group α = quot free_group.red.step

source

def free_group.mk {α : Type u} :

list (α × bool) → free_group α

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

Equations

free_group.mk L = quot.mk free_group.red.step L

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

@[instance]

def free_group.has_one {α : Type u} :

has_one (free_group α)

Equations

free_group.has_one = {one := free_group.mk list.nil}

source

theorem free_group.one_eq_mk {α : Type u} :

1 = free_group.mk list.nil

source

@[instance]

def free_group.inhabited {α : Type u} :

inhabited (free_group α)

Equations

free_group.inhabited = {default := 1}

source

@[instance]

def free_group.has_mul {α : Type u} :

has_mul (free_group α)

Equations

free_group.has_mul = {mul := λ (x y : free_group α), quot.lift_on x (λ (L₁ : list (α × bool)), quot.lift_on y (λ (L₂ : list (α × bool)), free_group.mk (L₁ ++ L₂)) _) _}

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

@[instance]

def free_group.has_inv {α : Type u} :

has_inv (free_group α)

Equations

free_group.has_inv = {inv := λ (x : free_group α), quot.lift_on x (λ (L : list (α × bool)), free_group.mk (list.map (λ (x : α × bool), (x.fst, !x.snd)) L).reverse) free_group.has_inv._proof_1}

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

@[instance]

def free_group.group {α : Type u} :

group (free_group α)

Equations

free_group.group = {mul := has_mul.mul free_group.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, inv := has_inv.inv free_group.has_inv, mul_left_inv := _}

source

def free_group.of {α : Type u} :

α → free_group α

of x 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

free_group.of x = free_group.mk [(x, bool.tt)]

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.inj {α : Type u} {x y : α} :

free_group.of x = free_group.of y → x = y

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

source

def free_group.to_group.aux {α : Type u} {β : Type v} [group β] :

(α → β) → list (α × bool) → β

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

Equations

free_group.to_group.aux f = λ (L : list (α × bool)), (list.map (λ (x : α × bool), cond x.snd (f x.fst) (f x.fst)⁻¹) L).prod

source

theorem free_group.red.step.to_group {α : Type u} {L₁ L₂ : list (α × bool)} {β : Type v} [group β] {f : α → β} :

free_group.red.step L₁ L₂ → free_group.to_group.aux f L₁ = free_group.to_group.aux f L₂

source

def free_group.to_group.to_fun {α : 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 β. Note that this is the bare function; the group homomorphism is to_group.

Equations

free_group.to_group.to_fun f = quot.lift (free_group.to_group.aux f) _

source

def free_group.to_group {α : 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

free_group.to_group f = monoid_hom.mk' (free_group.to_group.to_fun f) _

source

@[simp]

theorem free_group.to_group.mk {α : Type u} {L : list (α × bool)} {β : Type v} [group β] {f : α → β} :

⇑(free_group.to_group 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.to_group.of {α : Type u} {β : Type v} [group β] {f : α → β} {x : α} :

⇑(free_group.to_group f) (free_group.of x) = f x

source

@[instance]

def free_group.to_group.is_group_hom {α : Type u} {β : Type v} [group β] {f : α → β} :

is_group_hom ⇑(free_group.to_group f)

Equations

free_group.to_group.is_group_hom = is_group_hom.mk

source

@[simp]

theorem free_group.to_group.mul {α : Type u} {β : Type v} [group β] {f : α → β} {x y : free_group α} :

⇑(free_group.to_group f) (x * y) = ⇑(free_group.to_group f) x * ⇑(free_group.to_group f) y

source

@[simp]

theorem free_group.to_group.one {α : Type u} {β : Type v} [group β] {f : α → β} :

⇑(free_group.to_group f) 1 = 1

source

@[simp]

theorem free_group.to_group.inv {α : Type u} {β : Type v} [group β] {f : α → β} {x : free_group α} :

⇑(free_group.to_group f) x⁻¹ = (⇑(free_group.to_group f) x)⁻¹

source

theorem free_group.to_group.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.to_group f) x

source

theorem free_group.to_group.of_eq {α : Type u} (x : free_group α) :

⇑(free_group.to_group free_group.of) x = x

source

theorem free_group.to_group.range_subset {α : Type u} {β : Type v} [group β] {f : α → β} {s : subgroup β} :

set.range f ⊆ ↑s → set.range ⇑(free_group.to_group f) ⊆ ↑s

source

theorem free_group.closure_subset {G : Type u_1} [group G] {s : set G} {t : subgroup G} :

s ⊆ ↑t → subgroup.closure s ≤ t

source

theorem free_group.to_group.range_eq_closure {α : Type u} {β : Type v} [group β] {f : α → β} :

set.range ⇑(free_group.to_group f) = ↑(subgroup.closure (set.range f))

source

def free_group.map.aux {α : Type u} {β : Type v} :

(α → β) → list (α × bool) → list (β × bool)

Given f : α → β, the canonical map list (α × bool) → list (β × bool).

Equations

free_group.map.aux f L = list.map (λ (x : α × bool), (f x.fst, x.snd)) L

source

def free_group.map.to_fun {α : Type u} {β : Type v} :

(α → β) → free_group α → free_group β

Any function from α to β extends uniquely to a group homomorphism from the free group over α to the free group over β. Note that this is the bare function; for the group homomorphism use map.

Equations

free_group.map.to_fun f x = quot.lift_on x (λ (L : list (α × bool)), free_group.mk (free_group.map.aux f L)) _

source

def free_group.map {α : Type u} {β : Type v} :

(α → β) → 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

free_group.map f = monoid_hom.mk' (free_group.map.to_fun f) _

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

@[simp]

theorem free_group.map.mul {α : Type u} {β : Type v} {f : α → β} {x y : free_group α} :

⇑(free_group.map f) (x * y) = ⇑(free_group.map f) x * ⇑(free_group.map f) y

source

@[simp]

theorem free_group.map.one {α : Type u} {β : Type v} {f : α → β} :

⇑(free_group.map f) 1 = 1

source

@[simp]

theorem free_group.map.inv {α : Type u} {β : Type v} {f : α → β} {x : free_group α} :

⇑(free_group.map f) x⁻¹ = (⇑(free_group.map f) x)⁻¹

source

theorem free_group.map.unique {α : Type u} {β : Type v} {f : α → β} (g : free_group α → free_group β) [is_group_hom g] (hg : ∀ (x : α), g (free_group.of x) = free_group.of (f x)) {x : free_group α} :

g x = ⇑(free_group.map f) x

source

def free_group.free_group_congr {α : Type u_1} {β : Type u_2} :

α ≃ β → free_group α ≃ free_group β

Equivalent types give rise to equivalent free groups.

Equations

free_group.free_group_congr e = {to_fun := ⇑(free_group.map ⇑e), inv_fun := ⇑(free_group.map ⇑(e.symm)), left_inv := _, right_inv := _}

source

theorem free_group.map_eq_to_group {α : Type u} {β : Type v} {f : α → β} {x : free_group α} :

⇑(free_group.map f) x = ⇑(free_group.to_group (free_group.of ∘ f)) x

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

free_group.prod = free_group.to_group id

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

@[simp]

theorem free_group.prod.mul {α : Type u} [group α] {x y : free_group α} :

⇑free_group.prod (x * y) = ⇑free_group.prod x * ⇑free_group.prod y

source

@[simp]

theorem free_group.prod.one {α : Type u} [group α] :

⇑free_group.prod 1 = 1

source

@[simp]

theorem free_group.prod.inv {α : Type u} [group α] {x : free_group α} :

⇑free_group.prod x⁻¹ = (⇑free_group.prod 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.to_group_eq_prod_map {α : Type u} {β : Type v} [group β] {f : α → β} {x : free_group α} :

⇑(free_group.to_group f) x = ⇑free_group.prod (⇑(free_group.map f) x)

source

def free_group.sum {α : Type u} [add_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 additive version of prod.

Equations

x.sum = ⇑free_group.prod x

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

@[instance]

def free_group.sum.is_group_hom {α : Type u} [add_group α] :

is_group_hom free_group.sum

Equations

free_group.sum.is_group_hom = _

source

@[simp]

theorem free_group.sum.mul {α : Type u} [add_group α] {x y : free_group α} :

(x * y).sum = x.sum + y.sum

source

@[simp]

theorem free_group.sum.one {α : Type u} [add_group α] :

1.sum = 0

source

@[simp]

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

free_group.free_group_empty_equiv_unit = {to_fun := λ (_x : free_group empty), (), inv_fun := λ (_x : unit), 1, left_inv := free_group.free_group_empty_equiv_unit._proof_1, right_inv := free_group.free_group_empty_equiv_unit._proof_2}

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

free_group.free_group_unit_equiv_int = {to_fun := λ (x : free_group unit), ((free_group.map (λ (_x : unit), 1)).to_fun x).sum, inv_fun := λ (x : ℤ), free_group.of () ^ x, left_inv := free_group.free_group_unit_equiv_int._proof_1, right_inv := free_group.free_group_unit_equiv_int._proof_2}

source

@[instance]

def free_group.monad :

monad free_group

Equations

free_group.monad = monad.mk

source

theorem free_group.induction_on {α : Type u} {C : free_group α → Prop} (z : free_group α) :

C 1 → (∀ (x : α), C (has_pure.pure x)) → (∀ (x : α), C (has_pure.pure x) → C (has_pure.pure x)⁻¹) → (∀ (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 <$> has_pure.pure x = has_pure.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 : α) :

has_pure.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

@[instance]

def free_group.is_lawful_monad :

is_lawful_monad free_group

Equations

free_group.is_lawful_monad = _

source

def free_group.reduce {α : Type u} [decidable_eq α] :

list (α × bool) → list (α × bool)

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

Equations

free_group.reduce L = L.rec_on list.nil (λ (hd1 : α × bool) (tl1 ih : list (α × bool)), ih.cases_on [hd1] (λ (hd2 : α × bool) (tl2 : list (α × bool)), ite (hd1.fst = hd2.fst ∧ hd1.snd = !hd2.snd) tl2 (hd1 :: hd2 :: tl2)))

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 α] :

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 α] :

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 α] :

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 α] :

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 α] :

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 α] :

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

free_group.to_word = quot.lift free_group.reduce free_group.to_word._proof_1

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 α] :

free_group.red L₁ L₂ → free_group.red L₁ L₃ → {L₄ // free_group.red L₂ L₄ ∧ free_group.red L₃ L₄}

Constructive Church-Rosser theorem (compare church_rosser).

Equations

free_group.reduce.church_rosser H12 H13 = ⟨free_group.reduce L₁, _⟩

source

@[instance]

def free_group.decidable_eq {α : Type u} [decidable_eq α] :

decidable_eq (free_group α)

Equations

free_group.decidable_eq = function.injective.decidable_eq free_group.decidable_eq._proof_1

source

@[instance]

def free_group.red.decidable_rel {α : Type u} [decidable_eq α] :

decidable_rel free_group.red

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 (free_group.red.decidable_rel tl1 tl2)) (λ (h : ¬(x1, b1) = (x2, b2)), free_group.red.decidable_rel._match_3 x1 b1 tl1 x2 b2 tl2 h (free_group.red.decidable_rel tl1 ((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 (free_group.red.decidable_rel tl [(x, !b)])
free_group.red.decidable_rel list.nil (hd2 :: tl2) = decidable.is_false _
free_group.red.decidable_rel list.nil list.nil = 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 (decidable.is_true H) = decidable.is_true _
free_group.red.decidable_rel._match_2 x1 b1 tl1 x2 b2 tl2 h (decidable.is_false H) = decidable.is_false _
free_group.red.decidable_rel._match_3 x1 b1 tl1 x2 b2 tl2 h (decidable.is_true H) = decidable.is_true _
free_group.red.decidable_rel._match_3 x1 b1 tl1 x2 b2 tl2 h (decidable.is_false H) = decidable.is_false _
free_group.red.decidable_rel._match_1 x b tl (decidable.is_true H) = decidable.is_true _
free_group.red.decidable_rel._match_1 x b tl (decidable.is_false H) = decidable.is_false _