Documentation

Mathlib.Algebra.Free

Free constructions #

Main definitions #

inductive FreeAddMagma (α : Type u) :

If α is a type, then FreeAddMagma α is the free additive magma generated by α. This is an additive magma equipped with a function FreeAddMagma.of : α → FreeAddMagma α which has the following universal property: if M is any magma, and f : α → M is any function, then this function is the composite of FreeAddMagma.of and a unique additive homomorphism FreeAddMagma.lift f : FreeAddMagma α →ₙ+ M.

A typical element of FreeAddMagma α is a formal non-associative sum of elements of α. For example if x and y are terms of type α then x + ((y + y) + x) is a "typical" element of FreeAddMagma α. One can think of FreeAddMagma α as the type of binary trees with leaves labelled by α. In general, no pair of distinct elements in FreeAddMagma α will commute.

inductive FreeMagma (α : Type u) :

If α is a type, then FreeMagma α is the free magma generated by α. This is a magma equipped with a function FreeMagma.of : α → FreeMagma α which has the following universal property: if M is any magma, and f : α → M is any function, then this function is the composite of FreeMagma.of and a unique multiplicative homomorphism FreeMagma.lift f : FreeMagma α →ₙ* M.

A typical element of FreeMagma α is a formal non-associative product of elements of α. For example if x and y are terms of type α then x * ((y * y) * x) is a "typical" element of FreeMagma α. One can think of FreeMagma α as the type of binary trees with leaves labelled by α. In general, no pair of distinct elements in FreeMagma α will commute.

@[simp]
theorem FreeMagma.mul_eq {α : Type u} (x y : FreeMagma α) :
x.mul y = x * y
@[simp]
theorem FreeAddMagma.add_eq {α : Type u} (x y : FreeAddMagma α) :
x.add y = x + y
def FreeMagma.recOnMul {α : Type u} {C : FreeMagma αSort l} (x : FreeMagma α) (ih1 : (x : α) → C (of x)) (ih2 : (x y : FreeMagma α) → C xC yC (x * y)) :
C x

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

Equations
def FreeAddMagma.recOnAdd {α : Type u} {C : FreeAddMagma αSort l} (x : FreeAddMagma α) (ih1 : (x : α) → C (of x)) (ih2 : (x y : FreeAddMagma α) → C xC yC (x + y)) :
C x

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

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

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

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

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

Equations
def FreeMagma.lift {α : Type u} {β : Type v} [Mul β] :
(αβ) (FreeMagma α →ₙ* β)

The universal property of the free magma expressing its adjointness.

Equations
def FreeAddMagma.lift {α : Type u} {β : Type v} [Add β] :
(αβ) (FreeAddMagma α →ₙ+ β)

The universal property of the free additive magma expressing its adjointness.

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

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

