Triangulated Categories

This file contains the definition of triangulated categories, which are pretriangulated categories which satisfy the octahedron axiom.

structure CategoryTheory.Triangulated.Octahedron {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} (h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} (h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} (h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) : Type v_1

An octahedron is a type of datum whose existence is asserted by the octahedron axiom (TR 4). The input is given by the following diagram:

     u₁₃      v₂₃
  X₁ ────> X₃ ────> Z₂₃       Z₁₂⟦1⟧
   \      ^ \        \       ^
 u₁₂\ u₂₃/   \v₁₃     \w₂₃  /v₁₂⟦1⟧'
     V  /     V        V   /
      X₂       Z₁₃       X₂⟦1⟧
       \        \        ^
     v₁₂\        \w₁₃   /u₁₂⟦1⟧'
         V        V    /
          Z₁₂ ───> X₁⟦1⟧
              w₁₂

where u₁₂ ≫ u₂₃ = u₁₃ and (u₁₂,v₁₂,w₁₂), (u₁₃,v₁₃,w₁₃) and (u₂₃,v₂₃,w₂₃) are distinguished triangles.. An Octahedron for this data consists of maps m₁ : Z₁₂ ⟶ Z₁₃ and m₃ : Z₁₃ ⟶ Z₂₃ such that (m₁, m₃, w₂₃ ≫ v₁₂⟦1⟧') is a distinguished triangle and the completed diagram commutes:

     u₁₃      v₂₃
  X₁ ────> X₃ ────> Z₂₃ ────> Z₁₂⟦1⟧
   \      ^ \      ^  \       ^
 u₁₂\ u₂₃/   \v₁₃ /m₃  \w₂₃  /v₁₂⟦1⟧'
     V  /     V  /       V   /
      X₂       Z₁₃       X₂⟦1⟧
       \      ^  \        ^
     v₁₂\    /m₁  \w₁₃   /u₁₂⟦1⟧'
         V  /      V    /
          Z₁₂ ───> X₁⟦1⟧
              w₁₂

• m₁ : Z₁₂ ⟶ Z₁₃

  m₁ is the morphism a of (TR 4) as presented in Stacks.

• m₃ : Z₁₃ ⟶ Z₂₃

  m₃ is the morphism b of (TR 4) as presented in Stacks.

• comm₁ : CategoryStruct.comp v₁₂ self.m₁ = CategoryStruct.comp u₂₃ v₁₃
• comm₂ : CategoryStruct.comp self.m₁ w₁₃ = w₁₂
• comm₃ : CategoryStruct.comp v₁₃ self.m₃ = v₂₃
• comm₄ : CategoryStruct.comp w₁₃ ((shiftFunctor C 1).map u₁₂) = CategoryStruct.comp self.m₃ w₂₃
• mem : Pretriangulated.Triangle.mk self.m₁ self.m₃ (CategoryStruct.comp w₂₃ ((shiftFunctor C 1).map v₁₂)) ∈ Pretriangulated.distinguishedTriangles

instance CategoryTheory.Triangulated.instNonemptyOctahedron {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : C) : Nonempty (Octahedron ⋯ ⋯ ⋯ ⋯)

theorem CategoryTheory.Triangulated.Octahedron.comm₃_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (self : Octahedron comm h₁₂ h₂₃ h₁₃) {Z : C} (h : Z₂₃ ⟶ Z) : CategoryStruct.comp v₁₃ (CategoryStruct.comp self.m₃ h) = CategoryStruct.comp v₂₃ h

theorem CategoryTheory.Triangulated.Octahedron.comm₄_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (self : Octahedron comm h₁₂ h₂₃ h₁₃) {Z : C} (h : (shiftFunctor C 1).obj X₂ ⟶ Z) : CategoryStruct.comp w₁₃ (CategoryStruct.comp ((shiftFunctor C 1).map u₁₂) h) = CategoryStruct.comp self.m₃ (CategoryStruct.comp w₂₃ h)

theorem CategoryTheory.Triangulated.Octahedron.comm₁_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (self : Octahedron comm h₁₂ h₂₃ h₁₃) {Z : C} (h : Z₁₃ ⟶ Z) : CategoryStruct.comp v₁₂ (CategoryStruct.comp self.m₁ h) = CategoryStruct.comp u₂₃ (CategoryStruct.comp v₁₃ h)

theorem CategoryTheory.Triangulated.Octahedron.comm₂_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (self : Octahedron comm h₁₂ h₂₃ h₁₃) {Z : C} (h : (shiftFunctor C 1).obj X₁ ⟶ Z) : CategoryStruct.comp self.m₁ (CategoryStruct.comp w₁₃ h) = CategoryStruct.comp w₁₂ h

def CategoryTheory.Triangulated.Octahedron.triangle {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) : Pretriangulated.Triangle C

The triangle Z₁₂ ⟶ Z₁₃ ⟶ Z₂₃ ⟶ Z₁₂⟦1⟧ given by an octahedron.

@[simp]

theorem CategoryTheory.Triangulated.Octahedron.triangle_mor₂ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) : h.triangle.mor₂ = h.m₃

