# Free monoid over a given alphabet #

## Main definitions #

• FreeMonoid α: free monoid over alphabet α; defined as a synonym for List α with multiplication given by (++).
• FreeMonoid.of: embedding α → FreeMonoid α sending each element x to [x];
• FreeMonoid.lift: natural equivalence between α → M and FreeMonoid α →* M
• FreeMonoid.map: embedding of α → β into FreeMonoid α →* FreeMonoid β given by List.map.
def FreeAddMonoid (α : Type u_6) :
Type u_6

Free nonabelian additive monoid over a given alphabet

Equations
Instances For
def FreeMonoid (α : Type u_6) :
Type u_6

Free monoid over a given alphabet.

Equations
Instances For
def FreeAddMonoid.toList {α : Type u_1} :

The identity equivalence between FreeAddMonoid α and List α.

Equations
Instances For
def FreeMonoid.toList {α : Type u_1} :
List α

The identity equivalence between FreeMonoid α and List α.

Equations
• FreeMonoid.toList =
Instances For
def FreeAddMonoid.ofList {α : Type u_1} :

The identity equivalence between List α and FreeAddMonoid α.

Equations
Instances For
def FreeMonoid.ofList {α : Type u_1} :
List α

The identity equivalence between List α and FreeMonoid α.

Equations
Instances For
@[simp]
theorem FreeAddMonoid.toList_symm {α : Type u_1} :
@[simp]
theorem FreeMonoid.toList_symm {α : Type u_1} :
FreeMonoid.toList.symm = FreeMonoid.ofList
@[simp]
theorem FreeAddMonoid.ofList_symm {α : Type u_1} :
@[simp]
theorem FreeMonoid.ofList_symm {α : Type u_1} :
FreeMonoid.ofList.symm = FreeMonoid.toList
@[simp]
theorem FreeAddMonoid.toList_ofList {α : Type u_1} (l : List α) :
@[simp]
theorem FreeMonoid.toList_ofList {α : Type u_1} (l : List α) :
FreeMonoid.toList (FreeMonoid.ofList l) = l
@[simp]
theorem FreeAddMonoid.ofList_toList {α : Type u_1} (xs : ) :
@[simp]
theorem FreeMonoid.ofList_toList {α : Type u_1} (xs : ) :
FreeMonoid.ofList (FreeMonoid.toList xs) = xs
@[simp]
theorem FreeAddMonoid.toList_comp_ofList {α : Type u_1} :
@[simp]
theorem FreeMonoid.toList_comp_ofList {α : Type u_1} :
FreeMonoid.toList FreeMonoid.ofList = id
@[simp]
theorem FreeAddMonoid.ofList_comp_toList {α : Type u_1} :
@[simp]
theorem FreeMonoid.ofList_comp_toList {α : Type u_1} :
FreeMonoid.ofList FreeMonoid.toList = id
Equations
∀ (n : ) (x : ), nsmulRec (n + 1) x = nsmulRec (n + 1) x
∀ (x : ), nsmulRec 0 x = nsmulRec 0 x
instance FreeMonoid.instCancelMonoid {α : Type u_1} :
Equations
• FreeMonoid.instCancelMonoid =
instance FreeAddMonoid.instInhabited {α : Type u_1} :
Equations
• FreeAddMonoid.instInhabited = { default := 0 }
instance FreeMonoid.instInhabited {α : Type u_1} :
Equations
• FreeMonoid.instInhabited = { default := 1 }
@[simp]
theorem FreeAddMonoid.toList_zero {α : Type u_1} :
@[simp]
theorem FreeMonoid.toList_one {α : Type u_1} :
FreeMonoid.toList 1 = []
@[simp]
theorem FreeAddMonoid.ofList_nil {α : Type u_1} :
@[simp]
theorem FreeMonoid.ofList_nil {α : Type u_1} :
FreeMonoid.ofList [] = 1
@[simp]
theorem FreeAddMonoid.toList_add {α : Type u_1} (xs : ) (ys : ) :
@[simp]
theorem FreeMonoid.toList_mul {α : Type u_1} (xs : ) (ys : ) :
FreeMonoid.toList (xs * ys) = FreeMonoid.toList xs ++ FreeMonoid.toList ys
@[simp]
theorem FreeAddMonoid.ofList_append {α : Type u_1} (xs : List α) (ys : List α) :
@[simp]
theorem FreeMonoid.ofList_append {α : Type u_1} (xs : List α) (ys : List α) :
FreeMonoid.ofList (xs ++ ys) = FreeMonoid.ofList xs * FreeMonoid.ofList ys
@[simp]
theorem FreeAddMonoid.toList_sum {α : Type u_1} (xs : ) :
@[simp]
theorem FreeMonoid.toList_prod {α : Type u_1} (xs : List ()) :
FreeMonoid.toList xs.prod = (List.map (FreeMonoid.toList) xs).join
@[simp]
theorem FreeAddMonoid.ofList_join {α : Type u_1} (xs : List (List α)) :
@[simp]
theorem FreeMonoid.ofList_join {α : Type u_1} (xs : List (List α)) :
FreeMonoid.ofList xs.join = (List.map (FreeMonoid.ofList) xs).prod
def FreeAddMonoid.of {α : Type u_1} (x : α) :

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

