Triangulated derived functors using derivability structures

This file provides lemmas in order to show that derived functors are triangulated when they are "derived" by a left or right derivability structure whose underlying functor is triangulated.

theorem CategoryTheory.LocalizerMorphism.Derives.isTriangulated_of_isRightDerivedFunctor {C₁ : Type u_1} {C₂ : Type u_2} {H : Type u_3} {D₂ : Type u_4} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D₂] [Limits.HasZeroObject C₁] [HasShift C₁ ℤ] [Preadditive C₁] [Limits.HasZeroObject C₂] [HasShift C₂ ℤ] [Preadditive C₂] [Limits.HasZeroObject H] [HasShift H ℤ] [Preadditive H] [Limits.HasZeroObject D₂] [HasShift D₂ ℤ] [Preadditive D₂] [∀ (n : ℤ), (shiftFunctor C₁ n).Additive] [∀ (n : ℤ), (shiftFunctor C₂ n).Additive] [∀ (n : ℤ), (shiftFunctor H n).Additive] [∀ (n : ℤ), (shiftFunctor D₂ n).Additive] [Pretriangulated C₁] [Pretriangulated C₂] [Pretriangulated H] [Pretriangulated D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} [Φ.functor.CommShift ℤ] [Φ.functor.IsTriangulated] {F : Functor C₂ H} [F.CommShift ℤ] [F.IsTriangulated] (hF : Φ.Derives F) {L : Functor C₂ D₂} [L.IsLocalization W₂] [L.CommShift ℤ] [L.IsTriangulated] [L.mapArrow.EssSurj] [Φ.IsRightDerivabilityStructure] [Φ.arrow.HasRightResolutions] {RF : Functor D₂ H} [RF.CommShift ℤ] (α : F ⟶ L.comp RF) [NatTrans.CommShift α ℤ] [RF.IsRightDerivedFunctor α W₂] : RF.IsTriangulated

theorem CategoryTheory.LocalizerMorphism.Derives.isTriangulated_of_isLeftDerivedFunctor {C₁ : Type u_1} {C₂ : Type u_2} {H : Type u_3} {D₂ : Type u_4} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D₂] [Limits.HasZeroObject C₁] [HasShift C₁ ℤ] [Preadditive C₁] [Limits.HasZeroObject C₂] [HasShift C₂ ℤ] [Preadditive C₂] [Limits.HasZeroObject H] [HasShift H ℤ] [Preadditive H] [Limits.HasZeroObject D₂] [HasShift D₂ ℤ] [Preadditive D₂] [∀ (n : ℤ), (shiftFunctor C₁ n).Additive] [∀ (n : ℤ), (shiftFunctor C₂ n).Additive] [∀ (n : ℤ), (shiftFunctor H n).Additive] [∀ (n : ℤ), (shiftFunctor D₂ n).Additive] [Pretriangulated C₁] [Pretriangulated C₂] [Pretriangulated H] [Pretriangulated D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} [Φ.functor.CommShift ℤ] [Φ.functor.IsTriangulated] {F : Functor C₂ H} [F.CommShift ℤ] [F.IsTriangulated] (hF : Φ.Derives F) {L : Functor C₂ D₂} [L.IsLocalization W₂] [L.CommShift ℤ] [L.IsTriangulated] [L.mapArrow.EssSurj] [Φ.IsLeftDerivabilityStructure] [Φ.arrow.HasLeftResolutions] {LF : Functor D₂ H} [LF.CommShift ℤ] (α : L.comp LF ⟶ F) [NatTrans.CommShift α ℤ] [LF.IsLeftDerivedFunctor α W₂] : LF.IsTriangulated