Documentation

Mathlib.Algebra.Homology.DerivedCategory.Basic

The derived category of an abelian category #

In this file, we construct the derived category DerivedCategory C of an abelian category C. It is equipped with a triangulated structure.

The derived category is defined here as the localization of cochain complexes indexed by with respect to quasi-isomorphisms: it is a type synonym of HomologicalComplexUpToQuasiIso C (ComplexShape.up ℤ). Then, we have a localization functor DerivedCategory.Q : CochainComplex C ℤ ⥤ DerivedCategory C. It was already shown in the file Algebra.Homology.Localization that the induced functor DerivedCategory.Qh : HomotopyCategory C (ComplexShape.up ℤ) ⥤ DerivedCategory C is a localization functor with respect to the class of morphisms HomotopyCategory.quasiIso C (ComplexShape.up ℤ). In the lemma HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W we obtain that this class of morphisms consists of morphisms whose cone belongs to the triangulated subcategory HomotopyCategory.subcategoryAcyclic C of acyclic complexes. Then, the triangulated structure on DerivedCategory C is deduced from the triangulated structure on the homotopy category (see file Algebra.Homology.HomotopyCategory.Triangulated) using the localization theorem for triangulated categories which was obtained in the file CategoryTheory.Localization.Triangulated.

Implementation notes #

If C : Type u and Category.{v} C, the constructed localized category of cochain complexes with respect to quasi-isomorphisms has morphisms in Type (max u v). However, in certain circumstances, it shall be possible to prove that they are v-small (when C is a Grothendieck abelian category (e.g. the category of modules over a ring), it should be so by a theorem of Hovey.).

Then, when working with derived categories in mathlib, the user should add the variable [HasDerivedCategory.{w} C] which is the assumption that there is a chosen derived category with morphisms in Type w. When derived categories are used in order to prove statements which do not involve derived categories, the HasDerivedCategory.{max u v} instance should be obtained at the beginning of the proof, using the term HasDerivedCategory.standard C.

TODO (@joelriou) #

References #

@[reducible, inline]
abbrev HasDerivedCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] :
Type (max (max ((max u v) + 1) v) (w + 1))

The assumption that a localized category for (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) has been chosen, and that the morphisms in this chosen category are in Type w.

Equations
Instances For

    The derived category obtained using the constructed localized category of cochain complexes with respect to quasi-isomorphisms. This should be used only while proving statements which do not involve the derived category.

    Equations
    Instances For

      The derived category of an abelian category.

      Equations
      Instances For

        The localization functor CochainComplex C ℤ ⥤ DerivedCategory C.

        Equations
        • DerivedCategory.Q = HomologicalComplexUpToQuasiIso.Q
        Instances For

          The localization functor HomotopyCategory C (ComplexShape.up ℤ) ⥤ DerivedCategory C.

          Equations
          • DerivedCategory.Qh = HomologicalComplexUpToQuasiIso.Qh
          Instances For
            theorem DerivedCategory.mem_distTriang_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)) :
            T CategoryTheory.Pretriangulated.distinguishedTriangles ∃ (X : CochainComplex C ) (Y : CochainComplex C ) (f : X Y), Nonempty (T DerivedCategory.Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))

            The single functors C ⥤ DerivedCategory C for all n : ℤ along with their compatibilities with shifts.

            Equations
            Instances For
              @[reducible, inline]

              The shift functor C ⥤ DerivedCategory C which sends X : C to the single cochain complex with X sitting in degree n : ℤ.

              Equations
              Instances For

                The isomorphism DerivedCategory.singleFunctors C ≅ (CochainComplex.singleFunctors C).postcomp Q.

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