for all ;
reflects the order on subobjects;
is a comonadic adjunction.
The equivalence of these condition appears for instance as MacLaneMoerdijk, VII 4. lemma 3 and prop. 4.
We discuss the equivalence of these conditions:
The equivalence is a general property of adjoint functors (see there).
The implication works as follows:
To see that induces an injective function on subobjects let be a subobject with characteristic morphism and consider the image
of the pullback diagram that exhibits as a subobject. Since preserves pullbacks, this is still a pullback diagram.
If now but then both corresponding pullback diagrams are sent by to the same such diagram. By faithfulness this implies that also
commutes, and hence that also , so that in fact .
Next we consider the implication .
Assume is an isomorphism. We have to show that then is an isomorphism. Consider the image factorization . Since preserves pushouts and pullbacks, it preserves epis and monos and so takes this to the image factorization
of , where now the second morphism is an iso, because is assumed to be an iso. By the assumption that is injective on subobjects it follows that also and thus that is an epimorphism.
It remains to show that is also a monomorphism. For that it is sufficient to show that in the pullback square
we have . Write for the diagonal and let
be its image factorization. Doing the same for , which we have seen is a monomorphism, and using that preserves the pullback, we get
Now using again the assumption that is injective on subobjects, this implies and hence that is a monomorphism.
The statement about the comonadic adjunction we discuss below as prop. 2.
to the topos of coalgebras is a geometric surjection.
Up to equivalence, every geometric surjection is of this form.
This appears for instance as (MacLaneMoerdijk, VII 4., prop 4).
With observation 1 we only need to show that if is surjective, then there is such that
For this, take . This is a left exact functor by definition of geometric morphism. By assumption on and using the equivalent definition of def. 1 we have that is a conservative functor. This means that the conditions of the monadicity theorem are met, so so is a comonadic functor.
Section VII. 4. of