Equations
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
@[simp]
theorem FreeMagma.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
(map f) (of x) = of (f x)
@[simp]
theorem FreeAddMagma.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
(map f) (of x) = of (f 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.recOnPure {α : Type u} {C : FreeMagma αSort l} (x : FreeMagma α) (ih1 : (x : α) → C (pure x)) (ih2 : (x y : FreeMagma α) → C xC yC (x * y)) :
C x

Recursor on FreeMagma using pure instead of of.

Equations
def FreeAddMagma.recOnPure {α : Type u} {C : FreeAddMagma αSort l} (x : FreeAddMagma α) (ih1 : (x : α) → C (pure x)) (ih2 : (x y : FreeAddMagma α) → C xC yC (x + y)) :
C x

Recursor on FreeAddMagma using pure instead of of.

Equations
@[simp]
theorem FreeMagma.map_pure {α β : Type u} (f : αβ) (x : α) :
f <$> pure x = pure (f x)
@[simp]
theorem FreeAddMagma.map_pure {α β : Type u} (f : αβ) (x : α) :
f <$> pure x = pure (f x)
@[simp]
theorem FreeMagma.map_mul' {α β : Type u} (f : αβ) (x y : FreeMagma α) :
f <$> (x * y) = f <$> x * f <$> y
@[simp]
theorem FreeAddMagma.map_add' {α β : Type u} (f : αβ) (x y : FreeAddMagma α) :
f <$> (x + y) = f <$> x + f <$> y
@[simp]
theorem FreeMagma.pure_bind {α β : Type u} (f : αFreeMagma β) (x : α) :
pure x >>= f = f x
@[simp]
theorem FreeAddMagma.pure_bind {α β : Type u} (f : αFreeAddMagma β) (x : α) :
pure x >>= f = f x
@[simp]
theorem FreeMagma.mul_bind {α β : Type u} (f : αFreeMagma β) (x y : FreeMagma α) :
x * y >>= f = (x >>= f) * (y >>= f)
@[simp]
theorem FreeAddMagma.add_bind {α β : Type u} (f : αFreeAddMagma β) (x y : FreeAddMagma α) :
x + y >>= f = (x >>= f) + (y >>= f)
@[simp]
theorem FreeMagma.pure_seq {α β : Type u} {f : αβ} {x : FreeMagma α} :
pure f <*> x = f <$> x
@[simp]
theorem FreeAddMagma.pure_seq {α β : Type u} {f : αβ} {x : FreeAddMagma α} :
pure f <*> x = f <$> x
@[simp]
theorem FreeMagma.mul_seq {α β : Type u} {f g : FreeMagma (αβ)} {x : FreeMagma α} :
f * g <*> x = (f <*> x) * (g <*> x)
@[simp]
theorem FreeAddMagma.add_seq {α β : Type u} {f g : FreeAddMagma (αβ)} {x : FreeAddMagma α} :
f + g <*> x = (f <*> x) + (g <*> x)
def FreeMagma.traverse {m : Type u → Type u} [Applicative m] {α β : Type u} (F : αm β) :
FreeMagma αm (FreeMagma β)

FreeMagma is traversable.

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

FreeAddMagma is traversable.

Equations
@[simp]
theorem FreeMagma.traverse_pure {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : α) :
traverse F (pure x) = pure <$> F x
@[simp]
theorem FreeAddMagma.traverse_pure {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : α) :
traverse F (pure x) = pure <$> F x
@[simp]
theorem FreeMagma.traverse_pure' {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) :
traverse F pure = fun (x : α) => pure <$> F x
@[simp]
theorem FreeAddMagma.traverse_pure' {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) :
traverse F pure = fun (x : α) => pure <$> F x
@[simp]
theorem FreeMagma.traverse_mul {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x y : FreeMagma α) :
traverse F (x * y) = (fun (x1 x2 : FreeMagma β) => x1 * x2) <$> traverse F x <*> traverse F y
@[simp]
theorem FreeAddMagma.traverse_add {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x y : FreeAddMagma α) :
traverse F (x + y) = (fun (x1 x2 : FreeAddMagma β) => x1 + x2) <$> traverse F x <*> traverse F y
@[simp]
theorem FreeMagma.traverse_mul' {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) :
Function.comp (traverse F) HMul.hMul = fun (x y : FreeMagma α) => (fun (x1 x2 : FreeMagma β) => x1 * x2) <$> traverse F x <*> traverse F y
@[simp]
theorem FreeAddMagma.traverse_add' {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) :
Function.comp (traverse F) HAdd.hAdd = fun (x y : FreeAddMagma α) => (fun (x1 x2 : FreeAddMagma β) => x1 + x2) <$> traverse F x <*> traverse F y
@[simp]
theorem FreeMagma.traverse_eq {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : FreeMagma α) :
@[simp]
theorem FreeAddMagma.traverse_eq {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : FreeAddMagma α) :
@[deprecated "Use map_pure and seq_pure" (since := "2025-05-21")]
theorem FreeMagma.mul_map_seq {α : Type u} (x y : FreeMagma α) :
(fun (x1 x2 : FreeMagma α) => x1 * x2) <$> x <*> y = x * y
@[deprecated "Use map_pure and seq_pure" (since := "2025-05-21")]
theorem FreeAddMagma.add_map_seq {α : Type u} (x y : FreeAddMagma α) :
(fun (x1 x2 : FreeAddMagma α) => x1 + x2) <$> x <*> y = x + y
def FreeMagma.repr {α : Type u} [Repr α] :

Representation of an element of a free magma.

Equations

Representation of an element of a free additive magma.

Equations
instance instReprFreeMagma {α : Type u} [Repr α] :
Equations
instance instReprFreeAddMagma {α : Type u} [Repr α] :
Equations
def FreeMagma.length {α : Type u} :
FreeMagma α

Length of an element of a free magma.

Equations

Length of an element of a free additive magma.

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

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

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

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

inductive AddMagma.AssocRel (α : Type u) [Add α] :
ααProp

Associativity relations for an additive magma.

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

Associativity relations for a magma.

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

Semigroup quotient of a magma.

Equations
def AddMagma.FreeAddSemigroup (α : Type u) [Add α] :

Additive semigroup quotient of an additive magma.

Equations
theorem Magma.AssocQuotient.quot_mk_assoc {α : Type u} [Mul α] (x y z : α) :
Quot.mk (AssocRel α) (x * y * z) = Quot.mk (AssocRel α) (x * (y * z))
theorem AddMagma.FreeAddSemigroup.quot_mk_assoc {α : Type u} [Add α] (x y z : α) :
Quot.mk (AssocRel α) (x + y + z) = Quot.mk (AssocRel α) (x + (y + z))
theorem Magma.AssocQuotient.quot_mk_assoc_left {α : Type u} [Mul α] (x y z w : α) :
Quot.mk (AssocRel α) (x * (y * z * w)) = Quot.mk (AssocRel α) (x * (y * (z * w)))
theorem AddMagma.FreeAddSemigroup.quot_mk_assoc_left {α : Type u} [Add α] (x y z w : α) :
Quot.mk (AssocRel α) (x + (y + z + w)) = Quot.mk (AssocRel α) (x + (y + (z + w)))
Equations
Equations
  • One or more equations did not get rendered due to their size.

Embedding from magma to its free semigroup.

Equations

Embedding from additive magma to its free additive semigroup.

Equations
theorem Magma.AssocQuotient.induction_on {α : Type u} [Mul α] {C : AssocQuotient αProp} (x : AssocQuotient α) (ih : ∀ (x : α), C (of x)) :
C x
theorem AddMagma.FreeAddSemigroup.induction_on {α : Type u} [Add α] {C : FreeAddSemigroup αProp} (x : FreeAddSemigroup α) (ih : ∀ (x : α), C (of x)) :
C x
theorem Magma.AssocQuotient.hom_ext {α : Type u} [Mul α] {β : Type v} [Semigroup β] {f g : AssocQuotient α →ₙ* β} (h : f.comp of = g.comp of) :
f = g
theorem AddMagma.FreeAddSemigroup.hom_ext {α : Type u} [Add α] {β : Type v} [AddSemigroup β] {f g : FreeAddSemigroup α →ₙ+ β} (h : f.comp of = g.comp of) :
f = g
theorem Magma.AssocQuotient.hom_ext_iff {α : Type u} [Mul α] {β : Type v} [Semigroup β] {f g : AssocQuotient α →ₙ* β} :
f = g f.comp of = g.comp of
theorem AddMagma.FreeAddSemigroup.hom_ext_iff {α : Type u} [Add α] {β : Type v} [AddSemigroup β] {f g : FreeAddSemigroup α →ₙ+ β} :
f = g f.comp of = g.comp of
def Magma.AssocQuotient.lift {α : Type u} [Mul α] {β : Type v} [Semigroup β] :

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.

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]
@[simp]
theorem Magma.AssocQuotient.lift_symm_apply {α : Type u} [Mul α] {β : Type v} [Semigroup β] (f : AssocQuotient α →ₙ* β) :
@[simp]
theorem Magma.AssocQuotient.lift_of {α : Type u} [Mul α] {β : Type v} [Semigroup β] (f : α →ₙ* β) (x : α) :
(lift f) (of x) = f x
@[simp]
theorem AddMagma.FreeAddSemigroup.lift_of {α : Type u} [Add α] {β : Type v} [AddSemigroup β] (f : α →ₙ+ β) (x : α) :
(lift f) (of x) = f x
@[simp]
theorem Magma.AssocQuotient.lift_comp_of {α : Type u} [Mul α] {β : Type v} [Semigroup β] (f : α →ₙ* β) :
(lift f).comp of = f
@[simp]
theorem AddMagma.FreeAddSemigroup.lift_comp_of {α : Type u} [Add α] {β : Type v} [AddSemigroup β] (f : α →ₙ+ β) :
(lift f).comp of = f
@[simp]
theorem Magma.AssocQuotient.lift_comp_of' {α : Type u} [Mul α] {β : Type v} [Semigroup β] (f : AssocQuotient α →ₙ* β) :
lift (f.comp of) = f
@[simp]
theorem AddMagma.FreeAddSemigroup.lift_comp_of' {α : Type u} [Add α] {β : Type v} [AddSemigroup β] (f : FreeAddSemigroup α →ₙ+ β) :
lift (f.comp of) = f
def Magma.AssocQuotient.map {α : Type u} [Mul α] {β : Type v} [Mul β] (f : α →ₙ* β) :

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

