# mathlib3documentation

algebra.free_monoid.basic

# 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 for list α with multiplication given by (++).
• free_monoid.of: embedding α → free_monoid α sending each element x to [x];
• free_monoid.lift: natural equivalence between α → M and free_monoid α →* M
• free_monoid.map: embedding of α → β into free_monoid α →* free_monoid β given by list.map.
def free_add_monoid (α : Type u_1) :
Type u_1

Free nonabelian additive monoid over a given alphabet

Equations
Instances for free_add_monoid
def free_monoid (α : Type u_1) :
Type u_1

Free monoid over a given alphabet.

Equations
Instances for free_monoid
@[protected, instance]
Equations
@[protected, instance]
def free_monoid.decidable_eq {α : Type u_1} [decidable_eq α] :
Equations
def free_monoid.to_list {α : Type u_1} :
list α

The identity equivalence between free_monoid α and list α.

Equations
def free_add_monoid.to_list {α : Type u_1} :

The identity equivalence between free_add_monoid α and list α.

Equations
def free_monoid.of_list {α : Type u_1} :
list α

The identity equivalence between list α and free_monoid α.

Equations
def free_add_monoid.of_list {α : Type u_1} :

The identity equivalence between list α and free_add_monoid α.

Equations
@[simp]
theorem free_add_monoid.to_list_symm {α : Type u_1} :
@[simp]
theorem free_monoid.to_list_symm {α : Type u_1} :
@[simp]
theorem free_add_monoid.of_list_symm {α : Type u_1} :
@[simp]
theorem free_monoid.of_list_symm {α : Type u_1} :
@[simp]
theorem free_add_monoid.to_list_of_list {α : Type u_1} (l : list α) :
@[simp]
theorem free_monoid.to_list_of_list {α : Type u_1} (l : list α) :
@[simp]
theorem free_monoid.of_list_to_list {α : Type u_1} (xs : free_monoid α) :
@[simp]
@[simp]
@[simp]
theorem free_monoid.to_list_comp_of_list {α : Type u_1} :
@[simp]
theorem free_monoid.of_list_comp_to_list {α : Type u_1} :
@[simp]
@[protected, instance]
Equations
@[protected, instance]
def free_monoid.cancel_monoid {α : Type u_1} :
Equations
@[protected, instance]
def free_add_monoid.inhabited {α : Type u_1} :
Equations
@[protected, instance]
def free_monoid.inhabited {α : Type u_1} :
Equations
@[simp]
theorem free_add_monoid.to_list_zero {α : Type u_1} :
@[simp]
theorem free_monoid.to_list_one {α : Type u_1} :
@[simp]
theorem free_add_monoid.of_list_nil {α : Type u_1} :
@[simp]
theorem free_monoid.of_list_nil {α : Type u_1} :
@[simp]
theorem free_monoid.to_list_mul {α : Type u_1} (xs ys : free_monoid α) :
@[simp]
@[simp]
theorem free_add_monoid.of_list_append {α : Type u_1} (xs ys : list α) :
@[simp]
theorem free_monoid.of_list_append {α : Type u_1} (xs ys : list α) :
@[simp]
theorem free_monoid.to_list_prod {α : Type u_1} (xs : list (free_monoid α)) :
@[simp]
theorem free_add_monoid.to_list_sum {α : Type u_1} (xs : list ) :
@[simp]
theorem free_monoid.of_list_join {α : Type u_1} (xs : list (list α)) :
@[simp]
theorem free_add_monoid.of_list_join {α : Type u_1} (xs : list (list α)) :
def free_monoid.of {α : Type u_1} (x : α) :

Embeds an element of α into free_monoid α as a singleton list.

Equations
def free_add_monoid.of {α : Type u_1} (x : α) :

Embeds an element of α into free_add_monoid α as a singleton list.

Equations
@[simp]
theorem free_add_monoid.to_list_of {α : Type u_1} (x : α) :
@[simp]
theorem free_monoid.to_list_of {α : Type u_1} (x : α) :
theorem free_add_monoid.of_list_singleton {α : Type u_1} (x : α) :
theorem free_monoid.of_list_singleton {α : Type u_1} (x : α) :
@[simp]
theorem free_monoid.of_list_cons {α : Type u_1} (x : α) (xs : list α) :
@[simp]
theorem free_add_monoid.of_list_cons {α : Type u_1} (x : α) (xs : list α) :
theorem free_monoid.to_list_of_mul {α : Type u_1} (x : α) (xs : free_monoid α) :
=
theorem free_add_monoid.of_injective {α : Type u_1} :
theorem free_monoid.of_injective {α : Type u_1} :
def free_monoid.rec_on {α : Type u_1} {C : Sort u_2} (xs : free_monoid α) (h0 : C 1) (ih : Π (x : α) (xs : , C xs C * xs)) :
C xs

