# Free constructions #

## Main definitions #

• FreeMagma α: free magma (structure with binary operation without any axioms) over alphabet α, defined inductively, with traversable instance and decidable equality.
• MagmaAssocQuotient α: quotient of a magma α by the associativity equivalence relation.
• FreeSemigroup α: free semigroup over alphabet α, defined as a structure with two fields head : α and tail : List α (i.e. nonempty lists), with traversable instance and decidable equality.
• FreeMagmaAssocQuotientEquiv α: isomorphism between MagmaAssocQuotient (FreeMagma α) and FreeSemigroup α.
• FreeMagma.lift: the universal property of the free magma, expressing its adjointness.
inductive FreeAddMagma (α : Type u) :

Free nonabelian additive magma over a given alphabet.

• of: {α : Type u} → α
• add: {α : Type u} →
Instances For
{α : Type u_1} → [inst : ] →
Equations
inductive FreeMagma (α : Type u) :

Free magma over a given alphabet.

• of: {α : Type u} → α
• mul: {α : Type u} → → →
Instances For
instance instDecidableEqFreeMagma :
{α : Type u_1} → [inst : ] →
Equations
• instDecidableEqFreeMagma = decEqFreeMagma✝
instance FreeAddMagma.instInhabited {α : Type u} [] :
Equations
instance FreeMagma.instInhabited {α : Type u} [] :
Equations
Equations
instance FreeMagma.instMul {α : Type u} :
Equations
• FreeMagma.instMul = { mul := FreeMagma.mul }
@[simp]
theorem FreeAddMagma.add_eq {α : Type u} (x : ) (y : ) :
x.add y = x + y
@[simp]
theorem FreeMagma.mul_eq {α : Type u} (x : ) (y : ) :
x.mul y = x * y
def FreeAddMagma.recOnAdd {α : Type u} {C : Sort l} (x : ) (ih1 : (x : α) → C ) (ih2 : (x y : ) → C xC yC (x + y)) :
C x

Recursor for FreeAddMagma using x + y instead of FreeAddMagma.add x y.

Equations
Instances For
def FreeMagma.recOnMul {α : Type u} {C : Sort l} (x : ) (ih1 : (x : α) → C (FreeMagma.of x)) (ih2 : (x y : ) → C xC yC (x * y)) :
C x

Recursor for FreeMagma using x * y instead of FreeMagma.mul x y.

Equations
Instances For
f = g
theorem FreeMagma.hom_ext_iff {α : Type u} {β : Type v} [Mul β] {f : →ₙ* β} {g : →ₙ* β} :
f = g f FreeMagma.of = g FreeMagma.of
theorem FreeMagma.hom_ext {α : Type u} {β : Type v} [Mul β] {f : →ₙ* β} {g : →ₙ* β} (h : f FreeMagma.of = g FreeMagma.of) :
f = g
def FreeMagma.liftAux {α : Type u} {β : Type v} [Mul β] (f : αβ) :
β

Lifts a function α → β to a magma homomorphism FreeMagma α → β given a magma β.

Equations
Instances For
def FreeAddMagma.liftAux {α : Type u} {β : Type v} [Add β] (f : αβ) :
β

Lifts a function α → β to an additive magma homomorphism FreeAddMagma α → β given an additive magma β.