@[simp]

theorem CategoryTheory.Triangulated.Octahedron.triangle_mor₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) : h.triangle.mor₁ = h.m₁

@[simp]

theorem CategoryTheory.Triangulated.Octahedron.triangle_mor₃ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) : h.triangle.mor₃ = CategoryStruct.comp w₂₃ ((shiftFunctor C 1).map v₁₂)

@[simp]

theorem CategoryTheory.Triangulated.Octahedron.triangle_obj₂ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) : h.triangle.obj₂ = Z₁₃

@[simp]

theorem CategoryTheory.Triangulated.Octahedron.triangle_obj₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) : h.triangle.obj₁ = Z₁₂

@[simp]

theorem CategoryTheory.Triangulated.Octahedron.triangle_obj₃ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) : h.triangle.obj₃ = Z₂₃

def CategoryTheory.Triangulated.Octahedron.triangleMorphism₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ⟶ Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃

The first morphism of triangles given by an octahedron.

@[simp]

theorem CategoryTheory.Triangulated.Octahedron.triangleMorphism₁_hom₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) : h.triangleMorphism₁.hom₁ = CategoryStruct.id X₁

@[simp]

theorem CategoryTheory.Triangulated.Octahedron.triangleMorphism₁_hom₂ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) : h.triangleMorphism₁.hom₂ = u₂₃

@[simp]

theorem CategoryTheory.Triangulated.Octahedron.triangleMorphism₁_hom₃ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) : h.triangleMorphism₁.hom₃ = h.m₁

def CategoryTheory.Triangulated.Octahedron.triangleMorphism₂ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ⟶ Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃

The second morphism of triangles given an octahedron.

@[simp]

theorem CategoryTheory.Triangulated.Octahedron.triangleMorphism₂_hom₃ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) : h.triangleMorphism₂.hom₃ = h.m₃

@[simp]

theorem CategoryTheory.Triangulated.Octahedron.triangleMorphism₂_hom₂ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) : h.triangleMorphism₂.hom₂ = CategoryStruct.id X₃

@[simp]

theorem CategoryTheory.Triangulated.Octahedron.triangleMorphism₂_hom₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) : h.triangleMorphism₂.hom₁ = u₁₂

noncomputable def CategoryTheory.Triangulated.Octahedron.ofIso {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} (u₁₂ : X₁ ⟶ X₂) (u₂₃ : X₂ ⟶ X₃) (u₁₃ : X₁ ⟶ X₃) (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} (h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} (h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} (h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) {X₁' X₂' X₃' Z₁₂' Z₂₃' Z₁₃' : C} (u₁₂' : X₁' ⟶ X₂') (u₂₃' : X₂' ⟶ X₃') (u₁₃' : X₁' ⟶ X₃') (comm' : CategoryStruct.comp u₁₂' u₂₃' = u₁₃') (e₁ : X₁ ≅ X₁') (e₂ : X₂ ≅ X₂') (e₃ : X₃ ≅ X₃') (comm₁₂ : CategoryStruct.comp u₁₂ e₂.hom = CategoryStruct.comp e₁.hom u₁₂') (comm₂₃ : CategoryStruct.comp u₂₃ e₃.hom = CategoryStruct.comp e₂.hom u₂₃') (v₁₂' : X₂' ⟶ Z₁₂') (w₁₂' : Z₁₂' ⟶ (shiftFunctor C 1).obj X₁') (h₁₂' : Pretriangulated.Triangle.mk u₁₂' v₁₂' w₁₂' ∈ Pretriangulated.distinguishedTriangles) (v₂₃' : X₃' ⟶ Z₂₃') (w₂₃' : Z₂₃' ⟶ (shiftFunctor C 1).obj X₂') (h₂₃' : Pretriangulated.Triangle.mk u₂₃' v₂₃' w₂₃' ∈ Pretriangulated.distinguishedTriangles) (v₁₃' : X₃' ⟶ Z₁₃') (w₁₃' : Z₁₃' ⟶ (shiftFunctor C 1).obj X₁') (h₁₃' : Pretriangulated.Triangle.mk u₁₃' v₁₃' w₁₃' ∈ Pretriangulated.distinguishedTriangles) (H : Octahedron comm' h₁₂' h₂₃' h₁₃') : Octahedron comm h₁₂ h₂₃ h₁₃

