Take the definition of an elementary topos as a category with finite limits, exponential objects and a subobject classifier . Its power object is , and is precomposition with . Transposing a predicate on in either variable gives
Thus is left adjoint to the contravariant power-object functor .
Here are the remaining hypotheses for the crude monadicity theorem, obtained from those topos axioms. The unit of this adjunction is , internally . It is monic: if two such evaluations agree, evaluate on the singleton predicate classified by the diagonal to obtain . If is invertible, naturality therefore makes monic. The characteristic map of this mono, regarded as a global element of , pulls back along to the everywhere-true predicate on . Since is monic, that characteristic map was already everywhere true on . The classifier pullback then says that is invertible. Hence is a conservative functor.
It remains to check preservation of reflexive coequalizers in the opposite category. Equivalently, let be a coreflexive pair, with satisfying , and let be their equalizer. Both and are monic. For any mono , there is a direct-image map between power objects: a subobject is sent to its composite with . This uses only classification of monos, not the prior existence of general images or colimits. We have .
For a predicate , consider its direct image along . Its pullbacks along the two sections are
To verify the second equality, with implies after applying , and therefore ; conversely supplies that witness. This argument works for parameterized subobjects as well, so it is an equality of arrows between power objects.
Now if satisfies , then . Hence is its unique factorization through , uniqueness following from the section . Therefore
is a coequalizer. Finite limits supply every required coreflexive equalizer. The right adjoint reflects isomorphisms and preserves the corresponding reflexive coequalizers, so is monadic. In particular is equivalent to the Eilenberg-Moore category of the double-power-object monad on .
Let be a logical functor, and suppose . Preservation of exponentials and the classifier gives , compatibly with the units, counits and resulting monads. Thus is the algebra functor lifting the base functor through the two monadic power-object functors. The adjoint lifting theorem for monad algebra functors applies to the base adjunction : its required coequalizers exist in , because has finite equalizers. It supplies a left adjoint . Taking opposites gives , the required right adjoint to .
Preserving either of the two logical structures by itself is insufficient. For the exponential example take constant at . The constant-empty functor is its left adjoint, since both relevant hom-sets are singletons. Its canonical exponential comparison is , so it preserves exponentials. It has no right adjoint: a functor with a right adjoint would preserve the initial object, whereas .
For the classifier example take to be fixed points. The trivial-action functor is left adjoint to . In a group-action topos the classifier is the trivial-action two-element set, since invariant subsets have ordinary equivariant characteristic maps. Therefore preserves the classifier, its true arrow and the terminal object. But does not preserve the coequalizer of the identity and the nontrivial translation on the regular two-element group set: that coequalizer is , while the fixed-point sets of the domain and codomain of the parallel pair are empty. Their set-theoretic coequalizer is empty, not . Thus has no right adjoint.
Write the Cartesian comonad as , with preserving finite limits. A coalgebra for a comonad is with , and . Its forgetful functor is faithful, creates finite limits, and has the cofree coalgebra right adjoint . We construct the two remaining topos structures explicitly.
For exponential objects, take coalgebras and start with . Put , with structure , and let
Transpose the following two maps into maps :
using . The cofree adjunction transposes once more into coalgebra morphisms . Let be their equalizer. A coalgebra map corresponds to an arbitrary ambient map . It factors through precisely when
which is exactly the condition that be a coalgebra morphism. Therefore represents and is the required exponential in a coalgebra topos.
For the subobject classifier, let classify the mono . In the cofree coalgebra , form
Both arrows are coalgebra morphisms. The cofree transpose of factors through this equalizer and gives its true arrow. To verify classification, let have ambient characteristic map . It supports a subcoalgebra of exactly when it is invariant under , equivalently
The counit proves the reverse containment in the first equation; the forward containment supplies the restricted structure map, whose coalgebra laws follow through the mono. Under the cofree adjunction, the second equation says exactly that factors through . Pulling back its true arrow recovers , since . This proves the universal property of the subobject classifier of a coalgebra topos. Hence is a topos.
Now let be a geometric morphism, with . The comonad is Cartesian: preserves finite limits and the right adjoint preserves limits. Put , already a topos. The forgetful adjunction defines with , so is faithful.
The comparison functor
preserves finite limits. It has a right adjoint , given on a coalgebra by
Indeed, the transposed arrow corresponds to a coalgebra map exactly when it equalizes these two maps. Applying the finite-limit-preserving shows that is the equalizer of
That equalizer is . If equalizes the pair, then , proving the claimed universal property. Consequently the counit is invertible. The fully faithful adjoint criterion makes full and faithful.
Thus defines a geometric embedding , and identifies the composite with . The requested factorization is
where is a surjective geometric morphism and is full and faithful.
Write the comonad as and its category of coalgebras for a comonad as . A coalgebra for a comonad is a map with and . A morphism satisfies . Let be the forgetful functor and let be the cofree coalgebra. The adjunction has the explicit correspondence
We construct the three pieces of the elementary topos structure.
Because preserves finite limits, each underlying finite limiting cone has a unique coalgebra structure induced by the structures on its vertices. The counit and coassociativity equations can be checked after its jointly monic projections. Thus creates finite limits and reflects isomorphisms. A morphism of coalgebras is monic exactly when its underlying morphism is monic, by the diagonal criterion using the created pullback.
For exponentials in a coalgebra topos, fix coalgebras and and put in . On the cofree coalgebra there is an underlying evaluation
The two maps
use in the second expression. Transpose them in to maps , and then transpose across to coalgebra morphisms . Take their equalizer in .
An underlying map corresponds to a coalgebra map . The equation saying that the original map is a coalgebra morphism is precisely , since for the structure . By the cofree adjunction, this is equivalent to , hence to unique factorization through . Therefore
naturally in . This constructs the required exponential object.
For the subobject classifier of a coalgebra topos, let be the underlying subobject classifier, and let classify the mono . Its cofree transpose is the coalgebra endomorphism
Define as the equalizer of and . The transpose of factors through this equalizer and gives .
Indeed, for a subobject classified by , the pullback has characteristic map . It is always contained in , by naturality of the counit. Equality holds exactly when restricts to a coalgebra structure on ; its axioms then follow by composing with the monomorphisms and . Under , the classifying map becomes . The equality of subobjects is . Transposing this equality gives , so exactly the coalgebra subobjects correspond to maps . Their pullback of is the desired subcoalgebra, and uniqueness follows from uniqueness of .
Thus we have finite limits, exponentials and a subobject classifier:
The construction does not assume that preserves the underlying exponentials or underlying subobject classifier.
A Cartesian closed category has finite products in a category and, for every , an exponential object characterized naturally by
In , finite products and the terminal functor are computed pointwise. With , define
This is a set because is a small category. For , precomposition induces by precomposition of natural transformations, making a covariant functor.
Given , define its curry by
For , naturality of gives , proving that this is a natural transformation . The same formula with precomposed proves naturality of in .
Conversely, from define
Naturality of and its values proves naturality of . Currying this result recovers , since ; uncurrying a curry recovers by setting . These mutually inverse constructions are natural in , giving the adjunction required for an exponential object. Therefore
Suppose the small category is Cartesian closed. The Yoneda embedding preserves finite products. For , the Yoneda lemma and the exponential object adjunction give
The bijections are natural in , so
Thus the essential image of in its presheaf topos is full and closed under finite products and exponentials.
Let be a subterminal object in a Cartesian closed category. For every and , the exponential object adjunction gives
The set on the right has at most one element because is subterminal. Hence is subterminal, proving that is an exponential ideal.
Now let be reflective, with reflector and unit . Recall the useful form of its universal property: an object lies in precisely when every map factors uniquely through .
Suppose first that is an exponential ideal. Reflective subcategories are closed under ambient limits, so lies in . Given with , curry in the first variable to obtain . Since , this factors uniquely through and uncurries to . Curry once more, now in ; since , the result factors uniquely through . Thus every factors uniquely through
This makes a reflection of , so uniqueness of reflections gives
Conversely, suppose preserves binary products, and take . To prove , start with and let be its transpose. Since is reflective, factors uniquely through
Composing the resulting map with and currying produces an extension of . Product preservation identifies the unit on with , so the same universal property proves uniqueness. Therefore is reflective, and is an exponential ideal. This proves the reflector product criterion for an exponential ideal.
Finally consider the arrow category . For arrows and , let
Then the exponential is the arrow
Indeed, a commutative square from to this arrow is, after currying, exactly a commutative square . This establishes the required exponential adjunction and proves that is cartesian closed.
If is injective, two elements and of have
so injectivity gives . Hence is injective. The category of injective functions is therefore an exponential ideal in the arrow category. Its terminal object and binary products are inherited pointwise, so these same exponential objects make cartesian closed.
If every slice category is essentially small, the displayed exponential object and the set of sieves on a category at each are small even when is large. Together with pointwise finite limits, they give the elementary-topos constructions in a universe admitting the large diagrams. This does not force the entire functor category to be locally small in the original universe: a large discrete category has terminal slices, but maps between its constant-one and constant-two presheaves are arbitrary class-indexed binary families.
For a small Cartesian closed category, the Yoneda embedding into its presheaf category preserves exponential objects. At , the exponential in a presheaf category has value . Since , the Yoneda lemma identifies this with . Every identification is natural in all three objects.