The Relative Monad Eilenberg-Moore Construction

In previous posts, we have seen that relative adjunctions induce relative monads, and in fact every relative monad arises in this way via a Kleisli construction. The Kleisli construction is the initial adjunction that induces a given relative monad. In this post, we are going to look at an Eilenberg-Moore construction that yields a terminal resolution of every relative monad.

As relative monads are described as a variant of Kleisli triples, this made describing the Kleisli construction very straightforward. Unfortunately, this formulation will make the Eilenberg-Moore construction a little bit fiddlier.

Algebras of a Relative Monad

For a $J : \mathcal{C} \rightarrow \mathcal{D}$ -relative monad $(\mathbb{T},\eta,(-)^*)$ , an Eilenberg-Moore algebra consists of:

A carrier $\mathcal{D}$ -object $A$ .
For every $\mathcal{C}$ -object $X$ and $\mathcal{D}$ -morphism $v : J(X) \rightarrow A$ , a morphism $\alpha(v) : \mathbb{T}(X) \rightarrow A$ .

These must satisfy the following axioms:

For every $\mathcal{C}$ -object $X$ and $v : J(X) \rightarrow A$ , $v = \alpha(v) \cdot \eta_Z$ .
For every pair of $\mathcal{C}$ -objects $X$ and $Y$ , $\mathcal{C}$ -object $s : J(X) \rightarrow \mathbb{T}(Y)$ and $v : J(Y) \rightarrow A$ , $\alpha (\alpha(v) \cdot s) = \alpha(v) \cdot s^*$ .

A morphism of Eilenberg-Moore algebras of type $(A,\alpha) \rightarrow (B, \beta)$ is a $\mathcal{D}$ -morphism $h : A \rightarrow B$ such that for every $\mathcal{D}$ -morphism $v : J(Z) \rightarrow A$ :

$h \cdot \alpha(v) = \beta(h \cdot v)$

These form a category $\mathbf{EM}(\mathbb{T})$ , the Eilenberg-Moore category.

Compared to the definition of the Kleisli category for a relative monad, the Eilenberg-Moore category is rather cumbersome. To get some intuition for what is going on, we will look at a particular example in some detail. As suggested by the term Eilenberg-Moore algebra, we we consider an algebraic example.

Recall that a monoid is a structure with a binary operation, which we will write as $\times$ , and a unit, denoted $1$ , satisfying the following three equations:

Left unit: $1 \times x = x$ .
Right unit: $x \times 1 = x$ .
Associativity: $x \times (y \times z) = (x \times y) \times z$ .

Given a set $X$ , we can form the set of equivalence classes of terms built up from multiplication, the unit and variables. Terms are considered equivalent if they are provably equal in equational logic from the axioms of a monoid. For example

$1, 1 \times x, x \times 1, x \times (1 \times 1), x \times y, \ldots$

are all terms, and the first four are provably equal. Only finitely many variables may appear in any given term, but the collection of equivalence classes of terms over a finite set is infinite. For example, even if we have just one variable $x$ , non of the following terms can be proved equal:

$x, x \times x, x \times (x \times x), x \times (x \times (x \times x)), \ldots$

This suggests we consider the functor $J : \mathsf{FinSet} \rightarrow \mathsf{Set}$ including the finite sets into the infinite sets, relating the finite and infinite aspects at play. For any finite set $X$ , we can then take $\mathbb{T}(X)$ to be the equivalence class of terms over $X$ . There is an obvious function:

$\eta_X : J(X) \rightarrow \mathbb{T}(X)$

picking out the equivalence class of each variable in $J(X)$ . Finally, we can think of a function

$f : J(X) \rightarrow \mathbb{T}(Y)$

as specifying a family of equivalence classes of terms over the set finite $Y$ , indexed by the finite set $X$ . Informally, the extension

$f^* : \mathbb{T}(X) \rightarrow \mathbb{T}(Y)$

is a substitution operation, taking equivalence classes of terms over $X$ to those over $Y$ , replacing variables as specified by $f$ . This data together forms a $J$ -relative monad $(\mathbb{T},\eta,(-)^*)$ .

Remark: The relative monad we have just described is the one induced from the ordinary list monad. This is unsurprising as the list monad is the free monoid monad.

A monoid consists of a carrier set $A$ and a choice of:

A function $\times^A : A \times A \rightarrow A$ telling us how the binary operation behaves.
A constant $1^A \in A$ specifying the value of the unit.

Given a term such as

$x \times y \times 1$

