Derived functors

Stream: homology

[Joël Riou]

Given an additive functor F : C ⥤ D between abelian categories (such that C has enough injectives), I have just finished defining F.rightDerivedFunctorPlus : DerivedCategory.Plus C ⥤ DerivedCategory.Plus D, which is the total right derived functor $RF : D^+(C) ⥤ D^+(D)$ of the extension $K^+(C) ⥤ K^+(D)$ of F to the bounded below homotopy categories. In order to deal with the construction of total right derived functors, I have used the formalism of derivability structures introduced by Kahn and Maltsiniotis in https://webusers.imj-prg.fr/~georges.maltsiniotis/ps/bkgmdef.pdf
The most technical part was to construct a derivability structure for the inclusion of bounded below complexes of injectives in K^+(C), which involved showing that any bounded below complex is quasi-isomorphic to a bounded below complex of injectives. The dual version (projective replacement of complexes) was in the LTE, but here I proved a more general statement which could be used to construct a model category structure on $C^+(C)$: what I proved are the two parts of the factorization axiom CM5 (with cofibrations = mono, and fibrations = epi with degreewise injective kernel).
If we know that derived functors of triangulated functors are triangulated under some suitable assumptions (I have some Lean3 code doing exactly that), then $RF$ becomes a triangulated functor, which may ultimately be used in order to redefine the sequence of right derived functors $R^n F : C ⥤ D$. Then, it will be easy to show that we have long exact sequences for the $R^n F$ functors attached to any short exact sequence in C.

The main definition is at https://github.com/leanprover-community/mathlib4/pull/4197/files#diff-05aac5194a26085d7c2dd0468f679fdaa958ccc2f38af8b23e8783f09d91fb04R249-R251