# Documentation

Mathlib.CategoryTheory.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

• mk' :: (
• obj₁ : C

the first object of a triangle

• obj₂ : C

the second object of a triangle

• obj₃ : C

the third object of a triangle

• mor₁ : s.obj₁ s.obj₂

the first morphism of a triangle

• mor₂ : s.obj₂ s.obj₃

the second morphism of a triangle

• mor₃ : s.obj₃ ().obj s.obj₁

the third morphism of a triangle

• )

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
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.mk_mor₃ {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : Z ().obj X) :
().mor₃ = h
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.mk_mor₂ {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : Z ().obj X) :
().mor₂ = g
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.mk_obj₂ {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : Z ().obj X) :
().obj₂ = Y
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.mk_obj₁ {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : Z ().obj X) :
().obj₁ = X
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.mk_mor₁ {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : Z ().obj X) :
().mor₁ = f
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.mk_obj₃ {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : Z ().obj X) :
().obj₃ = Z
def CategoryTheory.Pretriangulated.Triangle.mk {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : Z ().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⟧.

Instances For
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]

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

Instances For
theorem CategoryTheory.Pretriangulated.TriangleMorphism.ext_iff {C : Type u} :
∀ {inst : } {inst_1 : } {T₁ T₂ : } (x y : ), x = y x.hom₁ = y.hom₁ x.hom₂ = y.hom₂ x.hom₃ = y.hom₃
theorem CategoryTheory.Pretriangulated.TriangleMorphism.ext {C : Type u} :
∀ {inst : } {inst_1 : } {T₁ T₂ : } (x y : ), x.hom₁ = y.hom₁x.hom₂ = y.hom₂x.hom₃ = y.hom₃x = y

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
@[simp]
theorem CategoryTheory.Pretriangulated.TriangleMorphism.comm₃_assoc {C : Type u} (self : ) {Z : C} (h : ().obj T₂.obj₁ Z) :
@[simp]
@[simp]
@[simp]

The identity triangle morphism.

Instances For

Composition of triangle morphisms gives a triangle morphism.

Instances For
@[simp]
theorem CategoryTheory.Pretriangulated.triangleCategory_comp {C : Type u} :
∀ {X Y Z : } (f : X Y) (g : Y Z),
@[simp]

Triangles with triangle morphisms form a category.

