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.
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 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.
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.
A monad on consists of an endofunctor and natural transformations , satisfying and . Its Eilenberg-Moore category has objects with , and . A morphism satisfies . An adjunction , with unit and counit , induces , . It is a monadic adjunction if the Eilenberg-Moore comparison functor is an equivalence with the Eilenberg-Moore category.
A fork is a split coequalizer if and there are , with , and . It is indeed a coequalizer: if , then , so factors uniquely through , which is split epic. Every functor preserves these splitting identities, making such coequalizers absolute.
The precise monadicity theorem states: for an adjunction , the comparison is an equivalence if and only if reflects isomorphisms and every pair in whose -image admits a split coequalizer has a coequalizer which preserves. Equivalently, the right adjoint creates these split-underlying coequalizers, with creation understood up to the canonical isomorphism of the prescribed underlying coequalizer. Here is a proof.
First consider the forgetful functor from monad algebras. It reflects isomorphisms: the inverse of an invertible algebra morphism also obeys the algebra-morphism identity, by multiplying that identity by the inverses. For an algebra pair with a split underlying coequalizer , all powers of preserve its coequalizer. If is the algebra structure on , the map coequalizes , so there is a unique with
The unit law follows by composing with the epimorphism : . For associativity, naturality and the algebra law give
Cancel the epimorphism to obtain . Thus is an algebra and is an algebra morphism. Any algebra morphism coequalizing the pair factors through on underlying objects, and its factor is an algebra morphism by cancellation of the epimorphism . This creates the coequalizer. Transporting these facts through an equivalence proves necessity.
For sufficiency, let be a -algebra. In consider the free pair
Its underlying pair is , with split coequalizer : the splittings are and , using the algebra unit law, the monad unit law and naturality of . By hypothesis its coequalizer exists and is preserved. Identify with by the unique coequalizer isomorphism, so . Naturality of the counit makes an algebra morphism, hence the comparison structure on satisfies . The map is split epic because , so . Every algebra is therefore isomorphic to a comparison algebra.
For an actual object , its counit is a coequalizer of the analogous free pair. It coequalizes that pair by counit naturality. Compare it with the coequalizer furnished by the hypothesis; applying gives an isomorphism, since both underlying arrows coequalize the same split pair. Reflection of isomorphisms makes the comparison map an isomorphism. This proves the counit's asserted coequalizer property.
Let be an algebra morphism. Its transpose is . The two composites of with the free pair have adjunct transposes and , equal because is an algebra morphism. Consequently factors uniquely through as . Applying gives ; the last factor is split epic, so . Conversely any lift of must satisfy by naturality and hence is unique. Thus is full and faithful, and the earlier construction makes it essentially surjective. The comparison is an equivalence, completing the theorem's proof.
Now take . Its left adjoint exists by the permitted topological result; it can be realized as the Stone-Čech compactification of the discrete input set. A bijective continuous map from a compact space to a Hausdorff space is a homeomorphism, so reflects isomorphisms.
For continuous with a split underlying fork , let be the relation of having the same -image. We claim
For the forward inclusion choose , : and supply the equality. For the reverse inclusion use . The subset is closed, because is Hausdorff, and compact. Its continuous image is compact and hence closed. A closed equivalence relation on a compact Hausdorff space has a compact Hausdorff quotient; its quotient map is a coequalizer here, since it identifies exactly the generated relation. Its underlying set coequalizer is the specified one up to the unique isomorphism. Thus preserves the needed coequalizers, and
The closedness argument is the closed relation generated by a set-split pair of compact Hausdorff maps lemma; the splitting maps themselves need not be continuous.
Theorems matter at least as much as definitions: they show when a categorical description captures actual mathematical structure. Definitions in category theory are exceptionally economical, but economy alone does not explain their applications.
An adjunction compresses a universal mapping property into natural hom-set bijections. The free-group adjunction, for example, records that assigning images to generators extends uniquely to a homomorphism. That is a useful definition, but proving that a free group exists and satisfies this property still requires mathematics. The definition organizes that proof rather than replaces it.
The Yoneda lemma offers a sharper example. A representable functor is easy to define; the theorem identifying natural transformations out of it with elements of another functor gives the definition its computational force. The representation of a set-valued functor as a colimit of representables is then a substantive consequence, and the theorem that filtered colimits commute with finite limits turns it into a criterion for finite-limit preservation. None of these conclusions follows merely from choosing attractive terminology.
Likewise a monad packages operations and their compatibility, while the Eilenberg-Moore category defines the corresponding algebras. The Beck monadicity theorem answers a different question: whether a given category is really recovered by that algebraic description. Applying it to compact Hausdorff spaces needs a topological argument about closed quotient relations. The definitions would not by themselves predict or justify the result.
Finally, abelian categories put kernels in a category, cokernels in a category and exactness into a setting where homological arguments can be reused. Some consequences, such as image factorization, become short because strong structural content has deliberately been included in the definition. Yet left derived functors, long exact sequences and the detection of projective objects supply information about obstructions to exactness which the terminology alone cannot provide.
Definitions and theorems therefore play complementary roles. A good definition states what should be invariant across examples; a theorem proves which constructions preserve it, which examples satisfy it, and what can be deduced from it. Category theory makes that partnership unusually visible, rather than making proofs less important.
A balanced category is one in which every morphism that is both monic and epic is an isomorphism. If a faithful functor sends to an isomorphism, then is monic: equality becomes , cancellation gives , and faithfulness gives . The same argument on the other side makes epic. Balance therefore makes an isomorphism. Thus a faithful functor out of a balanced category reflects isomorphisms.
Under the adjunction, the transpose of is . Hence if is faithful, forces and then , making every monic. Conversely, if the unit is pointwise monic and , naturality gives , whence . Therefore
We also use the standard adjunction fact with its justification: is full and faithful exactly when is invertible. Indeed the composite hom-set map is postcomposition by . If is full and faithful these maps are bijective; taking produces a right inverse, and taking gives injectivity and therefore a left inverse. Conversely an invertible unit makes these hom-set maps bijective.
For the final example, view the two-element ordered set as a category , and let have one object and only its identity. The unique is left adjoint to the functor selecting , since every is a singleton. Every arrow in an ordered-set category is monic, so the unit arrows and the identity counit are monic. But is not full: is empty whereas is a singleton. The example does not contradict the upcoming equivalence because is not balanced; its arrow is both monic and epic but not invertible.
Since the full endofunctor subcategory contains and is closed under composition, all belong to it. Terminality supplies unique natural transformations and . The monad unit laws compare arrows , both necessarily the unique endomorphism, namely the identity. The associativity law compares arrows , again necessarily equal. Every monad structure uses these two unique arrows, so .
For a monad with underlying functor in the subcategory, the unique is a monad morphism. Its unit and multiplication compatibility compare, respectively, arrows and and therefore follow from terminality. A -algebra restricts to the -algebra . The unit law is immediate. For multiplication, naturality and the monad-morphism law give
An algebra morphism for also commutes with the restricted action by naturality of . Keeping underlying objects and arrows gives the required functor .
Now define to be the set of ultrafilters on , and for define
Inverse images preserve inclusions, intersections and complements, so this is an ultrafilter; composition of inverse images makes a functor. There are no ultrafilters on the empty set. Every ultrafilter on a disjoint binary union chooses exactly one summand, and restriction to that summand gives an ultrafilter there; extension back is inverse to restriction. Hence canonically, and preserves finite coproducts, including the empty one.
Let be any other finite-coproduct-preserving endofunctor. For , put
The decomposition and coproduct preservation show that exactly one of belongs. Refining two subsets into the four disjoint parts shows that an element lying in both indicated summands lies in their intersection summand. The same refinement for proves upward closure. Thus is an ultrafilter. For , decomposition by and its complement shows
proving naturality.
For uniqueness, suppose is natural. Since is a singleton, naturality on the two inclusions forces to send every element in each of the two summands of to the corresponding principal ultrafilter. Apply naturality to the characteristic map . It gives precisely when lies in the selected summand, which by the decomposition is precisely when lies in . Hence for every . Therefore
This proves ultrafilter functor. For clarity, the resulting unit sends to its principal ultrafilter; multiplication sends an ultrafilter on to the ultrafilter whose members are with . Naturality and the monad laws for these formulas also follow from the terminal construction.
Throughout the algebraic questions, is a smooth projective connected algebraic curve over the algebraically closed field . This is the curve convention needed for the Jacobian variety; for an arbitrary singular or nonproper curve the assertions need not hold. Choose and write .
The degree- Picard functor of a curve is
with pullback as its action on morphisms. Equivalently, normalize by tensoring with and remember the resulting trivialization along . Since , an automorphism of a line bundle is multiplication by a base unit; preservation of this trivialization forces that unit to be . Thus normalized line bundles have effective descent and the displayed functor is already the appropriate sheaf, rather than just a list of classes over fields.
Here is a construction of its representing scheme. The symmetric product of a curve represents relative effective degree- Cartier divisors. It is projective, and its completed local ring at is a power-series ring in the elementary symmetric coefficients of local parameters at each . Thus it is smooth of dimension , in every characteristic. Put
This is open by the semicontinuity theorem for coherent cohomology. It is nonempty: choose points successively imposing independent vanishing conditions on , so that , and use Serre duality. The Riemann-Roch theorem gives on .
For any fixed line bundle of degree , use a copy of with the universal normalized line bundle . This represents exactly the open subfunctor on which . Indeed, cohomology and base change for line bundles on a curve makes a rank-one vector bundle. The evaluation morphism
has a unique relative zero Cartier divisor of degree and recovers the point of . No choice of a global generator on is needed. Conversely that zero Cartier divisor recovers modulo a bundle from .
These charts cover: given any degree- line bundle , choose a nonspecial effective degree- Cartier divisor and take . On the overlap of and , the unique effective representative of is constructed by the same rank-one evaluation map. It therefore gives a regular transition morphism; uniqueness gives both the inverse and the cocycle identity. Gluing gives a scheme representing , with a universal normalized line bundle.
The construction is of finite type, not an infinite union of indispensable charts. Choose and a fixed line bundle of degree . Every has a nonzero section by the Riemann-Roch theorem, so the universal effective Cartier divisor gives a surjection . The inverse images of the charts cover the projective, hence quasi-compact, symmetric product of a curve . A finite subcover gives finitely many charts for . This surjection also makes irreducible. The charts show that it is smooth of dimension .
For properness, apply the valuative criterion for properness. Let be a discrete valuation -algebra with fraction field , and let be a degree- line bundle on . A rational section represents it by a Cartier divisor. Its closure in the regular surface is again a Cartier divisor, since regular local rings are factorial. Thus extends to a line bundle on , whose fibre degree remains by constancy of line bundle degree in a family. Two extensions with the same generic class differ by a vertical Cartier divisor. The special fibre is irreducible, so that Cartier divisor is an integer multiple of the entire fibre, the principal Cartier divisor of a power of a uniformizer. The extensions therefore give the same normalized Picard class. This proves existence and uniqueness in the valuative criterion, hence separatedness and properness of the finite-type scheme .
Consequently is a smooth proper -variety of dimension . Tensoring by identifies it with . On the tensor product and inverse of line bundles induce the algebraic group operations; it is the Jacobian variety, an abelian variety.
Let be the unique arrow to the terminal object of . Define
This is a functor into the slice category , because , and . The terminal object of this slice is , exactly , so preserves the terminal object.
The composite preserves pullbacks by hypothesis, and reflects pullbacks by part (b). Part (a), restricted to the pullback shape, therefore shows that preserves pullbacks. The allowed finite-limit criterion now gives that preserves all finite categorical limits, and hence equalisers. Since preserves equalisers, their composite does too. Thus
This is equalizer preservation by pullback-preserving functors. The factorization supplies terminal-object preservation only in the slice; none is asserted for the original .
For a diagram shape , a functor preserves categorical limits of shape if every limiting cone over every diagram is carried to a limiting cone over . It reflects categorical limits of that shape if a cone in is limiting whenever its image cone is limiting. These properties concern cones which are given; reflection is not an assertion that every cone in the target lifts.
Suppose is a full and faithful functor and the image of is limiting. A cone in becomes a cone in , so there is a unique with . Fullness writes for some . Faithfulness gives , and also ensures uniqueness: two such would have the same image, by uniqueness of . Hence the original cone is limiting. This proves every full and faithful functor reflects categorical limits, the limits reflected by full and faithful functors criterion, with no essential-surjectivity requirement.
For a categorical presheaf on the open subsets, define the functors on objects by
To prove , a natural transformation must satisfy
for every open , since the restrictions of are identities. Thus it is determined by the function . Conversely such a function defines all by that equation, and the categorical presheaf restriction laws make the components compatible. Hence
For the other adjunction, a transformation is determined by its component , since
Every function supplies compatible components by this formula. Therefore , giving the adjoints to constant presheaves on open sets:
These are adjoints of the stated constant-presheaf functor, with its value at every open set including the empty one; no sheafification is involved.