When two diagrams are isomorphic, an octahedron for one gives an octahedron for the other.

structure CategoryTheory.Triangulated.Octahedron' {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} (h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} (h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} (h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) : Type v_1

An octahedron' is a type of datum whose existence follows from the octahedron axiom (TR 4). It is a rotated version of an octahedron. The input is given by the following diagram:

       v₁₂       u₁₃      w₂₃
  Z₁₂ ────> X₁ ─────> X₃ ─────> Z₂₃⟦1⟧
          ^  \       ^  \
      v₁₃/ u₁₂\  u₂₃/    \w₁₃
        /     V    /      V
      Z₁₃       X₂       Z₁₃⟦1⟧
                ^ \
            v₂₃/   \w₁₂
              /     V
           Z₂₃      Z₁₂⟦1⟧

where u₁₂ ≫ u₂₃ = u₁₃ and (v₁₂,u₁₂,w₁₂), (v₁₃,u₁₃,w₁₃) and (v₂₃,u₂₃,w₂₃) are distinguished triangles.. An Octahedron' for this data consists of maps m₁ : Z₁₂ ⟶ Z₁₃ and m₃ : Z₁₃ ⟶ Z₂₃ such that (m₁, m₃, v₂₃ ≫ w₁₂) is a distinguished triangle and the completed diagram commutes:

       v₁₂       u₁₃      w₂₃
  Z₁₂ ────> X₁ ─────> X₃ ─────> Z₂₃⟦1⟧
   \       ^  \       ^  \      ^
  m₁\  v₁₃/ u₁₂\  u₂₃/    \w₁₃ /m₃⟦1⟧'
     V   /     V    /      V  /
      Z₁₃       X₂       Z₁₃⟦1⟧
       \        ^ \      ^
      m₃\   v₂₃/   \w₁₂ /m₁⟦1⟧'
         V    /     V  /
          Z₂₃  ────> Z₁₂⟦1⟧

• m₁ : Z₁₂ ⟶ Z₁₃

  m₁ is the morphism a of (TR 4) as presented in Stacks.

• m₃ : Z₁₃ ⟶ Z₂₃

  m₁ is the morphism b of (TR 4) as presented in Stacks.

• comm₁ : CategoryStruct.comp self.m₁ v₁₃ = v₁₂
• comm₂ : CategoryStruct.comp w₁₂ ((shiftFunctor C 1).map self.m₁) = CategoryStruct.comp u₂₃ w₁₃
• comm₃ : CategoryStruct.comp w₁₃ ((shiftFunctor C 1).map self.m₃) = w₂₃
• comm₄ : CategoryStruct.comp self.m₃ v₂₃ = CategoryStruct.comp v₁₃ u₁₂
• mem : Pretriangulated.Triangle.mk self.m₁ self.m₃ (CategoryStruct.comp v₂₃ w₁₂) ∈ Pretriangulated.distinguishedTriangles

theorem CategoryTheory.Triangulated.Octahedron'.comm₁_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} {h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} {h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} {h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (self : Octahedron' comm h₁₂ h₂₃ h₁₃) {Z : C} (h : X₁ ⟶ Z) : CategoryStruct.comp self.m₁ (CategoryStruct.comp v₁₃ h) = CategoryStruct.comp v₁₂ h

