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.