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
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
lift_apply, and we mark
irreducible once we have established the universal property.
free algebra, non-unital, non-associative, free magma, magma algebra, universal property, forgetful functor, adjoint functor
If the coefficients are commutative amongst themselves, they also commute with the algebra multiplication.
X ↦ free_non_unital_non_assoc_algebra 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