Right derived functors are triangulated #
Let F : C ⥤ D, L : C ⥤ H, F' : H ⥤ D be functors between
pretriangulated categories. Let α : F ⟶ L ⋙ F' be a natural transformation.
We show that F' is triangulated if F, L, F' and α commute with
shifts, F and L are triangulated, and for any morphism f in H,
there exists a distinguished triangle T in C such that
Arrow.mk (L.map T.mor₁) ≅ Arrow.mk f, and α.app T.obj₁, α.app T.obj₂,
and α.app T.obj₃ are isomorphisms.
theorem
CategoryTheory.Functor.isTriangulated_of_leftExtension
{C : Type u_1}
{D : Type u_2}
{H : Type u_3}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[Category.{v_3, u_3} H]
(F' : Functor H D)
{F : Functor C D}
{L : Functor C H}
[HasShift C ℤ]
[HasShift D ℤ]
[HasShift H ℤ]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Limits.HasZeroObject H]
[Preadditive C]
[Preadditive D]
[Preadditive H]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[∀ (n : ℤ), (shiftFunctor H n).Additive]
[Pretriangulated C]
[Pretriangulated D]
[Pretriangulated H]
[F.CommShift ℤ]
[L.CommShift ℤ]
[F'.CommShift ℤ]
[F.IsTriangulated]
[L.IsTriangulated]
(α : F ⟶ L.comp F')
[NatTrans.CommShift α ℤ]
(h :
∀ ⦃X Y : H⦄ (f : X ⟶ Y),
∃ (T : Pretriangulated.Triangle C) (_ : T ∈ Pretriangulated.distinguishedTriangles) (_ : IsIso (α.app T.obj₁)) (_ :
IsIso (α.app T.obj₂)) (_ : IsIso (α.app T.obj₃)), Nonempty (Arrow.mk (L.map T.mor₁) ≅ Arrow.mk f))
: