Left derived functors are triangulated #
Let F : C ⥤ D, L : C ⥤ H, F' : H ⥤ D be functors between
pretriangulated categories. Let α : L ⋙ F' ⟶ 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_rightExtension {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] (α : L.comp F' ⟶ 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)) :