# Documentation

Mathlib.Algebra.Free

# 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) :
• of: {α : Type u} → α
• add: {α : Type u} →

Free nonabelian additive magma over a given alphabet.

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

Free magma over a given alphabet.

Instances For
instance instDecidableEqFreeMagma :
{α : Type u_1} → [inst : ] →
Equations
• instDecidableEqFreeMagma = decEqFreeMagma✝
Equations
instance FreeMagma.instInhabitedFreeMagma {α : Type u} [inst : ] :
Equations
• FreeMagma.instInhabitedFreeMagma = { default := FreeMagma.of default }
Equations
instance FreeMagma.instMulFreeMagma {α : Type u} :
Mul ()
Equations
• FreeMagma.instMulFreeMagma = { mul := FreeMagma.mul }
@[simp]
theorem FreeAddMagma.add_eq {α : Type u} (x : ) (y : ) :
= x + y
@[simp]
theorem FreeMagma.mul_eq {α : Type u} (x : ) (y : ) :
= x * y
noncomputable 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
noncomputable def FreeMagma.recOnMul {α : Type u} {C : Sort l} (x : ) (ih1 : (x : α) → C ()) (ih2 : (x y : ) → C xC yC (x * y)) :
C x

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

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

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

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

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

Equations
def FreeAddMagma.lift.proof_2 {α : Type u_1} {β : Type u_2} [inst : Add β] (f : αβ) :
(fun F => F FreeAddMagma.of) ((fun f => { toFun := , map_add' := (_ : ∀ (x y : ), FreeAddMagma.liftAux f (x + y) = FreeAddMagma.liftAux f (x + y)) }) f) = (fun F => F FreeAddMagma.of) ((fun f => { toFun := , map_add' := (_ : ∀ (x y : ), FreeAddMagma.liftAux f (x + y) = FreeAddMagma.liftAux f (x + y)) }) f)
Equations
• One or more equations did not get rendered due to their size.
def FreeAddMagma.lift {α : Type u} {β : Type v} [inst : Add β] :

Equations
• One or more equations did not get rendered due to their size.
def FreeAddMagma.lift.proof_1 {α : Type u_1} {β : Type u_2} [inst : Add β] (f : αβ) (x : ) (y : ) :
Equations
def FreeAddMagma.lift.proof_3 {α : Type u_1} {β : Type u_2} [inst : Add β] (F : AddHom () β) :
(fun f => { toFun := , map_add' := (_ : ∀ (x y : ), FreeAddMagma.liftAux f (x + y) = FreeAddMagma.liftAux f (x + y)) }) ((fun F => F FreeAddMagma.of) F) = F
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem FreeAddMagma.lift_symm_apply {α : Type u} {β : Type v} [inst : Add β] (F : AddHom () β) :
∀ (a : α), ↑(Equiv.symm FreeAddMagma.lift) F a = (F FreeAddMagma.of) a
@[simp]
theorem FreeMagma.lift_symm_apply {α : Type u} {β : Type v} [inst : Mul β] (F : →ₙ* β) :
∀ (a : α), ↑(Equiv.symm FreeMagma.lift) F a = (F FreeMagma.of) a
def FreeMagma.lift {α : Type u} {β : Type v} [inst : Mul β] :
(αβ) ( →ₙ* β)

The universal property of the free magma expressing its adjointness.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem FreeAddMagma.lift_of {α : Type u} {β : Type v} [inst : Add β] (f : αβ) (x : α) :
↑(FreeAddMagma.lift f) () = f x
@[simp]
theorem FreeMagma.lift_of {α : Type u} {β : Type v} [inst : Mul β] (f : αβ) (x : α) :
↑(FreeMagma.lift f) () = f x
@[simp]
theorem FreeAddMagma.lift_comp_of {α : Type u} {β : Type v} [inst : Add β] (f : αβ) :
@[simp]
theorem FreeMagma.lift_comp_of {α : Type u} {β : Type v} [inst : Mul β] (f : αβ) :
↑(FreeMagma.lift f) FreeMagma.of = f
@[simp]
theorem FreeAddMagma.lift_comp_of' {α : Type u} {β : Type v} [inst : Add β] (f : AddHom () β) :
@[simp]
theorem FreeMagma.lift_comp_of' {α : Type u} {β : Type v} [inst : Mul β] (f : →ₙ* β) :
FreeMagma.lift (f FreeMagma.of) = f
def FreeAddMagma.map {α : Type u} {β : Type v} (f : αβ) :

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

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

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

Equations
• = FreeMagma.lift (FreeMagma.of f)
@[simp]
theorem FreeAddMagma.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
↑() () = FreeAddMagma.of (f x)
@[simp]
theorem FreeMagma.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
↑() () = FreeMagma.of (f x)
Equations
noncomputable 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
noncomputable 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
@[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 => x) = f <$> x @[simp] theorem FreeMagma.pure_seq {α : Type u} {β : Type u} {f : αβ} {x : } : (Seq.seq (pure f) fun x => x) = f <$> x
@[simp]
(Seq.seq (f + g) fun x => x) = (Seq.seq f fun x => x) + Seq.seq g fun x => x
@[simp]
theorem FreeMagma.mul_seq {α : Type u} {β : Type u} {f : FreeMagma (αβ)} {g : FreeMagma (αβ)} {x : } :
(Seq.seq (f * g) fun x => x) = (Seq.seq f fun x => x) * Seq.seq g fun x => x
def FreeMagma.traverse {m : Type u → Type u} [inst : ] {α : Type u} {β : Type u} (F : αm β) :
m ()

FreeMagma is traversable.

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

FreeAddMagma is traversable.

Equations
@[simp]
theorem FreeAddMagma.traverse_pure {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) (x : α) :
traverse F (pure x) = pure <$> F x @[simp] theorem FreeMagma.traverse_pure {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) (x : α) : traverse F (pure x) = pure <$> F x
@[simp]
theorem FreeAddMagma.traverse_pure' {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) :
pure = fun x => pure <$> F x @[simp] theorem FreeMagma.traverse_pure' {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) : pure = fun x => pure <$> F x
@[simp]
theorem FreeAddMagma.traverse_add {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) (x : ) (y : ) :
traverse F (x + y) = Seq.seq ((fun x x_1 => x + x_1) <$> traverse F x) fun x => traverse F y @[simp] theorem FreeMagma.traverse_mul {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) (x : ) (y : ) : traverse F (x * y) = Seq.seq ((fun x x_1 => x * x_1) <$> traverse F x) fun x => traverse F y
@[simp]
theorem FreeAddMagma.traverse_add' {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) :
Add.add = fun x y => Seq.seq ((fun x x_1 => x + x_1) <$> traverse F x) fun x => traverse F y @[simp] theorem FreeMagma.traverse_mul' {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) : Mul.mul = fun x y => Seq.seq ((fun x x_1 => x * x_1) <$> traverse F x) fun x => traverse F y
@[simp]
theorem FreeAddMagma.traverse_eq {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) (x : ) :
= traverse F x
@[simp]
theorem FreeMagma.traverse_eq {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) (x : ) :
= traverse F x
@[simp]
theorem FreeAddMagma.add_map_seq {α : Type u} (x : ) (y : ) :
(Seq.seq ((fun x x_1 => x + x_1) <$> x) fun x => y) = x + y @[simp] theorem FreeMagma.mul_map_seq {α : Type u} (x : ) (y : ) : (Seq.seq ((fun x x_1 => x * x_1) <$> x) fun x => y) = x * y
Equations
• One or more equations did not get rendered due to their size.
∀ {F G : Type u_1 → Type u_1} [inst : ] [inst_1 : ] [inst_2 : ] [inst_3 : ] (η : ) (α β : Type u_1) (f : αF β) (x : ), (fun {α} => ) (traverse f x) = traverse ((fun {α} => ) f) x
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
∀ {F G : Type u_1 → Type u_1} [inst : ] [inst_1 : ] [inst_2 : ] [inst_3 : ] {α β γ : Type u_1} (f : βF γ) (g : αG β) (x : ), traverse (Functor.Comp.mk g) x = Functor.Comp.mk ( <$> traverse g x) Equations • One or more equations did not get rendered due to their size. Equations • One or more equations did not get rendered due to their size. def FreeMagma.repr {α : Type u} [inst : Repr α] : Representation of an element of a free magma. Equations def FreeAddMagma.repr {α : Type u} [inst : Repr α] : Representation of an element of a free additive magma. Equations instance instReprFreeAddMagma {α : Type u} [inst : Repr α] : Repr () Equations • instReprFreeAddMagma = { reprPrec := fun o x => } instance instReprFreeMagma {α : Type u} [inst : Repr α] : Repr () Equations • instReprFreeMagma = { reprPrec := fun o x => } def FreeMagma.length {α : Type u} : Length of an element of a free magma. Equations def FreeAddMagma.length {α : Type u} : Length of an element of a free additive magma. Equations inductive AddMagma.AssocRel (α : Type u) [inst : Add α] : ααProp Associativity relations for an additive magma. Instances For inductive Magma.AssocRel (α : Type u) [inst : Mul α] : ααProp Associativity relations for a magma. Instances For def AddMagma.FreeAddSemigroup (α : Type u) [inst : Add α] : Additive semigroup quotient of an additive magma. Equations def Magma.AssocQuotient (α : Type u) [inst : Mul α] : Semigroup quotient of a magma. Equations theorem AddMagma.FreeAddSemigroup.quot_mk_assoc {α : Type u} [inst : Add α] (x : α) (y : α) (z : α) : Quot.mk () (x + y + z) = Quot.mk () (x + (y + z)) theorem Magma.AssocQuotient.quot_mk_assoc {α : Type u} [inst : Mul α] (x : α) (y : α) (z : α) : Quot.mk () (x * y * z) = Quot.mk () (x * (y * z)) theorem AddMagma.FreeAddSemigroup.quot_mk_assoc_left {α : Type u} [inst : 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} [inst : Mul α] (x : α) (y : α) (z : α) (w : α) : Quot.mk () (x * (y * z * w)) = Quot.mk () (x * (y * (z * w))) def AddMagma.FreeAddSemigroup.instAddSemigroupAssocQuotient.proof_2 {α : Type u_1} [inst : Add α] (a₁ : α) (a₂ : α) (b : α) : AddMagma.AssocRel α a₁ a₂(fun x y => Quot.mk () (x + y)) a₁ b = (fun x y => Quot.mk () (x + y)) a₂ b Equations • One or more equations did not get rendered due to their size. def AddMagma.FreeAddSemigroup.instAddSemigroupAssocQuotient.proof_3 {α : Type u_1} [inst : Add α] (x : ) (y : ) (z : ) : x + y + z = x + (y + z) Equations • (_ : x + y + z = x + (y + z)) = (_ : x + y + z = x + (y + z)) Equations • AddMagma.FreeAddSemigroup.instAddSemigroupAssocQuotient = AddSemigroup.mk (_ : ∀ (x y z : ), x + y + z = x + (y + z)) def AddMagma.FreeAddSemigroup.instAddSemigroupAssocQuotient.proof_1 {α : Type u_1} [inst : Add α] (a : α) (b₁ : α) (b₂ : α) : AddMagma.AssocRel α b₁ b₂(fun x y => Quot.mk () (x + y)) a b₁ = (fun x y => Quot.mk () (x + y)) a b₂ Equations • One or more equations did not get rendered due to their size. Equations • Magma.AssocQuotient.instSemigroupAssocQuotient = Semigroup.mk (_ : ∀ (x y z : ), x * y * z = x * (y * z)) def AddMagma.FreeAddSemigroup.of.proof_1 {α : Type u_1} [inst : Add α] (_x : α) (_y : α) : Quot.mk () (_x + _y) = Quot.mk () (_x + _y) Equations def AddMagma.FreeAddSemigroup.of {α : Type u} [inst : Add α] : Embedding from additive magma to its free additive semigroup. Equations • AddMagma.FreeAddSemigroup.of = { toFun := , map_add' := (_ : ∀ (_x _y : α), Quot.mk () (_x + _y) = Quot.mk () (_x + _y)) } def Magma.AssocQuotient.of {α : Type u} [inst : Mul α] : Embedding from magma to its free semigroup. Equations • Magma.AssocQuotient.of = { toFun := , map_mul' := (_ : ∀ (_x _y : α), Quot.mk () (_x * _y) = Quot.mk () (_x * _y)) } instance AddMagma.FreeAddSemigroup.instInhabitedAssocQuotient {α : Type u} [inst : Add α] [inst : ] : Equations • AddMagma.FreeAddSemigroup.instInhabitedAssocQuotient = { default := AddMagma.FreeAddSemigroup.of default } instance Magma.AssocQuotient.instInhabitedAssocQuotient {α : Type u} [inst : Mul α] [inst : ] : Equations • Magma.AssocQuotient.instInhabitedAssocQuotient = { default := Magma.AssocQuotient.of default } theorem AddMagma.FreeAddSemigroup.induction_on {α : Type u} [inst : Add α] {C : } (x : ) (ih : (x : α) → C (AddMagma.FreeAddSemigroup.of x)) : C x theorem Magma.AssocQuotient.induction_on {α : Type u} [inst : Mul α] {C : } (x : ) (ih : (x : α) → C (Magma.AssocQuotient.of x)) : C x theorem AddMagma.FreeAddSemigroup.hom_ext {α : Type u} [inst : Add α] {β : Type v} [inst : ] {f : } {g : } (h : AddHom.comp f AddMagma.FreeAddSemigroup.of = AddHom.comp g AddMagma.FreeAddSemigroup.of) : f = g theorem Magma.AssocQuotient.hom_ext {α : Type u} [inst : Mul α] {β : Type v} [inst : ] {f : } {g : } (h : MulHom.comp f Magma.AssocQuotient.of = MulHom.comp g Magma.AssocQuotient.of) : f = g def AddMagma.FreeAddSemigroup.lift.proof_2 {α : Type u_1} [inst : Add α] {β : Type u_2} [inst : ] (f : AddHom α β) (x : ) (y : ) : (fun x => Quot.liftOn x f (_ : ∀ (a b : α), f a = f b)) (x + y) = (fun x => Quot.liftOn x f (_ : ∀ (a b : α), f a = f b)) x + (fun x => Quot.liftOn x f (_ : ∀ (a b : α), f a = f b)) y Equations • One or more equations did not get rendered due to their size. def AddMagma.FreeAddSemigroup.lift.proof_4 {α : Type u_1} [inst : Add α] {β : Type u_2} [inst : ] (f : ) : (fun f => { toFun := fun x => Quot.liftOn x f (_ : ∀ (a b : α), f a = f b), map_add' := (_ : ∀ (x y : ), (fun x => Quot.liftOn x f (_ : ∀ (a b : α), f a = f b)) (x + y) = (fun x => Quot.liftOn x f (_ : ∀ (a b : α), f a = f b)) x + (fun x => Quot.liftOn x f (_ : ∀ (a b : α), f a = f b)) y) }) ((fun f => AddHom.comp f AddMagma.FreeAddSemigroup.of) f) = f Equations • One or more equations did not get rendered due to their size. def AddMagma.FreeAddSemigroup.lift.proof_1 {α : Type u_1} [inst : Add α] {β : Type u_2} [inst : ] (f : AddHom α β) (a : α) (b : α) : f a = f b Equations • (_ : f a = f b) = (_ : f a = f b) def AddMagma.FreeAddSemigroup.lift.proof_3 {α : Type u_1} [inst : Add α] {β : Type u_2} [inst : ] (f : AddHom α β) : (fun f => AddHom.comp f AddMagma.FreeAddSemigroup.of) ((fun f => { toFun := fun x => Quot.liftOn x f (_ : ∀ (a b : α), f a = f b), map_add' := (_ : ∀ (x y : ), (fun x => Quot.liftOn x f (_ : ∀ (a b : α), f a = f b)) (x + y) = (fun x => Quot.liftOn x f (_ : ∀ (a b : α), f a = f b)) x + (fun x => Quot.liftOn x f (_ : ∀ (a b : α), f a = f b)) y) }) f) = f Equations • One or more equations did not get rendered due to their size. def AddMagma.FreeAddSemigroup.lift {α : Type u} [inst : Add α] {β : Type v} [inst : ] : AddHom α β 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. @[simp] theorem AddMagma.FreeAddSemigroup.lift_symm_apply {α : Type u} [inst : Add α] {β : Type v} [inst : ] (f : ) : ↑(Equiv.symm AddMagma.FreeAddSemigroup.lift) f = AddHom.comp f AddMagma.FreeAddSemigroup.of @[simp] theorem Magma.AssocQuotient.lift_symm_apply {α : Type u} [inst : Mul α] {β : Type v} [inst : ] (f : ) : ↑(Equiv.symm Magma.AssocQuotient.lift) f = MulHom.comp f Magma.AssocQuotient.of def Magma.AssocQuotient.lift {α : Type u} [inst : Mul α] {β : Type v} [inst : ] : (α →ₙ* β) () 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. @[simp] theorem AddMagma.FreeAddSemigroup.lift_of {α : Type u} [inst : Add α] {β : Type v} [inst : ] (f : AddHom α β) (x : α) : ↑(AddMagma.FreeAddSemigroup.lift f) (AddMagma.FreeAddSemigroup.of x) = f x @[simp] theorem Magma.AssocQuotient.lift_of {α : Type u} [inst : Mul α] {β : Type v} [inst : ] (f : α →ₙ* β) (x : α) : ↑(Magma.AssocQuotient.lift f) (Magma.AssocQuotient.of x) = f x @[simp] theorem AddMagma.FreeAddSemigroup.lift_comp_of {α : Type u} [inst : Add α] {β : Type v} [inst : ] (f : AddHom α β) : AddHom.comp (AddMagma.FreeAddSemigroup.lift f) AddMagma.FreeAddSemigroup.of = f @[simp] theorem Magma.AssocQuotient.lift_comp_of {α : Type u} [inst : Mul α] {β : Type v} [inst : ] (f : α →ₙ* β) : MulHom.comp (Magma.AssocQuotient.lift f) Magma.AssocQuotient.of = f @[simp] theorem AddMagma.FreeAddSemigroup.lift_comp_of' {α : Type u} [inst : Add α] {β : Type v} [inst : ] (f : ) : AddMagma.FreeAddSemigroup.lift (AddHom.comp f AddMagma.FreeAddSemigroup.of) = f @[simp] theorem Magma.AssocQuotient.lift_comp_of' {α : Type u} [inst : Mul α] {β : Type v} [inst : ] (f : ) : Magma.AssocQuotient.lift (MulHom.comp f Magma.AssocQuotient.of) = f def AddMagma.FreeAddSemigroup.map {α : Type u} [inst : Add α] {β : Type v} [inst : Add β] (f : AddHom α β) : From an additive magma homomorphism α → β→ β to an additive semigroup homomorphism AddMagma.AssocQuotient α → AddMagma.AssocQuotient β→ AddMagma.AssocQuotient β. Equations • = AddMagma.FreeAddSemigroup.lift (AddHom.comp AddMagma.FreeAddSemigroup.of f) def Magma.AssocQuotient.map {α : Type u} [inst : Mul α] {β : Type v} [inst : Mul β] (f : α →ₙ* β) : From a magma homomorphism α →ₙ* β→ₙ* β to a semigroup homomorphism Magma.AssocQuotient α →ₙ* Magma.AssocQuotient β→ₙ* Magma.AssocQuotient β. Equations • = Magma.AssocQuotient.lift (MulHom.comp Magma.AssocQuotient.of f) @[simp] theorem AddMagma.FreeAddSemigroup.map_of {α : Type u} [inst : Add α] {β : Type v} [inst : Add β] (f : AddHom α β) (x : α) : ↑() (AddMagma.FreeAddSemigroup.of x) = AddMagma.FreeAddSemigroup.of (f x) @[simp] theorem Magma.AssocQuotient.map_of {α : Type u} [inst : Mul α] {β : Type v} [inst : Mul β] (f : α →ₙ* β) (x : α) : ↑() (Magma.AssocQuotient.of x) = Magma.AssocQuotient.of (f x) structure FreeAddSemigroup (α : Type u) : • The head of the element head : α • The tail of the element tail : List α Free additive semigroup over a given alphabet. Instances For theorem FreeAddSemigroup.ext_iff {α : Type u} (x : ) (y : ) : x = y x.head = y.head x.tail = y.tail 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 theorem FreeSemigroup.ext_iff {α : Type u} (x : ) (y : ) : x = y x.head = y.head x.tail = y.tail structure FreeSemigroup (α : Type u) : • The head of the element head : α • The tail of the element tail : List α Free semigroup over a given alphabet. Instances For def FreeAddSemigroup.instAddSemigroupFreeAddSemigroup.proof_1 {α : Type u_1} (_L1 : ) (_L2 : ) (_L3 : ) : _L1 + _L2 + _L3 = _L1 + (_L2 + _L3) Equations • (_ : _L1 + _L2 + _L3 = _L1 + (_L2 + _L3)) = (_ : _L1 + _L2 + _L3 = _L1 + (_L2 + _L3)) Equations • FreeAddSemigroup.instAddSemigroupFreeAddSemigroup = AddSemigroup.mk (_ : ∀ (_L1 _L2 _L3 : ), _L1 + _L2 + _L3 = _L1 + (_L2 + _L3)) Equations • FreeSemigroup.instSemigroupFreeSemigroup = Semigroup.mk (_ : ∀ (_L1 _L2 _L3 : ), _L1 * _L2 * _L3 = _L1 * (_L2 * _L3)) @[simp] theorem FreeAddSemigroup.head_add {α : Type u} (x : ) (y : ) : (x + y).head = x.head @[simp] theorem FreeSemigroup.head_mul {α : Type u} (x : ) (y : ) : (x * y).head = x.head @[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 α → free_add_semigroup α→ free_add_semigroup α. Equations • = { head := x, tail := [] } @[simp] theorem FreeAddSemigroup.of_head {α : Type u} (x : α) : ().head = x @[simp] theorem FreeSemigroup.of_head {α : Type u} (x : α) : ().head = x @[simp] theorem FreeSemigroup.of_tail {α : Type u} (x : α) : ().tail = [] @[simp] theorem FreeAddSemigroup.of_tail {α : Type u} (x : α) : ().tail = [] def FreeSemigroup.of {α : Type u} (x : α) : The embedding α → FreeSemigroup α→ FreeSemigroup α. Equations • = { head := x, tail := [] } def FreeAddSemigroup.length {α : Type u} (x : ) : Length of an element of free additive semigroup Equations def FreeSemigroup.length {α : Type u} (x : ) : Length of an element of free semigroup. Equations @[simp] theorem FreeAddSemigroup.length_add {α : Type u} (x : ) (y : ) : @[simp] theorem FreeSemigroup.length_mul {α : Type u} (x : ) (y : ) : @[simp] theorem FreeAddSemigroup.length_of {α : Type u} (x : α) : @[simp] theorem FreeSemigroup.length_of {α : Type u} (x : α) : Equations instance FreeSemigroup.instInhabitedFreeSemigroup {α : Type u} [inst : ] : Equations noncomputable def FreeAddSemigroup.recOnAdd {α : Type u} {C : } (x : ) (ih1 : (x : α) → C ()) (ih2 : (x : α) → (y : ) → C ()C yC ()) : C x Recursor for free additive semigroup using of and +. Equations • One or more equations did not get rendered due to their size. noncomputable def FreeSemigroup.recOnMul {α : Type u} {C : } (x : ) (ih1 : (x : α) → C ()) (ih2 : (x : α) → (y : ) → C ()C yC ()) : C x Recursor for free semigroup using of and *. Equations • One or more equations did not get rendered due to their size. theorem FreeAddSemigroup.hom_ext {α : Type u} {β : Type v} [inst : Add β] {f : } {g : } (h : f FreeAddSemigroup.of = g FreeAddSemigroup.of) : f = g theorem FreeSemigroup.hom_ext {α : Type u} {β : Type v} [inst : Mul β] {f : } {g : } (h : f FreeSemigroup.of = g FreeSemigroup.of) : f = g def FreeAddSemigroup.lift {α : Type u} {β : Type v} [inst : ] : (αβ) 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. def FreeAddSemigroup.lift.proof_1 {α : Type u_1} {β : Type u_2} [inst : ] (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 Equations • One or more equations did not get rendered due to their size. def FreeAddSemigroup.lift.proof_3 {α : Type u_1} {β : Type u_2} [inst : ] (f : ) : (fun f => { toFun := fun x => List.foldl (fun a b => a + f b) (f x.head) x.tail, map_add' := (_ : ∀ (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) }) ((fun f => f FreeAddSemigroup.of) f) = f Equations • One or more equations did not get rendered due to their size. def FreeAddSemigroup.lift.proof_2 {α : Type u_1} {β : Type u_2} [inst : ] (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' := (_ : ∀ (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) }) 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' := (_ : ∀ (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) }) f) Equations • One or more equations did not get rendered due to their size. @[simp] theorem FreeSemigroup.lift_symm_apply {α : Type u} {β : Type v} [inst : ] (f : ) : ∀ (a : α), ↑(Equiv.symm FreeSemigroup.lift) f a = (f FreeSemigroup.of) a @[simp] theorem FreeAddSemigroup.lift_symm_apply {α : Type u} {β : Type v} [inst : ] (f : ) : ∀ (a : α), ↑(Equiv.symm FreeAddSemigroup.lift) f a = (f FreeAddSemigroup.of) a def FreeSemigroup.lift {α : Type u} {β : Type v} [inst : ] : (αβ) () Lifts a function α → β→ β to a semigroup homomorphism FreeSemigroup α → β→ β given a semigroup β. Equations • One or more equations did not get rendered due to their size. @[simp] theorem FreeAddSemigroup.lift_of {α : Type u} {β : Type v} [inst : ] (f : αβ) (x : α) : ↑(FreeAddSemigroup.lift f) () = f x @[simp] theorem FreeSemigroup.lift_of {α : Type u} {β : Type v} [inst : ] (f : αβ) (x : α) : ↑(FreeSemigroup.lift f) () = f x @[simp] theorem FreeAddSemigroup.lift_comp_of {α : Type u} {β : Type v} [inst : ] (f : αβ) : ↑(FreeAddSemigroup.lift f) FreeAddSemigroup.of = f @[simp] theorem FreeSemigroup.lift_comp_of {α : Type u} {β : Type v} [inst : ] (f : αβ) : ↑(FreeSemigroup.lift f) FreeSemigroup.of = f @[simp] theorem FreeAddSemigroup.lift_comp_of' {α : Type u} {β : Type v} [inst : ] (f : ) : FreeAddSemigroup.lift (f FreeAddSemigroup.of) = f @[simp] theorem FreeSemigroup.lift_comp_of' {α : Type u} {β : Type v} [inst : ] (f : ) : FreeSemigroup.lift (f FreeSemigroup.of) = f theorem FreeAddSemigroup.lift_of_add {α : Type u} {β : Type v} [inst : ] (f : αβ) (x : α) (y : ) : ↑(FreeAddSemigroup.lift f) () = f x + ↑(FreeAddSemigroup.lift f) y theorem FreeSemigroup.lift_of_mul {α : Type u} {β : Type v} [inst : ] (f : αβ) (x : α) (y : ) : ↑(FreeSemigroup.lift f) () = 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 • = FreeAddSemigroup.lift (FreeAddSemigroup.of f) 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) @[simp] theorem FreeAddSemigroup.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) : ↑() () = FreeAddSemigroup.of (f x) @[simp] theorem FreeSemigroup.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) : ↑() () = FreeSemigroup.of (f x) @[simp] theorem FreeAddSemigroup.length_map {α : Type u} {β : Type v} (f : αβ) (x : ) : @[simp] theorem FreeSemigroup.length_map {α : Type u} {β : Type v} (f : αβ) (x : ) : Equations Equations noncomputable 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 noncomputable 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 @[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 => x) = f <$> x
@[simp]
theorem FreeSemigroup.pure_seq {α : Type u} {β : Type u} {f : αβ} {x : } :
(Seq.seq (pure f) fun x => x) = f <$> x @[simp] theorem FreeAddSemigroup.add_seq {α : Type u} {β : Type u} {f : FreeAddSemigroup (αβ)} {g : FreeAddSemigroup (αβ)} {x : } : (Seq.seq (f + g) fun x => x) = (Seq.seq f fun x => x) + Seq.seq g fun x => x @[simp] theorem FreeSemigroup.mul_seq {α : Type u} {β : Type u} {f : FreeSemigroup (αβ)} {g : FreeSemigroup (αβ)} {x : } : (Seq.seq (f * g) fun x => x) = (Seq.seq f fun x => x) * Seq.seq g fun x => x noncomputable def FreeAddSemigroup.traverse {m : Type u → Type u} [inst : ] {α : Type u} {β : Type u} (F : αm β) (x : ) : m () FreeAddSemigroup is traversable. Equations noncomputable def FreeSemigroup.traverse {m : Type u → Type u} [inst : ] {α : Type u} {β : Type u} (F : αm β) (x : ) : m () FreeSemigroup is traversable. Equations @[simp] theorem FreeAddSemigroup.traverse_pure {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) (x : α) : traverse F (pure x) = pure <$> F x
@[simp]
theorem FreeSemigroup.traverse_pure {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) (x : α) :
traverse F (pure x) = pure <$> F x @[simp] theorem FreeAddSemigroup.traverse_pure' {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) : pure = fun x => pure <$> F x
@[simp]
theorem FreeSemigroup.traverse_pure' {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) :
pure = fun x => pure <$> F x @[simp] theorem FreeAddSemigroup.traverse_add {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) [inst : ] (x : ) (y : ) : traverse F (x + y) = Seq.seq ((fun x x_1 => x + x_1) <$> traverse F x) fun x => traverse F y
@[simp]
theorem FreeSemigroup.traverse_mul {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) [inst : ] (x : ) (y : ) :
traverse F (x * y) = Seq.seq ((fun x x_1 => x * x_1) <$> traverse F x) fun x => traverse F y @[simp] theorem FreeAddSemigroup.traverse_add' {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) [inst : ] : Add.add = fun x y => Seq.seq ((fun x x_1 => x + x_1) <$> traverse F x) fun x => traverse F y
@[simp]
theorem FreeSemigroup.traverse_mul' {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) [inst : ] :
Mul.mul = fun x y => Seq.seq ((fun x x_1 => x * x_1) <$> traverse F x) fun x => traverse F y @[simp] theorem FreeAddSemigroup.traverse_eq {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) (x : ) : @[simp] theorem FreeSemigroup.traverse_eq {α : Type u} {β : Type u} {m : Type u → Type u} [inst : ] (F : αm β) (x : ) : = traverse F x @[simp] theorem FreeAddSemigroup.add_map_seq {α : Type u} (x : ) (y : ) : (Seq.seq ((fun x x_1 => x + x_1) <$> x) fun x => y) = x + y
@[simp]
theorem FreeSemigroup.mul_map_seq {α : Type u} (x : ) (y : ) :
(Seq.seq ((fun x x_1 => x * x_1) <$> x) fun x => y) = x * y Equations • One or more equations did not get rendered due to their size. def FreeAddSemigroup.instIsLawfulTraversableFreeAddSemigroupInstTraversableFreeAddSemigroup.proof_3 : ∀ {F G : Type u_1 → Type u_1} [inst : ] [inst_1 : ] [inst_2 : ] [inst_3 : ] {α β γ : Type u_1} (f : βF γ) (g : αG β) (x : ), traverse (Functor.Comp.mk g) x = Functor.Comp.mk ( <$> traverse g x)
Equations
• One or more equations did not get rendered due to their size.
∀ {F G : Type u_1 → Type u_1} [inst : ] [inst_1 : ] [inst_2 : ] [inst_3 : ] (η : ) (α β : Type u_1) (f : αF β) (x : ), (fun {α} => ) (traverse f x) = traverse ((fun {α} => ) f) x
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
instance FreeSemigroup.instDecidableEqFreeSemigroup {α : Type u} [inst : ] :
Equations

The canonical additive morphism from FreeAddMagma α to FreeAddSemigroup α.

Equations

The canonical multiplicative morphism from FreeMagma α to FreeSemigroup α.

Equations
• FreeMagma.toFreeSemigroup = FreeMagma.lift FreeSemigroup.of
@[simp]
@[simp]
theorem FreeMagma.toFreeSemigroup_of {α : Type u} (x : α) :
FreeMagma.toFreeSemigroup () =
@[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 : αβ) :
MulHom.comp FreeMagma.toFreeSemigroup () = MulHom.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 : ) :
FreeSemigroup.length (FreeMagma.toFreeSemigroup x) =
def FreeAddMagmaAssocQuotientEquiv.proof_1 (α : Type u_1) :
Equations
• One or more equations did not get rendered due to their size.
def FreeAddMagmaAssocQuotientEquiv.proof_2 (α : Type u_1) :
Isomorphism between AddMagma.AssocQuotient (FreeAddMagma α) and FreeAddSemigroup α.
Isomorphism between Magma.AssocQuotient (FreeMagma α) and FreeSemigroup α.