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.
We will work in terms of formal monad theory, in a 2-category . 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 as the 2-category of categories, functors and natural transformations.
If we have a monad on some 0-cell , and a 1-cell
the question we would like to solve can we transfer the monad along , to give a monad on ? Obviously this is a rather imprecise specification, lets explore some possibilities.
We could assume that the right extension of along itself exists:
and this will induce a codensity monad on . This isn’t really in the spirit of the question though, as we have completely ignored the monad 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 .
To get the monad into the game, we modify our previous plan, and consider the right extension of along .
It turns out that this 1-cell carries a unique monad structure such that the universal 2-cell
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 and :
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 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 must be .
- Plugging in the multiplication preservation axiom into the left hand side of the right extension universal property, we find that the multiplication must be .
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 to show that the monad axioms are satisfied.
So we have found a construction that given a monad on a 0-cell , and a 1-cell , such that the right extension exists, there is a canonical monad induced on . We refer to this construction as the codensity monad transformer.
Example: If we take the monad 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 on , and an adjunction , the composite is a monad on . This result is known as Huber’s construction.
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.