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)

• construct the distinguished triangle associated to a short exact sequence of cochain complexes (done), and compare the associated connecting homomorphism with the one defined in Algebra.Homology.HomologySequence.
• refactor the definition of Ext groups using morphisms in the derived category (which may be shrunk to the universe v at least when C has enough projectives or enough injectives).

References

• [Jean-Louis Verdier, Des catégories dérivées des catégories abéliennes][verdier1996]
• [Mark Hovey, Model category structures on chain complexes of sheaves][hovey-2001]

def HomotopyCategory.subcategoryAcyclic (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Triangulated.Subcategory (HomotopyCategory C (ComplexShape.up ℤ))

The triangulated subcategory of HomotopyCategory C (ComplexShape.up ℤ) consisting of acyclic complexes.

Equations

• HomotopyCategory.subcategoryAcyclic C = (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).homologicalKernel

instance HomotopyCategory.instClosedUnderIsomorphismsIntUpPSubcategoryAcyclic (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.ClosedUnderIsomorphisms (HomotopyCategory.subcategoryAcyclic C).P

Equations

• ⋯ = ⋯

theorem HomotopyCategory.mem_subcategoryAcyclic_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : HomotopyCategory C (ComplexShape.up ℤ)) : (HomotopyCategory.subcategoryAcyclic C).P X ↔ ∀ (n : ℤ), CategoryTheory.Limits.IsZero ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n).obj X)

theorem HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_exactAt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (K : CochainComplex C ℤ) : (HomotopyCategory.subcategoryAcyclic C).P ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) ↔ ∀ (n : ℤ), HomologicalComplex.ExactAt K n

theorem HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) = (HomotopyCategory.subcategoryAcyclic C).W

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

• HasDerivedCategory C = (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)).HasLocalization

def HasDerivedCategory.standard (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : HasDerivedCategory C

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

• HasDerivedCategory.standard C = CategoryTheory.MorphismProperty.HasLocalization.standard (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))

def DerivedCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : Type (max u v)

The derived category of an abelian category.

Equations

• DerivedCategory C = HomologicalComplexUpToQuasiIso C (ComplexShape.up ℤ)

instance DerivedCategory.instCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Category.{w, max u v} (DerivedCategory C)

Equations

• DerivedCategory.instCategory C = id inferInstance

def DerivedCategory.Q {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Functor (CochainComplex C ℤ) (DerivedCategory C)

The localization functor CochainComplex C ℤ ⥤ DerivedCategory C.

Equations

• DerivedCategory.Q = HomologicalComplexUpToQuasiIso.Q

instance DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : DerivedCategory.Q.IsLocalization (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))

Equations

• ⋯ = ⋯

instance DerivedCategory.instIsIsoMapCochainComplexIntQ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {K : CochainComplex C ℤ} {L : CochainComplex C ℤ} (f : K ⟶ L) [QuasiIso f] : CategoryTheory.IsIso (DerivedCategory.Q.map f)

Equations

• ⋯ = ⋯

def DerivedCategory.Qh {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Functor (HomotopyCategory C (ComplexShape.up ℤ)) (DerivedCategory C)

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

Equations

• DerivedCategory.Qh = HomologicalComplexUpToQuasiIso.Qh

def DerivedCategory.quotientCompQhIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).comp DerivedCategory.Qh ≅ DerivedCategory.Q

The natural isomorphism HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh ≅ Q.

Equations

• DerivedCategory.quotientCompQhIso C = HomologicalComplexUpToQuasiIso.quotientCompQhIso C (ComplexShape.up ℤ)

instance DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhQuasiIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : DerivedCategory.Qh.IsLocalization (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))

Equations

• ⋯ = ⋯

instance DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhWSubcategoryAcyclic (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : DerivedCategory.Qh.IsLocalization (HomotopyCategory.subcategoryAcyclic C).W

Equations

• ⋯ = ⋯

noncomputable instance DerivedCategory.instPreadditive (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Preadditive (DerivedCategory C)

Equations

• DerivedCategory.instPreadditive C = CategoryTheory.Localization.preadditive DerivedCategory.Qh (HomotopyCategory.subcategoryAcyclic C).W

instance DerivedCategory.instAdditiveHomotopyCategoryIntUpQh (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : DerivedCategory.Qh.Additive

Equations

• ⋯ = ⋯

instance DerivedCategory.instAdditiveCochainComplexIntQ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : DerivedCategory.Q.Additive

Equations

• ⋯ = ⋯

noncomputable instance DerivedCategory.instHasZeroObject (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Limits.HasZeroObject (DerivedCategory C)

Equations

• ⋯ = ⋯

noncomputable instance DerivedCategory.instHasShiftInt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.HasShift (DerivedCategory C) ℤ

Equations

• DerivedCategory.instHasShiftInt C = CategoryTheory.HasShift.localized DerivedCategory.Qh (HomotopyCategory.subcategoryAcyclic C).W ℤ

noncomputable instance DerivedCategory.instCommShiftHomotopyCategoryIntUpQh (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : DerivedCategory.Qh.CommShift ℤ

Equations

• DerivedCategory.instCommShiftHomotopyCategoryIntUpQh C = CategoryTheory.Functor.CommShift.localized DerivedCategory.Qh (HomotopyCategory.subcategoryAcyclic C).W ℤ

noncomputable instance DerivedCategory.instCommShiftCochainComplexIntQ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : DerivedCategory.Q.CommShift ℤ

Equations

• DerivedCategory.instCommShiftCochainComplexIntQ C = CategoryTheory.Functor.CommShift.ofIso (DerivedCategory.quotientCompQhIso C) ℤ

instance DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.NatTrans.CommShift (DerivedCategory.quotientCompQhIso C).hom ℤ

Equations

• ⋯ = ⋯

instance DerivedCategory.instAdditiveShiftFunctorInt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) : (CategoryTheory.shiftFunctor (DerivedCategory C) n).Additive

Equations

• ⋯ = ⋯

noncomputable instance DerivedCategory.instPretriangulated (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Pretriangulated (DerivedCategory C)

Equations

• DerivedCategory.instPretriangulated C = CategoryTheory.Triangulated.Localization.pretriangulated DerivedCategory.Qh (HomotopyCategory.subcategoryAcyclic C).W

instance DerivedCategory.instIsTriangulatedHomotopyCategoryIntUpQh (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : DerivedCategory.Qh.IsTriangulated

Equations

• ⋯ = ⋯

noncomputable instance DerivedCategory.instIsTriangulated (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.IsTriangulated (DerivedCategory C)

Equations

• ⋯ = ⋯

instance DerivedCategory.instEssSurjArrowHomotopyCategoryIntUpMapArrowQh (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : DerivedCategory.Qh.mapArrow.EssSurj

Equations

• ⋯ = ⋯

instance DerivedCategory.instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] : ((CategoryTheory.whiskeringLeft (HomotopyCategory C (ComplexShape.up ℤ)) (DerivedCategory C) D).obj DerivedCategory.Qh).Full

Equations

• ⋯ = ⋯

instance DerivedCategory.instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] : ((CategoryTheory.whiskeringLeft (HomotopyCategory C (ComplexShape.up ℤ)) (DerivedCategory C) D).obj DerivedCategory.Qh).Faithful

Equations

• ⋯ = ⋯

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))