# mathlibdocumentation

algebra.free_monoid

# Free monoid over a given alphabet

## 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.
Type u_1Type u_1

Free nonabelian additive monoid over a given alphabet

def free_monoid  :
Type u_1Type u_1

Free monoid over a given alphabet.

Equations
@[instance]

@[instance]
def free_monoid.monoid {α : Type u_1} :

Equations
@[instance]
def free_add_monoid.inhabited {α : Type u_1} :

@[instance]
def free_monoid.inhabited {α : Type u_1} :

Equations
theorem free_monoid.one_def {α : Type u_1} :

theorem free_add_monoid.zero_def {α : Type u_1} :

theorem free_add_monoid.add_def {α : Type u_1} (xs ys : list α) :
xs + ys = xs ++ ys

theorem free_monoid.mul_def {α : Type u_1} (xs ys : list α) :
xs * ys = xs ++ ys

def free_monoid.of {α : Type u_1} :
α →

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

Equations
• = [x]
def free_add_monoid.of {α : Type u_1} :
α →

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

theorem free_monoid.of_def {α : Type u_1} (x : α) :
= [x]

theorem free_add_monoid.of_def {α : Type u_1} (x : α) :
= [x]

def free_monoid.rec_on {α : Type u_1} {C : Sort u_2} (xs : free_monoid α) :
C 1(Π (x : α) (xs : , C xsC ((free_monoid.of x) * xs))C xs

Recursor for free_monoid using 1 and 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 α) :
C 0(Π (x : α) (xs : , C xsC + xs))C xs

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

@[ext]
theorem free_monoid.hom_eq {α : Type u_1} {M : Type u_4} [monoid M] ⦃f g : →* M⦄ :
(∀ (x : α), f = 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 : →+ M⦄ :
(∀ (x : α), f = g f = g

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.

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 l).prod

theorem free_add_monoid.lift_apply {α : Type u_1} {M : Type u_4} [add_monoid M] (f : α → M) (l : free_add_monoid α) :
= (list.map f l).sum

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_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 α) :

def free_add_monoid.map {α : Type u_1} {β : Type u_2} :
(α → β)

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

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

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