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₃ ⟶ (CategoryTheory.shiftFunctor C 1).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
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
For each object in C
, there is a triangle of the form (X,X,0,𝟙 X,0,0)
Instances For
- 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₁ : CategoryTheory.CategoryStruct.comp T₁.mor₁ s.hom₂ = CategoryTheory.CategoryStruct.comp s.hom₁ T₂.mor₁
the first commutative square of a triangle morphism
- comm₂ : CategoryTheory.CategoryStruct.comp T₁.mor₂ s.hom₃ = CategoryTheory.CategoryStruct.comp s.hom₂ T₂.mor₂
the second commutative square of a triangle morphism
- comm₃ : CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map s.hom₁) = CategoryTheory.CategoryStruct.comp s.hom₃ T₂.mor₃
the third commutative square of a triangle morphism
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'
See https://stacks.math.columbia.edu/tag/0144.
Instances For
The identity triangle morphism.
Instances For
Composition of triangle morphisms gives a triangle morphism.
Instances For
Triangles with triangle morphisms form a category.