(The adjoint lifting theorem). Consider the following commutative square of functors:
and suppose that
Then, if has a left adjoint, then also has a left adjoint.
A detailed proof may be found in Sec. 4.5 of Vol. 2 of Borceux (see especially Theorem 4.5.6 on p. 226 and Ex. 4.8.6 on p. 252). Also (Johnstone, prop. 1.1.3) For a sketch of proof, see ahead.
If the bottom functor of the above square is the identity arrow (so that ), if and are monadic, and if has coequalizers of reflexive pairs, then is monadic.
The adjoint lifting theorem implies the existence of a left adjoint, and the rest is a straightforward application of the monadicity theorem.
Sketch of proof
We may assume the situation of the following diagram (with ):
where is a monad on , is a monad on , and are the forgetful functors, and and are the free algebra functors.
Let us write for the counit of the adjunction and for the counit of the adjunction . As usual, we have , , , and .
Finally, let be a left adjoint to (which exists by assumption), and let and be the unit and counit (respectively) of the adjunction .
We would like to construct a functor . To get a hint of what should look like, let us assume for a moment that such a already exists. In this case, we have . But is also left adjoint to , and by the uniqueness of a left adjoint we must have (at least up to a natural isomorphism).
From this, we already know how to define on free algebras. Also, being a left adjoint, preserves in particular all coequalizers. But every -algebra is the (object part) of a reflexive coequalizer, namely, the canonical presentation
Applying and using , we see that should be the object part of a reflexive coequalizer in of the form
(recall that we assume that has coequalizers of reflexive pairs).
To eventually define as a coequalizer (as above), we first need some reasonable guess for the ?-arrow. For this, we will need a lemma.
There exists a natural transformation for which the following diagram of functors and natural transformations is commutative:
Define , so that
The required commutativity may be verified by using the commutative diagrams in the definitions of a monad and an EM-algebra, naturality, and the triangular identities. For details, see the proof of Lemma 4.5.1 of Borceux, pp. 222-223. (Note that this lemma does not depend neither on the existence of a left adjoint for the bottom horizontal arrow, nor on the existence of coequalizers. Only the commutativity is required.)
We may now return to our task of defining the ?-arrow in the diagram preceding the lemma. We would like to get from to , and for this, we will construct a natural transformation in the following way. First, we have
Applying and composing with , we get
Applying and composing with , we finally get
Let us call the resulting natural transformation , that is,
Now we take the sought for ?-arrow to be , and define as the object of some fixed coequalizer of and :
In order to do this, we must first verify that the parallel arrows above have a common section (since we only assume that has coequalizers of reflexive pairs). To find a guess for a common section, note that the common section for the parallel pair in the above canonical presentation in is , and if exists, then applying gives . Having this guess, it is now straightforward to verify that is indeed a common section, as required.
So, we have defined an object function of a would be left adjoint . To make it into a functor left adjoint to , we will build a universal arrow from to , whose object part is (Theorem IV.1.2(ii) of Categories Work).
To get an arrow , suppose for a moment that we have a natural transformation such that . Then the left square in the following diagram commutes:
Since both rows are forks, it follows that has the same composition with the arrows of the upper
parallel pair, and hence there exists a unique arrow making the right square commutative (recall that the upper row is a coequalizer).
It is now possible to prove that the pair is a universal arrow from to , showing that is indeed (the object function) of a left adjoint (for details, see the proof of Theorem 4.5.6, pp. 226-227 in Borceux).
But we still have to prove the existence of a natural transformation such that . For this, we define . Since is faithful, to prove the required property of , it is enough to prove that , and this is a long, yet straightforward, computation (noting that and using the commutative diagram from Lemma 1; see Lemma 4.5.3, p. 224 of Borceux).
Forgetful functors between varieties of algebras
Since varieties of algebras are cocomplete and monadic over , the corollary implies that forgetful functors between varieties of algebras (e.g., the forgetful functor ) are monadic.
Sufficient conditions for cocompleteness of monadic categories
Let be an arbitrary category, and consider the commutative diagram
where is monadic, is the diagonal functor and . If is left adjoint
to , then is left adjoint to (using the unit and counit of the original adjunction, one can construct appropriate natural transformations that satisfy the triangular identities, see, e.g., p. 119 of Categories Work). Also, the conditions of the monadicity theorem for imply those for (basically because the definition of a split fork involves only compositions and identities, and because natural transformations are composed componentwise).
Now, if is -cocomplete (so that the bottom horizontal functor has a left adjoint) and has coequalizers of reflexive pairs, then the adjoint lifting theorem implies that is -cocomplete. In particular, if has coequalizers of reflexive pairs and is small-cocomplete, then is small cocomplete.