Only remains. Assume preserves small categorical limits, and choose a small cogenerating family in . Fix a set . The comma category is a complete category: underlying limits in , together with limit preservation by , lift compatible maps from . It is locally small, since its arrows form subsets of the hom-sets in .
We construct a weakly initial set in this comma category. Given , intersect all subobjects through which lifts under . There are only a set of subobjects because is well-powered; the family includes . Their intersection exists by completeness. Also preserves monomorphisms, since a map is monic precisely when its self-pullback diagonal is invertible, and preserves such pullbacks.
Thus all lifts of are unique and compatible, and preservation of the intersection gives
No proper subobject of supports a lift of : its composite into would belong to the intersected family, forcing it to contain . This is a minimal supported subobject.
For each , the map
is injective. Indeed, equal images mean lifts to the equalizer of the two maps, because preserves that equalizer. Minimality forces the equalizer to be invertible, so the maps agree.
The cogenerator property makes the evaluation map
a monomorphism: any two arrows into that agree after all these projections are equal. The indexing pairs inject into the fixed set
Their image is some subset . Consequently is isomorphic to a subobject of a product of the indexed by . There are only a set of such subsets , only a set of subobjects of each , and only a set of maps for each representative subobject .
Collect all these pairs . Every receives a comma arrow from one of them, via the isomorphic copy of and . Hence they form a weakly initial set. The initial-object lemma for complete categories with a weakly initial set, proved explicitly in Question 8, gives an initial object of . Its map from is a universal arrow from an object to a functor. Choosing these universal arrows for all defines a left adjoint to .
Thus
The products indexed by realized subsets are important: one cannot assume that has a map to every cogenerator and simply add arbitrary missing coordinates.
The general adjoint functor theorem says that, for a functor with a complete category and both categories locally small, has a left adjoint exactly when it preserves small categorical limits and satisfies the solution-set condition. The latter means that for each there is a set of arrows such that every factors as
Equivalently, has a weakly initial set.
The limit form of the special adjoint functor theorem says that, if in addition is well-powered and has a small cogenerating family, then has a left adjoint exactly when it preserves small limits. These are the limit/left-adjoint forms; their duals interchange limits with colimits, left with right adjoints, and cogenerators with generators.
For the first route, let be a complete category that is locally small and has a weakly initial set . Put . It is weakly initial: for any , choose an arrow and precompose with the corresponding product projection. The set indexes a simultaneous equalizer
It exists by completeness, for example as the equalizer of the two maps with components and . Since exists for each , is also weakly initial.
Choose . Applying the defining equation to gives , whence because is a monomorphism. If is any endomorphism, apply it to to obtain , hence and . Thus has only its identity endomorphism.
For two arrows , take their equalizer . Weak initiality of gives . Since is an endomorphism of , . The monic arrow with this right inverse is invertible; therefore . Existence of an arrow and this uniqueness show that is initial.
For the general adjoint functor theorem, limit preservation makes each comma category complete, and the solution-set condition makes it weakly initially generated by a set. The lemma provides an initial object . For , the universal property uniquely defines by
Uniqueness gives the functor laws. The same property gives natural bijections
so . Conversely a right adjoint preserves limits, by applying its hom-set bijections to cones, and its unit is already an initial object of each comma category, hence a singleton solution set. This proves necessity as well as sufficiency.
For the second route, assume the general adjoint functor theorem and the additional hypotheses of the Special adjoint functor theorem. Let be a small cogenerating family. Fix and an arrow . A limit-preserving functor preserves monomorphisms, by the self-pullback criterion. Intersect the set of all subobjects supporting . Preservation of this categorical limit gives a minimal supporting pair and a monomorphism with .
If have , their equalizer supports and must be invertible by minimality. Thus
The evaluation map into the product of all these cogenerator targets is monic, because the family coseparates arrows. Its coordinates inject into the fixed set
For every subset , form the product whose coordinate has target . Each minimal is isomorphic to a subobject of one such product, using precisely its realized coordinates. There is a set of subsets ; the well-powered category condition gives a set of representative subobjects of each product. For each representative , include every arrow , a set by local smallness of .
This is a solution-set condition: the minimal pair is isomorphic to one of these representatives, and its inclusion into supplies the required factorization of . The general adjoint functor theorem now gives the left adjoint. This is the cogenerator bound for comma-category solution sets proof of the special theorem. Necessity follows again because a right adjoint preserves limits. Both alternative proof routes are therefore supplied.
For the general alternative, let be a functor between locally small categories, with a complete category. The Freyd general adjoint functor theorem says that has a left adjoint if and only if it preserves small categorical limits and satisfies the solution-set condition. Explicitly, for every , there must be a set of morphisms such that every has the form for some and . Equivalently, each comma category has a weakly initial set.
We prove the initial-object lemma for complete categories with a weakly initial set. Let be a locally small category which is complete and has a weakly initial set . Its product in a category is weakly initial: for each , choose a morphism and compose with the projection . The hom-set is a set. Form equalizing every endomorphism of with , by taking the equalizer of the two morphisms
whose -coordinates are and . Then for every endomorphism , and is monic. There is a morphism for every , by composing with a weakly initial morphism out of .
To prove uniqueness, let and take their equalizer . Weak initiality of gives . The composite is an endomorphism, so . Cancel the monomorphism to obtain . Thus is both monic and split epic, hence an isomorphism: if , cancellation from gives . Since , it follows that . Therefore is an initial object, proving the lemma fully.
Now assume categorical limit preservation and the solution-set condition. The comma category is locally small. It is complete: for a small diagram in a category , take its underlying categorical limit in . Since preserves this categorical limit, the compatible give a unique . The same universal property shows that is the categorical limit in the comma category. Its weakly initial set and the proved lemma therefore supply an initial object . For , its universal property defines a unique with . Uniqueness proves the identity morphism and composition in a category laws and the naturality of . The same universal property gives the natural bijection , so .
For necessity, an adjunction supplies the singleton weakly initial set at . It also proves that preserves categorical limits: maps correspond to maps , and compatible families of the latter factor uniquely through any categorical limit in . Hence the image categorical cone under has the required universal property. This proves both directions of the general alternative.
For the special alternative, the limit form of the special adjoint functor theorem says: if is complete, locally small and well-powered, with a small cogenerating family , and is locally small, then has a left adjoint exactly when it preserves small categorical limits. A cogenerating set means that unequal parallel morphisms are distinguished by some morphism . We prove the needed solution-set condition, so that the general theorem applies.
Fix . A supporting subobject of is a monomorphism through whose image under the morphism factors. There is at least one, namely . Because is well-powered, choose a set of representatives of all these supporting subobjects. A limit-preserving functor preserves monomorphisms: a map is monic exactly when its diagonal into its self-pullback in a category is an isomorphism, and both the pullback in a category and this isomorphism are preserved. Consequently each factorization of through is unique. Form the intersection of subobjects of the supporting representatives, as a wide pullback in a category over . The unique lifts of are compatible and, since preserves that categorical limit, they give a factorization
This is a minimal supported subobject. More explicitly, if also supports , then is one of the supporting subobjects of . The intersection therefore factors through , giving with . Monicity of gives ; monicity of then makes invertible.
For any , if , the equalizer of supports , because preserves that equalizer. Minimality makes it invertible, so . We have therefore obtained injective functions
Let be the realized image subset of the fixed set . Use the unique morphism corresponding to each to form the evaluation embedding into cogenerator products
This morphism is monic: if two morphisms into have identical product composites, every morphism from to every gives identical composites, and the cogenerating property makes the two morphisms equal. There is only a set of possible families of subsets , and hence a set of possible products . Each has only a set of subobjects by well-poweredness, and each chosen subobject has only a set of morphisms by local smallness. Take all these pairs as a weakly initial set. Every original receives a morphism from a pair representing its , through . Thus the set is weakly initial in .
The general theorem now supplies a left adjoint. Necessity again follows from preservation of categorical limits by a right adjoint. This proves the special alternative, including its size argument. Using only the realized subsets avoids assuming that an arbitrary object admits a morphism into every cogenerator. Both adjoint functor theorem alternatives are proved.
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.
A localic geometric morphism presents , over , as sheaves on an internal locale of . Equivalently, subobjects of inverse images form a separating family. A hyperconnected geometric morphism has a full faithful inverse image whose essential image is closed under subobjects. In particular, it induces bijections
For this definition, subobject-closed means every subobject of is isomorphic, over , to the inverse image of a subobject of .
Here is the construction and proof of the hyperconnected-localic factorization. Given , its right adjoint gives natural bijections
Let be the internal locale whose frame of opens is . The frame operations are determined by these bijections: intersections are intersections of represented subobjects; the join of a family is its image under the projection from the parameter-indexed family. For an internal index object , evaluation of the family over becomes a subobject of , and its direct image to represents the join. Pullback stability of images makes this natural in , and distributivity follows from the corresponding subobject identity in . This explicitly constructs the internal frame rather than asserting it from the existence of alone.
Set , with its localic projection to . We construct . A basic open family is a map ; its represented object in is the subobject corresponding to . Meets and covering joins of open families become intersections and jointly epic families of these subobjects.
An internal sheaf on is presented by its local sections with their open domains and restrictions. Pull these domains back to the corresponding and identify two sections wherever their restrictions agree. This is an effective equivalence relation in , so its quotient defines of the sheaf. More concretely, if is the object of sections and gives their domains, start with . For two sections, the join of the opens on which they agree gives an -valued relation on , hence a subobject of . Restricted to , this is the germ equivalence relation used for the quotient. The restriction and sheaf axioms guarantee reflexivity, symmetry and transitivity. This construction is functorial. Products and equalizers are obtained by meeting domains and equalizing restrictions, so it preserves finite limits. A right adjoint is obtained by taking, over each open family , the parameterized maps for . These maps satisfy the sheaf condition because a covering join gives an effective gluing of the ; their parameter objects are supplied by the original adjunction and exponentials. The map bijection on basic open families, followed by gluing, proves this is right adjoint to . Thus is a geometric morphism.
We must check hyperconnectedness, not just construct a factorization. A map has a graph which is a subobject of . The represented-subobject bijection turns it into an -valued relation on . Its totality and single-valuedness say exactly that this relation is a map between the corresponding basic sheaf objects: totality uses the covering join, and single-valuedness uses intersections and the diagonal of . Thus maps between basic open families are precisely their maps in . Applying this to the local sections of arbitrary sheaves, compatible maps glue uniquely on both sides. Hence is full and faithful. Likewise a subobject of pulls back to subobjects of its basic ; each is again represented by an open family, and their compatibility glues to a subsheaf of . The essential image is therefore subobject-closed, proving that is hyperconnected.
The inverse image is the constant family over the whole locale. The construction sends it to , so ; taking right adjoints gives the required factorization
This argument uses the usual effective quotient and local-section constructions in a topos; it also explains why the relevant internal opens are relative subobjects of , not just global subobjects of the terminal object.
For uniqueness, suppose with hyperconnected and localic. Then for every ,
If is sheaves on an internal locale , the right side is represented by its frame . These identifications preserve intersections, joins and parameter change, so the representing internal frames are isomorphic: . The locale and its sheaf topos are therefore equivalent over . Under this equivalence the basic open families have the same images in , and their local-section presentations determine all other images and maps. Thus the two hyperconnected parts agree up to the same equivalence. The factorization is unique up to equivalence.
Finally suppose with a geometric embedding and hyperconnected. Let be the local operator on presenting the inclusion. For a subobject of , take the -closure of in . Hyperconnectedness makes it the inverse image of a unique subobject of . This defines a closure operation on ; its extensivity, idempotence, intersection preservation and pullback stability descend from the -closure. Let be its local operator.
Hyperconnectedness also gives , by the represented-subobject bijections. The direct image is the closed-truth object , and hence
This follows either by taking the equalizer of and the identity or by representing closed subobjects in the preceding closure construction. The internal locale with frame is the sublocale of the terminal locale determined by : covering joins are exactly closure by . Its sheaves are the -sheaves in , and its projection is their geometric inclusion. Applying the just-proved factorization to therefore gives
This supplies the requested reordered factorization.