mathlib documentation


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 of 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 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 projective_resolutions C : C ⥤ homotopy_category C.


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

  • projective_resolution Z: the -indexed chain complex (equipped with projective and exact instances)
  • projective_resolution.π Z: the chain map from projective_resolution Z to (single C _ 0).obj Z (all the components are equipped with epi instances, and when the category is abelian we will show π is a quasi-iso).

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


Auxiliary construction for lift.


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


An auxiliary definition for lift_homotopy_zero.


Any lift of the zero morphism is homotopic to zero.


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