theorem CategoryTheory.Triangulated.Octahedron'.comm₂_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} {h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} {h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} {h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (self : Octahedron' comm h₁₂ h₂₃ h₁₃) {Z : C} (h : (shiftFunctor C 1).obj Z₁₃ ⟶ Z) : CategoryStruct.comp w₁₂ (CategoryStruct.comp ((shiftFunctor C 1).map self.m₁) h) = CategoryStruct.comp u₂₃ (CategoryStruct.comp w₁₃ h)

theorem CategoryTheory.Triangulated.Octahedron'.comm₄_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} {h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} {h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} {h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (self : Octahedron' comm h₁₂ h₂₃ h₁₃) {Z : C} (h : X₂ ⟶ Z) : CategoryStruct.comp self.m₃ (CategoryStruct.comp v₂₃ h) = CategoryStruct.comp v₁₃ (CategoryStruct.comp u₁₂ h)

theorem CategoryTheory.Triangulated.Octahedron'.comm₃_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} {h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} {h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} {h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (self : Octahedron' comm h₁₂ h₂₃ h₁₃) {Z : C} (h : (shiftFunctor C 1).obj Z₂₃ ⟶ Z) : CategoryStruct.comp w₁₃ (CategoryStruct.comp ((shiftFunctor C 1).map self.m₃) h) = CategoryStruct.comp w₂₃ h

def CategoryTheory.Triangulated.Octahedron'.triangle {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} (h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} (h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} (h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) (h : Octahedron' comm h₁₂ h₂₃ h₁₃) : Pretriangulated.Triangle C

The triangle Z₁₂ ⟶ Z₁₃ ⟶ Z₂₃ ⟶ Z₁₂⟦1⟧ given by an Octahedron'.

@[simp]

theorem CategoryTheory.Triangulated.Octahedron'.triangle_mor₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} (h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} (h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} (h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) (h : Octahedron' comm h₁₂ h₂₃ h₁₃) : (triangle comm h₁₂ h₂₃ h₁₃ h).mor₁ = h.m₁

@[simp]

theorem CategoryTheory.Triangulated.Octahedron'.triangle_obj₃ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} (h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} (h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} (h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) (h : Octahedron' comm h₁₂ h₂₃ h₁₃) : (triangle comm h₁₂ h₂₃ h₁₃ h).obj₃ = Z₂₃

@[simp]

theorem CategoryTheory.Triangulated.Octahedron'.triangle_mor₂ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} (h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} (h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} (h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) (h : Octahedron' comm h₁₂ h₂₃ h₁₃) : (triangle comm h₁₂ h₂₃ h₁₃ h).mor₂ = h.m₃

@[simp]

theorem CategoryTheory.Triangulated.Octahedron'.triangle_obj₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} (h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} (h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} (h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) (h : Octahedron' comm h₁₂ h₂₃ h₁₃) : (triangle comm h₁₂ h₂₃ h₁₃ h).obj₁ = Z₁₂

@[simp]

theorem CategoryTheory.Triangulated.Octahedron'.triangle_mor₃ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} (h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} (h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} (h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) (h : Octahedron' comm h₁₂ h₂₃ h₁₃) : (triangle comm h₁₂ h₂₃ h₁₃ h).mor₃ = CategoryStruct.comp v₂₃ w₁₂

@[simp]

theorem CategoryTheory.Triangulated.Octahedron'.triangle_obj₂ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} (h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} (h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} (h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) (h : Octahedron' comm h₁₂ h₂₃ h₁₃) : (triangle comm h₁₂ h₂₃ h₁₃ h).obj₂ = Z₁₃

def CategoryTheory.Triangulated.Octahedron'.triangleMorphism₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} (h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} (h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} (h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) (h : Octahedron' comm h₁₂ h₂₃ h₁₃) : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ⟶ Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃

The first morphism of triangles given by an Octahedron'.

@[simp]

theorem CategoryTheory.Triangulated.Octahedron'.triangleMorphism₁_hom₂ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} (h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} (h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} (h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) (h : Octahedron' comm h₁₂ h₂₃ h₁₃) : (triangleMorphism₁ comm h₁₂ h₂₃ h₁₃ h).hom₂ = CategoryStruct.id X₁

@[simp]