theorem CategoryTheory.Pretriangulated.Triangle.hom_ext {C : Type u} (f : A B) (g : A B) (h₁ : f.hom₁ = g.hom₁) (h₂ : f.hom₂ = g.hom₂) (h₃ : f.hom₃ = g.hom₃) :
f = g
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.homMk_hom₂ {C : Type u} (hom₁ : A.obj₁ B.obj₁) (hom₂ : A.obj₂ B.obj₂) (hom₃ : A.obj₃ B.obj₃) (comm₁ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ B.mor₁) _auto✝) (comm₂ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ B.mor₂) _auto✝) (comm₃ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₃ (().map hom₁) = CategoryTheory.CategoryStruct.comp hom₃ B.mor₃) _auto✝) :
(CategoryTheory.Pretriangulated.Triangle.homMk A B hom₁ hom₂ hom₃).hom₂ = hom₂
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.homMk_hom₃ {C : Type u} (hom₁ : A.obj₁ B.obj₁) (hom₂ : A.obj₂ B.obj₂) (hom₃ : A.obj₃ B.obj₃) (comm₁ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ B.mor₁) _auto✝) (comm₂ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ B.mor₂) _auto✝) (comm₃ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₃ (().map hom₁) = CategoryTheory.CategoryStruct.comp hom₃ B.mor₃) _auto✝) :
(CategoryTheory.Pretriangulated.Triangle.homMk A B hom₁ hom₂ hom₃).hom₃ = hom₃
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.homMk_hom₁ {C : Type u} (hom₁ : A.obj₁ B.obj₁) (hom₂ : A.obj₂ B.obj₂) (hom₃ : A.obj₃ B.obj₃) (comm₁ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ B.mor₁) _auto✝) (comm₂ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ B.mor₂) _auto✝) (comm₃ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₃ (().map hom₁) = CategoryTheory.CategoryStruct.comp hom₃ B.mor₃) _auto✝) :
(CategoryTheory.Pretriangulated.Triangle.homMk A B hom₁ hom₂ hom₃).hom₁ = hom₁
def CategoryTheory.Pretriangulated.Triangle.homMk {C : Type u} (hom₁ : A.obj₁ B.obj₁) (hom₂ : A.obj₂ B.obj₂) (hom₃ : A.obj₃ B.obj₃) (comm₁ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ B.mor₁) _auto✝) (comm₂ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ B.mor₂) _auto✝) (comm₃ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₃ (().map hom₁) = CategoryTheory.CategoryStruct.comp hom₃ B.mor₃) _auto✝) :
A B
Instances For
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.isoMk_hom {C : Type u} (iso₁ : A.obj₁ B.obj₁) (iso₂ : A.obj₂ B.obj₂) (iso₃ : A.obj₃ B.obj₃) (comm₁ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₁ iso₂.hom = CategoryTheory.CategoryStruct.comp iso₁.hom B.mor₁) _auto✝) (comm₂ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₂ iso₃.hom = CategoryTheory.CategoryStruct.comp iso₂.hom B.mor₂) _auto✝) (comm₃ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₃ (().map iso₁.hom) = CategoryTheory.CategoryStruct.comp iso₃.hom B.mor₃) _auto✝) :
(CategoryTheory.Pretriangulated.Triangle.isoMk A B iso₁ iso₂ iso₃).hom = CategoryTheory.Pretriangulated.Triangle.homMk A B iso₁.hom iso₂.hom iso₃.hom
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.isoMk_inv {C : Type u} (iso₁ : A.obj₁ B.obj₁) (iso₂ : A.obj₂ B.obj₂) (iso₃ : A.obj₃ B.obj₃) (comm₁ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₁ iso₂.hom = CategoryTheory.CategoryStruct.comp iso₁.hom B.mor₁) _auto✝) (comm₂ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₂ iso₃.hom = CategoryTheory.CategoryStruct.comp iso₂.hom B.mor₂) _auto✝) (comm₃ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₃ (().map iso₁.hom) = CategoryTheory.CategoryStruct.comp iso₃.hom B.mor₃) _auto✝) :
(CategoryTheory.Pretriangulated.Triangle.isoMk A B iso₁ iso₂ iso₃).inv = CategoryTheory.Pretriangulated.Triangle.homMk B A iso₁.inv iso₂.inv iso₃.inv
def CategoryTheory.Pretriangulated.Triangle.isoMk {C : Type u} (iso₁ : A.obj₁ B.obj₁) (iso₂ : A.obj₂ B.obj₂) (iso₃ : A.obj₃ B.obj₃) (comm₁ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₁ iso₂.hom = CategoryTheory.CategoryStruct.comp iso₁.hom B.mor₁) _auto✝) (comm₂ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₂ iso₃.hom = CategoryTheory.CategoryStruct.comp iso₂.hom B.mor₂) _auto✝) (comm₃ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₃ (().map iso₁.hom) = CategoryTheory.CategoryStruct.comp iso₃.hom B.mor₃) _auto✝) :
A B
Instances For
theorem CategoryTheory.Pretriangulated.Triangle.eqToHom_hom₁ {C : Type u} (h : A = B) :
().hom₁ = CategoryTheory.eqToHom (_ : A.obj₁ = B.obj₁)
theorem CategoryTheory.Pretriangulated.Triangle.eqToHom_hom₂ {C : Type u} (h : A = B) :
().hom₂ = CategoryTheory.eqToHom (_ : A.obj₂ = B.obj₂)
theorem CategoryTheory.Pretriangulated.Triangle.eqToHom_hom₃ {C : Type u} (h : A = B) :
().hom₃ = CategoryTheory.eqToHom (_ : A.obj₃ = B.obj₃)