Free algebras #
Given a semiring R
and a type X
, we construct the free non-unital, non-associative algebra on
X
with coefficients in R
, together with its universal property. The construction is valuable
because it can be used to build free algebras with more structure, e.g., free Lie algebras.
Note that elsewhere we have a construction of the free unital, associative algebra. This is called
FreeAlgebra
.
Main definitions #
Implementation details #
We construct the free algebra as the magma algebra, with coefficients in R
, of the free magma on
X
. However we regard this as an implementation detail and thus deliberately omit the lemmas
of_apply
and lift_apply
, and we mark FreeNonUnitalNonAssocAlgebra
and lift
as
irreducible once we have established the universal property.
Tags #
free algebra, non-unital, non-associative, free magma, magma algebra, universal property, forgetful functor, adjoint functor
If α
is a type, and R
is a semiring, then FreeNonUnitalNonAssocAlgebra R α
is the free
non-unital non-associative R
-algebra generated by α
.
This is an R
-algebra equipped with a function
FreeNonUnitalNonAssocAlgebra.of R : α → FreeNonUnitalNonAssocAlgebra R α
which has
the following universal property: if A
is any R
-algebra, and f : α → A
is any function,
then this function is the composite of FreeNonUnitalNonAssocAlgebra.of R
and a unique non-unital R
-algebra homomorphism
FreeNonUnitalNonAssocAlgebra.lift R f : FreeNonUnitalNonAssocAlgebra R α →ₙₐ[R] A
.
A typical element of FreeNonUnitalNonAssocAlgebra R α
is an R
-linear combination of
nonempty formal (non-commutative, non-associative) products of elements of α
.
For example if x
and y
are terms of type α
and
a
, b
are terms of type R
then (3 * a * a) • (x * (y * x)) + (2 * b + 1) • (y * x)
is a
"typical" element of FreeNonUnitalNonAssocAlgebra R α
.
Equations
- FreeNonUnitalNonAssocAlgebra R X = MonoidAlgebra R (FreeMagma X)
Instances For
The embedding of X
into the free algebra with coefficients in R
.
Equations
Instances For
The functor X ↦ FreeNonUnitalNonAssocAlgebra R X
from the category of types to the
category of non-unital, non-associative algebras over R
is adjoint to the forgetful functor in the
other direction.