A locally small category with all small categorical limits and a small weakly initial set has an initial object. Take the product of the weakly initial family, then the simultaneous equalizer of all endomorphisms of and its identity. For any parallel , their equalizer receives a map . The equation forces , so is invertible and . Weak initiality supplies existence of maps from . This is the smallness mechanism in the Freyd general adjoint functor theorem.
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.
Use the Freyd general adjoint functor theorem: a functor , with complete and both categories locally small, has a left adjoint precisely when it preserves small categorical limits and satisfies the solution-set condition. The latter means that every comma category has a small weakly initial set.
Here is the proof. First prove the initial-object lemma for complete categories with a weakly initial set. In a complete locally small category , take the product in a category of a small weakly initial family. It is weakly initial: project to whichever member admits a morphism into the required object. Form the simultaneous equalizer of every endomorphism of and ; local smallness makes this a small limit.
For parallel , let be their equalizer. Weak initiality supplies . Since is an endomorphism of , the defining equalities give . Cancel the monomorphism to get . Thus is a split epimorphism as well as a monomorphism, hence invertible, and . Existence of a morphism follows by composing with a map . Therefore is an initial object.
Now, if preserves small categorical limits, each has them: take the limit of the underlying -diagram and use preservation to assemble its maps out of . It is locally small and has a weakly initial solution set, so the lemma produces an initial object . Its universal property gives natural bijections
The universal arrows define on morphisms, proving . Conversely, a right adjoint preserves categorical limits, and its unit supplies a singleton solution set in each comma category.
Apply this to . The functor category is complete and locally small because is small; pointwise limits in a functor category show preserves all small limits. For , verify the bounded subfunctor solution set for precomposition. Choose an infinite cardinal number at least as large as the number of -morphisms and . Given , set
Postcomposition makes a subfunctor, each value has cardinality at most , and factors through . After labelling its values by subsets of , only a set of possibilities for and exists. Their maps into give the required weakly initial set. Thus has a left adjoint.
It is the left Kan extension. The left Kan extension as a comma-category colimit makes it concrete:
Every representative maps under to . The colimit identifications and naturality make this well-defined, giving exactly .
Broadly in favour, if “trivial” means transparent once the correct structure has been identified. The value of category theory is often to isolate a universal property that makes a repeated argument automatic.
For example, two objects with the same universal property have unique connecting maps in each direction. Their composites and the identities satisfy the same defining conditions, so uniqueness makes those composites identities. This one argument explains the uniqueness of categorical products, categorical limits, adjoint functors and many other constructions. It also specifies which isomorphism is canonical, a point that an arbitrary objectwise choice would miss.
The Yoneda lemma makes this perspective systematic. A natural transformation out of is determined by its value at . Once that evaluation principle is recognized, questions about representable functors reduce to compositions in the original category. Similarly, the Beck monadicity theorem organizes many free-and-forgetful constructions around monad algebras, reflection of isomorphisms and specified coequalizers. The proof supplies a reusable explanation of why the algebraic structure can be reconstructed from the forgetful functor.
The substantial work lies in finding suitable definitions and verifying their hypotheses. The Freyd general adjoint functor theorem, for instance, needs completeness, local smallness and a solution set; none follows merely from calling a construction natural. The partial-operation tower below even has a monadic length that records how many distinct reconstruction steps are needed. These examples support the view that abstraction clarifies the source of an argument's simplicity. They also show why that simplicity is an achievement requiring proof.
Both alternatives can be proved using the same smallness mechanism. We first establish the initial-object lemma for complete categories with a weakly initial set, then obtain the two adjoint functor existence theorems and their applications.
Let be a locally small category with all small categorical limits and a weakly initial set . Its product in a category is weakly initial: given any object, choose a map from some and compose with the corresponding projection. Take the simultaneous equalizer of every endomorphism of and its identity; local smallness makes this a small categorical limit. Then is also weakly initial. If , form their equalizer and choose . Since is an endomorphism of , the construction of gives . Cancelling the monomorphism yields . Thus is both a monomorphism and a split epimorphism, hence invertible, and . There is therefore exactly one arrow from to every object: is initial.
The Freyd general adjoint functor theorem says that for a functor between locally small categories, with complete, a left adjoint exists exactly when preserves all small categorical limits and satisfies the solution-set condition. That condition requires, for each , a set of arrows such that every factors as for some and .
For sufficiency, the comma category is locally small and complete: form a diagram's categorical limit in , and use categorical limit preservation to obtain its arrow from . The solution set is a weakly initial set in this comma category. The lemma provides an initial object . Its universal property gives
For , define by . Uniqueness proves the identity and composition laws and naturality of the displayed bijections, hence . Conversely, an adjunction makes preserve categorical limits, since the corresponding hom-set functors turn a categorical limit cone into a categorical limit of sets. The single arrow is a solution set. This proves both directions of the theorem.
Now let have small domain and codomain. The functor categories and are locally small, and their categorical limits are pointwise. Thus the precomposition functor preserves categorical limits and its domain is complete. To verify its solution-set condition, fix and an arrow . Let be the subfunctor generated by all elements , where and . Explicitly,
These sets are stable under every . If is an infinite cardinal bounding and , every has cardinal at most . Replace each such set by a subset of a fixed set of size . There is only a set of choices of these subsets, of their action maps for the set of arrows of , and of maps from to their restrictions. These coded pairs form a solution set: factors through and then the inclusion . The general theorem now yields
Its values may also be written , the usual left Kan extension formula.
For the other alternative, the categorical limit form of the Special adjoint functor theorem says that a limit-preserving functor has a left adjoint if is locally small, complete and well-powered, has a cogenerating set , and is locally small. A cogenerating set means that maps into its members distinguish any two parallel arrows. The dual theorem says that a colimit-preserving functor from a locally small, cocomplete, well-copowered category with a small generating family has a right adjoint. These conclusions are also necessary in their preservation clauses.
Here is a proof of the special theorem rather than an invocation of the general theorem without its required solution set. Given , intersect all subobjects through which factors after application of . There are only a set of them by well-poweredness. Their intersection is a wide pullback, preserved by , so gives a smallest supporting pair . If satisfy , their equalizer is a supporting subobject. Minimality makes that equalizer invertible, whence . Consequently
is injective. The cogenerating property makes the evaluation arrow from into the product in a category of the , one factor for each map , a monic arrow. Its indexing set at each is identified with a subset of the fixed set . Only a set of such products in a category can occur. Each has only a set of subobjects, and each possible subobject has only a set of arrows from into its image under . These pairs give a weakly initial set in , since every original pair receives the arrow from its minimal supporting pair. The complete-category lemma now gives the adjoint. Reversing all arrows proves the colimit form of the special theorem.
Apply that dual form to . Its domain is cocomplete and locally small, and preserves pointwise colimits. The set of covariant representable functors generates the domain: by the Yoneda lemma, maps from these representables probe every element at every object and hence distinguish distinct natural transformations. Finally, epimorphisms in this functor category are pointwise surjective. Indeed, their pointwise images form subfunctors; if an image is proper, the two inclusions into the pointwise pushout of two copies of the target over that image distinguish the original map, contradicting epicity. Quotients of a fixed functor are therefore specified by compatible equivalence relations on its sets of values, and form a set. Thus the domain is a well-copowered category. All special-theorem hypotheses hold, giving
Here the Right Kan extension can be written . In particular both requested adjoints exist, although the two proofs use different smallness hypotheses.
Definitions organize category theory, but theorems give that organization mathematical force. I would therefore argue against treating the subject as an exception in which definitions are intrinsically more important than theorems. The distinction is especially misleading here because good categorical definitions are designed to expose hypotheses from which substantial theorems follow.
A category records objects, composable arrows, identities and associative composition. A functor preserves that structure. This language allows one to compare otherwise different mathematical settings, but it does not itself say which constructions exist. For example, the definition of a product in a category is not a recipe for forming a Cartesian product of underlying sets: it requires a universal factorization of pairs of arrows. If two products in a category and exist, the universal properties give unique arrows and respecting projections. The composites and respect the same projections as the identities, so uniqueness forces them to be identities. Thus a definition yields a genuine theorem: products in a category are unique up to unique compatible isomorphism. The proof matters because it licenses replacing a construction by any other realization of the same property.
The Yoneda lemma is a more substantial example. For a covariant representable functor and , a natural transformation is determined by . Naturality forces
Conversely this formula defines a natural transformation for every . Hence . The definition of naturality is indispensable, but the theorem identifies every possible transformation, proves representables detect arrows, and explains why universal objects can be studied through hom-sets. Merely knowing the definition does not supply this conclusion.
Similarly, an adjunction is defined by natural hom-set bijections. The construction of a free abelian group gives , because a group homomorphism is determined uniquely by its values on the basis. This makes a universal extension problem transparent. But the Freyd general adjoint functor theorem goes further: it turns categorical limit preservation and a solution set into an actual adjoint. Its smallness hypotheses cannot be discarded as bookkeeping. For instance, the underlying-set functor from finite groups to finite sets has no left adjoint at a singleton. A putative universal finite group with universal element of order could not map that element to a generator of a finite cyclic group of order greater than . The theorem's hypotheses separate existence from attractive notation.
The monoidal coherence theorem offers another example. A monoidal category has associativity and unit isomorphisms satisfying the pentagon identity for a monoidal category and triangle identity for a monoidal category. Coherence proves that every formal reassociation and unit insertion produces the same structural map. This is what justifies calculating without displaying all parentheses; it is not true merely because one has named an associator. Nor does it identify arbitrary additional maps, such as distinct braidings.
Finally, the opposite category construction shows how a definition can economize on proofs: reversing arrows takes products in a category to coproducts in a category, initial objects to terminal objects and monads to comonads. Yet this economy works because theorems and their proofs are invariant under the reversal. The subject is powerful precisely when definitions isolate reusable structure and theorems establish its consequences. Separating their importance obscures that partnership.
The Freyd general adjoint functor theorem is as follows. Let , with a complete category which is locally small. Then has a left adjoint if and only if it preserves all small categorical limits and satisfies the solution-set condition: for each , there is a set-indexed family
such that every can be written for some and some . The target category need not be complete. We prove all the existence steps.
First establish the initial-object lemma for complete categories with a weakly initial set. Let be locally small and complete, with a weakly initial set , meaning every object receives a map from at least one . Its categorical product is weakly initial: compose a categorical product projection with the map from the appropriate . Local smallness makes a set. Let be the simultaneous equaliser of every endomorphism of and the identity. Explicitly it is the equaliser of the two arrows
with components and . Thus for every endomorphism , and is monic.
Every object receives a morphism from , by composing with a map . To prove uniqueness, take parallel maps and their equaliser . Weak initiality of gives . The composite is an endomorphism of , so . Cancelling the monomorphism gives . Hence is both monic and a split epimorphism, and is therefore invertible. Since , this forces . We have proved is initial, without using a class-sized categorical product or equaliser.
For sufficiency in the theorem, fix and consider the comma category . Its objects are pairs ; a morphism satisfies . This category is locally small because each hom-set is a subset of . It is complete: for a small diagram of such pairs, take the underlying categorical limit in . The arrows from form a cone to its image under , and preservation of the categorical limit gives a unique inducing them. The same universal property gives all mediators in the comma category. The solution-set family is a weakly initial set in this comma category, so the lemma supplies an initial pair
For , initiality defines a unique satisfying . Uniqueness proves the identity and composition laws, making a functor. Initiality also gives bijections
The definition of proves naturality in , and postcomposition proves naturality in . These bijections are the required adjunction .
For necessity, if , the single arrow is a solution set: the transpose of any gives its factorization through . If is a limiting cone vertex of a small diagram in , then, naturally in ,
These are the canonical cone-factorization bijections, so with its image projections is a categorical limit of . Thus preserves all small categorical limits, completing both directions of the theorem.
For , the comma category has objects with and . A morphism is satisfying . Identities and composition are those of , and functoriality of verifies the condition under composition.
The Freyd general adjoint functor theorem states: if is a locally small category with all small categorical limits, and is locally small, then has a left adjoint if and only if it preserves small limits and satisfies the solution-set condition. The latter means that for each there is a set-indexed family such that every equals for some and some .
For necessity, use the standard result that a right adjoint preserves categorical limits. If , the singleton family containing the unit of an adjunction is a solution set, since transposition gives for a unique .
For sufficiency, use the following standard limit fact: if is complete and preserves limits, the projection creates small limits. Indeed, a compatible family induces a unique arrow into , and this makes the underlying limit a limit in the comma category. The comma category is locally small because each of its hom-sets is a subset of a hom-set of . Its solution family is a weakly initial set.
We prove the remaining initial-object lemma for complete categories with a weakly initial set. In any locally small category with all small limits and a weakly initial set , form . It is weakly initial: for any , some exists and may be composed with the projection . The empty family cannot be weakly initial in a nonempty complete category, which has a terminal object.
The set is small. Form a simultaneous equalizer of every endomorphism of and ; thus
This equalizer exists by completeness, for example as the equalizer of two maps . The object is still weakly initial, since it maps to .
Given , take their equalizer . Weak initiality of gives . Since is an endomorphism of , we have , and cancellation of the monomorphism gives . Thus is a split epimorphism as well as a monomorphism, so it is an isomorphism. From follows . There is at least one map by weak initiality, so is initial.
Apply this lemma to every and choose its initial object . For , initiality gives the unique satisfying . Uniqueness proves the functor laws. The same initiality gives natural bijections
Hence , completing the theorem without invoking another adjoint functor theorem.