The distinguished triangle of a short exact sequence in an abelian category

Given a short exact short complex S in an abelian category, we construct the associated distinguished triangle in the derived category: (singleFunctor C 0).obj S.X₁ ⟶ (singleFunctor C 0).obj S.X₂ ⟶ (singleFunctor C 0).obj S.X₃ ⟶ ...

TODO

• when the canonical t-structure on the derived category is formalized, refactor this definition to make it a particular case of the triangle induced by a short exact sequence in the heart of a t-structure

noncomputable def CategoryTheory.ShortComplex.ShortExact.singleδ {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] {S : ShortComplex C} (hS : S.ShortExact) : (DerivedCategory.singleFunctor C 0).obj S.X₃ ⟶ (shiftFunctor (DerivedCategory C) 1).obj ((DerivedCategory.singleFunctor C 0).obj S.X₁)

The connecting homomorphism (singleFunctor C 0).obj S.X₃ ⟶ ((singleFunctor C 0).obj S.X₁)⟦(1 : ℤ)⟧ in the derived category of C when S is a short exact short complex in C.

noncomputable def CategoryTheory.ShortComplex.ShortExact.singleTriangle {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] {S : ShortComplex C} (hS : S.ShortExact) : Pretriangulated.Triangle (DerivedCategory C)

The (distinguished) triangle in the derived category of C given by a short exact short complex in C.

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₁ {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] {S : ShortComplex C} (hS : S.ShortExact) : hS.singleTriangle.mor₁ = (DerivedCategory.singleFunctor C 0).map S.f

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₂ {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] {S : ShortComplex C} (hS : S.ShortExact) : hS.singleTriangle.obj₂ = (DerivedCategory.singleFunctor C 0).obj S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₂ {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] {S : ShortComplex C} (hS : S.ShortExact) : hS.singleTriangle.mor₂ = (DerivedCategory.singleFunctor C 0).map S.g

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₃ {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] {S : ShortComplex C} (hS : S.ShortExact) : hS.singleTriangle.mor₃ = hS.singleδ

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₁ {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] {S : ShortComplex C} (hS : S.ShortExact) : hS.singleTriangle.obj₁ = (DerivedCategory.singleFunctor C 0).obj S.X₁

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₃ {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] {S : ShortComplex C} (hS : S.ShortExact) : hS.singleTriangle.obj₃ = (DerivedCategory.singleFunctor C 0).obj S.X₃

noncomputable def CategoryTheory.ShortComplex.ShortExact.singleTriangleIso {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] {S : ShortComplex C} (hS : S.ShortExact) : hS.singleTriangle ≅ DerivedCategory.triangleOfSES ⋯

Given a short exact complex S in C that is short exact (hS), this is the canonical isomorphism between the triangle hS.singleTriangle in the derived category and the triangle attached to the corresponding short exact sequence of cochain complexes after the application of the single functor.

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁ {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] {S : ShortComplex C} (hS : S.ShortExact) : hS.singleTriangleIso.hom.hom₁ = ((DerivedCategory.singleFunctorsPostcompQIso C).hom.hom 0).app S.X₁

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃ {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] {S : ShortComplex C} (hS : S.ShortExact) : hS.singleTriangleIso.inv.hom₃ = ((DerivedCategory.singleFunctorsPostcompQIso C).inv.hom 0).app S.X₃

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂ {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] {S : ShortComplex C} (hS : S.ShortExact) : hS.singleTriangleIso.inv.hom₂ = ((DerivedCategory.singleFunctorsPostcompQIso C).inv.hom 0).app S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃ {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] {S : ShortComplex C} (hS : S.ShortExact) : hS.singleTriangleIso.hom.hom₃ = ((DerivedCategory.singleFunctorsPostcompQIso C).hom.hom 0).app S.X₃

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂ {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] {S : ShortComplex C} (hS : S.ShortExact) : hS.singleTriangleIso.hom.hom₂ = ((DerivedCategory.singleFunctorsPostcompQIso C).hom.hom 0).app S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁ {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] {S : ShortComplex C} (hS : S.ShortExact) : hS.singleTriangleIso.inv.hom₁ = ((DerivedCategory.singleFunctorsPostcompQIso C).inv.hom 0).app S.X₁

theorem CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] {S : ShortComplex C} (hS : S.ShortExact) : hS.singleTriangle ∈ Pretriangulated.distinguishedTriangles

The distinguished triangle in the derived category of C given by a short exact short complex in C.