# mathlibdocumentation

category_theory.triangulated.basic

# Triangles #

This file contains the definition of triangles in an additive category with an additive shift. It also defines morphisms between these triangles.

TODO: generalise this to n-angles in n-angulated categories as in https://arxiv.org/abs/1006.4592

structure category_theory.triangulated.triangle (C : Type u)  :
Type (max u v)

A triangle in C is a sextuple (X,Y,Z,f,g,h) where X,Y,Z are objects of C, and f : X ⟶ Y, g : Y ⟶ Z, h : Z ⟶ X⟦1⟧ are morphisms in C. See https://stacks.math.columbia.edu/tag/0144.

@[simp]
theorem category_theory.triangulated.triangle.mk_mor₁ (C : Type u) {X Y Z : C} (f : X Y) (g : Y Z) (h : Z .functor.obj X) :
@[simp]
theorem category_theory.triangulated.triangle.mk_mor₃ (C : Type u) {X Y Z : C} (f : X Y) (g : Y Z) (h : Z .functor.obj X) :
@[simp]
theorem category_theory.triangulated.triangle.mk_obj₂ (C : Type u) {X Y Z : C} (f : X Y) (g : Y Z) (h : Z .functor.obj X) :
@[simp]
theorem category_theory.triangulated.triangle.mk_obj₃ (C : Type u) {X Y Z : C} (f : X Y) (g : Y Z) (h : Z .functor.obj X) :
def category_theory.triangulated.triangle.mk (C : Type u) {X Y Z : C} (f : X Y) (g : Y Z) (h : Z .functor.obj X) :

A triangle (X,Y,Z,f,g,h) in C is defined by the morphisms f : X ⟶ Y, g : Y ⟶ Z and h : Z ⟶ X⟦1⟧.

Equations
@[simp]
theorem category_theory.triangulated.triangle.mk_obj₁ (C : Type u) {X Y Z : C} (f : X Y) (g : Y Z) (h : Z .functor.obj X) :
@[simp]
theorem category_theory.triangulated.triangle.mk_mor₂ (C : Type u) {X Y Z : C} (f : X Y) (g : Y Z) (h : Z .functor.obj X) :
@[instance]
Equations
@[simp]
@[simp]
@[simp]
@[simp]

For each object in C, there is a triangle of the form (X,X,0,𝟙 X,0,0)

Equations
@[simp]
@[simp]
@[ext]

A morphism of triangles (X,Y,Z,f,g,h) ⟶ (X',Y',Z',f',g',h') in C is a triple of morphisms a : X ⟶ X', b : Y ⟶ Y', c : Z ⟶ Z' such that a ≫ f' = f ≫ b, b ≫ g' = g ≫ c, and a⟦1⟧' ≫ h = h' ≫ c. In other words, we have a commutative diagram:

     f      g      h
X  ───> Y  ───> Z  ───> X⟦1⟧
│       │       │        │
│a      │b      │c       │a⟦1⟧'
V       V       V        V
X' ───> Y' ───> Z' ───> X'⟦1⟧
f'     g'     h'

theorem category_theory.triangulated.triangle_morphism.ext {C : Type u} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.has_shift C} {T₁ T₂ : category_theory.triangulated.triangle C} (x y : T₂) (h : x.hom₁ = y.hom₁) (h_1 : x.hom₂ = y.hom₂) (h_2 : x.hom₃ = y.hom₃) :
x = y
@[simp]
theorem category_theory.triangulated.triangle_morphism.comm₁ {C : Type u} {T₁ T₂ : category_theory.triangulated.triangle C} (self : T₂) :
T₁.mor₁ self.hom₂ = self.hom₁ T₂.mor₁
@[simp]
theorem category_theory.triangulated.triangle_morphism.comm₂ {C : Type u} {T₁ T₂ : category_theory.triangulated.triangle C} (self : T₂) :
T₁.mor₂ self.hom₃ = self.hom₂ T₂.mor₂
@[simp]
theorem category_theory.triangulated.triangle_morphism.comm₃ {C : Type u} {T₁ T₂ : category_theory.triangulated.triangle C} (self : T₂) :
T₁.mor₃ self.hom₁ = self.hom₃ T₂.mor₃
@[simp]
theorem category_theory.triangulated.triangle_morphism.comm₃_assoc {C : Type u} {T₁ T₂ : category_theory.triangulated.triangle C} (self : T₂) {X' : C} (f' : T₂.obj₁ X') :
T₁.mor₃ self.hom₁ f' = self.hom₃ T₂.mor₃ f'
@[simp]
theorem category_theory.triangulated.triangle_morphism.comm₁_assoc {C : Type u} {T₁ T₂ : category_theory.triangulated.triangle C} (self : T₂) {X' : C} (f' : T₂.obj₂ X') :
T₁.mor₁ self.hom₂ f' = self.hom₁ T₂.mor₁ f'
@[simp]
theorem category_theory.triangulated.triangle_morphism.comm₂_assoc {C : Type u} {T₁ T₂ : category_theory.triangulated.triangle C} (self : T₂) {X' : C} (f' : T₂.obj₃ X') :
T₁.mor₂ self.hom₃ f' = self.hom₂ T₂.mor₂ f'
@[simp]
@[simp]
@[simp]

The identity triangle morphism.

Equations
@[instance]
Equations

Composition of triangle morphisms gives a triangle morphism.

Equations
@[instance]

Triangles with triangle morphisms form a category.

Equations
@[simp]
@[simp]
theorem category_theory.triangulated.triangle_category_comp {C : Type u} (A B C_1 : category_theory.triangulated.triangle C) (f : A B) (g : B C_1) :