A note on the definition of derived functors

TL;DR

This paper clarifies the classical construction of derived functors, formalizes it within ZFC set theory, and extends the framework to general Grothendieck categories beyond abelian groups.

Contribution

It provides a detailed clarification of derived functors' construction and extends the formalization to broader categorical contexts within ZFC.

Findings

Classical constructions are clarified and formalized in ZFC.

Extension of derived functors to general Grothendieck categories.

The approach does not rely on derived categories.

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.