long exact sequences of derived functors

Stream: Is there code for X?

[Richard Hill]

Is the long exact sequence for right derived functors defined in Mathlib?
For example, is there an obvious way to remove this sorry (without inserting exact 0).

import Mathlib.Algebra.Homology.ShortComplex.ShortExact
import Mathlib.CategoryTheory.Abelian.RightDerived

open CategoryTheory Functor Limits

example (C D : Type) [Category C] [Category D] [Abelian C] [Abelian D] [EnoughInjectives C]
    (F : C ⥤ D) [PreservesLimits F] [F.Additive]
    (S : ShortComplex C) (hS : S.ShortExact) (n : ℕ) :
    (F.rightDerived n).obj S.X₃ ⟶ (F.rightDerived (n + 1)).obj S.X₁ := by
  sorry

[Edison Xie]

@Joël Riou @Andrew Yang

[Joël Riou]

I have this on a branch https://github.com/joelriou/mathlib4/blob/4e2559a08433acc41cc0b2c847fa800a87eba7dd/Mathlib/Algebra/Homology/DerivedCategory/RightDerivedFunctorPlus.lean#L240 which is meant to enter mathlib at some point...

[Joël Riou]

The idea is to construct the total derived functor $RF: D^+(C) \rightarrow D^+(D)$ and show that it is a triangulated functor. In order to do this, I am using a right derivability structure in the sense of https://webusers.imj-prg.fr/~georges.maltsiniotis/ps/bkgmdef.pdf which I constructed #33956 in the general context of model categories towards the fundamental lemma of homotopical algebra #26303.

[Joël Riou]

The bottle neck is the construction of the model category structure on bounded below complexes in C which depends on a technical factorization lemma https://github.com/joelriou/mathlib4/blob/4e2559a08433acc41cc0b2c847fa800a87eba7dd/Mathlib/Algebra/Homology/Factorizations/CM5a.lean

[Joël Riou]

Then, basically any functor from the bounded below homotopy category admits a total right derived functor https://github.com/joelriou/mathlib4/blob/4e2559a08433acc41cc0b2c847fa800a87eba7dd/Mathlib/Algebra/Homology/DerivedCategory/DerivabilityStructureInjectives.lean#L390

[Joël Riou]

Finally, we have to show that under suitable assumptions the derived functor of a triangulated functor is triangulated https://github.com/joelriou/mathlib4/blob/4e2559a08433acc41cc0b2c847fa800a87eba7dd/Mathlib/CategoryTheory/Functor/Derived/RightDerivedTriangulated.lean

[Joël Riou]

Apart from spectral sequences, this is my second-most priority for the integration of my formalization of homological algebra in mathlib. There should be some progress in the next few weeks.

[Richard Hill]

Many thanks!