category_theory.triangulated.triangulated

source

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

m₁ : Z₁₂ ⟶ Z₁₃
m₃ : Z₁₃ ⟶ Z₂₃
comm₁ : v₁₂ ≫ self.m₁ = u₂₃ ≫ v₁₃
comm₂ : self.m₁ ≫ w₁₃ = w₁₂
comm₃ : v₁₃ ≫ self.m₃ = v₂₃
comm₄ : w₁₃ ≫ (category_theory.shift_functor C 1).map u₁₂ = self.m₃ ≫ w₂₃
mem : category_theory.pretriangulated.triangle.mk self.m₁ self.m₃ (w₂₃ ≫ (category_theory.shift_functor C 1).map v₁₂) ∈ dist_triang C

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

category_theory.triangulated.octahedron.has_sizeof_inst
category_theory.triangulated.octahedron.nonempty

source

@[protected, instance]

def category_theory.triangulated.octahedron.nonempty {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 : C) :

nonempty (category_theory.triangulated.octahedron _ _ _ _)

source

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'

source

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'

source

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'

source

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'

source

@[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₂₃

source

@[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₁₃) :

h.triangle.mor₃ = w₂₃ ≫ (category_theory.shift_functor C 1).map v₁₂

source

@[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₁₃) :

h.triangle.mor₂ = h.m₃

source

@[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₁₃) :

h.triangle.mor₁ = h.m₁

source

@[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₁₂

source

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₁₃) :

category_theory.pretriangulated.triangle C

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

Equations

h.triangle = category_theory.pretriangulated.triangle.mk h.m₁ h.m₃ (w₂₃ ≫ (category_theory.shift_functor C 1).map v₁₂)

source

@[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₁₃

source

@[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₁₃) :

h.triangle_morphism₁.hom₂ = u₂₃

source

@[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₁₃) :

h.triangle_morphism₁.hom₃ = h.m₁

source

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₁₃) :

category_theory.pretriangulated.triangle.mk u₁₂ v₁₂ w₁₂ ⟶ category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃

The first morphism of triangles given by an octahedron.

Equations

h.triangle_morphism₁ = {hom₁ := 𝟙 X₁, hom₂ := u₂₃, hom₃ := h.m₁, comm₁' := _, comm₂' := _, comm₃' := _}

source

@[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₁₃) :

h.triangle_morphism₁.hom₁ = 𝟙 X₁

source

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₁₃) :

category_theory.pretriangulated.triangle.mk u₁₃ v₁₃ w₁₃ ⟶ category_theory.pretriangulated.triangle.mk u₂₃ v₂₃ w₂₃

The second morphism of triangles given an octahedron.

Equations

h.triangle_morphism₂ = {hom₁ := u₁₂, hom₂ := 𝟙 X₃, hom₃ := h.m₃, comm₁' := _, comm₂' := _, comm₃' := _}

source

@[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₁₃) :

h.triangle_morphism₂.hom₁ = u₁₂

source

@[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₁₃) :

h.triangle_morphism₂.hom₃ = h.m₃

source

@[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₁₃) :

h.triangle_morphism₂.hom₂ = 𝟙 X₃

source

@[class]

structure category_theory.is_triangulated (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] :

Type

octahedron_axiom : ∀ ⦃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), nonempty (category_theory.triangulated.octahedron comm h₁₂ h₂₃ h₁₃)

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

source

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

category_theory.triangulated.some_octahedron comm h₁₂ h₂₃ h₁₃ = _.some

mathlib documentation

Triangulated Categories #