Free monoid over a given alphabet #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
free_monoid α: free monoid over alphabetα; defined as a synonym forlist αwith multiplication given by(++).free_monoid.of: embeddingα → free_monoid αsending each elementxto[x];free_monoid.lift: natural equivalence betweenα → Mandfree_monoid α →* Mfree_monoid.map: embedding ofα → βintofree_monoid α →* free_monoid βgiven bylist.map.
Free nonabelian additive monoid over a given alphabet
Equations
- free_add_monoid α = list α
Instances for free_add_monoid
@[protected, instance]
Equations
@[protected, instance]
Equations
The identity equivalence between free_monoid α and list α.
Equations
The identity equivalence between free_add_monoid α and list α.
Equations
The identity equivalence between list α and free_monoid α.
Equations
The identity equivalence between list α and free_add_monoid α.
Equations
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[protected, instance]
Equations
- free_add_monoid.cancel_add_monoid = {add := λ (x y : free_add_monoid α), ⇑free_add_monoid.of_list (⇑free_add_monoid.to_list x ++ ⇑free_add_monoid.to_list y), add_assoc := _, add_left_cancel := _, zero := ⇑free_add_monoid.of_list list.nil, zero_add := _, add_zero := _, nsmul := add_left_cancel_monoid.nsmul._default (⇑free_add_monoid.of_list list.nil) (λ (x y : free_add_monoid α), ⇑free_add_monoid.of_list (⇑free_add_monoid.to_list x ++ ⇑free_add_monoid.to_list y)) list.nil_append list.append_nil, nsmul_zero' := _, nsmul_succ' := _, add_right_cancel := _}
@[protected, instance]
Equations
- free_monoid.cancel_monoid = {mul := λ (x y : free_monoid α), ⇑free_monoid.of_list (⇑free_monoid.to_list x ++ ⇑free_monoid.to_list y), mul_assoc := _, mul_left_cancel := _, one := ⇑free_monoid.of_list list.nil, one_mul := _, mul_one := _, npow := left_cancel_monoid.npow._default (⇑free_monoid.of_list list.nil) (λ (x y : free_monoid α), ⇑free_monoid.of_list (⇑free_monoid.to_list x ++ ⇑free_monoid.to_list y)) list.nil_append list.append_nil, npow_zero' := _, npow_succ' := _, mul_right_cancel := _}
@[protected, instance]
Equations
@[protected, instance]
Equations
- free_monoid.inhabited = {default := 1}
@[simp]
@[simp]
@[simp]
theorem
free_monoid.to_list_mul
{α : Type u_1}
(xs ys : free_monoid α) :
⇑free_monoid.to_list (xs * ys) = ⇑free_monoid.to_list xs ++ ⇑free_monoid.to_list ys
@[simp]
theorem
free_add_monoid.to_list_add
{α : Type u_1}
(xs ys : free_add_monoid α) :
⇑free_add_monoid.to_list (xs + ys) = ⇑free_add_monoid.to_list xs ++ ⇑free_add_monoid.to_list ys
@[simp]
theorem
free_add_monoid.of_list_append
{α : Type u_1}
(xs ys : list α) :
⇑free_add_monoid.of_list (xs ++ ys) = ⇑free_add_monoid.of_list xs + ⇑free_add_monoid.of_list ys
@[simp]
theorem
free_monoid.of_list_append
{α : Type u_1}
(xs ys : list α) :
⇑free_monoid.of_list (xs ++ ys) = ⇑free_monoid.of_list xs * ⇑free_monoid.of_list ys
@[simp]
@[simp]
@[simp]
@[simp]
Embeds an element of α into free_monoid α as a singleton list.
Equations
Embeds an element of α into free_add_monoid α as a singleton list.
Equations
@[simp]
@[simp]
theorem
free_monoid.to_list_of
{α : Type u_1}
(x : α) :
⇑free_monoid.to_list (free_monoid.of x) = [x]
@[simp]
theorem
free_monoid.of_list_cons
{α : Type u_1}
(x : α)
(xs : list α) :
⇑free_monoid.of_list (x :: xs) = free_monoid.of x * ⇑free_monoid.of_list xs
@[simp]
theorem
free_monoid.to_list_of_mul
{α : Type u_1}
(x : α)
(xs : free_monoid α) :
⇑free_monoid.to_list (free_monoid.of x * xs) = x :: ⇑free_monoid.to_list xs
def
free_monoid.rec_on
{α : Type u_1}
{C : free_monoid α → Sort u_2}
(xs : free_monoid α)
(h0 : C 1)
(ih : Π (x : α) (xs : free_monoid α), C xs → C (free_monoid.of x * xs)) :
C xs
Recursor for free_monoid using 1 and free_monoid.of x * xs instead of [] and
x :: xs.
def
free_add_monoid.rec_on
{α : Type u_1}
{C : free_add_monoid α → Sort u_2}
(xs : free_add_monoid α)
(h0 : C 0)
(ih : Π (x : α) (xs : free_add_monoid α), C xs → C (free_add_monoid.of x + xs)) :
C xs
Recursor for free_add_monoid using 0 and free_add_monoid.of x + xs instead of [] and
x :: xs.
@[simp]
theorem
free_add_monoid.rec_on_zero
{α : Type u_1}
{C : free_add_monoid α → Sort u_2}
(h0 : C 0)
(ih : Π (x : α) (xs : free_add_monoid α), C xs → C (free_add_monoid.of x + xs)) :
@[simp]
theorem
free_monoid.rec_on_one
{α : Type u_1}
{C : free_monoid α → Sort u_2}
(h0 : C 1)
(ih : Π (x : α) (xs : free_monoid α), C xs → C (free_monoid.of x * xs)) :
@[simp]
theorem
free_monoid.rec_on_of_mul
{α : Type u_1}
{C : free_monoid α → Sort u_2}
(x : α)
(xs : free_monoid α)
(h0 : C 1)
(ih : Π (x : α) (xs : free_monoid α), C xs → C (free_monoid.of x * xs)) :
(free_monoid.of x * xs).rec_on h0 ih = ih x xs (xs.rec_on h0 ih)
@[simp]
theorem
free_add_monoid.rec_on_of_add
{α : Type u_1}
{C : free_add_monoid α → Sort u_2}
(x : α)
(xs : free_add_monoid α)
(h0 : C 0)
(ih : Π (x : α) (xs : free_add_monoid α), C xs → C (free_add_monoid.of x + xs)) :
(free_add_monoid.of x + xs).rec_on h0 ih = ih x xs (xs.rec_on h0 ih)
def
free_add_monoid.cases_on
{α : Type u_1}
{C : free_add_monoid α → Sort u_2}
(xs : free_add_monoid α)
(h0 : C 0)
(ih : Π (x : α) (xs : free_add_monoid α), C (free_add_monoid.of x + xs)) :
C xs
A version of list.cases_on for free_add_monoid using 0 and free_add_monoid.of x + xs
instead of [] and x :: xs.
def
free_monoid.cases_on
{α : Type u_1}
{C : free_monoid α → Sort u_2}
(xs : free_monoid α)
(h0 : C 1)
(ih : Π (x : α) (xs : free_monoid α), C (free_monoid.of x * xs)) :
C xs
A version of list.cases_on for free_monoid using 1 and free_monoid.of x * xs instead of
[] and x :: xs.
@[simp]
theorem
free_add_monoid.cases_on_zero
{α : Type u_1}
{C : free_add_monoid α → Sort u_2}
(h0 : C 0)
(ih : Π (x : α) (xs : free_add_monoid α), C (free_add_monoid.of x + xs)) :
@[simp]
theorem
free_monoid.cases_on_one
{α : Type u_1}
{C : free_monoid α → Sort u_2}
(h0 : C 1)
(ih : Π (x : α) (xs : free_monoid α), C (free_monoid.of x * xs)) :
@[simp]
theorem
free_add_monoid.cases_on_of_add
{α : Type u_1}
{C : free_add_monoid α → Sort u_2}
(x : α)
(xs : free_add_monoid α)
(h0 : C 0)
(ih : Π (x : α) (xs : free_add_monoid α), C (free_add_monoid.of x + xs)) :
(free_add_monoid.of x + xs).cases_on h0 ih = ih x xs
@[simp]
theorem
free_monoid.cases_on_of_mul
{α : Type u_1}
{C : free_monoid α → Sort u_2}
(x : α)
(xs : free_monoid α)
(h0 : C 1)
(ih : Π (x : α) (xs : free_monoid α), C (free_monoid.of x * xs)) :
(free_monoid.of x * xs).cases_on h0 ih = ih x xs
@[ext]
theorem
free_monoid.hom_eq
{α : Type u_1}
{M : Type u_4}
[monoid M]
⦃f g : free_monoid α →* M⦄
(h : ∀ (x : α), ⇑f (free_monoid.of x) = ⇑g (free_monoid.of x)) :
f = g
@[ext]
theorem
free_add_monoid.hom_eq
{α : Type u_1}
{M : Type u_4}
[add_monoid M]
⦃f g : free_add_monoid α →+ M⦄
(h : ∀ (x : α), ⇑f (free_add_monoid.of x) = ⇑g (free_add_monoid.of x)) :
f = g
A variant of list.sum that has [x].sum = x true definitionally.
The purpose is to make free_add_monoid.lift_eval_of true by rfl.
Equations
- free_add_monoid.sum_aux l = l.rec_on 0 (λ (x : M) (xs : list M) (_x : M), list.foldl has_add.add x xs)
A variant of list.prod that has [x].prod = x true definitionally.
The purpose is to make free_monoid.lift_eval_of true by rfl.
Equations
- free_monoid.prod_aux l = l.rec_on 1 (λ (x : M) (xs : list M) (_x : M), list.foldl has_mul.mul x xs)
def
free_add_monoid.lift
{α : Type u_1}
{M : Type u_4}
[add_monoid M] :
(α → M) ≃ (free_add_monoid α →+ M)
Equivalence between maps α → A and additive monoid homomorphisms
free_add_monoid α →+ A.
Equations
- free_add_monoid.lift = {to_fun := λ (f : α → M), {to_fun := λ (l : free_add_monoid α), free_add_monoid.sum_aux (list.map f (⇑free_add_monoid.to_list l)), map_zero' := _, map_add' := _}, inv_fun := λ (f : free_add_monoid α →+ M) (x : α), ⇑f (free_add_monoid.of x), left_inv := _, right_inv := _}
Equivalence between maps α → M and monoid homomorphisms free_monoid α →* M.
Equations
- free_monoid.lift = {to_fun := λ (f : α → M), {to_fun := λ (l : free_monoid α), free_monoid.prod_aux (list.map f (⇑free_monoid.to_list l)), map_one' := _, map_mul' := _}, inv_fun := λ (f : free_monoid α →* M) (x : α), ⇑f (free_monoid.of x), left_inv := _, right_inv := _}
@[simp]
theorem
free_add_monoid.lift_symm_apply
{α : Type u_1}
{M : Type u_4}
[add_monoid M]
(f : free_add_monoid α →+ M) :
@[simp]
theorem
free_monoid.lift_symm_apply
{α : Type u_1}
{M : Type u_4}
[monoid M]
(f : free_monoid α →* M) :
⇑(free_monoid.lift.symm) f = ⇑f ∘ free_monoid.of
theorem
free_monoid.lift_apply
{α : Type u_1}
{M : Type u_4}
[monoid M]
(f : α → M)
(l : free_monoid α) :
⇑(⇑free_monoid.lift f) l = (list.map f (⇑free_monoid.to_list l)).prod
theorem
free_add_monoid.lift_apply
{α : Type u_1}
{M : Type u_4}
[add_monoid M]
(f : α → M)
(l : free_add_monoid α) :
⇑(⇑free_add_monoid.lift f) l = (list.map f (⇑free_add_monoid.to_list l)).sum
theorem
free_monoid.lift_comp_of
{α : Type u_1}
{M : Type u_4}
[monoid M]
(f : α → M) :
⇑(⇑free_monoid.lift f) ∘ free_monoid.of = f
@[simp]
theorem
free_add_monoid.lift_eval_of
{α : Type u_1}
{M : Type u_4}
[add_monoid M]
(f : α → M)
(x : α) :
⇑(⇑free_add_monoid.lift f) (free_add_monoid.of x) = f x
@[simp]
theorem
free_monoid.lift_eval_of
{α : Type u_1}
{M : Type u_4}
[monoid M]
(f : α → M)
(x : α) :
⇑(⇑free_monoid.lift f) (free_monoid.of x) = f x
@[simp]
theorem
free_monoid.lift_restrict
{α : Type u_1}
{M : Type u_4}
[monoid M]
(f : free_monoid α →* M) :
⇑free_monoid.lift (⇑f ∘ free_monoid.of) = f
@[simp]
theorem
free_add_monoid.lift_restrict
{α : Type u_1}
{M : Type u_4}
[add_monoid M]
(f : free_add_monoid α →+ M) :
theorem
free_add_monoid.comp_lift
{α : Type u_1}
{M : Type u_4}
[add_monoid M]
{N : Type u_5}
[add_monoid N]
(g : M →+ N)
(f : α → M) :
g.comp (⇑free_add_monoid.lift f) = ⇑free_add_monoid.lift (⇑g ∘ f)
theorem
free_monoid.hom_map_lift
{α : Type u_1}
{M : Type u_4}
[monoid M]
{N : Type u_5}
[monoid N]
(g : M →* N)
(f : α → M)
(x : free_monoid α) :
⇑g (⇑(⇑free_monoid.lift f) x) = ⇑(⇑free_monoid.lift (⇑g ∘ f)) x
theorem
free_add_monoid.hom_map_lift
{α : Type u_1}
{M : Type u_4}
[add_monoid M]
{N : Type u_5}
[add_monoid N]
(g : M →+ N)
(f : α → M)
(x : free_add_monoid α) :
⇑g (⇑(⇑free_add_monoid.lift f) x) = ⇑(⇑free_add_monoid.lift (⇑g ∘ f)) x
def
free_monoid.mk_mul_action
{α : Type u_1}
{β : Type u_2}
(f : α → β → β) :
mul_action (free_monoid α) β
Define a multiplicative action of free_monoid α on β.
Equations
- free_monoid.mk_mul_action f = {to_has_smul := {smul := λ (l : free_monoid α) (b : β), list.foldr f b (⇑free_monoid.to_list l)}, one_smul := _, mul_smul := _}
def
free_add_monoid.mk_add_action
{α : Type u_1}
{β : Type u_2}
(f : α → β → β) :
add_action (free_add_monoid α) β
Define an additive action of free_add_monoid α on β.
Equations
- free_add_monoid.mk_add_action f = {to_has_vadd := {vadd := λ (l : free_add_monoid α) (b : β), list.foldr f b (⇑free_add_monoid.to_list l)}, zero_vadd := _, add_vadd := _}
theorem
free_add_monoid.vadd_def
{α : Type u_1}
{β : Type u_2}
(f : α → β → β)
(l : free_add_monoid α)
(b : β) :
l +ᵥ b = list.foldr f b (⇑free_add_monoid.to_list l)
theorem
free_monoid.smul_def
{α : Type u_1}
{β : Type u_2}
(f : α → β → β)
(l : free_monoid α)
(b : β) :
l • b = list.foldr f b (⇑free_monoid.to_list l)
theorem
free_monoid.of_list_smul
{α : Type u_1}
{β : Type u_2}
(f : α → β → β)
(l : list α)
(b : β) :
⇑free_monoid.of_list l • b = list.foldr f b l
theorem
free_add_monoid.of_list_vadd
{α : Type u_1}
{β : Type u_2}
(f : α → β → β)
(l : list α)
(b : β) :
⇑free_add_monoid.of_list l +ᵥ b = list.foldr f b l
@[simp]
theorem
free_add_monoid.of_vadd
{α : Type u_1}
{β : Type u_2}
(f : α → β → β)
(x : α)
(y : β) :
free_add_monoid.of x +ᵥ y = f x y
@[simp]
theorem
free_monoid.of_smul
{α : Type u_1}
{β : Type u_2}
(f : α → β → β)
(x : α)
(y : β) :
free_monoid.of x • y = f x y
The unique additive monoid homomorphism free_add_monoid α →+ free_add_monoid β
that sends each of x to of (f x).
Equations
- free_add_monoid.map f = {to_fun := λ (l : free_add_monoid α), ⇑free_add_monoid.of_list (list.map f (⇑free_add_monoid.to_list l)), map_zero' := _, map_add' := _}
The unique monoid homomorphism free_monoid α →* free_monoid β that sends
each of x to of (f x).
Equations
- free_monoid.map f = {to_fun := λ (l : free_monoid α), ⇑free_monoid.of_list (list.map f (⇑free_monoid.to_list l)), map_one' := _, map_mul' := _}
@[simp]
theorem
free_add_monoid.map_of
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(x : α) :
⇑(free_add_monoid.map f) (free_add_monoid.of x) = free_add_monoid.of (f x)
@[simp]
theorem
free_monoid.map_of
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(x : α) :
⇑(free_monoid.map f) (free_monoid.of x) = free_monoid.of (f x)
theorem
free_add_monoid.to_list_map
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(xs : free_add_monoid α) :
⇑free_add_monoid.to_list (⇑(free_add_monoid.map f) xs) = list.map f (⇑free_add_monoid.to_list xs)
theorem
free_monoid.to_list_map
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(xs : free_monoid α) :
⇑free_monoid.to_list (⇑(free_monoid.map f) xs) = list.map f (⇑free_monoid.to_list xs)
theorem
free_add_monoid.of_list_map
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(xs : list α) :
⇑free_add_monoid.of_list (list.map f xs) = ⇑(free_add_monoid.map f) (⇑free_add_monoid.of_list xs)
theorem
free_monoid.of_list_map
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(xs : list α) :
⇑free_monoid.of_list (list.map f xs) = ⇑(free_monoid.map f) (⇑free_monoid.of_list xs)
theorem
free_monoid.lift_of_comp_eq_map
{α : Type u_1}
{β : Type u_2}
(f : α → β) :
⇑free_monoid.lift (λ (x : α), free_monoid.of (f x)) = free_monoid.map f
theorem
free_add_monoid.lift_of_comp_eq_map
{α : Type u_1}
{β : Type u_2}
(f : α → β) :
⇑free_add_monoid.lift (λ (x : α), free_add_monoid.of (f x)) = free_add_monoid.map f
theorem
free_add_monoid.map_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(g : β → γ)
(f : α → β) :
free_add_monoid.map (g ∘ f) = (free_add_monoid.map g).comp (free_add_monoid.map f)
theorem
free_monoid.map_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(g : β → γ)
(f : α → β) :
free_monoid.map (g ∘ f) = (free_monoid.map g).comp (free_monoid.map f)
@[simp]
@[simp]