A bit of univeral algebra
We will need some basic universal algebra for todays constructions. Intuitively what we are doing capturing classes of structures given by operations and equations they must satisfy, such as groups, rings and monoids.
We consider a signature of operation symbols. The elements of the signature are operation symbols, each with a specified arity in the natural numbers. Given a signature, and a set of variables
, the set of
–terms is defined inductively as follows:
- Each
is a term.
- If
are terms, and
has arity
, then
is a term.
We will generalize this notation to allow infix application of operations, writing rather than
when it is clearer to do so.
A –algebra consists of:
- A set
, the universe.
- For each
of arity
, a function
.
-algebras form a category
, with morphisms functions
between algebra universes, such that for every
:
.
For each term with variables in
, and variable assignment
, we define the interpretation of
in
, denoted
, as follows:
- If
is a variable
, then
.
- If
, then
.
For a fixed , a set of formal equations
is a set of pairs of terms over some set of variables
. A pair
is referred to as an equational presentation for a class of algebras. A
-algebra is a
-algebra such that for each
and variable assignment
:
Example: A monoid is a -algebra where
and
. Here,
has arity 0 (is a constant), and
has arity
(is a binary operation). A morphism of
-algebras is then a monoid morphism.
The category , of
-algebras, is the obvious full subcategory of
.
Back to adjunctions and monads
We now have enough abstract machinery in place to return to our efforts to construct monads. For an equational presentation , there is a forgetful functor
sending an algebra to its underlying universe. The key fact that we need is that this forgetful functor always has a left adjoint
which is also relatively easy to describe. is called the free algebra on
. For a set
, the universe of
is the set of terms with variables in
, quotiented by provable equality in equational logic, from the equations in
. In general, describing these equivalence classes may be extremely difficult, although is manageable in many examples of interest. Writing
for the equivalence class containing
, for an algebra
, and function
, we define
inductively on representatives as follows:
.
.
With this in place, we see that every equational presentation induces a monad
, with:
- Endofunctor:
is the set of equivalence classes of terms.
- Unit: The unit maps variables to their equivalence classes
.
- Multiplication: The multiplication is a flattening operation on nested equivalence classes. Formally,
.
The multiplication is probably easier to follow from an example.
Example: Returning to the equational presentation of monoids above, an example of the multiplication would be .
Any choice of operations and equations then produces a monad on the category , yielding boundless examples.
Example: There are monads on induced by the equational presentations of monoids, commutative monoids, groups, Abelian groups, rings, join semilattices, semigroups…
The monads that arise from equational presentations are known as the finitary monads. We may return to the question of exactly what that means in a future post. Possibly more important to note is that if we consider sufficiently liberal generalizations of the arities in our equational presentations, every monad can be described in such a way.
One thought on “Monads via Algebra”