# Commit 2021-07-03 16:33 531d8504

View on Github →feat(category_theory): left-derived functors (#7487)

# Left-derived functors

We define the left-derived functors `F.left_derived n : C ⥤ D`

for any additive functor `F`

out of a category with projective resolutions.
The definition is

```
projective_resolutions C ⋙ F.map_homotopy_category _ ⋙ homotopy_category.homology_functor D _ n
```

that is, we pick a projective resolution (thought of as an object of the homotopy category),
we apply `F`

objectwise, and compute `n`

-th homology.
We show that these left-derived functors can be calculated
on objects using any choice of projective resolution,
and on morphisms by any choice of lift to a chain map between chosen projective resolutions.
Similarly we define natural transformations between left-derived functors coming from
natural transformations between the original additive functors,
and show how to compute the components.

## Implementation

We don't assume the categories involved are abelian
(just preadditive, and have equalizers, cokernels, and image maps),
or that the functors are right exact.
None of these assumptions are needed yet.
It is often convenient, of course, to work with `[abelian C] [enough_projectives C] [abelian D]`

which (assuming the results from `category_theory.abelian.projective`

) are enough to
provide all the typeclass hypotheses assumed here.