Pretriangulated Categories #
This file contains the definition of pretriangulated categories and triangulated functors between them.
Implementation Notes #
We work under the assumption that pretriangulated categories are preadditive categories, but not necessarily additive categories, as is assumed in some sources.
TODO: generalise this to n-angulated categories as in https://arxiv.org/abs/1006.4592
- distinguishedTriangles : Set (CategoryTheory.Pretriangulated.Triangle C)
a class of triangle which are called
distinguished
- isomorphic_distinguished : ∀ (T₁ : CategoryTheory.Pretriangulated.Triangle C), T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → ∀ (T₂ : CategoryTheory.Pretriangulated.Triangle C), (T₂ ≅ T₁) → T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
a triangle that is isomorphic to a distinguished triangle is distinguished
- contractible_distinguished : ∀ (X : C), CategoryTheory.Pretriangulated.contractibleTriangle X ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
obvious triangles
X ⟶ X ⟶ 0 ⟶ X⟦1⟧
are distinguished - distinguished_cocone_triangle : ∀ {X Y : C} (f : X ⟶ Y), ∃ Z g h, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
any morphism
X ⟶ Y
is part of a distinguished triangleX ⟶ Y ⟶ Z ⟶ X⟦1⟧
- rotate_distinguished_triangle : ∀ (T : CategoryTheory.Pretriangulated.Triangle C), T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ CategoryTheory.Pretriangulated.Triangle.rotate T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
a triangle is distinguished iff it is so after rotating it
- complete_distinguished_triangle_morphism : ∀ (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C), T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂), CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ → ∃ c, CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧ CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map a) = CategoryTheory.CategoryStruct.comp c T₂.mor₃
given two distinguished triangle, a commutative square can be extended as morphism of triangles
A preadditive category C
with an additive shift, and a class of "distinguished triangles"
relative to that shift is called pretriangulated if the following hold:
- Any triangle that is isomorphic to a distinguished triangle is also distinguished.
- Any triangle of the form
(X,X,0,id,0,0)
is distinguished. - For any morphism
f : X ⟶ Y
there exists a distinguished triangle of the form(X,Y,Z,f,g,h)
. - The triangle
(X,Y,Z,f,g,h)
is distinguished if and only if(Y,Z,X⟦1⟧,g,h,-f⟦1⟧)
is. - Given a diagram:
where the left square commutes, and whose rows are distinguished triangles, there exists a morphismf g h X ───> Y ───> Z ───> X⟦1⟧ │ │ │ │a │b │a⟦1⟧' V V V X' ───> Y' ───> Z' ───> X'⟦1⟧ f' g' h'
c : Z ⟶ Z'
such that(a,b,c)
is a triangle morphism.
See https://stacks.math.columbia.edu/tag/0145
Instances
distinguished triangles in a pretriangulated category
Instances For
Given any distinguished triangle T
, then we know T.rotate
is also distinguished.
Given any distinguished triangle T
, then we know T.inv_rotate
is also distinguished.
Given any distinguished triangle
f g h
X ───> Y ───> Z ───> X⟦1⟧
the composition f ≫ g = 0
.
See https://stacks.math.columbia.edu/tag/0146
Given any distinguished triangle
f g h
X ───> Y ───> Z ───> X⟦1⟧
the composition g ≫ h = 0
.
See https://stacks.math.columbia.edu/tag/0146
Given any distinguished triangle
f g h
X ───> Y ───> Z ───> X⟦1⟧
the composition h ≫ f⟦1⟧ = 0
.
See https://stacks.math.columbia.edu/tag/0146
Any morphism Y ⟶ Z
is part of a distinguished triangle X ⟶ Y ⟶ Z ⟶ X⟦1⟧
Any morphism Z ⟶ X⟦1⟧
is part of a distinguished triangle X ⟶ Y ⟶ Z ⟶ X⟦1⟧
A commutative square involving the morphisms mor₂
of two distinguished triangles
can be extended as morphism of triangles
A commutative square involving the morphisms mor₃
of two distinguished triangles
can be extended as morphism of triangles
Obvious triangles 0 ⟶ X ⟶ X ⟶ 0⟦1⟧
are distinguished
Obvious triangles X ⟶ 0 ⟶ X⟦1⟧ ⟶ X⟦1⟧
are distinguished