Proof

We discuss the equivalence of these conditions:

The equivalence $(f^* \; faithful) \Leftrightarrow (Id \to f^* f_* \;is \; mono)$ is a general property of adjoint functors (see there).

The implication $(f^* faithful) \Rightarrow (f^* induces\;injection\;on\;subobjects)$ works as follows:

first of all $f^*$ does indeed preserves subobjects: since it respects pullbacks and since monomorphisms are characterized as those morphisms whose domain is stable under pullback along themselves.

To see that $f^*$ induces an injective function on subobjects let $U \hookrightarrow X$ be a subobject with characteristic morphism $char U : X \to \Omega$ and consider the image

of the pullback diagram that exhibits $U$ as a subobject. Since $f^*$ preserves pullbacks, this is still a pullback diagram.

If now $U \leq \tilde U$ but $f^* (U) = f^*(\tilde U)$ then both corresponding pullback diagrams are sent by $f^*$ to the same such diagram. By faithfulness this implies that also

commutes, and hence that also $\tilde U \subset U$, so that in fact $\tilde U \simeq U$.

Next we consider the implication ($(f^{*}\mathrm{induces}\mathrm{injection}\mathrm{on}\mathrm{subobjects})\Rightarrow (f^{*}\mathrm{is}\mathrm{conservative})$ (f^* f^* induces injection on subobjects) \Rightarrow (f^* is conservative) . induces injection on subobjects)$\Rightarrow$ ($f^*$ is conservative).

Assume $f^* (X \stackrel{\phi}{\to} X')$ is an isomorphism. We have to show that then $\phi$ is an isomorphism. Consider the image factorization $X \to im(\phi) \hookrightarrow X'$. Since $f^*$ preserves pushouts and pullbacks, it preserves epis and monos and so takes this to the image factorization

of $f^* \phi$, where now the second morphism is an iso, because $f^* \phi$ is assumed to be an iso. By the assumption that $f^*$ is injective on subobjects it follows that also $im \phi \simeq X'$ and thus that $\phi$ is an epimorphism.

It remains to show that $\phi$ is also a monomorphism. For that it is sufficient to show that in the pullback square

we have $X \times_{X'} X \simeq X$. Write $\Delta : X \to X \times_{X'} X$ for the diagonal and let

be its image factorization. Doing the same for $f^* \phi$, which we have seen is a monomorphism, and using that $f^*$ preserves the pullback, we get

Now using again the assumption that $f^*$ is injective on subobjects, this implies $im \Delta_\phi = X \times_{X'} X$ and hence that $\phi$ is a monomorphism.

(…)

The statement about the comonadic adjunction we discuss below as prop. 2.

Proof

By the discussion at topos of coalgebras the inverse image is the forgetful functor to the underlying $\mathcal{E}$-objects. This is clearly a faithful functor.

Proof

With observation 1 we only need to show that if $f : \mathcal{E} \to \mathcal{F}$ is surjective, then there is $T$ such that

For this, take $T := f^* f_*$. This is a left exact functor by definition of geometric morphism. By assumption on $f$ and using the equivalent definition of def. 1 we have that $f^*$ is a conservative functor. This means that the conditions of the monadicity theorem are met, so so $f^*$ is a comonadic functor.