Documentation

Mathlib.CategoryTheory.Preadditive.ProjectiveResolution

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 quasi-isomorphism P.π from C to the chain complex consisting just of Z in degree zero.

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.

Instances For

    the morphism to the single chain complex with Z in degree 0 is a quasi-isomorphism

    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

      The (limit) cokernel cofork given by the composition P.complex.X 1 ⟶ P.complex.X 0 ⟶ Z when P : ProjectiveResolution Z.

      Equations
      Instances For

        Z is the cokernel of P.complex.X 1 ⟶ P.complex.X 0 when P : ProjectiveResolution Z.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For