The right derived functor on the bounded below derived category

If F : C ⥤ D is an additive functor between abelian categories, where C has enough injectives, we define the right derived functor F.rightDerivedFunctorPlus : DerivedCategory.Plus C ⥤ DerivedCategory.Plus D between the corresponding bounded below derived categories.

TODO(@joelriou): show that this functor is triangulated and refactor the definiton of Functor.rightDerived

noncomputable def CategoryTheory.Functor.rightDerivedFunctorPlus {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] (F : Functor C D) [F.Additive] [EnoughInjectives C] : Functor (DerivedCategory.Plus C) (DerivedCategory.Plus D)

The right derived functor DerivedCategory.Plus C ⥤ DerivedCategory.Plus D when F : C ⥤ D is an additive functor between abelian categories and C has enough injectives.

Equations

• F.rightDerivedFunctorPlus = (F.mapHomotopyCategoryPlus.comp DerivedCategory.Plus.Qh).totalRightDerived DerivedCategory.Plus.Qh (HomotopyCategory.Plus.quasiIso C)

noncomputable def CategoryTheory.Functor.rightDerivedFunctorPlusUnit {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] (F : Functor C D) [F.Additive] [EnoughInjectives C] : F.mapHomotopyCategoryPlus.comp DerivedCategory.Plus.Qh ⟶ DerivedCategory.Plus.Qh.comp F.rightDerivedFunctorPlus

The natural transformation that is part of the data of the right derived functor DerivedCategory.Plus C ⥤ DerivedCategory.Plus D when F : C ⥤ D is an additive functor between abelian categories and C has enough injectives.

Equations

• F.rightDerivedFunctorPlusUnit = (F.mapHomotopyCategoryPlus.comp DerivedCategory.Plus.Qh).totalRightDerivedUnit DerivedCategory.Plus.Qh (HomotopyCategory.Plus.quasiIso C)

instance CategoryTheory.Functor.instIsRightDerivedFunctorPlusPlusRightDerivedFunctorPlusRightDerivedFunctorPlusUnitQuasiIso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] (F : Functor C D) [F.Additive] [EnoughInjectives C] : F.rightDerivedFunctorPlus.IsRightDerivedFunctor F.rightDerivedFunctorPlusUnit (HomotopyCategory.Plus.quasiIso C)