Documentation

Mathlib.CategoryTheory.Abelian.LeftDerived

Left-derived functors #

We define the left-derived functors F.leftDerived n : C ⥤ D for any additive functor F out of a category with projective resolutions.

We first define a functor F.leftDerivedToHomotopyCategory : C ⥤ HomotopyCategory D (ComplexShape.down ℕ) which is projectiveResolutions C ⋙ F.mapHomotopyCategory _. We show that if X : C and P : ProjectiveResolution X, then F.leftDerivedToHomotopyCategory.obj X identifies to the image in the homotopy category of the functor F applied objectwise to P.complex (this isomorphism is P.isoLeftDerivedToHomotopyCategoryObj F).

Then, the left-derived functors F.leftDerived n : C ⥤ D are obtained by composing F.leftDerivedToHomotopyCategory with the homology functors on the homotopy category.

Similarly we define natural transformations between left-derived functors coming from natural transformations between the original additive functors, and show how to compute the components.

Main results #

TODO #

When F : C ⥤ D is an additive functor, this is the functor C ⥤ HomotopyCategory D (ComplexShape.down ℕ) which sends X : C to F applied to a projective resolution of X.

Equations
Instances For

    If P : ProjectiveResolution Z and F : C ⥤ D is an additive functor, this is an isomorphism between F.leftDerivedToHomotopyCategory.obj X and the complex obtained by applying F to P.complex.

    Equations
    Instances For

      The left derived functors of an additive functor.

      Equations
      Instances For

        We can compute a left derived functor using a chosen projective resolution.

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

          The higher derived functors vanish on projective objects.

          We can compute a left derived functor on a morphism using a descent of that morphism to a chain map between chosen projective resolutions.

          The natural transformation F.leftDerivedToHomotopyCategory ⟶ G.leftDerivedToHomotopyCategory induced by a natural transformation F ⟶ G between additive functors.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            noncomputable def CategoryTheory.NatTrans.leftDerived {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {F G : Functor C D} [F.Additive] [G.Additive] (α : F G) (n : ) :

            The natural transformation between left-derived functors induced by a natural transformation.

            Equations
            Instances For

              A component of the natural transformation between left-derived functors can be computed using a chosen projective resolution.

              If P : ProjectiveResolution X and F is an additive functor, this is the canonical morphism from the opcycles in degree 0 of (F.mapHomologicalComplex _).obj P.complex to F.obj X.

              Equations
              Instances For

                The natural transformation F.leftDerived 0 ⟶ F.

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

                  The canonical isomorphism F.leftDerived 0 ≅ F when F is right exact (i.e. preserves finite colimits).

                  Equations
                  Instances For