The bounded derived category as a localization

Let C be an abelian category. Mathlib defines the bounded derived category DerivedCategory.Bounded C as the full subcategory of DerivedCategory C on the objects that are cohomologically bounded for the canonical t-structure. This file shows that it is the localization of the homotopy category TauCeti.HomotopyCategory.Bounded C of strictly bounded complexes with respect to the quasi-isomorphisms (TauCeti.HomotopyCategory.Bounded.quasiIso), through the functor TauCeti.DerivedCategory.Bounded.Qh. Hence functors out of K^b(C) inverting quasi-isomorphisms descend to D^b(C), together with their shift and triangulated structure. The functor Qh is compatible with the single functors (singleFunctorCompQhIso).

The proof reduces to Mathlib's corresponding statement for bounded below complexes (DerivedCategory.Plus.Qh). Inside the bounded below homotopy category, the bounded complexes form a left localizing subcategory with respect to the acyclic complexes in the sense of Verdier: a morphism from a complex strictly ≤ b to an acyclic bounded below complex Y factors through the canonical truncation Y.truncLE b, which is again acyclic and is bounded. Localizing fully faithful localizer morphisms compose, so the induced functor from the localization of K^b(C) to D(C) is fully faithful; its essential image is D^b(C).

References

• Mathlib's Mathlib/Algebra/Homology/DerivedCategory/Plus.lean, which proves the bounded below version and supplies the formal pattern followed here.
• Jean-Louis Verdier, Des catégories dérivées des catégories abéliennes, Astérisque 239 (1996).

noncomputable def TauCeti.DerivedCategory.Bounded.Qh (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Functor (HomotopyCategory.Bounded C) (DerivedCategory.Bounded C)

The localization functor K^b(C) ⥤ D^b(C) from the homotopy category of bounded cochain complexes to the bounded derived category.

noncomputable def TauCeti.DerivedCategory.Bounded.QhCompιIsoιCompQh (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (Qh C).comp DerivedCategory.Bounded.ι ≅ (HomotopyCategory.Bounded.ι C).comp DerivedCategory.Qh

The functor Qh C : K^b(C) ⥤ D^b(C) is induced by DerivedCategory.Qh : HomotopyCategory C (.up ℤ) ⥤ DerivedCategory C.

The bodies of Qh and QhCompιIsoιCompQh are not exposed, so the following characterizing lemmas are proved with (rfl), unfolding them inside this module, rather than exported as definitional equalities.

theorem TauCeti.DerivedCategory.Bounded.Qh_obj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : HomotopyCategory.Bounded C) : ((Qh C).obj X).obj = DerivedCategory.Qh.obj X.obj

The underlying object in D(C) of the image of X under Qh C is the image of the underlying complex under DerivedCategory.Qh.

@[simp]

theorem TauCeti.DerivedCategory.Bounded.QhCompιIsoιCompQh_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : HomotopyCategory.Bounded C) : (QhCompιIsoιCompQh C).hom.app X = CategoryTheory.eqToHom ⋯

The components of QhCompιIsoιCompQh are identities, transported along Qh_obj_obj.

@[simp]

theorem TauCeti.DerivedCategory.Bounded.QhCompιIsoιCompQh_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : HomotopyCategory.Bounded C) : (QhCompιIsoιCompQh C).inv.app X = CategoryTheory.eqToHom ⋯

The components of the inverse of QhCompιIsoιCompQh are identities, transported along Qh_obj_obj.

@[instance_reducible]

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

instance TauCeti.DerivedCategory.Bounded.instCommShiftBoundedDerivedCategoryHomFunctorQhCompιIsoιCompQhInt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.NatTrans.CommShift (QhCompιIsoιCompQh C).hom ℤ

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

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

noncomputable def TauCeti.DerivedCategory.Bounded.singleFunctorCompQhIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) : (HomotopyCategory.Bounded.singleFunctor C n).comp (Qh C) ≅ singleFunctor C n

The functor Qh C : K^b(C) ⥤ D^b(C) sends an object placed in degree n to that object placed in degree n.

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

The functor Qh C : K^b(C) ⥤ D^b(C) is the localization of the bounded homotopy category at the morphisms whose cone is acyclic.

instance TauCeti.DerivedCategory.Bounded.instIsLocalizationBoundedBoundedQhQuasiIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (Qh C).IsLocalization (HomotopyCategory.Bounded.quasiIso C)

The bounded derived category is a localization of the bounded homotopy category. The functor Qh C : K^b(C) ⥤ D^b(C) is the localization at the quasi-isomorphisms.

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