Equations
Instances For
theorem FreeAddMagma.lift.proof_2 {α : Type u_1} {β : Type u_2} [Add β] (f : αβ) :
(fun (F : AddHom (FreeAddMagma α) β) => F FreeAddMagma.of) ((fun (f : αβ) => { toFun := , map_add' := }) f) = (fun (F : AddHom (FreeAddMagma α) β) => F FreeAddMagma.of) ((fun (f : αβ) => { toFun := , map_add' := }) f)
theorem FreeAddMagma.lift.proof_1 {α : Type u_1} {β : Type u_2} [Add β] (f : αβ) (x : ) (y : ) :
(fun (f : αβ) => { toFun := , map_add' := }) ((fun (F : AddHom (FreeAddMagma α) β) => F FreeAddMagma.of) F) = F
def FreeAddMagma.lift {α : Type u} {β : Type v} [Add β] :

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem FreeMagma.lift_symm_apply {α : Type u} {β : Type v} [Mul β] (F : →ₙ* β) :
∀ (a : α), FreeMagma.lift.symm F a = (F FreeMagma.of) a
@[simp]
def FreeMagma.lift {α : Type u} {β : Type v} [Mul β] :
(αβ) ( →ₙ* β)

The universal property of the free magma expressing its adjointness.

Equations
• FreeMagma.lift = { toFun := fun (f : αβ) => { toFun := , map_mul' := }, invFun := fun (F : →ₙ* β) => F FreeMagma.of, left_inv := , right_inv := }
Instances For
@[simp]
theorem FreeAddMagma.lift_of {α : Type u} {β : Type v} [Add β] (f : αβ) (x : α) :
@[simp]
theorem FreeMagma.lift_of {α : Type u} {β : Type v} [Mul β] (f : αβ) (x : α) :
(FreeMagma.lift f) (FreeMagma.of x) = f x
@[simp]
theorem FreeAddMagma.lift_comp_of {α : Type u} {β : Type v} [Add β] (f : αβ) :
@[simp]
theorem FreeMagma.lift_comp_of {α : Type u} {β : Type v} [Mul β] (f : αβ) :
(FreeMagma.lift f) FreeMagma.of = f
@[simp]
@[simp]
theorem FreeMagma.lift_comp_of' {α : Type u} {β : Type v} [Mul β] (f : →ₙ* β) :
FreeMagma.lift (f FreeMagma.of) = f
def FreeAddMagma.map {α : Type u} {β : Type v} (f : αβ) :

The unique additive magma homomorphism FreeAddMagma α → FreeAddMagma β that sends each of x to of (f x).

Equations
Instances For
def FreeMagma.map {α : Type u} {β : Type v} (f : αβ) :

The unique magma homomorphism FreeMagma α →ₙ* FreeMagma β that sends each of x to of (f x).

Equations
• = FreeMagma.lift (FreeMagma.of f)
Instances For
@[simp]
theorem FreeAddMagma.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
@[simp]
theorem FreeMagma.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
Equations
def FreeAddMagma.recOnPure {α : Type u} {C : Sort l} (x : ) (ih1 : (x : α) → C (pure x)) (ih2 : (x y : ) → C xC yC (x + y)) :
C x

Recursor on FreeAddMagma using pure instead of of.

Equations
• x.recOnPure ih1 ih2 = x.recOnAdd ih1 ih2
Instances For
def FreeMagma.recOnPure {α : Type u} {C : Sort l} (x : ) (ih1 : (x : α) → C (pure x)) (ih2 : (x y : ) → C xC yC (x * y)) :
C x

Recursor on FreeMagma using pure instead of of.

Equations
• x.recOnPure ih1 ih2 = x.recOnMul ih1 ih2
Instances For
@[simp]
theorem FreeAddMagma.map_pure {α : Type u} {β : Type u} (f : αβ) (x : α) :
f <$> pure x = pure (f x) @[simp] theorem FreeMagma.map_pure {α : Type u} {β : Type u} (f : αβ) (x : α) : f <$> pure x = pure (f x)
@[simp]
theorem FreeAddMagma.map_add' {α : Type u} {β : Type u} (f : αβ) (x : ) (y : ) :
f <$> (x + y) = f <$> x + f <$> y @[simp] theorem FreeMagma.map_mul' {α : Type u} {β : Type u} (f : αβ) (x : ) (y : ) : f <$> (x * y) = f <$> x * f <$> y
@[simp]
theorem FreeAddMagma.pure_bind {α : Type u} {β : Type u} (f : α) (x : α) :
pure x >>= f = f x
@[simp]
theorem FreeMagma.pure_bind {α : Type u} {β : Type u} (f : α) (x : α) :
pure x >>= f = f x
@[simp]
theorem FreeAddMagma.add_bind {α : Type u} {β : Type u} (f : α) (x : ) (y : ) :
x + y >>= f = (x >>= f) + (y >>= f)
@[simp]
theorem FreeMagma.mul_bind {α : Type u} {β : Type u} (f : α) (x : ) (y : ) :
x * y >>= f = (x >>= f) * (y >>= f)
@[simp]
theorem FreeAddMagma.pure_seq {α : Type u} {β : Type u} {f : αβ} {x : } :
(Seq.seq (pure f) fun (x_1 : Unit) => x) = f <$> x @[simp] theorem FreeMagma.pure_seq {α : Type u} {β : Type u} {f : αβ} {x : } : (Seq.seq (pure f) fun (x_1 : Unit) => x) = f <$> x
@[simp]
(Seq.seq (f + g) fun (x_1 : Unit) => x) = (Seq.seq f fun (x_1 : Unit) => x) + Seq.seq g fun (x_1 : Unit) => x
@[simp]
theorem FreeMagma.mul_seq {α : Type u} {β : Type u} {f : FreeMagma (αβ)} {g : FreeMagma (αβ)} {x : } :
(Seq.seq (f * g) fun (x_1 : Unit) => x) = (Seq.seq f fun (x_1 : Unit) => x) * Seq.seq g fun (x_1 : Unit) => x
Equations
Equations
def FreeMagma.traverse {m : Type u → Type u} [] {α : Type u} {β : Type u} (F : αm β) :
m (FreeMagma β)

FreeMagma is traversable.

Equations
Instances For
def FreeAddMagma.traverse {m : Type u → Type u} [] {α : Type u} {β : Type u} (F : αm β) :

FreeAddMagma is traversable.

Equations
Instances For
@[simp]
theorem FreeAddMagma.traverse_pure {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) (x : α) :
traverse F (pure x) = pure <$> F x @[simp] theorem FreeMagma.traverse_pure {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) (x : α) : traverse F (pure x) = pure <$> F x
@[simp]
theorem FreeAddMagma.traverse_pure' {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) :
pure = fun (x : α) => pure <$> F x @[simp] theorem FreeMagma.traverse_pure' {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) : pure = fun (x : α) => pure <$> F x
@[simp]
theorem FreeAddMagma.traverse_add {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) (x : ) (y : ) :
traverse F (x + y) = Seq.seq ((fun (x1 x2 : ) => x1 + x2) <$> traverse F x) fun (x : Unit) => traverse F y @[simp] theorem FreeMagma.traverse_mul {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) (x : ) (y : ) : traverse F (x * y) = Seq.seq ((fun (x1 x2 : ) => x1 * x2) <$> traverse F x) fun (x : Unit) => traverse F y
@[simp]
theorem FreeAddMagma.traverse_add' {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) :
HAdd.hAdd = fun (x y : ) => Seq.seq ((fun (x1 x2 : ) => x1 + x2) <$> traverse F x) fun (x : Unit) => traverse F y @[simp] theorem FreeMagma.traverse_mul' {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) : HMul.hMul = fun (x y : ) => Seq.seq ((fun (x1 x2 : ) => x1 * x2) <$> traverse F x) fun (x : Unit) => traverse F y
@[simp]
theorem FreeAddMagma.traverse_eq {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) (x : ) :
= traverse F x
@[simp]
theorem FreeMagma.traverse_eq {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) (x : ) :
= traverse F x
@[simp]
theorem FreeAddMagma.add_map_seq {α : Type u} (x : ) (y : ) :
(Seq.seq ((fun (x1 x2 : ) => x1 + x2) <$> x) fun (x : Unit) => y) = x + y @[simp] theorem FreeMagma.mul_map_seq {α : Type u} (x : ) (y : ) : (Seq.seq ((fun (x1 x2 : ) => x1 * x2) <$> x) fun (x : Unit) => y) = x * y
Equations
def FreeMagma.repr {α : Type u} [Repr α] :

Representation of an element of a free magma.

Equations
Instances For
def FreeAddMagma.repr {α : Type u} [Repr α] :

Representation of an element of a free additive magma.

Equations
Instances For
instance instReprFreeAddMagma {α : Type u} [Repr α] :
Equations
• instReprFreeAddMagma = { reprPrec := fun (o : ) (x : ) => o.repr }
instance instReprFreeMagma {α : Type u} [Repr α] :
Equations
• instReprFreeMagma = { reprPrec := fun (o : ) (x : ) => o.repr }
def FreeMagma.length {α : Type u} :

Length of an element of a free magma.

Equations
Instances For
def FreeAddMagma.length {α : Type u} :

Length of an element of a free additive magma.

Equations
Instances For
theorem FreeAddMagma.length_pos {α : Type u} (x : ) :
0 < x.length

The length of an element of a free additive magma is positive.

theorem FreeMagma.length_pos {α : Type u} (x : ) :
0 < x.length

The length of an element of a free magma is positive.

ααProp

Associativity relations for an additive magma.

Instances For
inductive Magma.AssocRel (α : Type u) [Mul α] :
ααProp

Associativity relations for a magma.

Instances For

Equations
Instances For
def Magma.AssocQuotient (α : Type u) [Mul α] :

Semigroup quotient of a magma.

Equations
Instances For
theorem AddMagma.FreeAddSemigroup.quot_mk_assoc {α : Type u} [Add α] (x : α) (y : α) (z : α) :
Quot.mk (x + y + z) = Quot.mk (x + (y + z))
theorem Magma.AssocQuotient.quot_mk_assoc {α : Type u} [Mul α] (x : α) (y : α) (z : α) :
Quot.mk (x * y * z) = Quot.mk (x * (y * z))
theorem AddMagma.FreeAddSemigroup.quot_mk_assoc_left {α : Type u} [Add α] (x : α) (y : α) (z : α) (w : α) :
Quot.mk (x + (y + z + w)) = Quot.mk (x + (y + (z + w)))
theorem Magma.AssocQuotient.quot_mk_assoc_left {α : Type u} [Mul α] (x : α) (y : α) (z : α) (w : α) :
Quot.mk (x * (y * z * w)) = Quot.mk (x * (y * (z * w)))
AddMagma.AssocRel α a₁ a₂(fun (x y : α) => Quot.mk (x + y)) a₁ b = (fun (x y : α) => Quot.mk (x + y)) a₂ b
AddMagma.AssocRel α b₁ b₂(fun (x y : α) => Quot.mk (x + y)) a b₁ = (fun (x y : α) => Quot.mk (x + y)) a b₂
Equations
x + y + z = x + (y + z)
instance Magma.AssocQuotient.instSemigroup {α : Type u} [Mul α] :
Equations
• Magma.AssocQuotient.instSemigroup =

Equations
Instances For
Quot.mk (_x + _y) = Quot.mk (_x + _y)
def Magma.AssocQuotient.of {α : Type u} [Mul α] :

Embedding from magma to its free semigroup.

Equations
• Magma.AssocQuotient.of = { toFun := , map_mul' := }
Instances For
Equations
instance Magma.AssocQuotient.instInhabited {α : Type u} [Mul α] [] :
Equations
• Magma.AssocQuotient.instInhabited = { default := Magma.AssocQuotient.of default }
C x
theorem Magma.AssocQuotient.induction_on {α : Type u} [Mul α] {C : } (x : ) (ih : ∀ (x : α), C (Magma.AssocQuotient.of x)) :
C x
f = g
theorem AddMagma.FreeAddSemigroup.hom_ext_iff {α : Type u} [Add α] {β : Type v} [] {f : } {g : } :
theorem Magma.AssocQuotient.hom_ext_iff {α : Type u} [Mul α] {β : Type v} [] {f : } {g : } :
f = g f.comp Magma.AssocQuotient.of = g.comp Magma.AssocQuotient.of
theorem Magma.AssocQuotient.hom_ext {α : Type u} [Mul α] {β : Type v} [] {f : } {g : } (h : f.comp Magma.AssocQuotient.of = g.comp Magma.AssocQuotient.of) :
f = g

Lifts an additive magma homomorphism α → β to an additive semigroup homomorphism AddMagma.AssocQuotient α → β given an additive semigroup β.

Equations
• One or more equations did not get rendered due to their size.
Instances For
(fun (f : ) => f.comp AddMagma.FreeAddSemigroup.of) ((fun (f : AddHom α β) => { toFun := fun (x : ) => Quot.liftOn x f , map_add' := }) f) = f
theorem AddMagma.FreeAddSemigroup.lift.proof_2 {α : Type u_1} [Add α] {β : Type u_2} [] (f : AddHom α β) (x : ) (y : ) :
(fun (x : ) => Quot.liftOn x f ) (x + y) = (fun (x : ) => Quot.liftOn x f ) x + (fun (x : ) => Quot.liftOn x f ) y
theorem AddMagma.FreeAddSemigroup.lift.proof_4 {α : Type u_1} [Add α] {β : Type u_2} [] (f : ) :
(fun (f : AddHom α β) => { toFun := fun (x : ) => Quot.liftOn x f , map_add' := }) ((fun (f : ) => f.comp AddMagma.FreeAddSemigroup.of) f) = f
theorem AddMagma.FreeAddSemigroup.lift.proof_1 {α : Type u_1} [Add α] {β : Type u_2} [] (f : AddHom α β) (a : α) (b : α) :
f a = f b
@[simp]
theorem Magma.AssocQuotient.lift_symm_apply {α : Type u} [Mul α] {β : Type v} [] (f : ) :
Magma.AssocQuotient.lift.symm f = f.comp Magma.AssocQuotient.of
@[simp]
theorem AddMagma.FreeAddSemigroup.lift_symm_apply {α : Type u} [Add α] {β : Type v} [] (f : ) :
def Magma.AssocQuotient.lift {α : Type u} [Mul α] {β : Type v} [] :
(α →ₙ* β)

Lifts a magma homomorphism α → β to a semigroup homomorphism Magma.AssocQuotient α → β given a semigroup β.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
theorem Magma.AssocQuotient.lift_of {α : Type u} [Mul α] {β : Type v} [] (f : α →ₙ* β) (x : α) :
(Magma.AssocQuotient.lift f) (Magma.AssocQuotient.of x) = f x
@[simp]
@[simp]
theorem Magma.AssocQuotient.lift_comp_of {α : Type u} [Mul α] {β : Type v} [] (f : α →ₙ* β) :
(Magma.AssocQuotient.lift f).comp Magma.AssocQuotient.of = f
@[simp]
theorem AddMagma.FreeAddSemigroup.lift_comp_of' {α : Type u} [Add α] {β : Type v} [] (f : ) :
@[simp]
theorem Magma.AssocQuotient.lift_comp_of' {α : Type u} [Mul α] {β : Type v} [] (f : ) :
Magma.AssocQuotient.lift (f.comp Magma.AssocQuotient.of) = f

From an additive magma homomorphism α → β to an additive semigroup homomorphism AddMagma.AssocQuotient α → AddMagma.AssocQuotient β.

Equations
Instances For
def Magma.AssocQuotient.map {α : Type u} [Mul α] {β : Type v} [Mul β] (f : α →ₙ* β) :

From a magma homomorphism α →ₙ* β to a semigroup homomorphism Magma.AssocQuotient α →ₙ* Magma.AssocQuotient β.

Equations
• = Magma.AssocQuotient.lift (Magma.AssocQuotient.of.comp f)
Instances For
@[simp]
@[simp]
theorem Magma.AssocQuotient.map_of {α : Type u} [Mul α] {β : Type v} [Mul β] (f : α →ₙ* β) (x : α) :
(Magma.AssocQuotient.of x) = Magma.AssocQuotient.of (f x)
structure FreeAddSemigroup (α : Type u) :

Free additive semigroup over a given alphabet.

• tail : List α

The tail of the element

Instances For
theorem FreeAddSemigroup.ext_iff {α : Type u} {x : } {y : } :
theorem FreeSemigroup.ext_iff {α : Type u} {x : } {y : } :
theorem FreeAddSemigroup.ext {α : Type u} {x : } {y : } (head : x.head = y.head) (tail : x.tail = y.tail) :
x = y
theorem FreeSemigroup.ext {α : Type u} {x : } {y : } (head : x.head = y.head) (tail : x.tail = y.tail) :
x = y
structure FreeSemigroup (α : Type u) :

Free semigroup over a given alphabet.

• tail : List α

The tail of the element

Instances For
theorem FreeAddSemigroup.instAddSemigroup.proof_1 {α : Type u_1} (_L1 : ) (_L2 : ) (_L3 : ) :
_L1 + _L2 + _L3 = _L1 + (_L2 + _L3)
Equations
instance FreeSemigroup.instSemigroup {α : Type u} :
Equations
• FreeSemigroup.instSemigroup =
@[simp]
@[simp]
theorem FreeSemigroup.head_mul {α : Type u} (x : ) (y : ) :
@[simp]
theorem FreeAddSemigroup.tail_add {α : Type u} (x : ) (y : ) :
(x + y).tail = x.tail ++ y.head :: y.tail
@[simp]
theorem FreeSemigroup.tail_mul {α : Type u} (x : ) (y : ) :
(x * y).tail = x.tail ++ y.head :: y.tail
@[simp]
theorem FreeAddSemigroup.mk_add_mk {α : Type u} (x : α) (y : α) (L1 : List α) (L2 : List α) :
{ head := x, tail := L1 } + { head := y, tail := L2 } = { head := x, tail := L1 ++ y :: L2 }
@[simp]
theorem FreeSemigroup.mk_mul_mk {α : Type u} (x : α) (y : α) (L1 : List α) (L2 : List α) :
{ head := x, tail := L1 } * { head := y, tail := L2 } = { head := x, tail := L1 ++ y :: L2 }
def FreeAddSemigroup.of {α : Type u} (x : α) :

The embedding α → FreeAddSemigroup α.

Equations
• = { head := x, tail := [] }
Instances For
@[simp]
theorem FreeAddSemigroup.of_tail {α : Type u} (x : α) :
.tail = []
@[simp]
@[simp]
theorem FreeSemigroup.of_tail {α : Type u} (x : α) :
.tail = []
@[simp]
theorem FreeSemigroup.of_head {α : Type u} (x : α) :
def FreeSemigroup.of {α : Type u} (x : α) :

The embedding α → FreeSemigroup α.

Equations
• = { head := x, tail := [] }
Instances For
def FreeAddSemigroup.length {α : Type u} (x : ) :

Length of an element of free additive semigroup

Equations
• x.length = x.tail.length + 1
Instances For
def FreeSemigroup.length {α : Type u} (x : ) :

Length of an element of free semigroup.

Equations
• x.length = x.tail.length + 1
Instances For
@[simp]
theorem FreeAddSemigroup.length_add {α : Type u} (x : ) (y : ) :
(x + y).length = x.length + y.length
@[simp]
theorem FreeSemigroup.length_mul {α : Type u} (x : ) (y : ) :
(x * y).length = x.length + y.length
@[simp]
theorem FreeAddSemigroup.length_of {α : Type u} (x : α) :
.length = 1
@[simp]
theorem FreeSemigroup.length_of {α : Type u} (x : α) :
.length = 1
instance FreeAddSemigroup.instInhabited {α : Type u} [] :
Equations
instance FreeSemigroup.instInhabited {α : Type u} [] :
Equations
def FreeAddSemigroup.recOnAdd {α : Type u} {C : } (x : ) (ih1 : (x : α) → C ) (ih2 : (x : α) → (y : ) → C C yC ( + y)) :
C x

Recursor for free additive semigroup using of and +.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def FreeSemigroup.recOnMul {α : Type u} {C : } (x : ) (ih1 : (x : α) → C ) (ih2 : (x : α) → (y : ) → C C yC ( * y)) :
C x

Recursor for free semigroup using of and *.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem FreeAddSemigroup.hom_ext {α : Type u} {β : Type v} [Add β] {f : } {g : } (h : f FreeAddSemigroup.of = g FreeAddSemigroup.of) :
f = g
theorem FreeSemigroup.hom_ext_iff {α : Type u} {β : Type v} [Mul β] {f : } {g : } :
f = g f FreeSemigroup.of = g FreeSemigroup.of
theorem FreeAddSemigroup.hom_ext_iff {α : Type u} {β : Type v} [Add β] {f : } {g : } :
theorem FreeSemigroup.hom_ext {α : Type u} {β : Type v} [Mul β] {f : } {g : } (h : f FreeSemigroup.of = g FreeSemigroup.of) :
f = g
theorem FreeAddSemigroup.lift.proof_1 {α : Type u_1} {β : Type u_2} [] (f : αβ) (x : ) (y : ) :
List.foldl (fun (a : β) (b : α) => a + f b) (f x.head) (x.tail ++ y.head :: y.tail) = List.foldl (fun (x : β) (y : α) => x + f y) (f x.head) x.tail + List.foldl (fun (x : β) (y : α) => x + f y) (f y.head) y.tail
theorem FreeAddSemigroup.lift.proof_2 {α : Type u_1} {β : Type u_2} [] (f : αβ) :
(fun (f : ) => f FreeAddSemigroup.of) ((fun (f : αβ) => { toFun := fun (x : ) => List.foldl (fun (a : β) (b : α) => a + f b) (f x.head) x.tail, map_add' := }) f) = (fun (f : ) => f FreeAddSemigroup.of) ((fun (f : αβ) => { toFun := fun (x : ) => List.foldl (fun (a : β) (b : α) => a + f b) (f x.head) x.tail, map_add' := }) f)
def FreeAddSemigroup.lift {α : Type u} {β : Type v} [] :
(αβ)

Lifts a function α → β to an additive semigroup homomorphism FreeAddSemigroup α → β given an additive semigroup β.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem FreeAddSemigroup.lift.proof_3 {α : Type u_1} {β : Type u_2} [] (f : ) :
(fun (f : αβ) => { toFun := fun (x : ) => List.foldl (fun (a : β) (b : α) => a + f b) (f x.head) x.tail, map_add' := }) ((fun (f : ) => f FreeAddSemigroup.of) f) = f
@[simp]
theorem FreeAddSemigroup.lift_symm_apply {α : Type u} {β : Type v} [] (f : ) :
@[simp]
theorem FreeSemigroup.lift_symm_apply {α : Type u} {β : Type v} [] (f : ) :
∀ (a : α), FreeSemigroup.lift.symm f a = (f FreeSemigroup.of) a
def FreeSemigroup.lift {α : Type u} {β : Type v} [] :
(αβ) ( →ₙ* β)

Lifts a function α → β to a semigroup homomorphism FreeSemigroup α → β given a semigroup β.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem FreeAddSemigroup.lift_of {α : Type u} {β : Type v} [] (f : αβ) (x : α) :
@[simp]
theorem FreeSemigroup.lift_of {α : Type u} {β : Type v} [] (f : αβ) (x : α) :
(FreeSemigroup.lift f) = f x
@[simp]
theorem FreeAddSemigroup.lift_comp_of {α : Type u} {β : Type v} [] (f : αβ) :
@[simp]
theorem FreeSemigroup.lift_comp_of {α : Type u} {β : Type v} [] (f : αβ) :
(FreeSemigroup.lift f) FreeSemigroup.of = f
@[simp]
theorem FreeAddSemigroup.lift_comp_of' {α : Type u} {β : Type v} [] (f : ) :
@[simp]
theorem FreeSemigroup.lift_comp_of' {α : Type u} {β : Type v} [] (f : ) :
FreeSemigroup.lift (f FreeSemigroup.of) = f
theorem FreeAddSemigroup.lift_of_add {α : Type u} {β : Type v} [] (f : αβ) (x : α) (y : ) :
(FreeAddSemigroup.lift f) ( + y) = f x + (FreeAddSemigroup.lift f) y
theorem FreeSemigroup.lift_of_mul {α : Type u} {β : Type v} [] (f : αβ) (x : α) (y : ) :
(FreeSemigroup.lift f) ( * y) = f x * (FreeSemigroup.lift f) y
def FreeAddSemigroup.map {α : Type u} {β : Type v} (f : αβ) :

The unique additive semigroup homomorphism that sends of x to of (f x).

Equations
Instances For
def FreeSemigroup.map {α : Type u} {β : Type v} (f : αβ) :

The unique semigroup homomorphism that sends of x to of (f x).

Equations
• = FreeSemigroup.lift (FreeSemigroup.of f)
Instances For
@[simp]
theorem FreeAddSemigroup.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
@[simp]
theorem FreeSemigroup.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
@[simp]
theorem FreeAddSemigroup.length_map {α : Type u} {β : Type v} (f : αβ) (x : ) :
( x).length = x.length
@[simp]
theorem FreeSemigroup.length_map {α : Type u} {β : Type v} (f : αβ) (x : ) :
( x).length = x.length
def FreeAddSemigroup.recOnPure {α : Type u} {C : } (x : ) (ih1 : (x : α) → C (pure x)) (ih2 : (x : α) → (y : ) → C (pure x)C yC (pure x + y)) :
C x

Recursor that uses pure instead of of.

Equations
• x.recOnPure ih1 ih2 = x.recOnAdd ih1 ih2
Instances For
def FreeSemigroup.recOnPure {α : Type u} {C : } (x : ) (ih1 : (x : α) → C (pure x)) (ih2 : (x : α) → (y : ) → C (pure x)C yC (pure x * y)) :
C x

Recursor that uses pure instead of of.

Equations
• x.recOnPure ih1 ih2 = x.recOnMul ih1 ih2
Instances For
@[simp]
theorem FreeAddSemigroup.map_pure {α : Type u} {β : Type u} (f : αβ) (x : α) :
f <$> pure x = pure (f x) @[simp] theorem FreeSemigroup.map_pure {α : Type u} {β : Type u} (f : αβ) (x : α) : f <$> pure x = pure (f x)
@[simp]
theorem FreeAddSemigroup.map_add' {α : Type u} {β : Type u} (f : αβ) (x : ) (y : ) :
f <$> (x + y) = f <$> x + f <$> y @[simp] theorem FreeSemigroup.map_mul' {α : Type u} {β : Type u} (f : αβ) (x : ) (y : ) : f <$> (x * y) = f <$> x * f <$> y
@[simp]
theorem FreeAddSemigroup.pure_bind {α : Type u} {β : Type u} (f : α) (x : α) :
pure x >>= f = f x
@[simp]
theorem FreeSemigroup.pure_bind {α : Type u} {β : Type u} (f : α) (x : α) :
pure x >>= f = f x
@[simp]
theorem FreeAddSemigroup.add_bind {α : Type u} {β : Type u} (f : α) (x : ) (y : ) :
x + y >>= f = (x >>= f) + (y >>= f)
@[simp]
theorem FreeSemigroup.mul_bind {α : Type u} {β : Type u} (f : α) (x : ) (y : ) :
x * y >>= f = (x >>= f) * (y >>= f)
@[simp]
theorem FreeAddSemigroup.pure_seq {α : Type u} {β : Type u} {f : αβ} {x : } :
(Seq.seq (pure f) fun (x_1 : Unit) => x) = f <$> x @[simp] theorem FreeSemigroup.pure_seq {α : Type u} {β : Type u} {f : αβ} {x : } : (Seq.seq (pure f) fun (x_1 : Unit) => x) = f <$> x
@[simp]
(Seq.seq (f + g) fun (x_1 : Unit) => x) = (Seq.seq f fun (x_1 : Unit) => x) + Seq.seq g fun (x_1 : Unit) => x
@[simp]
theorem FreeSemigroup.mul_seq {α : Type u} {β : Type u} {f : FreeSemigroup (αβ)} {g : FreeSemigroup (αβ)} {x : } :
(Seq.seq (f * g) fun (x_1 : Unit) => x) = (Seq.seq f fun (x_1 : Unit) => x) * Seq.seq g fun (x_1 : Unit) => x
Equations
def FreeAddSemigroup.traverse {m : Type u → Type u} [] {α : Type u} {β : Type u} (F : αm β) (x : ) :
m

FreeAddSemigroup is traversable.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def FreeSemigroup.traverse {m : Type u → Type u} [] {α : Type u} {β : Type u} (F : αm β) (x : ) :
m

FreeSemigroup is traversable.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem FreeAddSemigroup.traverse_pure {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) (x : α) :
traverse F (pure x) = pure <$> F x @[simp] theorem FreeSemigroup.traverse_pure {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) (x : α) : traverse F (pure x) = pure <$> F x
@[simp]
theorem FreeAddSemigroup.traverse_pure' {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) :
pure = fun (x : α) => pure <$> F x @[simp] theorem FreeSemigroup.traverse_pure' {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) : pure = fun (x : α) => pure <$> F x
@[simp]
theorem FreeAddSemigroup.traverse_add {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) (x : ) (y : ) :
traverse F (x + y) = Seq.seq ((fun (x1 x2 : ) => x1 + x2) <$> traverse F x) fun (x : Unit) => traverse F y @[simp] theorem FreeSemigroup.traverse_mul {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) (x : ) (y : ) : traverse F (x * y) = Seq.seq ((fun (x1 x2 : ) => x1 * x2) <$> traverse F x) fun (x : Unit) => traverse F y
@[simp]
theorem FreeAddSemigroup.traverse_add' {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) :
HAdd.hAdd = fun (x y : ) => Seq.seq ((fun (x1 x2 : ) => x1 + x2) <$> traverse F x) fun (x : Unit) => traverse F y @[simp] theorem FreeSemigroup.traverse_mul' {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) : HMul.hMul = fun (x y : ) => Seq.seq ((fun (x1 x2 : ) => x1 * x2) <$> traverse F x) fun (x : Unit) => traverse F y
@[simp]
theorem FreeAddSemigroup.traverse_eq {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) (x : ) :
@[simp]
theorem FreeSemigroup.traverse_eq {α : Type u} {β : Type u} {m : Type u → Type u} [] (F : αm β) (x : ) :
= traverse F x
@[simp]
theorem FreeAddSemigroup.add_map_seq {α : Type u} (x : ) (y : ) :
(Seq.seq ((fun (x1 x2 : ) => x1 + x2) <$> x) fun (x : Unit) => y) = x + y @[simp] theorem FreeSemigroup.mul_map_seq {α : Type u} (x : ) (y : ) : (Seq.seq ((fun (x1 x2 : ) => x1 * x2) <$> x) fun (x : Unit) => y) = x * y
instance FreeAddSemigroup.instDecidableEq {α : Type u} [] :
Equations
instance FreeSemigroup.instDecidableEq {α : Type u} [] :
Equations

The canonical additive morphism from FreeAddMagma α to FreeAddSemigroup α.

Equations
Instances For

The canonical multiplicative morphism from FreeMagma α to FreeSemigroup α.

Equations
• FreeMagma.toFreeSemigroup = FreeMagma.lift FreeSemigroup.of
Instances For
@[simp]
@[simp]
theorem FreeMagma.toFreeSemigroup_of {α : Type u} (x : α) :
FreeMagma.toFreeSemigroup (FreeMagma.of x) =
@[simp]
@[simp]
theorem FreeMagma.toFreeSemigroup_comp_of {α : Type u} :
FreeMagma.toFreeSemigroup FreeMagma.of = FreeSemigroup.of
theorem FreeAddMagma.toFreeAddSemigroup_comp_map {α : Type u} {β : Type v} (f : αβ) :
theorem FreeMagma.toFreeSemigroup_comp_map {α : Type u} {β : Type v} (f : αβ) :
FreeMagma.toFreeSemigroup.comp = .comp FreeMagma.toFreeSemigroup
theorem FreeAddMagma.toFreeAddSemigroup_map {α : Type u} {β : Type v} (f : αβ) (x : ) :
theorem FreeMagma.toFreeSemigroup_map {α : Type u} {β : Type v} (f : αβ) (x : ) :
FreeMagma.toFreeSemigroup ( x) = (FreeMagma.toFreeSemigroup x)
@[simp]
@[simp]
theorem FreeMagma.length_toFreeSemigroup {α : Type u} (x : ) :
(FreeMagma.toFreeSemigroup x).length = x.length
theorem FreeAddMagmaAssocQuotientEquiv.proof_2 (α : Type u_1) :

Isomorphism between AddMagma.AssocQuotient (FreeAddMagma α) and FreeAddSemigroup α.

Equations
Isomorphism between Magma.AssocQuotient (FreeMagma α) and FreeSemigroup α.