Recursor for free_monoid using 1 and free_monoid.of x * xs instead of [] and x :: xs.

Equations
• xs.rec_on h0 ih = list.rec_on xs h0 ih
def free_add_monoid.rec_on {α : Type u_1} {C : Sort u_2} (xs : free_add_monoid α) (h0 : C 0) (ih : Π (x : α) (xs : , C xs C + xs)) :
C xs

Recursor for free_add_monoid using 0 and free_add_monoid.of x + xs instead of [] and x :: xs.

Equations
• xs.rec_on h0 ih = list.rec_on xs h0 ih
@[simp]
theorem free_add_monoid.rec_on_zero {α : Type u_1} {C : Sort u_2} (h0 : C 0) (ih : Π (x : α) (xs : , C xs C + xs)) :
0.rec_on h0 ih = h0
@[simp]
theorem free_monoid.rec_on_one {α : Type u_1} {C : Sort u_2} (h0 : C 1) (ih : Π (x : α) (xs : , C xs C * xs)) :
1.rec_on h0 ih = h0
@[simp]
theorem free_monoid.rec_on_of_mul {α : Type u_1} {C : Sort u_2} (x : α) (xs : free_monoid α) (h0 : C 1) (ih : Π (x : α) (xs : , C xs C * xs)) :
* 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 : Sort u_2} (x : α) (xs : free_add_monoid α) (h0 : C 0) (ih : Π (x : α) (xs : , C xs C + xs)) :
+ xs).rec_on h0 ih = ih x xs (xs.rec_on h0 ih)
def free_add_monoid.cases_on {α : Type u_1} {C : Sort u_2} (xs : free_add_monoid α) (h0 : C 0) (ih : Π (x : α) (xs : , C + 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.

Equations
def free_monoid.cases_on {α : Type u_1} {C : Sort u_2} (xs : free_monoid α) (h0 : C 1) (ih : Π (x : α) (xs : , C * 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.

Equations
@[simp]
theorem free_add_monoid.cases_on_zero {α : Type u_1} {C : Sort u_2} (h0 : C 0) (ih : Π (x : α) (xs : , C + xs)) :
0.cases_on h0 ih = h0
@[simp]
theorem free_monoid.cases_on_one {α : Type u_1} {C : Sort u_2} (h0 : C 1) (ih : Π (x : α) (xs : , C * xs)) :
1.cases_on h0 ih = h0
@[simp]
theorem free_add_monoid.cases_on_of_add {α : Type u_1} {C : Sort u_2} (x : α) (xs : free_add_monoid α) (h0 : C 0) (ih : Π (x : α) (xs : , C + xs)) :
+ xs).cases_on h0 ih = ih x xs
@[simp]
theorem free_monoid.cases_on_of_mul {α : Type u_1} {C : Sort u_2} (x : α) (xs : free_monoid α) (h0 : C 1) (ih : Π (x : α) (xs : , C * xs)) :
* 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 : →* M⦄ (h : (x : α), f = g ) :
f = g
@[ext]
theorem free_add_monoid.hom_eq {α : Type u_1} {M : Type u_4} [add_monoid M] ⦃f g : →+ M⦄ (h : (x : α), f = g ) :
f = g
def free_add_monoid.sum_aux {M : Type u_1} [add_monoid M] (l : list M) :
M

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
• = l.rec_on 0 (λ (x : M) (xs : list M) (_x : M), xs)
def free_monoid.prod_aux {M : Type u_1} [monoid M] (l : list M) :
M

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
• = l.rec_on 1 (λ (x : M) (xs : list M) (_x : M), xs)
theorem free_add_monoid.sum_aux_eq {M : Type u_4} [add_monoid M] (l : list M) :
theorem free_monoid.prod_aux_eq {M : Type u_4} [monoid M] (l : list M) :
def free_add_monoid.lift {α : Type u_1} {M : Type u_4} [add_monoid M] :
M) →+ M)

Equivalence between maps α → A and additive monoid homomorphisms free_add_monoid α →+ A.

Equations
def free_monoid.lift {α : Type u_1} {M : Type u_4} [monoid M] :
M) →* M)

Equivalence between maps α → M and monoid homomorphisms free_monoid α →* M.

