nLab
monadic functor

Idea

A functor $U:D\to C$ is monadic iff it has a left adjoint $F:C\to D$ and the adjunction $F\dashv G$ ‘comes from’ the induced monad on $C$ – that is, $U$ monadic iff $F\dashv U$ is a monadic adjunction.

In this situation $U$ in some sense ‘looks like’ the forgetful functor from the Eilenberg-Moore category of the monad $(U\circ F,\eta,U\epsilon_F)$ on $C$, and has ‘nice properties’ similar to these forgetful functors.

The monadicity theorem characterizes monadic functors and makes these ‘nice properties’ precise.

Definition

Given a pair of adjoint functors $F: C \to D :U$, $F \dashv U$, with unit $\eta: Id_C \to U \circ F$ and counit $\epsilon: F \circ U \to Id_D$, one constructs a monad $\mathbf{T}=(T,\mu,\eta)$ setting $T = U \circ F: C \to C$, $\mu = U \epsilon F: T T = U F U F \to U F = T$.

Consider the Eilenberg-Moore category $C^{\mathbf{T}}$ of $T$-algebras ($T$-modules) in $C$. Clearly $U (\epsilon_M): T U M = U F U M \to U M$ is a $T$-action. In fact there is a canonical comparison functor $K^{\mathbf{T}}: D \to C^{\mathbf{T}}$ given on objects by $K(M)=(U M, U (\epsilon_M))$. We then say that we have a (resp. strictly) monadic adjunction iff $K$ is an equivalence (resp. isomorphism) of categories.

A functor $U: D \to C$ is monadic (resp. strictly monadic) if it has a left adjoint $F: C\to D$ and the comparison functor $K^{\mathbf{T}}: D \to C^{\mathbf{T}}$ is an equivalence of categories (resp. an isomorphism of categories). In other words, up to equivalence, monadic functors are precisely the forgetful functors defined on Eilenberg–Moore categories for monads, and strictly monadic functors are the same as these forgetful functors up to isomorphism. A category $D$ is monadic over a category $C$ if there is a functor $U: D \to C$ which is monadic.

Properties

Various versions of Beck’s monadicity theorem (old-fashioned name of some schools: tripleability theorem) give sufficient, and sometimes necessary, conditions for a given functor to be monadic. There are also dual, comonadic versions.

A monadic functor is strictly monadic if and only if it is also an amnestic isofibration: clearly, a strictly monadic functor is an amnestic isofibration; and if a monadic functor $U$ is amnestic, then the comparison functor $K$ is also amnestic, and if $U$ is a monadic isofibration, so is $K$; therefore in this case $K$ must be an isomorphism of categories.

Beware that monadic functors are not closed under composition. For a specific example: the category of reflexive quivers is monadic over $Set$ via the functor $RefGph \to Set$ sending a graph to its set of edges, and the category of categories is monadic over reflexive graphs via the forgetful functor $Cat \to RefGph$, but $Cat$ is not monadic over $Set$ (via any functor whatsoever, since such categories are regular categories but $Cat$ is not).

Related concepts

• monadic adjunction, structure-semantics adjunction

• comonadic functor, monadicity theorem

• If the comparison functor is only fully faithful, a functor is sometimes said to be of descent type.

• monadic decomposition