and a monoid $(A, \times^A, 1^A)$ , we can evaluate this term to an element of the carrier using the specified multiplication operation and unit constant, if we are given an element in the carrier for each of the variables. In fact, we should get the same value for any term provably equal to this one such as

$x \times y$

Therefore, for any valuation, $v : J(X) \rightarrow A$ , a monoid allows us to build a function

$\alpha(v) : \mathbb{T}(X) \rightarrow A$

which inductively evaluates terms over the same finite set, using the valuation to assign values to the unknowns. This function has some nice properties. Firstly, if a term is the equivalence class of a variable, it will return the value assigned to that variable. This is captured by the equation:

$\alpha(v) \cdot \eta_X = v$

Secondly, it respects the compositional structure of terms. We can think of a function $s : J(X) \rightarrow \mathbb{T}(Y)$ as specifying a substitution, which allows us to build a “bigger” $\mathbb{T}(Y)$ term from a $\mathbb{T}(X)$ term, by using the substitution to replace all the variables with terms over $Y$ . Our evaluation function $\alpha$ builds up results inductively, so we can either evaluate subterms, and then combine them, or evaluate an entire composite term, and we get the same result. This intuition is encoded in the equation:

$\alpha (\alpha(v) \cdot s) = \alpha(v) \cdot s^*$

From the discussion above, a monoid induces an Eilenberg-Moore algebra. In fact, the two axioms forcing good behaviour in terms of variables and compositional structure mean that every Eilenberg-Moore algebra encodes the structure of a monoid. This is similar to how the good behaviour of the Eilenberg-Moore algebras of an ordinary monad was encoded in the unit and multiplication axioms they are required to satisfying. A bit more work shows that the morphisms in the Eilenberg-Moore category correspond to monoid morphisms, so the Eilenberg-Moore category is actually the category of monoids.

Remark: The Eilenberg-Moore algebras may have infinite carriers, despite the fact the terms and valuations are built up from finite sets of variables.

From this example, our intuitions for an Eilenberg-Moore algebra should be:

The carrier is the carrier of some algebraic object.
The elements of $\mathbb{T}(X)$ can be thought of as terms over some object of variables.
$\alpha(v)$ tells us how to evaluate such terms, with the valuation $v$ specifying the values of the variables.
The axioms specify that the operation $\alpha(v)$ must evaluate terms in an inductive manner, built up from the variables in a compositional manner, using a fixed interpretation for each of the operations.

There is nothing in the above discussion which is specific to monoids. We can choose any algebraic structure presented by finite operations and a set of equations, and the class of models will emerge as the Eilenberg-Moore category of the corresponding $J$ -relative monad.

The Eilenberg-Moore Resolution

For $J : \mathcal{C} \rightarrow \mathcal{D}$ , and $J$ -relative monad $(\mathbb{T},\eta,(-)^*)$ , there is an obvious forgetful functor:

$U^{\mathbb{T}} : \mathbf{EM}(\mathbb{T}) \rightarrow \mathcal{D}$ .

sending an algebra to its carrier. There is also a functor

$F^{\mathbb{T}} : \mathcal{C} \rightarrow \mathbf{EM}(\mathbb{T})$ ,

such that $F^{\mathbb{T}}(X)$ has universe $\mathbb{T}(X)$ , and for $v : J(W) \rightarrow X$ :

$\alpha(v) = v^*$

On morphisms:

$F^{\mathbb{T}}(f) = \mathbb{T}(f)$ .

In fact, $F^{\mathbb{T}}$ is $J$ -relative left adjoint to $U^{\mathbb{T}}$ , and is the terminal resolution of the original relative monad $\mathbb{T}$ .

Conclusion

It is satisfying given the apparently slightly ad-hoc formulation of relative monad that a satisfactory connection with adjunctions emerges. We get two canonical resolutions, the initial Kleisli resolution and the terminal Eilenberg-Moore resolution, exactly as we did in the world of ordinary monad theory.

Our main example was from universal algebra. The relative monad structure allowed us to separate out finitary concerns about variables from infinitary aspects involving the carriers of algebras. This was not directly possible in the ordinary monadic setting, as the restriction to endofunctors forces “all the bookkeeping to happen in the same place”.

Further reading: The Eilenberg-Moore construction is introduced in the original “Monads need not be endofunctors” paper, which as usual is recommended reading.

Algebras of a Relative Monad

The Eilenberg-Moore Resolution

Conclusion

Share this:

Related

Leave a comment Cancel reply