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
- 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
@[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) :
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') :
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') :
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') :
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') :
@[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₁₃) :
@[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₁₃) :
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
- h.triangle = category_theory.pretriangulated.triangle.mk h.m₁ h.m₃ (w₂₃ ≫ (category_theory.shift_functor C 1).map v₁₂)
@[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₁₃) :
@[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₂₃
@[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₁
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.
@[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₁
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.
@[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₁₂
@[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₃
@[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₃
@[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] :
- 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
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