Documentation

Mathlib.CategoryTheory.Triangulated.Triangulated

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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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) :
Type u_2

An octahedron is a type of datum whose existence is asserted by the octahedron axiom (TR 4), see https://stacks.math.columbia.edu/tag/05QK

Instances For
    theorem CategoryTheory.Triangulated.Octahedron.comm₂_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj X₁ Z) :
    theorem CategoryTheory.Triangulated.Octahedron.comm₄_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj X₂ Z) :
    theorem CategoryTheory.Triangulated.Octahedron.comm₁_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) {Z : C} (h : Z₁₃ Z) :
    theorem CategoryTheory.Triangulated.Octahedron.comm₃_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) {Z : C} (h : Z₂₃ Z) :
    @[simp]
    theorem CategoryTheory.Triangulated.Octahedron.triangle_obj₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
    @[simp]
    theorem CategoryTheory.Triangulated.Octahedron.triangle_mor₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
    @[simp]
    theorem CategoryTheory.Triangulated.Octahedron.triangle_obj₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
    @[simp]
    theorem CategoryTheory.Triangulated.Octahedron.triangle_mor₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
    @[simp]
    theorem CategoryTheory.Triangulated.Octahedron.triangle_mor₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
    @[simp]
    theorem CategoryTheory.Triangulated.Octahedron.triangle_obj₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
    def CategoryTheory.Triangulated.Octahedron.triangle {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :

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

    Equations
    Instances For
      @[simp]
      theorem CategoryTheory.Triangulated.Octahedron.triangleMorphism₁_hom₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
      @[simp]
      theorem CategoryTheory.Triangulated.Octahedron.triangleMorphism₁_hom₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
      @[simp]
      theorem CategoryTheory.Triangulated.Octahedron.triangleMorphism₁_hom₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
      def CategoryTheory.Triangulated.Octahedron.triangleMorphism₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :

      The first morphism of triangles given by an octahedron.

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.Triangulated.Octahedron.triangleMorphism₂_hom₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
        @[simp]
        theorem CategoryTheory.Triangulated.Octahedron.triangleMorphism₂_hom₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
        @[simp]
        theorem CategoryTheory.Triangulated.Octahedron.triangleMorphism₂_hom₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
        def CategoryTheory.Triangulated.Octahedron.triangleMorphism₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :

        The second morphism of triangles given an octahedron.

        Equations
        Instances For
          def CategoryTheory.Triangulated.Octahedron.ofIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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) {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₃') (comm₁₂ : CategoryTheory.CategoryStruct.comp u₁₂ e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom u₁₂') (comm₂₃ : CategoryTheory.CategoryStruct.comp u₂₃ e₃.hom = CategoryTheory.CategoryStruct.comp e₂.hom 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 (CategoryTheory.CategoryStruct.comp u₁₂' u₂₃') v₁₃' w₁₃' CategoryTheory.Pretriangulated.distinguishedTriangles) (H : CategoryTheory.Triangulated.Octahedron h₁₂' h₂₃' h₁₃') :
          CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            A triangulated category is a pretriangulated category which satisfies the octahedron axiom (TR 4), see https://stacks.math.columbia.edu/tag/05QK

            Instances
              def CategoryTheory.Triangulated.someOctahedron' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} [CategoryTheory.IsTriangulated C] :
              CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃

              A choice of octahedron given by the octahedron axiom.

              Equations
              Instances For
                def CategoryTheory.Triangulated.someOctahedron {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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) :
                CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃

                A choice of octahedron given by the octahedron axiom.

                Equations
                Instances For
                  theorem CategoryTheory.IsTriangulated.mk' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [CategoryTheory.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₃) (_ : CategoryTheory.CategoryStruct.comp u₁₂' e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom u₁₂) (_ : CategoryTheory.CategoryStruct.comp u₂₃' e₃.hom = CategoryTheory.CategoryStruct.comp e₂.hom 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 (CategoryTheory.CategoryStruct.comp u₁₂ u₂₃) v₁₃ w₁₃ CategoryTheory.Pretriangulated.distinguishedTriangles), Nonempty (CategoryTheory.Triangulated.Octahedron h₁₂ h₂₃ h₁₃)) :

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