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₂]
:
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₂]
: