Pushforward monads

Abstract

Given a monad $T$ on $\mathscr{A}$ and a functor $G \colon \mathscr{A} \to \mathscr{B}$, one can construct a monad $G_\#T$ on $\mathscr{B}$ subject to the existence of a certain Kan extension; this is the pushforward of $T$ along $G$. We develop the general theory of this construction in a $2$-category, giving two universal properties it satisfies. In the case of monads in $\mathsf{CAT}$, this gives, among other things, two adjunctions between categories of monads on $\mathscr{A}$ and $\mathscr{B}$. We conclude by computing the pushforward of several familiar monads on the category of finite sets along the inclusion $\mathsf{FinSet} \hookrightarrow \mathsf{FinSet}$, which produces the monad for continuous lattices, among others. We also show that, with two trivial exceptions, these pushforwards never have rank.