Let be a Cartesian comonad, so its endofunctor preserves finite limits. A coalgebra for a comonad is with , and . Its morphisms satisfy . Write for the forgetful functor and for the cofree coalgebra. Transposition is
The forgetful functor creates finite limits, since preserves them. We construct both exponential objects and the subobject classifier.
For coalgebras , set and in the ambient topos. Define by transposing
where . Their cofree transposes are coalgebra morphisms
Let be their coalgebra equalizer. For a coalgebra , an arrow corresponds to a map . Its evaluation respects coalgebra structure exactly when
Under the displayed transpositions this is precisely the condition that it equalize . Thus naturally, and is the required exponential in a coalgebra topos.
Let classify . In take the equalizer
The truth map into is and factors through this equalizer. To verify its universal property, take an underlying subobject of a coalgebra. It carries a compatible coalgebra structure exactly when maps into . Such a structure, if it exists, is unique because is monic; its laws follow by cancellation of . Moreover always: applying to a point of lands in . Thus stability is equivalent to .
If classifies , this last equality is exactly
The cofree transpose satisfies this equation precisely when it factors through . Indeed transposing the equality gives the equation above. Pulling back its truth map recovers , because classifies . Hence is the subobject classifier of a coalgebra topos. We have obtained finite limits, exponentials and a classifier, proving is a topos.
Now let be a geometric morphism, and put , , with unit . Both functors preserve finite limits, so is a Cartesian comonad on . Put . Its comparison functor
is left exact and has right adjoint
To check the adjunction, transpose an underlying map to . The coalgebra-morphism equation becomes exactly the equality of the two composites into , so the transposed arrow factors uniquely through the displayed equalizer.
The counit is invertible. Applying to the defining equalizer gives the equalizer of . The structure map is exactly that equalizer: it equalizes by coassociativity; if equalizes, apply to obtain , giving its unique factorization through . Thus the underlying comparison counit is an isomorphism, and the forgetful functor reflects isomorphisms. Therefore is full and faithful.
The adjunctions and define
Here is faithful, so is a surjective geometric morphism; is full and faithful, so is a geometric embedding. Their inverse-image composite is , establishing the surjection-embedding factorization of a geometric morphism.
For uniqueness, let be the class of arrows in inverted by . In any surjection-embedding factorization , conservativity of shows that is also the class inverted by . The essential image of the fully faithful consists exactly of the -local objects , namely those for which is bijective for every in . One direction follows from the adjunction. For the converse, the reflector unit belongs to ; locality gives a retraction, and locality of the reflected object makes that retraction also a right inverse. Thus the unit is invertible. The image subcategory is consequently determined by , independently of the factorization. The two intermediate toposes are equivalent over , and their inverse-image composites with the embeddings determine the surjection legs. This proves uniqueness up to equivalence.
A geometric morphism is surjective when its inverse-image functor is faithful, equivalently conservative for geometric inverse images. Reflection of isomorphisms of subobjects already proves faithfulness by applying the inverse image to equalizers of parallel arrows. The surjection-embedding factorization of a geometric morphism separates this property from a fully faithful direct image.