# Commit 2021-05-31 13:18 7fe456d8

View on Github →feat(algebra/homology): projective resolutions (#7486)

# Projective resolutions

A projective resolution `P : ProjectiveResolution Z`

of an object `Z : C`

consists of
a `ℕ`

-indexed chain complex `P.complex`

of projective objects,
along with a chain map `P.π`

from `C`

to the chain complex consisting just of `Z`

in degree zero,
so that the augmented chain complex is exact.
When `C`

is abelian, this exactness condition is equivalent to `π`

being a quasi-isomorphism.
It turns out that this formulation allows us to set up the basic theory derived functors
without even assuming `C`

is abelian.
(Typically, however, to show `has_projective_resolutions C`

one will assume `enough_projectives C`

and `abelian C`

.
This construction appears in `category_theory.abelian.projectives`

.)
We show that give `P : ProjectiveResolution X`

and `Q : ProjectiveResolution Y`

,
any morphism `X ⟶ Y`

admits a lift to a chain map `P.complex ⟶ Q.complex`

.
(It is a lift in the sense that
the projection maps `P.π`

and `Q.π`

intertwine the lift and the original morphism.)
Moreover, we show that any two such lifts are homotopic.
As a consequence, if every object admits a projective resolution,
we can construct a functor `projective_resolutions C : C ⥤ homotopy_category C`

.