CategoryTheory.IsTriangulated.octahedron_axiom

theorem CategoryTheory.IsTriangulated.octahedron_axiom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C] [self : CategoryTheory.IsTriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} (h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂} (h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} (h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), Nonempty (CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)

The theorem `CategoryTheory.IsTriangulated.octahedron_axiom` states the octahedron axiom (TR 4) in the setting of pre-triangulated categories. Given a category `C` that is preadditive, has a zero object, has shifts, and is pretriangulated, and given morphisms `X₁ ⟶ X₂`, `X₂ ⟶ X₃`, `X₁ ⟶ X₃` such that their composition equals `u₁₃`. Also, given three distinguished triangles `X₁ ⟶ X₂ ⟶ Z₁₂`, `X₂ ⟶ X₃ ⟶ Z₂₃`, and `X₁ ⟶ X₃ ⟶ Z₁₃`, the axiom asserts the existence of a triangulated octahedron. This octahedron is a commutative diagram involving the vertices and morphisms of the given distinguished triangles, and it provides a specific relationship between the morphisms and objects in a triangulated category.

More concisely: Given a preadditive, zero-object-having, pretriangulated category with shifts, and given morphisms and distinguished triangles as in the statement, the octahedron axiom asserts the existence of a commutative diagram relating their morphisms and vertices.