English
Let C be a triangulated, preadditive category with integer shifts. For any triangle in C, rotating the indices yields a new triangle. Thus rotation defines a functor on the category of triangles, sending each distinguished triangle to a rotated one.
Русский
Пусть C — треангулированная прeддобавляема категория с целыми сдвигами. Для любого треугольника в C разворот индексов даёт новый треугольник. Следовательно, поворот задаёт функтор на категории треугольников, отправляющий каждый выделенный треугольник в повернутый.
LaTeX
$$$\\rotate_C : \\mathbf{TriangulatedTriangle}(C) \\to \\mathbf{TriangulatedTriangle}(C)$ является эндофунктором, полученным вращением треугольников. В частности, для треугольника\n$X \\xrightarrow{f} Y \\xrightarrow{g} Z \\xrightarrow{h} X[1]$\nего вращённый образ имеет вид\n$Y \\xrightarrow{g} Z \\xrightarrow{h} X[1] \\xrightarrow{-f[1]} Y[1]$.$$
Lean4
/-- If you rotate a triangle, you get another triangle.
Given a triangle of the form:
```
f g h
X ───> Y ───> Z ───> X⟦1⟧
```
applying `rotate` gives a triangle of the form:
```
g h -f⟦1⟧'
Y ───> Z ───> X⟦1⟧ ───> Y⟦1⟧
```
-/
@[simps!]
def rotate (T : Triangle C) : Triangle C :=
Triangle.mk T.mor₂ T.mor₃ (-T.mor₁⟦1⟧')
