Projective resolutions

A projective resolution P : ProjectiveResolution Z of an object Z : C consists of an ℕ-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 of derived functors without even assuming C is abelian.

(Typically, however, to show HasProjectiveResolutions C one will assume EnoughProjectives C and Abelian C. This construction appears in CategoryTheory.Abelian.Projective.)

We show that given 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 projectiveResolutions C : C ⥤ HomotopyCategory C.

structure CategoryTheory.ProjectiveResolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] (Z : C) : Type (max u v)

• complex : ChainComplex C ℕ
• π : s.complex ⟶ (ChainComplex.single₀ C).obj Z
• projective : ∀ (n : ℕ), CategoryTheory.Projective (HomologicalComplex.X s.complex n)
• exact₀ : CategoryTheory.Exact (HomologicalComplex.d s.complex 1 0) (HomologicalComplex.Hom.f s.π 0)
• exact : ∀ (n : ℕ), CategoryTheory.Exact (HomologicalComplex.d s.complex (n + 2) (n + 1)) (HomologicalComplex.d s.complex (n + 1) n)
• epi : CategoryTheory.Epi (HomologicalComplex.Hom.f s.π 0)

A ProjectiveResolution Z consists of a bundled ℕ-indexed chain complex of projective objects, along with a quasi-isomorphism to the complex consisting of just Z supported in degree 0.

(We don't actually ask here that the chain map is a quasi-iso, just exactness everywhere: that π is a quasi-iso is a lemma when the category is abelian. Should we just ask for it here?)

Except in situations where you want to provide a particular projective resolution (for example to compute a derived functor), you will not typically need to use this bundled object, and will instead use

• ProjectiveResolution Z: the ℕ-indexed chain complex (equipped with Projective and Exact instances)
• ProjectiveResolution.π Z: the chain map from ProjectiveResolution Z to (ChainComplex.single₀ C).obj Z (all the components are equipped with Epi instances, and when the category is Abelian we will show π is a quasi-iso).

class CategoryTheory.HasProjectiveResolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] (Z : C) : Prop

• out : Nonempty (CategoryTheory.ProjectiveResolution Z)

An object admits a projective resolution.

class CategoryTheory.HasProjectiveResolutions (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] : Prop

• out : ∀ (Z : C), CategoryTheory.HasProjectiveResolution Z

You will rarely use this typeclass directly: it is implied by the combination [EnoughProjectives C] and [Abelian C]. By itself it's enough to set up the basic theory of derived functors.

@[simp]

theorem CategoryTheory.ProjectiveResolution.π_f_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) (n : ℕ) : HomologicalComplex.Hom.f P.π (n + 1) = 0

@[simp]

theorem CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P.complex 1 0) (HomologicalComplex.Hom.f P.π 0) = 0

@[simp]

theorem CategoryTheory.ProjectiveResolution.complex_d_succ_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P.complex (n + 2) (n + 1)) (HomologicalComplex.d P.complex (n + 1) n) = 0

instance CategoryTheory.ProjectiveResolution.instEpiXNatDownToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidStrictOrderedSemiringToOneCanonicallyOrderedCommSemiringComplexObjToQuiverToCategoryStructChainComplexToQuiverToCategoryStructInstCategoryHomologicalComplexToPrefunctorSingle₀Fπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) (n : ℕ) : CategoryTheory.Epi (HomologicalComplex.Hom.f P.π n)

def CategoryTheory.ProjectiveResolution.self {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] (Z : C) [CategoryTheory.Projective Z] : CategoryTheory.ProjectiveResolution Z

A projective object admits a trivial projective resolution: itself in degree 0.

def CategoryTheory.ProjectiveResolution.liftZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {Y : C} {Z : C} (f : Y ⟶ Z) (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z) : HomologicalComplex.X P.complex 0 ⟶ HomologicalComplex.X Q.complex 0

Auxiliary construction for lift.

def CategoryTheory.ProjectiveResolution.liftOne {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {Y : C} {Z : C} (f : Y ⟶ Z) (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z) : HomologicalComplex.X P.complex 1 ⟶ HomologicalComplex.X Q.complex 1

Auxiliary construction for lift.

@[simp]

theorem CategoryTheory.ProjectiveResolution.liftOne_zero_comm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {Y : C} {Z : C} (f : Y ⟶ Z) (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.liftOne f P Q) (HomologicalComplex.d Q.complex 1 0) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P.complex 1 0) (CategoryTheory.ProjectiveResolution.liftZero f P Q)

Auxiliary lemma for lift.

def CategoryTheory.ProjectiveResolution.liftSucc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {Y : C} {Z : C} (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z) (n : ℕ) (g : HomologicalComplex.X P.complex n ⟶ HomologicalComplex.X Q.complex n) (g' : HomologicalComplex.X P.complex (n + 1) ⟶ HomologicalComplex.X Q.complex (n + 1)) (w : CategoryTheory.CategoryStruct.comp g' (HomologicalComplex.d Q.complex (n + 1) n) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P.complex (n + 1) n) g) : (g'' : HomologicalComplex.X P.complex (n + 2) ⟶ HomologicalComplex.X Q.complex (n + 2)) ×' CategoryTheory.CategoryStruct.comp g'' (HomologicalComplex.d Q.complex (n + 2) (n + 1)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P.complex (n + 2) (n + 1)) g'

Auxiliary construction for lift.

def CategoryTheory.ProjectiveResolution.lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {Y : C} {Z : C} (f : Y ⟶ Z) (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z) : P.complex ⟶ Q.complex

A morphism in C lifts to a chain map between projective resolutions.

@[simp]

