(Beck’s monadicity theorem, tripleability theorem)
A functor $U : D \rightarrow C$ is monadic (tripleable) if and only if
A proof is reproduced at (Borceux, vol 2, theorem 4.4.4).
Here a parallel pair $f,g : a \rightarrow b$ in $D$ is $U$-split if the pair $U f, U g$ has a split coequalizer in $C$. Specifically, this means that there is a diagram in $C$:
where $h$ has a section $s$ and $U f$ has a section $t$ such that $U g \cdot t = s \cdot h$. This implies that the arrow $h$ is necessarily a coequalizer of $U f$ and $U g$. To say that $U$ creates coequalizers of $U$-split pairs is to say that for any such $U$-split pair, there exists a coequalizer $e$ of $f,g$ in $D$ which is preserved by $U$, and moreover any fork in $D$ whose image in $C$ is a split coequalizer must itself be a coequalizer (not necessarily split).
An equivalent, and sometimes easier, way to state these conditions is to say that
A functor $U : D \to C$ is monadic precisely if
This is equivalent because a conservative functor reflects any limits or colimits which exist in its domain and which it preserves, while monadic functors are always conservative.
The crude monadicity theorem gives a sufficient, but not necessary, condition for a functor to be monadic. It states that a functor $U : D \rightarrow C$ is monadic if
(Recall that a parallel pair $f,g : a \rightarrow b$ is reflexive if $f$ and $g$ have a common section.) This sufficient, but not necessary, condition is sometimes easier to verify in practice. In contrast to the crude monadicity theorem, the necessary and sufficient condition above is sometimes called the precise monadicity theorem.
Duskin’s monadicity theorem gives a different sufficient, but not necessary, condition which refers only to quotients of congruences. It says that a functor $U \colon D \to C$ is monadic if
We can weaken the hypothesis a bit further to obtain the theorem:
As usual, we can also modify it by replacing reflection of limits by reflection of isomorphisms.
If we view the objects of $D$ as underlying $C$-objects with structure, this says that any congruence in $D$ induces a $D$-structure on its quotient in $C$. As with the crude monadicity theorem, this condition is sometimes easier to verify since quotients of congruences are often better-behaved than arbitrary coequalizers. This is the case in many “algebraic” situations.
Duskin actually gave a slightly more precise version only assuming the categories $C$ and $D$ to have particular finite limits, rather than all of them.
In the case when the base category $C$ is Set, one can further refine the requisite conditions. Linton proved that a functor $U\colon D\to Set$ is monadic if and only if
There are other versions of this theorem, including generalizations to monadicity over presheaf categories, which can be viewed as analogues of Giraud's theorem.
The version of the monadicity theorem given in Categories Work uses an evil notion of “creation of limits” and concludes that the comparison functor is an isomorphism of categories, rather than merely an equivalence. But the versions mentioned above can be found in the exercises.
Note however that if $U: D \to C$ is an amnestic isofibration, then $U$ is monadic iff it is strictly monadic. For an application of this observation, see for example the discussion of algebraically free monads at free monad.
We will use Duskin’s variant to prove that the forgetful functor $U\colon$Grp$\to$Set is monadic. Of course, this is also easy to show by explicit computation, but it serves as a useful example of how to use a monadicity theorem. We first need it to have a left adjoint: this is easy to show by a direct construction of free groups, but we could also invoke the adjoint functor theorem. It is also easy to show that it is conservative (a bijective group homomorphism is a group isomorphism), so it remains to consider congruences.
Since limits in $Grp$ are created in $Set$, a congruence in $Grp$ on a group $G$ is an equivalence relation on $G$ which is also a subgroup of $G\times G$. This latter condition means that if $g_1\sim g_2$ and $h_1\sim h_2$, then also $g_1^{-1}\sim g_2^{-1}$ and $g_1 h_1 \sim g_2 h_2$. Since $g\sim g$ for all $g$, it follows that $g\sim h$ if and only if $1\sim h g^{-1}$, so $\sim$ is determined by the subset $H\subseteq G$ of those $h\in G$ such that $1\sim h$. This $H$ is clearly a subgroup of $G$, and moreover a normal subgroup, since if $h\in H$ and $g\in G$ we have $1 = g^{-1} g \sim g^{-1} h g$, so $g^{-1} h g\in H$. Conversely, it is easy to construct a congruence from any normal subgroup, so the two notions are equivalent. It remains only to observe that the quotient of a group by a normal subgroup is, in fact, a quotient of its associated congruence in $Grp$, which is preserved by $U$. Thus, by Duskin’s monadicity theorem, $U$ is monadic.
The monadicity theorem becomes more important when the base category $C$ is more complicated and harder to work with explicitly, and when the objects of $D$ are not obviously defined as “objects of $C$ with extra structure.” For instance, the category of strict 2-categories is monadic over the category of 2-globular sets, essentially by definition, but it is much less trivial to show that it is also monadic over the category of 2-computads. This latter fact can, however, be proven using the monadicity theorem.
The monadicity theorem also plays a central role in monadic descent.
There is a version of the monadicity theorem for (∞,1)-monads in section 3.4 of
There is also a 2-categorical approach using quasicategories in
Canonical textbook references include
Section VI.7 of Categories Work.
Chapter 3 of Michael Barr, Charles Wells, Triples, toposes, and theories , Grundlehren der math. Wissenschaften 278, Springer-Verlag 1983, ftp, web, pdf
Other references include:
Jean Bénabou, Jacques Roubaud, Monades et descente , C. R. Acad. Sc. Paris, t. 270 (12 Janvier 1970), Serie A, 96–98
Duško Pavlović, Categorical interpolation: descent and the Beck-Chevalley condition without direct images, Category theory Como 1990, pp. 306–325, Lecture Notes in Mathematics 1488, Springer 1991
Pierre Deligne, Catégories Tannakiennes , Grothendieck Festschrift, vol. II, Birkhäuser Progress in Math. 87 (1990) pp. 111-195.
wikipedia: monadicity theorem
John Bourke, Two dimensional monadicity, arxiv/1212.5123
There is a version for Morita contexts instead of monads:
Discussion for (infinity,1)-monads is in
and realized in the context of quasi-categories in