is split if there are morphisms and such that , and ; it is elementary that every split fork is an (absolute) equalizer.
Theorem. Let , , be an adjoint pair of functors with unit and counit , and the corresponding comonad. Then is comonadic, i.e. the comparison functor , is an equivalence iff has the property that every fork
in such that its image by is a split equalizer sequence in , is itself an equalizer sequence.
We now sketch a proof in the presence of axiom of choice. The fact that the condition on the forks is necessary follows from the fact that the condition is invariant under an equivalence of categories over , while for the Eilenberg-Moore (EM) category the property is easy to check. For the opposite condition, we sketch a slightly nonstandard direct proof, exhibiting a quasiinverse of the comparison map; for the Beck’s theorem in above form this is really easy for objects with a bit more discussion using universality of equalizers for morphisms.
The crucial observation is that, for any -comodule, the diagram
manifestly exhibits a split equalizer sequence; hence, by the assumption, for each -comodule there is an equalizer of the form
Using the axiom of choice we can therefore form a map . Once a choice of map is made, for any , by the universality of equalizers, one has a unique map for which the diagram
sequentially commutes. Again, by the universality of equalizers, it is easy to show that this rule is functorial; hence becomes a functor.
It is now sufficient to exhibit natural isomorphisms and .
Special case of Beck theorem. Let be an adjoint pair its associated monad, and its associated comonad.
If preserves and reflects coequalizers of all parallel pairs in (for which coequalizers exists) and if any parallel pair mapped by into a pair having a coequalizer in has a coequalizer in , then the comparison functor is an equivalence of categories.
If preserves and reflects equalizers of all parallel pairs in (for which equalizers exists) and if any parallel pair mapped by into a pair having an equalizer in has an equalizer in , then the comparison functor is an equivalence of categories.