# mathlib3documentation

category_theory.triangulated.basic

# Triangles #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.pretriangulated.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.

Instances for category_theory.pretriangulated.triangle
@[simp]
theorem category_theory.pretriangulated.triangle.mk_mor₂ {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z) (h : Z X) :
@[simp]
theorem category_theory.pretriangulated.triangle.mk_mor₁ {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z) (h : Z X) :
@[simp]
theorem category_theory.pretriangulated.triangle.mk_obj₂ {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z) (h : Z X) :
@[simp]
theorem category_theory.pretriangulated.triangle.mk_obj₁ {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z) (h : Z X) :
def category_theory.pretriangulated.triangle.mk {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z) (h : Z 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.pretriangulated.triangle.mk_mor₃ {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z) (h : Z X) :
@[simp]
theorem category_theory.pretriangulated.triangle.mk_obj₃ {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z) (h : Z X) :
@[protected, instance]
Equations

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

Equations
@[simp]
@[simp]
@[simp]
@[simp]
@[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'

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

The identity triangle morphism.

Equations
@[simp]
@[simp]
@[simp]
@[protected, instance]
Equations

Composition of triangle morphisms gives a triangle morphism.

Equations
@[protected, instance]

Triangles with triangle morphisms form a category.

Equations
@[simp]
def category_theory.pretriangulated.triangle.hom_mk {C : Type u} (hom₁ : A.obj₁ B.obj₁) (hom₂ : A.obj₂ B.obj₂) (hom₃ : A.obj₃ B.obj₃) (comm₁ : A.mor₁ hom₂ = hom₁ B.mor₁) (comm₂ : A.mor₂ hom₃ = hom₂ B.mor₂) (comm₃ : A.mor₃ hom₁ = hom₃ B.mor₃) :
A B

a constructor for morphisms of triangles

Equations
@[simp]
theorem category_theory.pretriangulated.triangle.hom_mk_hom₁ {C : Type u} (hom₁ : A.obj₁ B.obj₁) (hom₂ : A.obj₂ B.obj₂) (hom₃ : A.obj₃ B.obj₃) (comm₁ : A.mor₁ hom₂ = hom₁ B.mor₁) (comm₂ : A.mor₂ hom₃ = hom₂ B.mor₂) (comm₃ : A.mor₃ hom₁ = hom₃ B.mor₃) :
(A.hom_mk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₁ = hom₁
@[simp]
theorem category_theory.pretriangulated.triangle.hom_mk_hom₃ {C : Type u} (hom₁ : A.obj₁ B.obj₁) (hom₂ : A.obj₂ B.obj₂) (hom₃ : A.obj₃ B.obj₃) (comm₁ : A.mor₁ hom₂ = hom₁ B.mor₁) (comm₂ : A.mor₂ hom₃ = hom₂ B.mor₂) (comm₃ : A.mor₃ hom₁ = hom₃ B.mor₃) :
(A.hom_mk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₃ = hom₃
@[simp]
theorem category_theory.pretriangulated.triangle.hom_mk_hom₂ {C : Type u} (hom₁ : A.obj₁ B.obj₁) (hom₂ : A.obj₂ B.obj₂) (hom₃ : A.obj₃ B.obj₃) (comm₁ : A.mor₁ hom₂ = hom₁ B.mor₁) (comm₂ : A.mor₂ hom₃ = hom₂ B.mor₂) (comm₃ : A.mor₃ hom₁ = hom₃ B.mor₃) :
(A.hom_mk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₂ = hom₂
def category_theory.pretriangulated.triangle.iso_mk {C : Type u} (iso₁ : A.obj₁ B.obj₁) (iso₂ : A.obj₂ B.obj₂) (iso₃ : A.obj₃ B.obj₃) (comm₁ : A.mor₁ iso₂.hom = iso₁.hom B.mor₁) (comm₂ : A.mor₂ iso₃.hom = iso₂.hom B.mor₂) (comm₃ : A.mor₃ iso₁.hom = iso₃.hom B.mor₃) :
A B

a constructor for isomorphisms of triangles

Equations
@[simp]
theorem category_theory.pretriangulated.triangle.iso_mk_hom {C : Type u} (iso₁ : A.obj₁ B.obj₁) (iso₂ : A.obj₂ B.obj₂) (iso₃ : A.obj₃ B.obj₃) (comm₁ : A.mor₁ iso₂.hom = iso₁.hom B.mor₁) (comm₂ : A.mor₂ iso₃.hom = iso₂.hom B.mor₂) (comm₃ : A.mor₃ iso₁.hom = iso₃.hom B.mor₃) :
(A.iso_mk B iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).hom = A.hom_mk B iso₁.hom iso₂.hom iso₃.hom comm₁ comm₂ comm₃
@[simp]
theorem category_theory.pretriangulated.triangle.iso_mk_inv {C : Type u} (iso₁ : A.obj₁ B.obj₁) (iso₂ : A.obj₂ B.obj₂) (iso₃ : A.obj₃ B.obj₃) (comm₁ : A.mor₁ iso₂.hom = iso₁.hom B.mor₁) (comm₂ : A.mor₂ iso₃.hom = iso₂.hom B.mor₂) (comm₃ : A.mor₃ iso₁.hom = iso₃.hom B.mor₃) :
(A.iso_mk B iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).inv = B.hom_mk A iso₁.inv iso₂.inv iso₃.inv _ _ _