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
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
- distinguishedTriangles : Set (CategoryTheory.Pretriangulated.Triangle C)
a class of triangle which are called
distinguished
- isomorphic_distinguished : ∀ 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 : C) (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X), 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 ↔ T.rotate ∈ 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 : T₁.obj₃ ⟶ T₂.obj₃), 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
Instances
distinguished triangles in a pretriangulated category
Equations
- One or more equations did not get rendered due to their size.
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
The short complex T.obj₁ ⟶ T.obj₂ ⟶ T.obj₃
attached to a distinguished triangle.
Equations
- CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT = CategoryTheory.ShortComplex.mk T.mor₁ T.mor₂ ⋯
Instances For
The isomorphism between the short complex attached to two isomorphic distinguished triangles.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Given a distinguished triangle T
such that T.mor₃ = 0
and the datum of morphisms
inr : T.obj₃ ⟶ T.obj₂
and fst : T.obj₂ ⟶ T.obj₁
satisfying suitable relations, this
is the binary biproduct data expressing that T.obj₂
identifies to the binary
biproduct of T.obj₁
and T.obj₃
.
See also exists_iso_binaryBiproduct_of_distTriang
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A chosen extension of a commutative square into a morphism of distinguished triangles.
Equations
- CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ a b comm = { hom₁ := a, hom₂ := b, hom₃ := ⋯.choose, comm₁ := comm, comm₂ := ⋯, comm₃ := ⋯ }
Instances For
A product of distinguished triangles is distinguished
A choice of isomorphism T₁ ≅ T₂
between two distinguished triangles
when we are given two isomorphisms e₁ : T₁.obj₁ ≅ T₂.obj₁
and e₂ : T₁.obj₂ ≅ T₂.obj₂
.
Equations
- CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm = T₁.isoMk T₂ e₁ e₂ (CategoryTheory.Pretriangulated.Triangle.π₃.mapIso ⋯.choose) comm ⋯ ⋯