mathlib documentation

category_theory.preadditive.projective_resolution

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.

@[nolint]

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).
@[class]

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.

Instances

Auxiliary construction for lift.

Equations

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

Equations

An auxiliary definition for lift_homotopy_zero.

Equations

Any lift of the zero morphism is homotopic to zero.

Equations

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