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.
Write the square as , with final and a discrete fibration. For , choose an object of the nonempty comma category . Lift uniquely to an arrow
over , and tentatively put .
A morphism in this comma category is an arrow with . The composite is a lift of with codomain . Uniqueness of lifts gives , including equality of their source objects. Since the comma category is connected by zigzags, is independent of the choice. Thus is well defined and .
For , take . Lift into , obtaining . Composing with gives a lift of into , whose source must be . Hence . Set . Uniqueness of this lift makes the definition independent of the chosen comma object and proves and .
At , choose . Its lift is , so . For , is the unique lift of into , so . We have constructed the required functor with and .
If is another filler, must equal by unique lifting. Thus for every object. Its arrows are then forced by unique lifting into those objects. Therefore
This proves the orthogonality of final functors and discrete fibrations.
For each , let , the collection of connected components, where connectedness means connection by a zigzag of arrows. Precomposition with gives a function . Identity and composition are inherited from precomposition.
Construct a category whose objects are pairs with . An arrow is an arrow satisfying . Composition is that of , and the component equation is preserved by composition. The projection is a discrete fibration: an arrow has precisely one lift into , namely the arrow from represented by .
Define by
This is well defined because and lie in the same component of whenever . Clearly .
For an object of , an object of is exactly a pair representing the component . Its morphisms are exactly the arrows in between such objects. Thus this comma category is the component itself, which is nonempty and connected. This proves that is a final functor, and hence
This is the final-discrete-fibration factorization. For small categories the collections are sets and this construction is the category of elements of the presheaf . For categories of a larger size, the construction is interpreted in the same chosen ambient size framework.
Suppose are two such factorizations, with final and discrete fibrations. Apply the unique diagonal construction to the square with left side , top , bottom and right side . It gives a unique functor such that and . Reversing the two factorizations gives with and .
Both and fill the square with left side , top , bottom and right side . Uniqueness from part (i) gives . Similarly . Thus
In particular the conclusion is a canonical isomorphism of intermediate categories, not just an unspecified equivalence.
Write the monad identities as
If is invertible, its two right inverses agree, so . Conversely, suppose . Naturality of at , followed by that equality at , gives
Together with this proves
This is the equivalence defining an idempotent monad.
For the equalizer submonad of a monad, let equalize and . If , naturality of these two transformations shows that equalizes the corresponding pair at . There is therefore a unique satisfying
Uniqueness gives and , so is a functor and is a natural transformation.
Take the stipulated factorizations and . Naturality of at rewrites their defining equations as
The composites on the right are natural in ; cancellation of the monic arrow therefore makes and natural. We now verify every monad law, rather than assuming that restricting the structure automatically preserves them.
For the two unit laws, naturality and the unit laws of give
Cancelling proves . For associativity, the same naturality equations give
These are equal by associativity of ; cancelling proves associativity of . Thus
The remaining claims use two split equalizers associated with a monad. First, is a split equalizer of . Its retraction is , and the splitting of the parallel pair is , since
The equalizing equation follows from naturality of . In general, identities , , and prove that is an equalizer: if , then , with unique factorization . Hence and are two equalizers of the same pair. Their comparison is , and its inverse is . In particular
Second, is a split equalizer of , with retraction and splitting . Indeed,
This is precisely the parallel pair in the PDF's diagram after . The map equalizes that pair, because applying to the defining equalizer equation gives their equality on . Put
The split-equalizer factorization and give
If is invertible, then is a monic arrow. Conversely, if is a monic arrow, the equation
forces , so is the inverse of . Therefore
Notice that, under either condition, is actually a split monomorphism, with retraction . Thus is a monic arrow too, since a functor preserves split monomorphisms. We have not assumed that preserves arbitrary monomorphisms.
Now prove the specified naturality square is a pullback in a category. Let and satisfy . Naturality of , followed by the equalizer equation for , gives
Cancel the monic arrow . Thus equalizes and factors uniquely as with . Naturality of then gives
Cancel to obtain . This is exactly existence and uniqueness in the pullback universal property.
Because the square is a pullback and is a monic arrow, is a monic arrow. Naturality of and the formula for now give
Cancelling proves . The other composite is already one of the unit laws. Hence is invertible. If the equivalent monicity conditions hold for every , we conclude
A preadditive category has an abelian-group structure on every hom-set and bilinear composition. One equivalent definition of an additive category is a preadditive category with a zero object and finite products in a category; the following argument proves that these products in a category are automatically coproducts in a category. An abelian category is an additive category with kernels and cokernels in which every monomorphism is a kernel and every epimorphism is a cokernel. Equivalently, for every arrow the canonical map from its coimage to its image is invertible.
Let , with projections . Define by , where the diagonal entry is the identity and the others are zero. Since its composites with all projections are identities,
Given , the map satisfies . If another map has those composites, multiplying the displayed identity by that map forces it to equal . Thus is also a coproduct in a category. The empty case is the zero object. Reversing arrows proves that a finite coproduct in a category is likewise a product in a category. Hence finite products in a category and coproducts in a category are canonically biproducts in an additive category.
For the category of abelian groups, let be a directed diagram, with no injectivity assumption on its transition maps. Its set colimit consists of classes , with
Directedness proves transitivity of this relation. Define addition by moving representatives to a common upper index:
Moving all indices involved to one further upper bound proves independence of representatives and of . Define and use the common class of the zeros as zero. The abelian-group laws hold at a common index, so descend to the quotient. Every canonical map is a homomorphism, and a compatible cocone induces the homomorphism . This is the unique extension. Moreover the formula for addition is forced by those canonical homomorphisms, proving that the underlying-set functor creates directed colimits. This establishes directed colimits created by the abelian-group forgetful functor explicitly.
If a cocone has injective legs, the induced map is injective. Indeed, equal images of and give, at a common index ,
Injectivity of gives equal representatives at . Since monomorphisms of abelian groups are exactly injective homomorphisms, we have proved that the category of abelian groups is a finitary abelian category in the directed-union sense of the question.
Now let be complete, cocomplete and finitary. Index by finite subsets and put . For , insert the additional zero coordinates. A compatible cocone on these finite biproducts is exactly a family of maps from every , so their directed colimit is .
Each finite biproduct has a map using its coordinates in and zeros outside . Projection to the finite set of coordinates in is a retraction, so is a split monomorphism. These maps form a cocone of monomorphisms. The finitary property makes its induced map a monic arrow, and that induced map is exactly the canonical infinite identity matrix:
This proves the coproduct-to-product comparison in a finitary abelian category. The PDF's use of finite products in a category in the hint is valid because these are the same finite biproducts.
If is also a cofinitary abelian category, apply this argument in its opposite category. The same canonical comparison is then an epic arrow in . In an abelian category an arrow that is both a monomorphism and an epimorphism is invertible, so is an isomorphism.
For countably many copies of , put and let , where is the product in a category diagonal. Let denote the coproduct in a category injections, let shift them by , and let be the codiagonal. Comparing every product in a category coordinate gives
Since is a monic arrow, . Also and . Therefore, for ,
Hom-sets are abelian groups, so cancellation gives . Any arrow to or from is consequently zero by composition with its identity. Thus every object is both initial and terminal, and
This is the countable shift-and-fold argument behind countable biproducts in an additive category force triviality.
A monoidal category consists of a category , a bifunctor , a unit object , and natural isomorphisms
The associator and unitors satisfy the pentagon identity for a monoidal category and triangle identity for a monoidal category
All compositions here have the displayed parenthesized sources and targets; no strictness assumption is being made.
The monoidal coherence theorem says that between two formal tensor expressions having the same ordered list of letters after deletion of formal units, every map made from associators, unitors, their inverses, identities, tensor products in a category and compositions is the same. Thus every diagram of such structural maps commutes. It does not permit permutation of letters or identify different additional maps such as braidings.
We prove this by canonical normalization. We first derive three necessary unit identities from the axioms, avoiding a circular appeal to coherence:
For the first identity, take the pentagon on and postcompose by . Naturality of and the triangle identify its left-hand path as ; they identify its right-hand path as
Cancel . Taking permits cancellation of the operation , since the natural isomorphism makes that functor faithful. This proves the first identity. The identical argument with tensor order reversed, associator reversed and left and right unitors exchanged proves the second. Finally, naturality of at the map gives , after cancellation of . Apply the second identity at and compare with the triangle at to obtain . Set and use the same faithfulness to conclude . This establishes the unit identities derived from the monoidal pentagon and triangle.
For an ordered word , define a right-associated normal tensor, including a terminal unit, by
Define canonical concatenation maps recursively:
All these maps are invertible. The derived unit identities give, by induction on ,
The empty base case is ; the induction step is exactly the right-unitor identity above.
A second induction, again on , proves the concatenation identity
For , naturality of and give the equality. For , expand each occurrence with first word beginning in by the recursive formula. Naturality moves the maps and through the associators. The two paths of associators on agree by the pentagon; the remaining maps inside the factor agree by the induction hypothesis for . This proves the concatenation identity for every triple of words, including empty words.
For a formal tensor expression , let be its ordered word after deleting formal units. Define an isomorphism recursively by
Here the first case means a formal letter , and the second means the distinguished formal unit. Applying the concatenation identity and naturality of gives
Similarly, naturality of the unitors and the two empty-word concatenation identities give
Thus normalization commutes with each generating associator or unitor. It also commutes with their inverses. The recursive tensor formula shows the same for a generating map applied inside any larger tensor expression, and composition preserves the property. Consequently every structural map satisfies , whence
This depends only on the source and target expressions, so any two structural paths agree. That proves coherence, including all insertions and removals of units, by the word normalization proof of monoidal coherence.

Articles by others on the same topic (0)

There are currently no matching articles.