Equations

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

Equations
@[simp]
theorem Magma.AssocQuotient.map_of {α : Type u} [Mul α] {β : Type v} [Mul β] (f : α →ₙ* β) (x : α) :
(map f) (of x) = of (f x)
@[simp]
theorem AddMagma.FreeAddSemigroup.map_of {α : Type u} [Add α] {β : Type v} [Add β] (f : α →ₙ+ β) (x : α) :
(map f) (of x) = of (f x)
structure FreeAddSemigroup (α : Type u) :

If α is a type, then FreeAddSemigroup α is the free additive semigroup generated by α. This is an additive semigroup equipped with a function FreeAddSemigroup.of : α → FreeAddSemigroup α which has the following universal property: if M is any additive semigroup, and f : α → M is any function, then this function is the composite of FreeAddSemigroup.of and a unique semigroup homomorphism FreeAddSemigroup.lift f : FreeAddSemigroup α →ₙ+ M.

A typical element of FreeAddSemigroup α is a nonempty formal sum of elements of α. For example if x and y are terms of type α then x + y + y + x is a "typical" element of FreeAddSemigroup α. In particular if α is empty then FreeAddSemigroup α is also empty, and if α has one term then FreeAddSemigroup α is isomorphic to ℕ+. If α has two or more terms then FreeAddSemigroup α is not commutative. One can think of FreeAddSemigroup α as the type of nonempty lists of α, with addition given by concatenation.

  • head : α

    The head of the element

  • tail : List α

    The tail of the element

