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