theorem CategoryTheory.Triangulated.Octahedron'.triangleMorphism₁_hom₃ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} (h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} (h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} (h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) (h : Octahedron' comm h₁₂ h₂₃ h₁₃) : (triangleMorphism₁ comm h₁₂ h₂₃ h₁₃ h).hom₃ = u₂₃

@[simp]

theorem CategoryTheory.Triangulated.Octahedron'.triangleMorphism₁_hom₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} (h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} (h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} (h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) (h : Octahedron' comm h₁₂ h₂₃ h₁₃) : (triangleMorphism₁ comm h₁₂ h₂₃ h₁₃ h).hom₁ = h.m₁

def CategoryTheory.Triangulated.Octahedron'.triangleMorphism₂ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} (h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} (h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} (h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) (h : Octahedron' comm h₁₂ h₂₃ h₁₃) : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ⟶ Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃

The second morphism of triangles given by an Octahedron'.

@[simp]

theorem CategoryTheory.Triangulated.Octahedron'.triangleMorphism₂_hom₃ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} (h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} (h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} (h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) (h : Octahedron' comm h₁₂ h₂₃ h₁₃) : (triangleMorphism₂ comm h₁₂ h₂₃ h₁₃ h).hom₃ = CategoryStruct.id X₃

@[simp]

theorem CategoryTheory.Triangulated.Octahedron'.triangleMorphism₂_hom₂ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} (h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} (h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} (h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) (h : Octahedron' comm h₁₂ h₂₃ h₁₃) : (triangleMorphism₂ comm h₁₂ h₂₃ h₁₃ h).hom₂ = u₁₂

@[simp]

theorem CategoryTheory.Triangulated.Octahedron'.triangleMorphism₂_hom₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} (h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} (h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} (h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) (h : Octahedron' comm h₁₂ h₂₃ h₁₃) : (triangleMorphism₂ comm h₁₂ h₂₃ h₁₃ h).hom₁ = h.m₃

class CategoryTheory.IsTriangulated (C : Type u_1) [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : Prop

A triangulated category is a pretriangulated category which satisfies the octahedron axiom (TR 4).

• octahedron_axiom {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} (h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} (h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} (h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) : Nonempty (Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)

  the octahedron axiom (TR 4)

noncomputable def CategoryTheory.Triangulated.someOctahedron {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} (h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} (h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} (h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) : Octahedron comm h₁₂ h₂₃ h₁₃

A choice of octahedron given by the octahedron axiom.

noncomputable def CategoryTheory.Triangulated.someOctahedron' {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁} {w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂} (h₁₂ : Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃} (h₂₃ : Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃} (h₁₃ : Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles) : Octahedron' comm h₁₂ h₂₃ h₁₃

A choice of octahedron' given by the octahedron axiom.

theorem CategoryTheory.IsTriangulated.mk' {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (h : ∀ ⦃X₁' X₂' X₃' : C⦄ (u₁₂' : X₁' ⟶ X₂') (u₂₃' : X₂' ⟶ X₃'), ∃ (X₁ : C) (X₂ : C) (X₃ : C) (Z₁₂ : C) (Z₂₃ : C) (Z₁₃ : C) (u₁₂ : X₁ ⟶ X₂) (u₂₃ : X₂ ⟶ X₃) (e₁ : X₁' ≅ X₁) (e₂ : X₂' ≅ X₂) (e₃ : X₃' ≅ X₃) (_ : CategoryStruct.comp u₁₂' e₂.hom = CategoryStruct.comp e₁.hom u₁₂) (_ : CategoryStruct.comp u₂₃' e₃.hom = CategoryStruct.comp e₂.hom u₂₃) (v₁₂ : X₂ ⟶ Z₁₂) (w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁) (h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) (v₂₃ : X₃ ⟶ Z₂₃) (w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂) (h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) (v₁₃ : X₃ ⟶ Z₁₃) (w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁) (h₁₃ : Pretriangulated.Triangle.mk (CategoryStruct.comp u₁₂ u₂₃) v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles), Nonempty (Triangulated.Octahedron ⋯ h₁₂ h₂₃ h₁₃)) : IsTriangulated C

Constructor for IsTriangulated C which shows that it suffices to obtain an octahedron for a suitable isomorphic diagram instead of the given diagram.