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.{u_2, 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 u_2

An octahedron is a type of datum whose existence is asserted by the octahedron axiom (TR 4).

• 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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

theorem CategoryTheory.Triangulated.Octahedron.comm₁_assoc {C : Type u_1} [Category.{u_2, 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)

def CategoryTheory.Triangulated.Octahedron.triangle {C : Type u_1} [Category.{u_2, 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_obj₁ {C : Type u_1} [Category.{u_2, 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_mor₃ {C : Type u_1} [Category.{u_2, 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.{u_2, 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_mor₂ {C : Type u_1} [Category.{u_2, 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.{u_2, 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_obj₃ {C : Type u_1} [Category.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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₁

def CategoryTheory.Triangulated.Octahedron.triangleMorphism₂ {C : Type u_1} [Category.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.ofIso {C : Type u_1} [Category.{u_2, 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.

class CategoryTheory.IsTriangulated (C : Type u_1) [Category.{u_2, 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)

def CategoryTheory.Triangulated.someOctahedron' {C : Type u_1} [Category.{u_2, 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} [IsTriangulated C] : Octahedron comm h₁₂ h₂₃ h₁₃

A choice of octahedron given by the octahedron axiom.

def CategoryTheory.Triangulated.someOctahedron {C : Type u_1} [Category.{u_2, 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.

theorem CategoryTheory.IsTriangulated.mk' {C : Type u_1} [Category.{u_2, 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.