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.