where has a section and has a section such that . This implies that the arrow is necessarily a coequalizer of and .
The functor is said to create coequalizers of -split pairs if for any such -split pair, there exists a coequalizer of in which is preserved by , and moreover any fork in whose image in is a split coequalizer must itself be a coequalizer (not necessarily split).
(Beck’s monadicity theorem, tripleability theorem)
A proof is reproduced at (Borceux, vol 2, theorem 4.4.4).
An equivalent, and sometimes easier, way to state these conditions is to say that
A functor is monadic precisely if
The crude monadicity theorem gives a sufficient, but not necessary, condition for a functor to be monadic. It states that a functor is monadic if
(Recall that a parallel pair is reflexive if and 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 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 as underlying -objects with structure, this says that any congruence in induces a -structure on its quotient in . 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 and to have particular finite limits, rather than all of them.
In the case when the base category is Set, one can further refine the requisite conditions. Linton proved that a functor is monadic if and only if
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 is an amnestic isofibration, then 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 GrpSet 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 are created in , a congruence in on a group is an equivalence relation on which is also a subgroup of . This latter condition means that if and , then also and . Since for all , it follows that if and only if , so is determined by the subset of those such that . This is clearly a subgroup of , and moreover a normal subgroup, since if and we have , so . 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 , which is preserved by . Thus, by Duskin’s monadicity theorem, is monadic.
The monadicity theorem becomes more important when the base category is more complicated and harder to work with explicitly, and when the objects of are not obviously defined as “objects of 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 also a 2-categorical approach using quasicategories in
Canonical textbook references include
Section VI.7 of Categories Work.
Other references include:
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
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