mathlib documentation

category_theory.triangulated.triangulated

Triangulated Categories #

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

structure category_theory.triangulated.octahedron {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} (comm : u₁₂ u₂₃ = u₁₃) {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} (h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C) {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} (h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C) {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} (h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C) :
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 category_theory.triangulated.octahedron
theorem category_theory.triangulated.octahedron.comm₂_assoc {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} {h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} {h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} {h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C} (self : category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃) {X' : C} (f' : (category_theory.shift_functor C 1).obj X₁ X') :
self.m₁ w₁₃ f' = w₁₂ f'
theorem category_theory.triangulated.octahedron.comm₁_assoc {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} {h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} {h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} {h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C} (self : category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃) {X' : C} (f' : Z₁₃ X') :
v₁₂ self.m₁ f' = u₂₃ v₁₃ f'
theorem category_theory.triangulated.octahedron.comm₄_assoc {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} {h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} {h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} {h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C} (self : category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃) {X' : C} (f' : (category_theory.shift_functor C 1).obj X₂ X') :
w₁₃ (category_theory.shift_functor C 1).map u₁₂ f' = self.m₃ w₂₃ f'
theorem category_theory.triangulated.octahedron.comm₃_assoc {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} {h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} {h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} {h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C} (self : category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃) {X' : C} (f' : Z₂₃ X') :
v₁₃ self.m₃ f' = v₂₃ f'
@[simp]
theorem category_theory.triangulated.octahedron.triangle_obj₃ {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} {h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} {h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} {h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C} (h : category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃) :
h.triangle.obj₃ = Z₂₃
@[simp]
theorem category_theory.triangulated.octahedron.triangle_mor₃ {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} {h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} {h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} {h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C} (h : category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃) :
@[simp]
theorem category_theory.triangulated.octahedron.triangle_mor₂ {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} {h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} {h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} {h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C} (h : category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃) :
@[simp]
theorem category_theory.triangulated.octahedron.triangle_mor₁ {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} {h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} {h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} {h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C} (h : category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃) :
@[simp]
theorem category_theory.triangulated.octahedron.triangle_obj₁ {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} {h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} {h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} {h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C} (h : category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃) :
h.triangle.obj₁ = Z₁₂
def category_theory.triangulated.octahedron.triangle {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} {h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} {h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} {h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C} (h : category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃) :

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

Equations
@[simp]
theorem category_theory.triangulated.octahedron.triangle_obj₂ {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} {h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} {h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} {h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C} (h : category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃) :
h.triangle.obj₂ = Z₁₃
@[simp]
theorem category_theory.triangulated.octahedron.triangle_morphism₁_hom₂ {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} {h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} {h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} {h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C} (h : category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃) :
@[simp]
theorem category_theory.triangulated.octahedron.triangle_morphism₁_hom₃ {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} {h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} {h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} {h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C} (h : category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃) :
def category_theory.triangulated.octahedron.triangle_morphism₁ {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} {h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} {h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} {h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C} (h : category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃) :

The first morphism of triangles given by an octahedron.

Equations
@[simp]
theorem category_theory.triangulated.octahedron.triangle_morphism₁_hom₁ {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} {h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} {h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} {h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C} (h : category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃) :
def category_theory.triangulated.octahedron.triangle_morphism₂ {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} {h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} {h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} {h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C} (h : category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃) :

The second morphism of triangles given an octahedron.

Equations
@[simp]
theorem category_theory.triangulated.octahedron.triangle_morphism₂_hom₁ {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} {h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} {h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} {h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C} (h : category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃) :
@[simp]
theorem category_theory.triangulated.octahedron.triangle_morphism₂_hom₃ {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} {h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} {h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} {h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C} (h : category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃) :
@[simp]
theorem category_theory.triangulated.octahedron.triangle_morphism₂_hom₂ {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} {h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} {h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} {h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C} (h : category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃) :
@[class]

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

Instances for category_theory.is_triangulated
  • category_theory.is_triangulated.has_sizeof_inst
noncomputable def category_theory.triangulated.some_octahedron {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ] [ (n : ), (category_theory.shift_functor C n).additive] [category_theory.pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} (comm : u₁₂ u₂₃ = u₁₃) {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ (category_theory.shift_functor C 1).obj X₁} (h₁₂ : category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ dist_triang C) {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ (category_theory.shift_functor C 1).obj X₂} (h₂₃ : category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃ dist_triang C) {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ (category_theory.shift_functor C 1).obj X₁} (h₁₃ : category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ dist_triang C) [category_theory.is_triangulated C] :
category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃

A choice of octahedron given by the octahedron axiom.

Equations