structure FreeSemigroup (α : Type u) :

If α is a type, then FreeSemigroup α is the free semigroup generated by α. This is a semigroup equipped with a function FreeSemigroup.of : α → FreeSemigroup α which has the following universal property: if M is any semigroup, and f : α → M is any function, then this function is the composite of FreeSemigroup.of and a unique semigroup homomorphism FreeSemigroup.lift f : FreeSemigroup α →ₙ* M.

A typical element of FreeSemigroup α is a nonempty formal product of elements of α. For example if x and y are terms of type α then x * y * y * x is a "typical" element of FreeSemigroup α. In particular if α is empty then FreeSemigroup α is also empty, and if α has one term then FreeSemigroup α is isomorphic to Multiplicative ℕ+. If α has two or more terms then FreeSemigroup α is not commutative. One can think of FreeSemigroup α as the type of nonempty lists of α, with multiplication given by concatenation.

  • head : α

    The head of the element

  • tail : List α

    The tail of the element

theorem FreeAddSemigroup.ext {α : Type u} {x y : FreeAddSemigroup α} (head : x.head = y.head) (tail : x.tail = y.tail) :
x = y
theorem FreeSemigroup.ext_iff {α : Type u} {x y : FreeSemigroup α} :
x = y x.head = y.head x.tail = y.tail
theorem FreeAddSemigroup.ext_iff {α : Type u} {x y : FreeAddSemigroup α} :
x = y x.head = y.head x.tail = y.tail
theorem FreeSemigroup.ext {α : Type u} {x y : FreeSemigroup α} (head : x.head = y.head) (tail : x.tail = y.tail) :
x = y
Equations
Equations
@[simp]
theorem FreeSemigroup.head_mul {α : Type u} (x y : FreeSemigroup α) :
(x * y).head = x.head
@[simp]
theorem FreeAddSemigroup.head_add {α : Type u} (x y : FreeAddSemigroup α) :
(x + y).head = x.head
@[simp]
theorem FreeSemigroup.tail_mul {α : Type u} (x y : FreeSemigroup α) :
(x * y).tail = x.tail ++ y.head :: y.tail
@[simp]
theorem FreeAddSemigroup.tail_add {α : Type u} (x y : FreeAddSemigroup α) :
(x + y).tail = x.tail ++ y.head :: y.tail
@[simp]
theorem FreeSemigroup.mk_mul_mk {α : Type u} (x y : α) (L1 L2 : List α) :
{ head := x, tail := L1 } * { head := y, tail := L2 } = { head := x, tail := L1 ++ y :: L2 }
@[simp]
theorem FreeAddSemigroup.mk_add_mk {α : Type u} (x y : α) (L1 L2 : List α) :
{ head := x, tail := L1 } + { head := y, tail := L2 } = { head := x, tail := L1 ++ y :: L2 }
def FreeSemigroup.of {α : Type u} (x : α) :