Equations
Instances For
def FreeMonoid.of {α : Type u_1} (x : α) :

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

Equations
• = FreeMonoid.ofList [x]
Instances For
@[simp]
theorem FreeAddMonoid.toList_of {α : Type u_1} (x : α) :
@[simp]
theorem FreeMonoid.toList_of {α : Type u_1} (x : α) :
FreeMonoid.toList () = [x]
theorem FreeAddMonoid.ofList_singleton {α : Type u_1} (x : α) :
theorem FreeMonoid.ofList_singleton {α : Type u_1} (x : α) :
FreeMonoid.ofList [x] =
@[simp]
theorem FreeAddMonoid.ofList_cons {α : Type u_1} (x : α) (xs : List α) :
@[simp]
theorem FreeMonoid.ofList_cons {α : Type u_1} (x : α) (xs : List α) :
FreeMonoid.ofList (x :: xs) = * FreeMonoid.ofList xs
theorem FreeAddMonoid.toList_of_add {α : Type u_1} (x : α) (xs : ) :
theorem FreeMonoid.toList_of_mul {α : Type u_1} (x : α) (xs : ) :
FreeMonoid.toList ( * xs) = x :: FreeMonoid.toList xs
theorem FreeAddMonoid.of_injective {α : Type u_1} :
theorem FreeMonoid.of_injective {α : Type u_1} :
Function.Injective FreeMonoid.of
def FreeAddMonoid.recOn {α : Type u_1} {C : Sort u_6} (xs : ) (h0 : C 0) (ih : (x : α) → (xs : ) → C xsC ()) :
C xs

Recursor for FreeAddMonoid using 0 and FreeAddMonoid.of x + xsinstead of[]andx :: xs.

Equations
Instances For
def FreeMonoid.recOn {α : Type u_1} {C : Sort u_6} (xs : ) (h0 : C 1) (ih : (x : α) → (xs : ) → C xsC ( * xs)) :
C xs

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

Equations
Instances For
@[simp]
theorem FreeAddMonoid.recOn_zero {α : Type u_1} {C : Sort u_6} (h0 : C 0) (ih : (x : α) → (xs : ) → C xsC ()) :
@[simp]
theorem FreeMonoid.recOn_one {α : Type u_1} {C : Sort u_6} (h0 : C 1) (ih : (x : α) → (xs : ) → C xsC ( * xs)) :
FreeMonoid.recOn 1 h0 ih = h0
@[simp]
theorem FreeAddMonoid.recOn_of_add {α : Type u_1} {C : Sort u_6} (x : α) (xs : ) (h0 : C 0) (ih : (x : α) → (xs : ) → C xsC ()) :
().recOn h0 ih = ih x xs (xs.recOn h0 ih)
@[simp]
theorem FreeMonoid.recOn_of_mul {α : Type u_1} {C : Sort u_6} (x : α) (xs : ) (h0 : C 1) (ih : (x : α) → (xs : ) → C xsC ( * xs)) :
( * xs).recOn h0 ih = ih x xs (xs.recOn h0 ih)
def FreeAddMonoid.casesOn {α : Type u_1} {C : Sort u_6} (xs : ) (h0 : C 0) (ih : (x : α) → (xs : ) → C ()) :
C xs

