# 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} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} (comm : = u₁₃) {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} (h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles) {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} (h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles) {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} (h₁₃ : 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₁ {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
theorem CategoryTheory.Triangulated.Octahedron.comm₂ {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
CategoryTheory.CategoryStruct.comp self.m₁ w₁₃ = w₁₂
theorem CategoryTheory.Triangulated.Octahedron.comm₃ {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
CategoryTheory.CategoryStruct.comp v₁₃ self.m₃ = v₂₃
theorem CategoryTheory.Triangulated.Octahedron.comm₄ {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
theorem CategoryTheory.Triangulated.Octahedron.mem {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
CategoryTheory.Pretriangulated.Triangle.mk self.m₁ self.m₃ (CategoryTheory.CategoryStruct.comp w₂₃ (.map v₁₂)) CategoryTheory.Pretriangulated.distinguishedTriangles
instance CategoryTheory.Triangulated.instNonemptyOctahedron {C : Type u_1} [] [∀ (n : ), .Additive] (X : C) :
Equations
• =
theorem CategoryTheory.Triangulated.Octahedron.comm₂_assoc {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) {Z : C} (h : .obj X₁ Z) :
theorem CategoryTheory.Triangulated.Octahedron.comm₄_assoc {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) {Z : C} (h : .obj X₂ Z) :
theorem CategoryTheory.Triangulated.Octahedron.comm₁_assoc {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : 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} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : 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} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
h.triangle.obj₁ = Z₁₂
@[simp]
theorem CategoryTheory.Triangulated.Octahedron.triangle_mor₂ {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
h.triangle.mor₂ = h.m₃
@[simp]
theorem CategoryTheory.Triangulated.Octahedron.triangle_obj₃ {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
h.triangle.obj₃ = Z₂₃
@[simp]
theorem CategoryTheory.Triangulated.Octahedron.triangle_mor₃ {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
h.triangle.mor₃ = CategoryTheory.CategoryStruct.comp w₂₃ (.map v₁₂)
@[simp]
theorem CategoryTheory.Triangulated.Octahedron.triangle_mor₁ {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
h.triangle.mor₁ = h.m₁
@[simp]
theorem CategoryTheory.Triangulated.Octahedron.triangle_obj₂ {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
h.triangle.obj₂ = Z₁₃
def CategoryTheory.Triangulated.Octahedron.triangle {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : 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} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
h.triangleMorphism₁.hom₂ = u₂₃
@[simp]
theorem CategoryTheory.Triangulated.Octahedron.triangleMorphism₁_hom₃ {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
h.triangleMorphism₁.hom₃ = h.m₁
@[simp]
theorem CategoryTheory.Triangulated.Octahedron.triangleMorphism₁_hom₁ {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
h.triangleMorphism₁.hom₁ =
def CategoryTheory.Triangulated.Octahedron.triangleMorphism₁ {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :

The first morphism of triangles given by an octahedron.

Equations
• h.triangleMorphism₁ = { hom₁ := , hom₂ := u₂₃, hom₃ := h.m₁, comm₁ := , comm₂ := , comm₃ := }
Instances For
@[simp]
theorem CategoryTheory.Triangulated.Octahedron.triangleMorphism₂_hom₃ {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
h.triangleMorphism₂.hom₃ = h.m₃
@[simp]
theorem CategoryTheory.Triangulated.Octahedron.triangleMorphism₂_hom₂ {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
h.triangleMorphism₂.hom₂ =
@[simp]
theorem CategoryTheory.Triangulated.Octahedron.triangleMorphism₂_hom₁ {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :
h.triangleMorphism₂.hom₁ = u₁₂
def CategoryTheory.Triangulated.Octahedron.triangleMorphism₂ {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} {comm : = u₁₃} {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) :

The second morphism of triangles given an octahedron.

Equations
• h.triangleMorphism₂ = { hom₁ := u₁₂, hom₂ := , hom₃ := h.m₃, comm₁ := , comm₂ := , comm₃ := }
Instances For
def CategoryTheory.Triangulated.Octahedron.ofIso {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} (u₁₂ : X₁ X₂) (u₂₃ : X₂ X₃) (u₁₃ : X₁ X₃) (comm : = u₁₃) {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} (h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles) {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} (h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles) {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} (h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles) {X₁' : C} {X₂' : C} {X₃' : C} {Z₁₂' : C} {Z₂₃' : C} {Z₁₃' : C} (u₁₂' : X₁' X₂') (u₂₃' : X₂' X₃') (u₁₃' : X₁' X₃') (comm' : = u₁₃') (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₁₂' .obj X₁') (h₁₂' : CategoryTheory.Pretriangulated.Triangle.mk u₁₂' v₁₂' w₁₂' CategoryTheory.Pretriangulated.distinguishedTriangles) (v₂₃' : X₃' Z₂₃') (w₂₃' : Z₂₃' .obj X₂') (h₂₃' : CategoryTheory.Pretriangulated.Triangle.mk u₂₃' v₂₃' w₂₃' CategoryTheory.Pretriangulated.distinguishedTriangles) (v₁₃' : X₃' Z₁₃') (w₁₃' : Z₁₃' .obj X₁') (h₁₃' : CategoryTheory.Pretriangulated.Triangle.mk u₁₃' v₁₃' w₁₃' CategoryTheory.Pretriangulated.distinguishedTriangles) (H : CategoryTheory.Triangulated.Octahedron comm' 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
class CategoryTheory.IsTriangulated (C : Type u_1) [] [∀ (n : ), .Additive] :

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

• octahedron_axiom : ∀ {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} (comm : = u₁₃) {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} (h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles) {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} (h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles) {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} (h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles), Nonempty (CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)

the octahedron axiom (TR 4)

Instances
theorem CategoryTheory.IsTriangulated.octahedron_axiom {C : Type u_1} [] [∀ (n : ), .Additive] [self : ] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} (comm : = u₁₃) {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} (h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles) {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} (h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles) {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} (h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles) :
Nonempty (CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)

the octahedron axiom (TR 4)

def CategoryTheory.Triangulated.someOctahedron' {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} (comm : = u₁₃) {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.distinguishedTriangles} :
CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃

A choice of octahedron given by the octahedron axiom.

Equations
• = .some
Instances For
def CategoryTheory.Triangulated.someOctahedron {C : Type u_1} [] [∀ (n : ), .Additive] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {Z₁₃ : C} {u₁₂ : X₁ X₂} {u₂₃ : X₂ X₃} {u₁₃ : X₁ X₃} (comm : = u₁₃) {v₁₂ : X₂ Z₁₂} {w₁₂ : Z₁₂ .obj X₁} (h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles) {v₂₃ : X₃ Z₂₃} {w₂₃ : Z₂₃ .obj X₂} (h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles) {v₁₃ : X₃ Z₁₃} {w₁₃ : Z₁₃ .obj X₁} (h₁₃ : 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} [] [∀ (n : ), .Additive] (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₁₂ .obj X₁) (h₁₂ : CategoryTheory.Pretriangulated.distinguishedTriangles) (v₂₃ : X₃ Z₂₃) (w₂₃ : Z₂₃ .obj X₂) (h₂₃ : CategoryTheory.Pretriangulated.distinguishedTriangles) (v₁₃ : X₃ Z₁₃) (w₁₃ : Z₁₃ .obj X₁) (h₁₃ : 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.