The embedding α → FreeSemigroup α.

Equations
def FreeAddSemigroup.of {α : Type u} (x : α) :

The embedding α → FreeAddSemigroup α.

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

Length of an element of free semigroup.

Equations

Length of an element of free additive semigroup

Equations
@[simp]
theorem FreeSemigroup.length_mul {α : Type u} (x y : FreeSemigroup α) :
(x * y).length = x.length + y.length
@[simp]
theorem FreeAddSemigroup.length_add {α : Type u} (x y : FreeAddSemigroup α) :
(x + y).length = x.length + y.length
@[simp]
theorem FreeSemigroup.length_of {α : Type u} (x : α) :
(of x).length = 1
@[simp]
theorem FreeAddSemigroup.length_of {α : Type u} (x : α) :
(of x).length = 1
def FreeSemigroup.recOnMul {α : Type u} {C : FreeSemigroup αSort l} (x : FreeSemigroup α) (ih1 : (x : α) → C (of x)) (ih2 : (x : α) → (y : FreeSemigroup α) → C (of x)C yC (of x * y)) :
C x

Recursor for free semigroup using of and *.

Equations
  • One or more equations did not get rendered due to their size.
def FreeAddSemigroup.recOnAdd {α : Type u} {C : FreeAddSemigroup αSort l} (x : FreeAddSemigroup α) (ih1 : (x : α) → C (of x)) (ih2 : (x : α) → (y : FreeAddSemigroup α) → C (of x)C yC (of x + y)) :
C x

Recursor for free additive semigroup using of and +.

Equations
  • One or more equations did not get rendered due to their size.
theorem FreeSemigroup.hom_ext {α : Type u} {β : Type v} [Mul β] {f g : FreeSemigroup α →ₙ* β} (h : f of = g of) :
f = g
theorem FreeAddSemigroup.hom_ext {α : Type u} {β : Type v} [Add β] {f g : FreeAddSemigroup α →ₙ+ β} (h : f of = g of) :
f = g
theorem FreeSemigroup.hom_ext_iff {α : Type u} {β : Type v} [Mul β] {f g : FreeSemigroup α →ₙ* β} :
f = g f of = g of
theorem FreeAddSemigroup.hom_ext_iff {α : Type u} {β : Type v} [Add β] {f g : FreeAddSemigroup α →ₙ+ β} :
f = g f of = g of
def FreeSemigroup.lift {α : Type u} {β : Type v} [Semigroup β] :
(αβ) (FreeSemigroup α →ₙ* β)

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

Equations
  • One or more equations did not get rendered due to their size.