A version of List.casesOn for FreeAddMonoid using 0 and FreeAddMonoid.of x + xs instead of [] and x :: xs.

Equations
Instances For
def FreeMonoid.casesOn {α : Type u_1} {C : Sort u_6} (xs : ) (h0 : C 1) (ih : (x : α) → (xs : ) → C ( * xs)) :
C xs

A version of List.cases_on for FreeMonoid using 1 and FreeMonoid.of x * xs instead of [] and x :: xs.

Equations
Instances For
@[simp]
theorem FreeAddMonoid.casesOn_zero {α : Type u_1} {C : Sort u_6} (h0 : C 0) (ih : (x : α) → (xs : ) → C ()) :
= h0
@[simp]
theorem FreeMonoid.casesOn_one {α : Type u_1} {C : Sort u_6} (h0 : C 1) (ih : (x : α) → (xs : ) → C ( * xs)) :
@[simp]
theorem FreeAddMonoid.casesOn_of_add {α : Type u_1} {C : Sort u_6} (x : α) (xs : ) (h0 : C 0) (ih : (x : α) → (xs : ) → C ()) :
().casesOn h0 ih = ih x xs
@[simp]
theorem FreeMonoid.casesOn_of_mul {α : Type u_1} {C : Sort u_6} (x : α) (xs : ) (h0 : C 1) (ih : (x : α) → (xs : ) → C ( * xs)) :
( * xs).casesOn h0 ih = ih x xs
theorem FreeAddMonoid.hom_eq {α : Type u_1} {M : Type u_4} [] ⦃f : ⦃g : (h : ∀ (x : α), f () = g ()) :
f = g
theorem FreeMonoid.hom_eq {α : Type u_1} {M : Type u_4} [] ⦃f : →* M ⦃g : →* M (h : ∀ (x : α), f () = g ()) :
f = g
def FreeAddMonoid.sumAux {M : Type u_6} [] :
List MM

A variant of List.sum that has [x].sum = x true definitionally. The purpose is to make FreeAddMonoid.lift_eval_of true by rfl.

Equations
Instances For
abbrev FreeAddMonoid.sumAux.match_1 {M : Type u_1} (motive : List MSort u_2) :
(x : List M) → (Unitmotive [])((x : M) → (xs : List M) → motive (x :: xs))motive x
Equations
Instances For
def FreeMonoid.prodAux {M : Type u_6} [] :
List MM

A variant of List.prod that has [x].prod = x true definitionally. The purpose is to make FreeMonoid.lift_eval_of true by rfl.

