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

source

structure CategoryTheory.Pretriangulated.Triangle (C : Type u) [Category.{v, u} C] [HasShift C ℤ] :

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.

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₁ : self.obj₁ ⟶ self.obj₂
the first morphism of a triangle
mor₂ : self.obj₂ ⟶ self.obj₃
the second morphism of a triangle
mor₃ : self.obj₃ ⟶ (shiftFunctor C 1).obj self.obj₁
the third morphism of a triangle

)

Instances For

source

def CategoryTheory.Pretriangulated.Triangle.mk {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (shiftFunctor C 1).obj X) :

Triangle C

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

CategoryTheory.Pretriangulated.Triangle.mk f g h = { obj₁ := X, obj₂ := Y, obj₃ := Z, mor₁ := f, mor₂ := g, mor₃ := h }

Instances For

source

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.mk_mor₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (shiftFunctor C 1).obj X) :

(mk f g h).mor₂ = g

source

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.mk_mor₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (shiftFunctor C 1).obj X) :

(mk f g h).mor₁ = f

source

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.mk_obj₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (shiftFunctor C 1).obj X) :

(mk f g h).obj₃ = Z

source

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.mk_obj₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (shiftFunctor C 1).obj X) :

(mk f g h).obj₁ = X

source

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.mk_obj₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (shiftFunctor C 1).obj X) :

(mk f g h).obj₂ = Y

source

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.mk_mor₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (shiftFunctor C 1).obj X) :

(mk f g h).mor₃ = h

source

instance CategoryTheory.Pretriangulated.instInhabitedTriangle {C : Type u} [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] :

Inhabited (Triangle C)

Equations

CategoryTheory.Pretriangulated.instInhabitedTriangle = { default := { obj₁ := 0, obj₂ := 0, obj₃ := 0, mor₁ := 0, mor₂ := 0, mor₃ := 0 } }

source

def CategoryTheory.Pretriangulated.contractibleTriangle {C : Type u} [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) :

Triangle C

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

Equations

CategoryTheory.Pretriangulated.contractibleTriangle X = CategoryTheory.Pretriangulated.Triangle.mk (CategoryTheory.CategoryStruct.id X) 0 0

Instances For

source

@[simp]

theorem CategoryTheory.Pretriangulated.contractibleTriangle_obj₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) :

(contractibleTriangle X).obj₃ = 0

source

@[simp]

theorem CategoryTheory.Pretriangulated.contractibleTriangle_mor₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) :

(contractibleTriangle X).mor₃ = 0

source

@[simp]

theorem CategoryTheory.Pretriangulated.contractibleTriangle_obj₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) :

(contractibleTriangle X).obj₁ = X

source

@[simp]

theorem CategoryTheory.Pretriangulated.contractibleTriangle_mor₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) :

(contractibleTriangle X).mor₁ = CategoryStruct.id X

source

@[simp]

theorem CategoryTheory.Pretriangulated.contractibleTriangle_obj₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) :

(contractibleTriangle X).obj₂ = X

source

@[simp]

theorem CategoryTheory.Pretriangulated.contractibleTriangle_mor₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) :

(contractibleTriangle X).mor₂ = 0

source

structure CategoryTheory.Pretriangulated.TriangleMorphism {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (T₁ T₂ : Triangle C) :

Type v

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'

hom₁ : T₁.obj₁ ⟶ T₂.obj₁
the first morphism in a triangle morphism
hom₂ : T₁.obj₂ ⟶ T₂.obj₂
the second morphism in a triangle morphism
hom₃ : T₁.obj₃ ⟶ T₂.obj₃
the third morphism in a triangle morphism
comm₁ : CategoryStruct.comp T₁.mor₁ self.hom₂ = CategoryStruct.comp self.hom₁ T₂.mor₁
the first commutative square of a triangle morphism
comm₂ : CategoryStruct.comp T₁.mor₂ self.hom₃ = CategoryStruct.comp self.hom₂ T₂.mor₂
the second commutative square of a triangle morphism
comm₃ : CategoryStruct.comp T₁.mor₃ ((shiftFunctor C 1).map self.hom₁) = CategoryStruct.comp self.hom₃ T₂.mor₃
the third commutative square of a triangle morphism