English
The rotation operation defines a functor on the category of triangles, sending morphisms between triangles to corresponding rotated morphisms, preserving the triangle structure.
Русский
Поворот определяет функтор на категории треугольников, сопоставляющий области morphisms повернутые стрелки и сохраняющий структуру треугольников.
LaTeX
$$$\\text{rotate} : \\mathbf{Triangle}(C) \\to \\mathbf{Triangle}(C)$ является функтором, и для любого гомоморфизма \\(f: X\\to Y\\) существует соответствующий поворотный гомоморфизм, сохраняющий композиции.$$
Lean4
/-- Rotating triangles gives an endofunctor on the category of triangles in `C`.
-/
@[simps]
def rotate : Triangle C ⥤ Triangle C where
obj := Triangle.rotate
map
f :=
{ hom₁ := f.hom₂
hom₂ := f.hom₃
hom₃ := f.hom₁⟦1⟧'
comm₃ := by
dsimp
simp only [comp_neg, neg_comp, ← Functor.map_comp, f.comm₁] }