Equations
• = match x with | [] => 1 | x :: xs => List.foldl (fun (x x_1 : M) => x * x_1) x xs
Instances For
abbrev FreeAddMonoid.sumAux_eq.match_1 {M : Type u_1} (motive : List MProp) :
∀ (x : List M), (Unitmotive [])(∀ (head : M) (xs : List M), motive (head :: xs))motive x
Equations
• =
Instances For
theorem FreeAddMonoid.sumAux_eq {M : Type u_4} [] (l : List M) :
= l.sum
theorem FreeMonoid.prodAux_eq {M : Type u_4} [] (l : List M) :
= l.prod
def FreeAddMonoid.lift {α : Type u_1} {M : Type u_4} [] :
(αM) ()

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem FreeAddMonoid.lift.proof_1 {α : Type u_2} {M : Type u_1} [] (f : αM) :
(fun (l : ) => FreeAddMonoid.sumAux (List.map f (FreeAddMonoid.toList l))) 0 = (fun (l : ) => FreeAddMonoid.sumAux (List.map f (FreeAddMonoid.toList l))) 0
theorem FreeAddMonoid.lift.proof_2 {α : Type u_1} {M : Type u_2} [] (f : αM) :
theorem FreeAddMonoid.lift.proof_4 {α : Type u_1} {M : Type u_2} [] (f : ) :
(fun (f : αM) => { toFun := fun (l : ) => FreeAddMonoid.sumAux (List.map f (FreeAddMonoid.toList l)), map_zero' := , map_add' := }) ((fun (f : ) (x : α) => f ()) f) = f
theorem FreeAddMonoid.lift.proof_3 {α : Type u_1} {M : Type u_2} [] (f : αM) :
(fun (f : ) (x : α) => f ()) ((fun (f : αM) => { toFun := fun (l : ) => FreeAddMonoid.sumAux (List.map f (FreeAddMonoid.toList l)), map_zero' := , map_add' := }) f) = (fun (f : ) (x : α) => f ()) ((fun (f : αM) => { toFun := fun (l : ) => FreeAddMonoid.sumAux (List.map f (FreeAddMonoid.toList l)), map_zero' := , map_add' := }) f)
def FreeMonoid.lift {α : Type u_1} {M : Type u_4} [] :
(αM) ( →* M)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem FreeAddMonoid.lift_ofList {α : Type u_1} {M : Type u_4} [] (f : αM) (l : List α) :
@[simp]
theorem FreeMonoid.lift_ofList {α : Type u_1} {M : Type u_4} [] (f : αM) (l : List α) :
(FreeMonoid.lift f) (FreeMonoid.ofList l) = (List.map f l).prod
@[simp]
theorem FreeAddMonoid.lift_symm_apply {α : Type u_1} {M : Type u_4} [] (f : ) :
@[simp]
theorem FreeMonoid.lift_symm_apply {α : Type u_1} {M : Type u_4} [] (f : →* M) :
FreeMonoid.lift.symm f = f FreeMonoid.of
theorem FreeAddMonoid.lift_apply {α : Type u_1} {M : Type u_4} [] (f : αM) (l : ) :
theorem FreeMonoid.lift_apply {α : Type u_1} {M : Type u_4} [] (f : αM) (l : ) :
(FreeMonoid.lift f) l = (List.map f (FreeMonoid.toList l)).prod
theorem FreeAddMonoid.lift_comp_of {α : Type u_1} {M : Type u_4} [] (f : αM) :
theorem FreeMonoid.lift_comp_of {α : Type u_1} {M : Type u_4} [] (f : αM) :
(FreeMonoid.lift f) FreeMonoid.of = f
@[simp]
theorem FreeAddMonoid.lift_eval_of {α : Type u_1} {M : Type u_4} [] (f : αM) (x : α) :
(FreeAddMonoid.lift f) () = f x
@[simp]
theorem FreeMonoid.lift_eval_of {α : Type u_1} {M : Type u_4} [] (f : αM) (x : α) :
(FreeMonoid.lift f) () = f x
@[simp]
theorem FreeAddMonoid.lift_restrict {α : Type u_1} {M : Type u_4} [] (f : ) :
@[simp]
theorem FreeMonoid.lift_restrict {α : Type u_1} {M : Type u_4} [] (f : →* M) :
FreeMonoid.lift (f FreeMonoid.of) = f
theorem FreeAddMonoid.comp_lift {α : Type u_1} {M : Type u_4} [] {N : Type u_5} [] (g : M →+ N) (f : αM) :
theorem FreeMonoid.comp_lift {α : Type u_1} {M : Type u_4} [] {N : Type u_5} [] (g : M →* N) (f : αM) :
g.comp (FreeMonoid.lift f) = FreeMonoid.lift (g f)
theorem FreeAddMonoid.hom_map_lift {α : Type u_1} {M : Type u_4} [] {N : Type u_5} [] (g : M →+ N) (f : αM) (x : ) :
theorem FreeMonoid.hom_map_lift {α : Type u_1} {M : Type u_4} [] {N : Type u_5} [] (g : M →* N) (f : αM) (x : ) :
g ((FreeMonoid.lift f) x) = (FreeMonoid.lift (g f)) x
theorem FreeAddMonoid.mkAddAction.proof_2 {α : Type u_1} {β : Type u_2} (f : αββ) :
∀ (x x_1 : ) (x_2 : β), List.foldr f x_2 (FreeAddMonoid.toList x ++ FreeAddMonoid.toList x_1) = List.foldr f (List.foldr f x_2 (FreeAddMonoid.toList x_1)) (FreeAddMonoid.toList x)
theorem FreeAddMonoid.mkAddAction.proof_1 {α : Type u_2} {β : Type u_1} (f : αββ) :
∀ (x : β), 0 +ᵥ x = 0 +ᵥ x
def FreeAddMonoid.mkAddAction {α : Type u_1} {β : Type u_2} (f : αββ) :

