We shall now start to explore one of the two categories that accompany every monad. The second construction, the Kleisli category, will follow shortly after.
For a monad on category , an Eilenberg-Moore algebra is a -object , and a -morphism , satisfying the following two axioms:
- Unit axiom: .
- Multiplication axiom: .
A morphism of Eilenberg-Moore algebras is a -morphism such that . Eilenberg-Moore algebras and their morphisms form a category, the Eilenberg-Moore category, denoted . Composition and identities are as in .
To get some intuition for this definition, lets assume that the monad is given by an equational presentation, with a signature consisting of a single binary operation , and no equations. For a set , consists of terms built up from elements of by repeated applying the operation . For example, the following are all terms:
A function can be seen as a way of evaluating a term built up of elements of , to yield a new element. If we consider the unit axiom, it is equivalent to requiring:
That is, bare variables are evaluated to themselves.
To see what the multiplication axiom means, we must first introduce a bit of notation for substitution. If is a term, we shall write for the term resulting from substituting for each occurrence of in . For example:
We shall also write a shorthand for multiple simultaneous substitutions, when it is well-defined to do so. For example if and , then:
The multiplication axiom is then equivalent to requiring:
So evaluating a composite term can be broken up into evaluating sub-terms and then evaluating the parent term to combine the results. For example, we must have:
These two axioms force to behave exactly as if it had picked a binary function , and then evaluates all terms by recursively applying in the obvious way.
For our example, we only required the set of equations to be empty to avoid lots of distracting equivalence class brackets everywhere. For a general equational presentation , the axioms again force that the Eilenberg-Moore algebras must evaluate by recursively applying fixed functions for each operation symbol. The quotient by provable equality simply forces that terms that are provably equal syntactically are evaluated to the same value.
Example: For the list monad, an Eilenberg-Moore algebra on is a function such that
Example: For a closure operator , the Eilenberg-Moore algebras are elements such that . The two axioms are trivial in this case. As every closure operator has , by irreflexivity, the Eilenberg-Moore algebras can be identified with the elements of the form , the closed elements of .