Equations
@[simp]
theorem free_add_monoid.lift_symm_apply {α : Type u_1} {M : Type u_4} [add_monoid M] (f : →+ M) :
@[simp]
theorem free_monoid.lift_symm_apply {α : Type u_1} {M : Type u_4} [monoid M] (f : →* M) :
theorem free_monoid.lift_apply {α : Type u_1} {M : Type u_4} [monoid M] (f : α M) (l : free_monoid α) :
l = (list.map f .prod
theorem free_add_monoid.lift_apply {α : Type u_1} {M : Type u_4} [add_monoid M] (f : α M) (l : free_add_monoid α) :
theorem free_add_monoid.lift_comp_of {α : Type u_1} {M : Type u_4} [add_monoid M] (f : α M) :
theorem free_monoid.lift_comp_of {α : Type u_1} {M : Type u_4} [monoid M] (f : α M) :
@[simp]
theorem free_add_monoid.lift_eval_of {α : Type u_1} {M : Type u_4} [add_monoid M] (f : α M) (x : α) :
= f x
@[simp]
theorem free_monoid.lift_eval_of {α : Type u_1} {M : Type u_4} [monoid M] (f : α M) (x : α) :
= f x
@[simp]
theorem free_monoid.lift_restrict {α : Type u_1} {M : Type u_4} [monoid M] (f : →* M) :
@[simp]
theorem free_add_monoid.lift_restrict {α : Type u_1} {M : Type u_4} [add_monoid M] (f : →+ M) :
theorem free_monoid.comp_lift {α : Type u_1} {M : Type u_4} [monoid M] {N : Type u_5} [monoid N] (g : M →* N) (f : α 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) :
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 α) :
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 α) :
def free_monoid.mk_mul_action {α : Type u_1} {β : Type u_2} (f : α β β) :
β

Define a multiplicative action of free_monoid α on β.

Equations
def free_add_monoid.mk_add_action {α : Type u_1} {β : Type u_2} (f : α β β) :

Define an additive action of free_add_monoid α on β.

Equations
theorem free_add_monoid.vadd_def {α : Type u_1} {β : Type u_2} (f : α β β) (l : free_add_monoid α) (b : β) :
l +ᵥ b =
theorem free_monoid.smul_def {α : Type u_1} {β : Type u_2} (f : α β β) (l : free_monoid α) (b : β) :
l b = b
theorem free_monoid.of_list_smul {α : Type u_1} {β : Type u_2} (f : α β β) (l : list α) (b : β) :
= b l
theorem free_add_monoid.of_list_vadd {α : Type u_1} {β : Type u_2} (f : α β β) (l : list α) (b : β) :
= b l
@[simp]
theorem free_add_monoid.of_vadd {α : Type u_1} {β : Type u_2} (f : α β β) (x : α) (y : β) :
= f x y
@[simp]
theorem free_monoid.of_smul {α : Type u_1} {β : Type u_2} (f : α β β) (x : α) (y : β) :
= f x y
def free_add_monoid.map {α : Type u_1} {β : Type u_2} (f : α β) :

The unique additive monoid homomorphism free_add_monoid α →+ free_add_monoid β that sends each of x to of (f x).

Equations
def free_monoid.map {α : Type u_1} {β : Type u_2} (f : α β) :

The unique monoid homomorphism free_monoid α →* free_monoid β that sends each of x to of (f x).

Equations
@[simp]
theorem free_add_monoid.map_of {α : Type u_1} {β : Type u_2} (f : α β) (x : α) :
@[simp]
theorem free_monoid.map_of {α : Type u_1} {β : Type u_2} (f : α β) (x : α) :
theorem free_add_monoid.to_list_map {α : Type u_1} {β : Type u_2} (f : α β) (xs : free_add_monoid α) :
theorem free_monoid.to_list_map {α : Type u_1} {β : Type u_2} (f : α β) (xs : free_monoid α) :
theorem free_add_monoid.of_list_map {α : Type u_1} {β : Type u_2} (f : α β) (xs : list α) :
theorem free_monoid.of_list_map {α : Type u_1} {β : Type u_2} (f : α β) (xs : list α) :
theorem free_monoid.lift_of_comp_eq_map {α : Type u_1} {β : Type u_2} (f : α β) :
free_monoid.lift (λ (x : α), free_monoid.of (f x)) =
theorem free_add_monoid.lift_of_comp_eq_map {α : Type u_1} {β : Type u_2} (f : α β) :
theorem free_add_monoid.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β γ) (f : α β) :
theorem free_monoid.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β γ) (f : α β) :
@[simp]
theorem free_add_monoid.map_id {α : Type u_1} :
@[simp]
theorem free_monoid.map_id {α : Type u_1} :