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.
Here the usual homological algebra convention is that the right-exact functor is additive. Module categories have enough projective modules, because any module is a quotient of a free module. Choose a projective resolution
Apply to the unaugmented chain complex and define the left derived functors by
Additivity ensures that preserves zero maps, sums of maps and homotopy identities, so the transformed differentials still compose to zero.
For a module homomorphism , lift it to a chain map between chosen projective resolutions. In degree zero, lift through using projectivity of . In each higher degree, the already constructed map lands in the next kernel; exactness of and projectivity of supply the next lift. Any two lifts are chain homotopic: their degree-zero difference lands in , so it lifts to . Inductively lift the remaining difference after subtracting the preceding homotopy term. This gives
Applying preserves this identity, so the lifts induce the same homology map. Identity lifts and composable lifts show that is a functor. Comparison lifts between two resolutions over the identity of are inverse up to chain homotopy; hence the construction is independent of the chosen resolution up to its canonical natural isomorphism.
Right exactness identifies naturally with . For a projective module , the length-zero resolution gives for . For a short exact sequence , the horseshoe lemma builds a degreewise split short exact sequence of projective resolutions. Concretely, lift the projective generators covering into and combine them with generators covering ; repeat on the kernels. The middle projective term in each degree is the direct sum of the two outer ones. An additive functor preserves these split sequences, and lifting cycles, taking their differentials and returning to the subcomplex produces the connecting maps in
This is the natural long exact derived-functor sequence. In particular, if has projective, then for , and . These are dimension-shifting formulas. Positive degrees can be killed by the surjection . If is exact, it preserves every resolution's exactness and all its positive left derived functors vanish. Conversely, if vanishes on all modules, the displayed long exact sequence makes exact. A natural transformation between additive right-exact functors induces transformations on the left derived functors by applying it termwise.
For extension of scalars , these derived functors are the Tor functors . When and is a non-zero-divisor, there is the length-one free resolution
Although the construction above resolves , one may instead use this resolution of . To justify that calculation, tensor a free resolution of with the two-term resolution of to form a double complex. Taking homology first along the resolution of leaves ; taking it first along the resolution of leaves . The free terms preserve exactness under tensoring. The double complex is first-quadrant with finitely many terms on each total diagonal, so both filtrations compute the same total homology. This proves the required balancing directly.
The kernel and cokernel of multiplication by now give Tor for a principal non-zero-divisor quotient:
These are naturally -modules. For , the degree-one group is zero; for , multiplication by is zero and both degrees zero and one are . Thus, when , degree one explicitly detects the failure of this base-change functor to be exact.
In an abelian category with enough projectives, a projective object has a resolution concentrated in degree zero, so every first left derived functor vanishes on it. Conversely choose with projective and use the additive functor with target the opposite of the category of abelian groups. This functor is right exact in that target. If , the derived exact sequence makes monic, meaning that is surjective in abelian groups. Extending gives a retraction of , so the sequence splits and is a direct summand of the projective .
An additive functor between abelian categories is right exact functor when it sends every exact sequence to an exact sequence . Equivalently, it preserves cokernels in a category, since additivity already preserves finite biproducts. This is the convention used in constructing left derived functors. Left exactness preserves the initial part instead. Contravariant Hom becomes a right exact functor covariant functor with target the opposite abelian category.
An additive functor between abelian categories is right exact when it preserves categorical cokernels, equivalently when it sends every exact sequence ending in zero to an exact sequence ending in zero. Additivity and preservation of cokernels in a category imply preservation of finite colimits. The additivity assumption is part of the ordinary left derived functor construction.