The derived category of a linear abelian category is linear

@[instance_reducible]

noncomputable instance DerivedCategory.instLinear (R : Type t) [Ring R] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear R C] [HasDerivedCategory C] : CategoryTheory.Linear R (DerivedCategory C)

Equations

• DerivedCategory.instLinear R C = CategoryTheory.Localization.linear R DerivedCategory.Qh (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))

instance DerivedCategory.instLinearHomotopyCategoryIntUpQh (R : Type t) [Ring R] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear R C] [HasDerivedCategory C] : CategoryTheory.Functor.Linear R Qh

instance DerivedCategory.instLinearCochainComplexIntQ (R : Type t) [Ring R] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear R C] [HasDerivedCategory C] : CategoryTheory.Functor.Linear R Q

instance DerivedCategory.instLinearShiftFunctorInt (R : Type t) [Ring R] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear R C] [HasDerivedCategory C] (n : ℤ) : CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor (DerivedCategory C) n)

instance DerivedCategory.instLinearSingleFunctor (R : Type t) [Ring R] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear R C] [HasDerivedCategory C] (n : ℤ) : CategoryTheory.Functor.Linear R (singleFunctor C n)