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 Mathlib/Algebra/Homology/Localization.lean 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 file HomotopyCategory.Acyclic, it was shown that this class of quasiisomorphisms 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 Mathlib/Algebra/Homology/HomotopyCategory/Triangulated.lean) using the localization theorem for triangulated categories which was obtained in the file Mathlib/CategoryTheory/Localization/Triangulated.lean.

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.

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]

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

@[implicit_reducible]

noncomputable 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.

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.

@[implicit_reducible]

noncomputable instance instCategoryDerivedCategory (C : Type u_2) [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Category.{u_1, max u_2 u_3} (DerivedCategory C)

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.

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

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

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.

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

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

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

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

@[implicit_reducible]

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

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

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

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

@[implicit_reducible]

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

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

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

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

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

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

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

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

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 ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))

theorem DerivedCategory.mappingCone_triangle_distinguished {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) : Q.mapTriangle.obj (CochainComplex.mappingCone.triangle φ) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

theorem DerivedCategory.mappingCocone_triangle_distinguished {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) : Q.mapTriangle.obj (CochainComplex.mappingCocone.triangle φ) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

noncomputable def DerivedCategory.singleFunctors (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.SingleFunctors C (DerivedCategory C) ℤ

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

@[reducible, inline]

noncomputable abbrev DerivedCategory.singleFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) : CategoryTheory.Functor C (DerivedCategory C)

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

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

@[simp]

theorem DerivedCategory.Qh_obj_singleFunctors_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) (X : C) : Qh.obj (((HomotopyCategory.singleFunctors C).functor n).obj X) = (singleFunctor C n).obj X

noncomputable def DerivedCategory.singleFunctorsPostcompQhIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : singleFunctors C ≅ (HomotopyCategory.singleFunctors C).postcomp Qh

The isomorphism DerivedCategory.singleFunctors C ≅ (HomotopyCategory.singleFunctors C).postcomp Qh given by the definition of DerivedCategory.singleFunctors.

noncomputable def DerivedCategory.singleFunctorsPostcompQIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : singleFunctors C ≅ (CochainComplex.singleFunctors C).postcomp Q

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

theorem DerivedCategory.singleFunctorsPostcompQIso_hom_hom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) : (singleFunctorsPostcompQIso C).hom.hom n = CategoryTheory.CategoryStruct.id ((singleFunctors C).functor n)

theorem DerivedCategory.singleFunctorsPostcompQIso_inv_hom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) : (singleFunctorsPostcompQIso C).inv.hom n = CategoryTheory.CategoryStruct.id (((CochainComplex.singleFunctors C).postcomp Q).functor n)

noncomputable def DerivedCategory.singleFunctorIsoCompQ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) : singleFunctor C n ≅ (CochainComplex.singleFunctor C n).comp Q

The isomorphism singleFunctor C n ≅ CochainComplex.singleFunctor C n ⋙ Q.

theorem DerivedCategory.isIso_Q_map_iff_quasiIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) : CategoryTheory.IsIso (Q.map φ) ↔ QuasiIso φ

theorem DerivedCategory.Q_map_eq_of_homotopy (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {K L : CochainComplex C ℤ} {f g : K ⟶ L} (h : Homotopy f g) : Q.map f = Q.map g