Define an additive action of FreeAddMonoid α on β.

Equations
Instances For
def FreeMonoid.mkMulAction {α : Type u_1} {β : Type u_2} (f : αββ) :
MulAction () β

Define a multiplicative action of FreeMonoid α on β.

Equations
Instances For
theorem FreeAddMonoid.vadd_def {α : Type u_1} {β : Type u_2} (f : αββ) (l : ) (b : β) :
l +ᵥ b = List.foldr f b (FreeAddMonoid.toList l)
theorem FreeMonoid.smul_def {α : Type u_1} {β : Type u_2} (f : αββ) (l : ) (b : β) :
l b = List.foldr f b (FreeMonoid.toList l)
theorem FreeAddMonoid.ofList_vadd {α : Type u_1} {β : Type u_2} (f : αββ) (l : List α) (b : β) :
FreeAddMonoid.ofList l +ᵥ b = List.foldr f b l
theorem FreeMonoid.ofList_smul {α : Type u_1} {β : Type u_2} (f : αββ) (l : List α) (b : β) :
FreeMonoid.ofList l b = List.foldr f b l
@[simp]
theorem FreeAddMonoid.of_vadd {α : Type u_1} {β : Type u_2} (f : αββ) (x : α) (y : β) :
= f x y
@[simp]
theorem FreeMonoid.of_smul {α : Type u_1} {β : Type u_2} (f : αββ) (x : α) (y : β) :
= f x y
theorem FreeAddMonoid.map.proof_1 {α : Type u_2} {β : Type u_1} (f : αβ) :
(fun (l : ) => FreeAddMonoid.ofList (List.map f (FreeAddMonoid.toList l))) 0 = (fun (l : ) => FreeAddMonoid.ofList (List.map f (FreeAddMonoid.toList l))) 0
theorem FreeAddMonoid.map.proof_2 {α : Type u_1} {β : Type u_2} (f : αβ) :
def FreeAddMonoid.map {α : Type u_1} {β : Type u_2} (f : αβ) :

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

Equations
• = { toFun := fun (l : ) => FreeAddMonoid.ofList (List.map f (FreeAddMonoid.toList l)), map_zero' := , map_add' := }
Instances For
def FreeMonoid.map {α : Type u_1} {β : Type u_2} (f : αβ) :

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

Equations
• = { toFun := fun (l : ) => FreeMonoid.ofList (List.map f (FreeMonoid.toList l)), map_one' := , map_mul' := }
Instances For
@[simp]
theorem FreeAddMonoid.map_of {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) :
@[simp]
theorem FreeMonoid.map_of {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) :
() () = FreeMonoid.of (f x)
theorem FreeAddMonoid.toList_map {α : Type u_1} {β : Type u_2} (f : αβ) (xs : ) :
theorem FreeMonoid.toList_map {α : Type u_1} {β : Type u_2} (f : αβ) (xs : ) :
FreeMonoid.toList (() xs) = List.map f (FreeMonoid.toList xs)
theorem FreeAddMonoid.ofList_map {α : Type u_1} {β : Type u_2} (f : αβ) (xs : List α) :
theorem FreeMonoid.ofList_map {α : Type u_1} {β : Type u_2} (f : αβ) (xs : List α) :
FreeMonoid.ofList (List.map f xs) = () (FreeMonoid.ofList xs)
theorem FreeAddMonoid.lift_of_comp_eq_map {α : Type u_1} {β : Type u_2} (f : αβ) :
theorem FreeMonoid.lift_of_comp_eq_map {α : Type u_1} {β : Type u_2} (f : αβ) :
(FreeMonoid.lift fun (x : α) => FreeMonoid.of (f x)) =
theorem FreeAddMonoid.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : βγ) (f : αβ) :
theorem FreeMonoid.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : βγ) (f : αβ) :
FreeMonoid.map (g f) = ().comp ()
@[simp]
theorem FreeAddMonoid.map_id {α : Type u_1} :
@[simp]
theorem FreeMonoid.map_id {α : Type u_1} :
The only invertible element of the free monoid is 1; this instance enables units_eq_one`.