A note on the definition of derived functors
João Schwarz
TL;DR
The paper addresses the foundational problem of defining and functorializing derived functors in ZFC, extending to Grothendieck targets, and avoiding set-theoretic issues of the traditional approach. It formalizes δ-functors in ZFC and demonstrates that left derived functors $L_n(F)$ can be constructed as limits over a small category of minimal-rank projective resolutions using Scott's trick, with $L_n(F)(M)=\mathrm{Lim}_{\mathcal{I}} H^n(F(P_i))$. The construction is shown to be functorial in morphisms and to satisfy Grothendieck's δ-functor axioms, all without invoking the axiom of choice beyond what's available in ZFC, and while generalizing to targets in any Grothendieck category via Gabriel-Popescu. The work contrasts with the conventional derived-category approach, clarifies foundational issues, and discusses metamathematical considerations and open questions about extending the formalism to broader abelian targets.
Abstract
The purpose of this note is to consider in detail the construction of derived functors. The classical construction, such as in Cartan-Eilenberg or Grothendieck, is clarified, and it is shown, at the same time, that everything can be formalized in ZFC, unlike the approach using derived categories. Our work is done in a more general context in which the codomain of our functors is any Grothendieck category, not necessarily abelian groups.