# 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} (Z : C) :
Type (max u v)

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).
Instances For

An object admits a projective resolution.

Instances
• out : ∀ (Z : C),

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.

Instances
@[simp]
@[simp]

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

Instances For
def CategoryTheory.ProjectiveResolution.liftZero {C : Type u} {Y : C} {Z : C} (f : Y Z) :

Auxiliary construction for lift.

Instances For
def CategoryTheory.ProjectiveResolution.liftOne {C : Type u} {Y : C} {Z : C} (f : Y Z) :

Auxiliary construction for lift.

Instances For
@[simp]

Auxiliary lemma for lift.

def CategoryTheory.ProjectiveResolution.liftSucc {C : Type u} {Y : C} {Z : C} (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.

Instances For
def CategoryTheory.ProjectiveResolution.lift {C : Type u} {Y : C} {Z : C} (f : Y Z) :
P.complex Q.complex

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

Instances For
@[simp]
theorem CategoryTheory.ProjectiveResolution.lift_commutes_assoc {C : Type u} {Y : C} {Z : C} (f : Y Z) {Z : } (h : ().obj Z Z) :
@[simp]
theorem CategoryTheory.ProjectiveResolution.lift_commutes {C : Type u} {Y : C} {Z : C} (f : Y Z) :

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

def CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero {C : Type u} {Y : C} {Z : C} (f : P.complex Q.complex) (comm : ) :

An auxiliary definition for liftHomotopyZero.

Instances For
def CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne {C : Type u} {Y : C} {Z : C} (f : P.complex Q.complex) (comm : ) :

An auxiliary definition for liftHomotopyZero.

Instances For
def CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc {C : Type u} {Y : C} {Z : C} (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.

Instances For
def CategoryTheory.ProjectiveResolution.liftHomotopyZero {C : Type u} {Y : C} {Z : C} (f : P.complex Q.complex) (comm : ) :

Any lift of the zero morphism is homotopic to zero.

Instances For
def CategoryTheory.ProjectiveResolution.liftHomotopy {C : Type u} {Y : C} {Z : C} (f : Y Z) (g : P.complex Q.complex) (h : P.complex Q.complex) (g_comm : = CategoryTheory.CategoryStruct.comp P (().map f)) (h_comm : = CategoryTheory.CategoryStruct.comp P (().map f)) :

Two lifts of the same morphism are homotopic.

Instances For

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

Instances For
def CategoryTheory.ProjectiveResolution.liftCompHomotopy {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :

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

Instances For

Any two projective resolutions are homotopy equivalent.

Instances For
@[simp]
theorem CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π_assoc {C : Type u} {X : C} {Z : } (h : ().obj X Z) :
@[simp]
@[simp]
theorem CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π_assoc {C : Type u} {X : C} {Z : } (h : ().obj X Z) :
@[simp]
Instances For
@[inline, reducible]

An arbitrarily chosen projective resolution of an object.

Instances For
@[inline, reducible]

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

Instances For
@[inline, reducible]

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

Instances For

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

Instances For