def FreeAddSemigroup.lift {α : Type u} {β : Type v} [AddSemigroup β] :
(αβ) (FreeAddSemigroup α →ₙ+ β)

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.
@[simp]
theorem FreeSemigroup.lift_symm_apply {α : Type u} {β : Type v} [Semigroup β] (f : FreeSemigroup α →ₙ* β) (a✝ : α) :
lift.symm f a✝ = (f of) a✝
@[simp]
theorem FreeAddSemigroup.lift_symm_apply {α : Type u} {β : Type v} [AddSemigroup β] (f : FreeAddSemigroup α →ₙ+ β) (a✝ : α) :
lift.symm f a✝ = (f of) a✝
@[simp]
theorem FreeSemigroup.lift_of {α : Type u} {β : Type v} [Semigroup β] (f : αβ) (x : α) :
(lift f) (of x) = f x
@[simp]
theorem FreeAddSemigroup.lift_of {α : Type u} {β : Type v} [AddSemigroup β] (f : αβ) (x : α) :
(lift f) (of x) = f x
@[simp]
theorem FreeSemigroup.lift_comp_of {α : Type u} {β : Type v} [Semigroup β] (f : αβ) :
(lift f) of = f
@[simp]
theorem FreeAddSemigroup.lift_comp_of {α : Type u} {β : Type v} [AddSemigroup β] (f : αβ) :
(lift f) of = f
@[simp]
theorem FreeSemigroup.lift_comp_of' {α : Type u} {β : Type v} [Semigroup β] (f : FreeSemigroup α →ₙ* β) :
lift (f of) = f
@[simp]
theorem FreeAddSemigroup.lift_comp_of' {α : Type u} {β : Type v} [AddSemigroup β] (f : FreeAddSemigroup α →ₙ+ β) :
lift (f of) = f
theorem FreeSemigroup.lift_of_mul {α : Type u} {β : Type v} [Semigroup β] (f : αβ) (x : α) (y : FreeSemigroup α) :
(lift f) (of x * y) = f x * (lift f) y
theorem FreeAddSemigroup.lift_of_add {α : Type u} {β : Type v} [AddSemigroup β] (f : αβ) (x : α) (y : FreeAddSemigroup α) :
(lift f) (of x + y) = f x + (lift f) y
def FreeSemigroup.map {α : Type u} {β : Type v} (f : αβ) :

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

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

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

Equations
@[simp]
theorem FreeSemigroup.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
(map f) (of x) = of (f x)
@[simp]
theorem FreeAddSemigroup.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
(map f) (of x) = of (f x)
@[simp]
theorem FreeSemigroup.length_map {α : Type u} {β : Type v} (f : αβ) (x : FreeSemigroup α) :
((map f) x).length = x.length
@[simp]
theorem FreeAddSemigroup.length_map {α : Type u} {β : Type v} (f : αβ) (x : FreeAddSemigroup α) :
((map f) x).length = x.length
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 FreeSemigroup.recOnPure {α : Type u} {C : FreeSemigroup αSort l} (x : FreeSemigroup α) (ih1 : (x : α) → C (pure x)) (ih2 : (x : α) → (y : FreeSemigroup α) → C (pure x)C yC (pure x * y)) :
C x

Recursor that uses pure instead of of.

Equations
def FreeAddSemigroup.recOnPure {α : Type u} {C : FreeAddSemigroup αSort l} (x : FreeAddSemigroup α) (ih1 : (x : α) → C (pure x)) (ih2 : (x : α) → (y : FreeAddSemigroup α) → C (pure x)C yC (pure x + y)) :
C x

Recursor that uses pure instead of of.

