Free monoid over a given alphabet
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 monoid over a given alphabet.
Equations
- free_monoid α = list α
Free nonabelian additive monoid over a given alphabet
@[instance]
@[instance]
Equations
- free_monoid.inhabited = {default := 1}
Embeds an element of α into free_add_monoid α as a singleton list.
Embeds an element of α into free_monoid α as a singleton list.
Equations
- free_monoid.of x = [x]
def
free_add_monoid.rec_on
{α : Type u_1}
{C : free_add_monoid α → Sort u_2}
(xs : free_add_monoid α) :
C 0 → (Π (x : α) (xs : free_add_monoid α), C xs → C (free_add_monoid.of x + xs)) → C xs
Recursor for free_add_monoid using 0 and of x + xs instead of [] and x :: xs.
def
free_monoid.rec_on
{α : Type u_1}
{C : free_monoid α → Sort u_2}
(xs : free_monoid α) :
C 1 → (Π (x : α) (xs : free_monoid α), C xs → C (free_monoid.of x * xs)) → C xs
Recursor for free_monoid using 1 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 : free_monoid α →* M⦄ :
(∀ (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⦄ :
(∀ (x : α), ⇑f (free_add_monoid.of x) = ⇑g (free_add_monoid.of x)) → f = g
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.
Equivalence between maps α → M and monoid homomorphisms free_monoid α →* M.
Equations
- free_monoid.lift = {to_fun := λ (f : α → M), {to_fun := λ (l : free_monoid α), (list.map f l).prod, 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_add_monoid.lift_apply
{α : Type u_1}
{M : Type u_4}
[add_monoid M]
(f : α → M)
(l : free_add_monoid α) :
theorem
free_monoid.lift_apply
{α : Type u_1}
{M : Type u_4}
[monoid M]
(f : α → M)
(l : free_monoid α) :
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_add_monoid.lift_restrict
{α : Type u_1}
{M : Type u_4}
[add_monoid M]
(f : free_add_monoid α →+ M) :
@[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
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) :
g.comp (⇑free_monoid.lift f) = ⇑free_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
The unique monoid homomorphism free_monoid α →* free_monoid β that sends
each of x to of (f x).
def
free_add_monoid.map
{α : Type u_1}
{β : Type u_2} :
(α → β) → free_add_monoid α →+ free_add_monoid β
The unique additive monoid homomorphism free_add_monoid α →+ free_add_monoid β
that sends each of x to 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)
@[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)
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_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)
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)