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.

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

    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.

      @[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

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

        Instances For