Pushforward monads

TL;DR

This paper develops a general theory for the pushforward of monads along functors using Kan extensions, establishing universal properties and adjunctions, with applications to monads on finite sets and continuous lattices.

Contribution

It introduces a 2-categorical framework for pushforward monads, providing universal properties, adjunctions, and explicit computations for familiar monads.

Findings

Pushforward monads satisfy two universal properties in a 2-category.

Established adjunctions between categories of monads on different categories.

Computed pushforwards of monads on finite sets, including the monad for continuous lattices.

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.