In recent posts, we have encountered Kan extensions and the codensity monad, and explored some basic aspects of formal monad theory. This lead to a representation result, relating monad morphisms with domain a codensity monad, and monad actions. Todays post will continue those themes, yielding yet another approach to building and moving monads around.

Transferring Monads

We will work in terms of formal monad theory, in a 2-category $\mathcal{C}$ . This is primarily to show that very little structure is actually need for the result to go through, and will require no complicated background. Readers that want to keep things a bit more concrete can think of $\mathcal{C}$ as the 2-category of categories, functors and natural transformations.

If we have a monad $(\mathbb{T}, \eta, \mu)$ on some 0-cell $\mathcal{A}$ , and a 1-cell

$\mathcal{A} \xrightarrow{F} \mathcal{B}$ ,

the question we would like to solve can we transfer the monad $\mathbb{T}$ along $F$ , to give a monad on $\mathcal{B}$ ? Obviously this is a rather imprecise specification, lets explore some possibilities.

We could assume that the right extension of $F$ along itself exists:

$\mathsf{Ran}_F(F) : \mathcal{B} \rightarrow \mathcal{B}$ ,

and this will induce a codensity monad on $\mathcal{B}$ . This isn’t really in the spirit of the question though, as we have completely ignored the monad $\mathbb{T}$ in our construction. So we consider this approach to be unsatisfactory, as would be other trivial solutions, such as simply taking the identity monad on $\mathcal{B}$ .

To get the monad $\mathbb{T}$ into the game, we modify our previous plan, and consider the right extension of $F \circ \mathbb{T}$ along $F$ .

$\mathsf{Ran}_F(F \circ \mathbb{T}) : \mathcal{B} \rightarrow \mathcal{B}$ .

It turns out that this 1-cell carries a unique monad structure such that the universal 2-cell

$\mathsf{run} : \mathsf{Ran}_{F}(F \circ \mathbb{T}) \circ F \Rightarrow F \circ \mathbb{T}$

is an Eilenberg-Moore law. Our aim now is to use this extra criterion to deduce the required unit and multiplication.

The universal property of the required right extension can equivalently be written for all $\alpha H \circ F \Rightarrow F \circ \mathbb{T}$ and $\beta : H \Rightarrow \mathsf{Ran}_F(F \circ \mathbb{T})$ :

$\alpha = \mathsf{run} \cdot (\beta \circ F) \;\Leftrightarrow\; \hat{\alpha} = \beta$

This formulation is useful as the two axioms of an Eilenberg-Moore law require that a pair of equations must hold, and the equivalence allows us to deduce further equations. Defining $\mathbb{S} := \mathsf{Ran}_{F}(F \circ \mathbb{T})$ to simplify notation, we find that:

Plugging in the unit preservation axiom into the left hand side of the right extension universal property, the unit of the monad on $\mathcal{B}$ must be $\widehat{(F \circ \eta)} : \mathsf{Id} \Rightarrow \mathbb{S}$ .
Plugging in the multiplication preservation axiom into the left hand side of the right extension universal property, we find that the multiplication must be $\widehat{\mu \cdot (\mathsf{run} \circ \mathbb{S}) \cdot (\mathbb{S} \circ \mathsf{run})} : \mathbb{S} \circ \mathbb{S} \Rightarrow \mathbb{S}$ .

So there are unique choices of potential unit and multiplication for the resulting monad. It is then a routine calculation using the properties of extensions and the monad $\mathbb{T}$ to show that the monad axioms are satisfied.

So we have found a construction that given a monad on a 0-cell $\mathcal{A}$ , and a 1-cell $F : \mathcal{A} \rightarrow \mathcal{B}$ , such that the right extension $\mathsf{Ran}_F(F \circ \mathbb{T})$ exists, there is a canonical monad induced on $\mathcal{B}$ . We refer to this construction as the codensity monad transformer.

Example: If we take the monad $\mathbb{T}$ in this construction to be the identity monad, we recover ordinary codensity monad as a special case.

We saw a similar construction, building a new monad from a parameter monad and some additional data, in a an earlier post. There, given a monad $\mathbb{T}$ on $\mathcal{A}$ , and an adjunction $L \dashv R : \mathcal{A} \rightarrow \mathcal{B}$ , the composite $R \circ \mathbb{T} \circ L$ is a monad on $\mathcal{B}$ . This result is known as Huber’s construction.

Conclusion

This result is mentioned in Street’s “Formal Theory of Monads”, although not as a theorem in that paper. Presumably the result was well known before that, although I am currently unaware of an original source, and would welcome further information.

As we worked formally in terms of an arbitrary 2-category, we see that the codensity monad transformer does not hinge on anything specific to categories, functors and natural transformations, or specific right Kan extension constructions in terms of certain limits. From this perspective, once you are comfortable with it, the abstraction of working formally actually simplifies the analysis as it removes irrelevant structure and other distracting details.

Further reading: The calculations to verify this result might be somewhat intimidating to readers new to (or less comfortable with) Kan extensions, although they are in principle quite simple. I would recommend using the graphical notation introduced in my co-author Ralf Hinze’s paper “Kan Extensions for Program Optimisation Or: Art and Dan Explain an Old Trick”. This notation might take a little bit of getting used to, but once digested I find it takes a lot of the pain out of reasoning with Kan extensions.

The Codensity Monad Transformer

Transferring Monads

Conclusion

Leave a Reply Cancel reply

Transferring Monads

Conclusion

Share this:

Like this:

Related

Leave a Reply Cancel reply