For a functor between Eilenberg-Moore categories lying over a right adjoint on the base categories and compatible with the monad structures, an adjoint lifting theorem constructs a left adjoint when the required reflexive coequalizers of algebra presentations exist. Applied through power-object monadicity, this converts a left adjoint of a logical functor into a right adjoint of that logical functor. The coequalizer hypotheses are part of the theorem; commutation with the forgetful functors alone is insufficient.
Put , the power object, with acting by inverse image of predicates. Transposing a predicate on gives natural bijections
Thus is left adjoint to . Its unit sends to evaluation at , namely the predicate . This unit is monic: two generalized elements having the same evaluation on all predicates agree by testing the singleton predicate of the first, or equivalently its graph in the relevant parameter product.
We verify a sufficient form of Beck's monadicity theorem: a right adjoint is monadic if it reflects isomorphisms and its domain has, and it preserves, coequalizers of reflexive pairs. Suppose is invertible. Then is invertible, and naturality of the monic unit shows that is monic. Regard it as the subobject . Its characteristic predicate and the constantly true predicate have the same restriction to , so injectivity of makes them equal. Thus this subobject is all of , and is invertible. Hence reflects isomorphisms.
A reflexive pair in is a coreflexive pair in , with a common retraction such that . Its equalizer exists. We show that is the coequalizer of . Direct image of subobjects along the mono defines , and similarly . At every parameter object the identities are
For the middle identity, an equality forces after applying ; their common point must therefore lie in the equalizer. This proves the identity for parameterized predicates, not merely for global elements. If satisfies , composing with gives . Thus it factors through , and the last displayed identity gives uniqueness. This proves that power objects turn coreflexive equalizers into coequalizers. All hypotheses of the monadicity criterion have now been checked, so is monadic, with
A logical functor preserves finite limits, exponentials and the classifier, hence gives compatible natural isomorphisms and . They respect units and multiplications, because these are defined by evaluation and transposition. Under the displayed equivalences, is therefore the induced functor on double-power Eilenberg-Moore categories. Their forgetful functors create finite limits, and the underlying preserves them. Consequently the induced functor preserves finite limits, so does too. Reversing arrows proves every logical functor preserves finite colimits.
For the first counterexample, the constant-terminal functor has the constant-empty functor as left adjoint: both sets of maps in the adjunction are singletons. It preserves exponentials, since with the canonical comparison. It does not preserve the initial object, because . Thus preservation of exponentials alone is insufficient.
For the second, take the fixed-point functor for . Its left adjoint gives a set the trivial action. The classifier of -sets is the two-element set with trivial action, so preserves it and its truth map. Let be the free two-element -set. The coequalizer of its identity and its swapping automorphism is the singleton -set. Applying gives two maps followed by , whereas their coequalizer in sets is . Thus preserves the classifier but not all finite colimits. These examples also explain why both requirements in logicalness matter.
Use the elementary, or weak, topos axioms: finite limits and a power object for every object , naturally representing . No arbitrary products or coproducts are assumed. In particular is the subobject classifier. Inverse image of the membership relation defines for .
Interchanging the factors in a relation gives natural bijections
Thus the contravariant power-object functor has left adjoint . Its adjunction unit sends a generalized element to the predicate on given by membership of .
This unit is monic. If have the same image under , membership of and agrees in every -parameterized subobject of . Apply this to the graph of in : membership of is true, so membership of is true, which means . This argument uses parameterized relations, not an assumption that global elements detect morphisms.
The functor reflects isomorphisms. Suppose is invertible. Then is invertible, and naturality together with monicity of shows that is monic. Regard as a subobject of . Its inverse image along itself is the whole of , just as for the whole subobject of . Those two subobjects correspond to maps ; since is monic, they coincide. Therefore the subobject is all of , and is an isomorphism.
We now prove the preservation condition for the crude monadicity theorem. A reflexive pair in is a coreflexive pair in , with for some . Let be its equalizer. For any monomorphism , define on power objects by composing a parameterized subobject with ; no general image construction is needed because is monic. Inverse image followed by this extension obeys .
Here both are monic. For a parameterized subobject of , an element belongs to exactly when for some . Applying gives , so this condition is precisely and . Consequently, as morphisms of power objects,
If equalizes , these identities give
It therefore factors uniquely through , which is a split epimorphism with section . Since , also equalizes . Hence is their coequalizer. This proves explicitly that power objects turn coreflexive equalizers into coequalizers.
Finite equalizers in give all coequalizers of reflexive pairs in , and we have shown that preserves them and reflects isomorphisms. The crude monadicity theorem now yields
Fix a set of cardinality . If has -indexed products in a category, its Eilenberg-Moore category for the double-power monad has them, since the forgetful functor creates existing limits. The displayed equivalence then gives -products in , hence -coproducts in a category in .
For the converse, suppose those coproducts exist. The diagonal is a logical functor, because all the elementary topos structure in is pointwise, and it has left adjoint . Apply power-object monadicity to both toposes. Under their monadic identifications, is the lift of to the double-power Eilenberg-Moore categories. The base functor is a right adjoint to , so the adjoint lifting theorem for monad algebra functors gives a left adjoint to its algebra lift. Its required reflexive coequalizers exist in , since they are opposites of finite equalizers in . Taking opposites gives a right adjoint to , which is exactly the -product functor. Thus the products and coproducts of fixed cardinality in a topos satisfy
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.
For an elementary topos, existence of products in a category indexed by a fixed set is equivalent to existence of the corresponding coproducts in a category. The power-object monadicity equivalence gives the forward direction because Eilenberg-Moore categories create limits. For the converse, the diagonal into the pointwise product category is a logical functor. A coproduct is its left adjoint; the adjoint lifting theorem for monad algebra functors, applied through power-object monadicity, then gives its right adjoint, namely the product. The required reflexive coequalizers on the algebra side are opposites of finite equalizers in the topos.