mathlib documentation

group_theory.​free_group

group_theory.​free_group

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

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

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

Reflexive-transitive closure of red.step

Equations
theorem free_group.​red.​refl {α : Type u} {L : list × bool)} :

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₃

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₄

@[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_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_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)} :
free_group.red.step L₂ L₃free_group.red.step (L₁ ++ L₂) (L₁ ++ L₃)

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

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

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₂

theorem free_group.​red.​not_step_singleton {α : Type u} {L : list × bool)} {p : α × bool} :

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₂

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₂

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

theorem free_group.​red.​step.​to_red {α : Type u} {L₁ L₂ : list × bool)} :
free_group.red.step L₁ L₂free_group.red L₁ L₂

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.

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

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₂

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₂

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

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₂

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} :
free_group.red [x] 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} :

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_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)])

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

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

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

theorem free_group.​red.​sizeof_of_step {α : Type u} {L₁ L₂ : list × bool)} :
free_group.red.step L₁ L₂L₂.sizeof < L₁.sizeof

theorem free_group.​red.​length {α : Type u} {L₁ L₂ : list × bool)} :
free_group.red L₁ L₂(∃ (n : ), L₁.length = L₂.length + 2 * n)

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

theorem free_group.​join_red_of_step {α : 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 uType 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
def free_group.​mk {α : Type u} :
list × bool)free_group α

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

Equations
@[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)), free_group.red.step L₁ L₂f L₁ = f L₂) :
quot.lift f H (free_group.mk L) = 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)), free_group.red.step L₁ L₂f L₁ = f L₂) :

@[instance]
def free_group.​has_one {α : Type u} :

Equations
@[instance]
def free_group.​inhabited {α : Type u} :

Equations
@[instance]
def free_group.​has_mul {α : Type u} :

Equations
@[simp]
theorem free_group.​mul_mk {α : Type u} {L₁ L₂ : list × bool)} :

@[instance]
def free_group.​has_inv {α : Type u} :

Equations
@[simp]
theorem free_group.​inv_mk {α : Type u} {L : list × bool)} :

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

theorem free_group.​of.​inj {α : Type u} {x y : α} :

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

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

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

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

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

@[simp]
theorem free_group.​to_group.​of {α : Type u} {β : Type v} [group β] {f : α → β} {x : α} :

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

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

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

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

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

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

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

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

def free_group.​map.​aux {α : Type u} {β : Type v} :
(α → β)list × bool)list × bool)

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

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

@[simp]
theorem free_group.​map.​id {α : Type u} {x : free_group α} :

@[simp]
theorem free_group.​map.​id' {α : Type u} {x : free_group α} :
(free_group.map (λ (z : α), z)) x = x

theorem free_group.​map.​comp {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} {x : free_group α} :

@[simp]
theorem free_group.​map.​of {α : Type u} {β : Type v} {f : α → β} {x : α} :

@[simp]
theorem free_group.​map.​mul {α : Type u} {β : Type v} {f : α → β} {x y : free_group α} :

@[simp]
theorem free_group.​map.​one {α : Type u} {β : Type v} {f : α → β} :

@[simp]
theorem free_group.​map.​inv {α : Type u} {β : Type v} {f : α → β} {x : free_group α} :

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

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
theorem free_group.​map_eq_to_group {α : Type u} {β : Type v} {f : α → β} {x : free_group α} :

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

Equations
@[simp]
theorem free_group.​prod_mk {α : Type u} {L : list × bool)} [group α] :

@[simp]
theorem free_group.​prod.​of {α : Type u} [group α] {x : α} :

@[simp]

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

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

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

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

@[simp]
theorem free_group.​sum.​of {α : Type u} [add_group α] {x : α} :

@[simp]
theorem free_group.​sum.​mul {α : Type u} [add_group α] {x y : free_group α} :
(x * y).sum = x.sum + y.sum

@[simp]
theorem free_group.​sum.​one {α : Type u} [add_group α] :
1.sum = 0

@[simp]
theorem free_group.​sum.​inv {α : Type u} [add_group α] {x : free_group α} :

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
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 xC yC (x * y))C z

@[simp]
theorem free_group.​map_pure {α β : Type u} (f : α → β) (x : α) :

@[simp]
theorem free_group.​map_one {α β : Type u} (f : α → β) :
f <$> 1 = 1

@[simp]
theorem free_group.​map_mul {α β : Type u} (f : α → β) (x y : free_group α) :
f <$> (x * y) = f <$> x * f <$> y

@[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 : α → free_group β) (x : α) :

@[simp]
theorem free_group.​one_bind {α β : Type u} (f : α → free_group β) :
1 >>= f = 1

@[simp]
theorem free_group.​mul_bind {α β : Type u} (f : α → free_group β) (x y : free_group α) :
x * y >>= f = (x >>= f) * (y >>= f)

@[simp]
theorem free_group.​inv_bind {α β : Type u} (f : α → free_group β) (x : free_group α) :
x⁻¹ >>= f = (x >>= f)⁻¹

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

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_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

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

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

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

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

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

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

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

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

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

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

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

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

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
theorem free_group.​to_word.​mk {α : Type u} [decidable_eq α] {x : free_group α} :

theorem free_group.​to_word.​inj {α : Type u} [decidable_eq α] (x y : free_group α) :
x.to_word = y.to_wordx = y

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

Equations
@[instance]

Equations
def free_group.​red.​enum {α : Type u} [decidable_eq α] :
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 α] :
L₂ free_group.red.enum L₁free_group.red L₁ L₂

theorem free_group.​red.​enum.​complete {α : Type u} {L₁ L₂ : list × bool)} [decidable_eq α] :
free_group.red L₁ L₂L₂ free_group.red.enum L₁

@[instance]
def free_group.​fintype {α : Type u} {L₁ : list × bool)} [decidable_eq α] :
fintype {L₂ // free_group.red L₁ L₂}

Equations