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 nonabelian additive monoid over a given alphabet
Equations
- free_add_monoid α = list α
Free monoid over a given alphabet.
Equations
- free_monoid α = list α
@[protected, instance]
Equations
- free_add_monoid.add_monoid = {add := λ (x y : free_add_monoid α), x ++ y, add_assoc := _, zero := list.nil α, zero_add := _, add_zero := _, nsmul := nsmul_rec (add_zero_class.to_has_add (free_add_monoid α)), nsmul_zero' := _, nsmul_succ' := _}
@[protected, instance]
Equations
- free_monoid.monoid = {mul := λ (x y : free_monoid α), x ++ y, mul_assoc := _, one := list.nil α, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (free_monoid α)), npow_zero' := _, npow_succ' := _}
@[protected, instance]
Equations
@[protected, instance]
Equations
- free_monoid.inhabited = {default := 1}
Embeds an element of α into free_monoid α as a singleton list.
Equations
- free_monoid.of x = [x]
Embeds an element of α into free_add_monoid α as a singleton list.
Equations
- free_add_monoid.of x = [x]
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 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 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⦄
(h : ∀ (x : α), ⇑f (free_monoid.of x) = ⇑g (free_monoid.of x)) :
f = g
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
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 α), (list.map f l).sum, 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 α), (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_monoid.lift_apply
{α : Type u_1}
{M : Type u_4}
[monoid M]
(f : α → M)
(l : free_monoid α) :
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_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_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_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
The unique additive monoid homomorphism free_add_monoid α →+ free_add_monoid β
that sends each of x to of (f x).
The unique monoid homomorphism free_monoid α →* free_monoid β that sends
each of x to 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)
@[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_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)