Equations
@[simp]
theorem FreeSemigroup.map_pure {α β : Type u} (f : αβ) (x : α) :
f <$> pure x = pure (f x)
@[simp]
theorem FreeAddSemigroup.map_pure {α β : Type u} (f : αβ) (x : α) :
f <$> pure x = pure (f x)
@[simp]
theorem FreeSemigroup.map_mul' {α β : Type u} (f : αβ) (x y : FreeSemigroup α) :
f <$> (x * y) = f <$> x * f <$> y
@[simp]
theorem FreeAddSemigroup.map_add' {α β : Type u} (f : αβ) (x y : FreeAddSemigroup α) :
f <$> (x + y) = f <$> x + f <$> y
@[simp]
theorem FreeSemigroup.pure_bind {α β : Type u} (f : αFreeSemigroup β) (x : α) :
pure x >>= f = f x
@[simp]
theorem FreeAddSemigroup.pure_bind {α β : Type u} (f : αFreeAddSemigroup β) (x : α) :
pure x >>= f = f x
@[simp]
theorem FreeSemigroup.mul_bind {α β : Type u} (f : αFreeSemigroup β) (x y : FreeSemigroup α) :
x * y >>= f = (x >>= f) * (y >>= f)
@[simp]
theorem FreeAddSemigroup.add_bind {α β : Type u} (f : αFreeAddSemigroup β) (x y : FreeAddSemigroup α) :
x + y >>= f = (x >>= f) + (y >>= f)
@[simp]
theorem FreeSemigroup.pure_seq {α β : Type u} {f : αβ} {x : FreeSemigroup α} :
pure f <*> x = f <$> x
@[simp]
theorem FreeAddSemigroup.pure_seq {α β : Type u} {f : αβ} {x : FreeAddSemigroup α} :
pure f <*> x = f <$> x
@[simp]
theorem FreeSemigroup.mul_seq {α β : Type u} {f g : FreeSemigroup (αβ)} {x : FreeSemigroup α} :
f * g <*> x = (f <*> x) * (g <*> x)
@[simp]
theorem FreeAddSemigroup.add_seq {α β : Type u} {f g : FreeAddSemigroup (αβ)} {x : FreeAddSemigroup α} :
f + g <*> x = (f <*> x) + (g <*> x)
def FreeSemigroup.traverse {m : Type u → Type u} [Applicative m] {α β : Type u} (F : αm β) (x : FreeSemigroup α) :

FreeSemigroup is traversable.

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

FreeAddSemigroup is traversable.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem FreeSemigroup.traverse_pure {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : α) :
traverse F (pure x) = pure <$> F x
@[simp]
theorem FreeAddSemigroup.traverse_pure {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : α) :
traverse F (pure x) = pure <$> F x
@[simp]
theorem FreeSemigroup.traverse_pure' {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) :
traverse F pure = fun (x : α) => pure <$> F x
@[simp]
theorem FreeAddSemigroup.traverse_pure' {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) :
traverse F pure = fun (x : α) => pure <$> F x
@[simp]
theorem FreeSemigroup.traverse_mul {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) [LawfulApplicative m] (x y : FreeSemigroup α) :
traverse F (x * y) = (fun (x1 x2 : FreeSemigroup β) => x1 * x2) <$> traverse F x <*> traverse F y
@[simp]
theorem FreeAddSemigroup.traverse_add {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) [LawfulApplicative m] (x y : FreeAddSemigroup α) :
traverse F (x + y) = (fun (x1 x2 : FreeAddSemigroup β) => x1 + x2) <$> traverse F x <*> traverse F y
@[simp]
theorem FreeSemigroup.traverse_mul' {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) [LawfulApplicative m] :
Function.comp (traverse F) HMul.hMul = fun (x y : FreeSemigroup α) => (fun (x1 x2 : FreeSemigroup β) => x1 * x2) <$> traverse F x <*> traverse F y
@[simp]
theorem FreeAddSemigroup.traverse_add' {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) [LawfulApplicative m] :
Function.comp (traverse F) HAdd.hAdd = fun (x y : FreeAddSemigroup α) => (fun (x1 x2 : FreeAddSemigroup β) => x1 + x2) <$> traverse F x <*> traverse F y
@[simp]
theorem FreeSemigroup.traverse_eq {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : FreeSemigroup α) :
@[simp]
theorem FreeAddSemigroup.traverse_eq {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : FreeAddSemigroup α) :
@[deprecated "Use map_pure and seq_pure" (since := "2025-05-21")]
theorem FreeSemigroup.mul_map_seq {α : Type u} (x y : FreeSemigroup α) :
(fun (x1 x2 : FreeSemigroup α) => x1 * x2) <$> x <*> y = x * y
@[deprecated "Use map_pure and seq_pure" (since := "2025-05-21")]
theorem FreeAddSemigroup.add_map_seq {α : Type u} (x y : FreeAddSemigroup α) :
(fun (x1 x2 : FreeAddSemigroup α) => x1 + x2) <$> x <*> y = x + y
Equations
Equations
theorem FreeMagma.toFreeSemigroup_map {α : Type u} {β : Type v} (f : αβ) (x : FreeMagma α) :