invRotate — Mathlib

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 }

Похожие утверждения