mathlib documentation

algebra.free_monoid

Free monoid over a given alphabet #

Main definitions #

source
def free_add_monoid (α : Type u_1) :
Type u_1

Free nonabelian additive monoid over a given alphabet

Equations
source
def free_monoid (α : Type u_1) :
Type u_1

Free monoid over a given alphabet.

Equations
source
@[protected, instance]
def free_add_monoid.add_monoid {α : Type u_1} :
add_monoid (free_add_monoid α)
Equations
source
@[protected, instance]
def free_monoid.monoid {α : Type u_1} :
monoid (free_monoid α)
Equations
source
@[protected, instance]
def free_add_monoid.inhabited {α : Type u_1} :
inhabited (free_add_monoid α)
Equations
source
@[protected, instance]
def free_monoid.inhabited {α : Type u_1} :
inhabited (free_monoid α)
Equations
source
theorem free_monoid.one_def {α : Type u_1} :
1 = list.nil
source
theorem free_add_monoid.zero_def {α : Type u_1} :
0 = list.nil
source
theorem free_add_monoid.add_def {α : Type u_1} (xs ys : list α) :
xs + ys = xs ++ ys
source
theorem free_monoid.mul_def {α : Type u_1} (xs ys : list α) :
xs * ys = xs ++ ys
source
def free_monoid.of {α : Type u_1} (x : α) :
free_monoid α

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

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

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

Equations
source
theorem free_monoid.of_def {α : Type u_1} (x : α) :
free_monoid.of x = [x]
source
theorem free_add_monoid.of_def {α : Type u_1} (x : α) :
free_add_monoid.of x = [x]
source
theorem free_add_monoid.of_injective {α : Type u_1} :
function.injective free_add_monoid.of
source
theorem free_monoid.of_injective {α : Type u_1} :
function.injective free_monoid.of
source
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.

Equations
  • xs.rec_on h0 ih = list.rec_on xs h0 ih
source
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.

Equations
  • xs.rec_on h0 ih = list.rec_on xs h0 ih
source
@[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
source
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
source
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
source
def free_monoid.lift {α : Type u_1} {M : Type u_4} [monoid M] :
(α → M) ≃ (free_monoid α →* M)

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

Equations
source
@[simp]
theorem free_add_monoid.lift_symm_apply {α : Type u_1} {M : Type u_4} [add_monoid M] (f : free_add_monoid α →+ M) :
⇑(free_add_monoid.lift.symm) f = ⇑f ∘ free_add_monoid.of
source
@[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
source
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 l).prod
source
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 l).sum
source
theorem free_add_monoid.lift_comp_of {α : Type u_1} {M : Type u_4} [add_monoid M] (f : α → M) :
⇑(⇑free_add_monoid.lift f) ∘ free_add_monoid.of = f
source
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
source
@[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
source
@[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
source
@[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
source
@[simp]
theorem free_add_monoid.lift_restrict {α : Type u_1} {M : Type u_4} [add_monoid M] (f : free_add_monoid α →+ M) :
⇑free_add_monoid.lift (⇑f ∘ free_add_monoid.of) = f
source
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)
source
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)
source
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
source
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
source
def free_add_monoid.map {α : Type u_1} {β : Type u_2} (f : α → β) :
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).

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

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

Equations
source
@[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)
source
@[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)
source
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
source
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
source
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)
source
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)
source
@[protected, instance]
def free_monoid.star_monoid {α : Type u_1} :
star_monoid (free_monoid α)
Equations
source
@[simp]
theorem free_monoid.star_of {α : Type u_1} (x : α) :
star (free_monoid.of x) = free_monoid.of x
source
@[simp]
theorem free_monoid.star_one {α : Type u_1} :
star 1 = 1

Note that star_one is already a global simp lemma, but this one works with dsimp too