Completing morphisms of stable triangles

A commutative square on the first arrow of distinguished stable triangles extends to a morphism of triangles. This is the morphism axiom for the Happel triangulation, proved without assuming a pretriangulated structure on the stable category.

Completion holds both for the standard triangles arising from conflations and for all distinguished stable triangles, giving the morphism-of-triangles axiom (TR3).

References

• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2.

theorem TauCeti.ExactStructure.IsFrobenius.complete_stable_distinguished_triangle_morphism {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.IsFrobenius) (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle E.ProjectiveStableCategory) : T₁ ∈ hE.stableDistinguishedTriangles → T₂ ∈ hE.stableDistinguishedTriangles → ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂), CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ → ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧ CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor E.ProjectiveStableCategory 1).map a) = CategoryTheory.CategoryStruct.comp c T₂.mor₃

The morphism axiom for distinguished stable triangles: every commutative square on their first arrows extends to a morphism of triangles. No triangulated structure is assumed.