theorem CategoryTheory.ProjectiveResolution.lift_commutes_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {Y : C} {Z : C} (f : Y ⟶ Z) (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z) {Z : ChainComplex C ℕ} (h : (ChainComplex.single₀ C).obj Z ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.lift f P Q) (CategoryTheory.CategoryStruct.comp Q.π h) = CategoryTheory.CategoryStruct.comp P.π (CategoryTheory.CategoryStruct.comp ((ChainComplex.single₀ C).map f) h)

@[simp]

theorem CategoryTheory.ProjectiveResolution.lift_commutes {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {Y : C} {Z : C} (f : Y ⟶ Z) (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.lift f P Q) Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)

The resolution maps intertwine the lift of a morphism and that morphism.

def CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {Y : C} {Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0) : HomologicalComplex.X P.complex 0 ⟶ HomologicalComplex.X Q.complex 1

An auxiliary definition for liftHomotopyZero.

def CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {Y : C} {Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0) : HomologicalComplex.X P.complex 1 ⟶ HomologicalComplex.X Q.complex 2

An auxiliary definition for liftHomotopyZero.

def CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {Y : C} {Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z} (f : P.complex ⟶ Q.complex) (n : ℕ) (g : HomologicalComplex.X P.complex n ⟶ HomologicalComplex.X Q.complex (n + 1)) (g' : HomologicalComplex.X P.complex (n + 1) ⟶ HomologicalComplex.X Q.complex (n + 2)) (w : HomologicalComplex.Hom.f f (n + 1) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P.complex (n + 1) n) g + CategoryTheory.CategoryStruct.comp g' (HomologicalComplex.d Q.complex (n + 2) (n + 1))) : HomologicalComplex.X P.complex (n + 2) ⟶ HomologicalComplex.X Q.complex (n + 3)

An auxiliary definition for liftHomotopyZero.

def CategoryTheory.ProjectiveResolution.liftHomotopyZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {Y : C} {Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0) : Homotopy f 0

Any lift of the zero morphism is homotopic to zero.

def CategoryTheory.ProjectiveResolution.liftHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {Y : C} {Z : C} (f : Y ⟶ Z) {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z} (g : P.complex ⟶ Q.complex) (h : P.complex ⟶ Q.complex) (g_comm : CategoryTheory.CategoryStruct.comp g Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)) (h_comm : CategoryTheory.CategoryStruct.comp h Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)) : Homotopy g h

Two lifts of the same morphism are homotopic.

def CategoryTheory.ProjectiveResolution.liftIdHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] (X : C) (P : CategoryTheory.ProjectiveResolution X) : Homotopy (CategoryTheory.ProjectiveResolution.lift (CategoryTheory.CategoryStruct.id X) P P) (CategoryTheory.CategoryStruct.id P.complex)

The lift of the identity morphism is homotopic to the identity chain map.

def CategoryTheory.ProjectiveResolution.liftCompHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (R : CategoryTheory.ProjectiveResolution Z) : Homotopy (CategoryTheory.ProjectiveResolution.lift (CategoryTheory.CategoryStruct.comp f g) P R) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.lift f P Q) (CategoryTheory.ProjectiveResolution.lift g Q R))

The lift of a composition is homotopic to the composition of the lifts.

def CategoryTheory.ProjectiveResolution.homotopyEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {X : C} (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution X) : HomotopyEquiv P.complex Q.complex

Any two projective resolutions are homotopy equivalent.

@[simp]

theorem CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {X : C} (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution X) {Z : HomologicalComplex C (ComplexShape.down ℕ)} (h : (ChainComplex.single₀ C).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.homotopyEquiv P Q).hom (CategoryTheory.CategoryStruct.comp Q.π h) = CategoryTheory.CategoryStruct.comp P.π h

@[simp]

theorem CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {X : C} (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.homotopyEquiv P Q).hom Q.π = P.π

@[simp]

theorem CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {X : C} (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution X) {Z : HomologicalComplex C (ComplexShape.down ℕ)} (h : (ChainComplex.single₀ C).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.homotopyEquiv P Q).inv (CategoryTheory.CategoryStruct.comp P.π h) = CategoryTheory.CategoryStruct.comp Q.π h

@[simp]

theorem CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {X : C} (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.homotopyEquiv P Q).inv P.π = Q.π

def CategoryTheory.projectiveResolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] (Z : C) [CategoryTheory.HasProjectiveResolution Z] : CategoryTheory.ProjectiveResolution Z

@[inline, reducible]

abbrev CategoryTheory.projectiveResolution.complex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] (Z : C) [CategoryTheory.HasProjectiveResolution Z] : ChainComplex C ℕ

An arbitrarily chosen projective resolution of an object.

@[inline, reducible]

abbrev CategoryTheory.projectiveResolution.π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] (Z : C) [CategoryTheory.HasProjectiveResolution Z] : CategoryTheory.projectiveResolution.complex Z ⟶ (ChainComplex.single₀ C).obj Z

The chain map from the arbitrarily chosen projective resolution projectiveResolution.complex Z back to the chain complex consisting of Z supported in degree 0.

@[inline, reducible]

abbrev CategoryTheory.projectiveResolution.lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.HasProjectiveResolution X] [CategoryTheory.HasProjectiveResolution Y] : CategoryTheory.projectiveResolution.complex X ⟶ CategoryTheory.projectiveResolution.complex Y

The lift of a morphism to a chain map between the arbitrarily chosen projective resolutions.

def CategoryTheory.projectiveResolutions (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.HasProjectiveResolutions C] : CategoryTheory.Functor C (HomotopyCategory C (ComplexShape.down ℕ))

Taking projective resolutions is functorial, if considered with target the homotopy category (ℕ-indexed chain complexes and chain maps up to homotopy).