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. We define this derived functor as the derived functor of the functor F.mapHomotopyCategoryPlus induced by F on the bounded below homotopy categories. We take advantage of this definition in order to show that F.rightDerivedFunctorPlus is a triangulated functor. We also show that F.rightDerivedFunctorPlus may also be thought of as a derived functor of the functor F.mapCochainComplexPlus that F induces on the categories of bounded below cochain complexes.

TODO(@joelriou): refactor the definition 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.rightDerivedFunctorPlusUnith {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 F.rightDerivedFunctorPlus : DerivedCategory.Plus C ⥤ DerivedCategory.Plus D when F : C ⥤ D is an additive functor between abelian categories and C has enough injectives. It is defined here as a derived functor of F.mapHomotopyCategoryPlus : HomotopyCategory.Plus C ⥤ HomotopyCategory.Plus D, postcomposed with DerivedCategory.Plus.Qh. (See Functor.rightDerivedFunctorPlusUnit for the similar result regarding F.mapCochainComplexPlus : CochainComplex.Plus C ⥤ CochainComplex.Plus D.)

Equations

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

instance CategoryTheory.Functor.instIsRightDerivedFunctorPlusPlusRightDerivedFunctorPlusRightDerivedFunctorPlusUnithQuasiIso {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.rightDerivedFunctorPlusUnith (HomotopyCategory.Plus.quasiIso C)

@[instance_reducible]

noncomputable instance CategoryTheory.Functor.instCommShiftPlusRightDerivedFunctorPlusInt {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.CommShift ℤ

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Functor.instCommShiftPlusPlusRightDerivedFunctorPlusUnithInt {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] : NatTrans.CommShift F.rightDerivedFunctorPlusUnith ℤ

instance CategoryTheory.Functor.instIsTriangulatedPlusRightDerivedFunctorPlus {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.IsTriangulated

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.mapCochainComplexPlus.comp DerivedCategory.Plus.Q ⟶ DerivedCategory.Plus.Q.comp F.rightDerivedFunctorPlus

A natural transformation that is part of the data of the right derived functor F.rightDerivedFunctorPlus : DerivedCategory.Plus C ⥤ DerivedCategory.Plus D when F : C ⥤ D is an additive functor between abelian categories and C has enough injectives. While the right derived functor was defined using bounded below homotopy categories, this natural transformation allows to say that it is also the derived functor of the functor F.mapCochainComplexPlus : CochainComplex.Plus C ⥤ CochainComplex.Plus D, postcomposed with DerivedCategory.Plus.Q.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Functor.rightDerivedFunctorPlusUnit_app {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] (X : CochainComplex.Plus C) : F.rightDerivedFunctorPlusUnit.app X = CategoryStruct.comp ((DerivedCategory.Plus.quotientCompQhIso D).inv.app (F.mapCochainComplexPlus.obj X)) (CategoryStruct.comp (DerivedCategory.Plus.Qh.map (F.quotientCompMapHomotopyCategoryPlusIso.inv.app X)) (CategoryStruct.comp (F.rightDerivedFunctorPlusUnith.app ((HomotopyCategory.Plus.quotient C).obj X)) (F.rightDerivedFunctorPlus.map ((DerivedCategory.Plus.quotientCompQhIso C).hom.app X))))

instance CategoryTheory.Functor.instCommShiftPlusPlusRightDerivedFunctorPlusUnitInt {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] : NatTrans.CommShift F.rightDerivedFunctorPlusUnit ℤ

instance CategoryTheory.Functor.instIsIsoPlusAppPlusRightDerivedFunctorPlusUnitObjInjectiveObjectMapCochainComplexPlusι {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] (K : CochainComplex.Plus (InjectiveObject C)) : IsIso (F.rightDerivedFunctorPlusUnit.app ((InjectiveObject.ι C).mapCochainComplexPlus.obj K))

theorem CochainComplex.Plus.localizerMorphism_derives_mapCochainComplexPlus {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [HasDerivedCategory D] (F : CategoryTheory.Functor C D) [F.Additive] : (localizerMorphism C).Derives (F.mapCochainComplexPlus.comp DerivedCategory.Plus.Q)

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 (CochainComplex.Plus.quasiIso C)