English
The rotation operation defines an equivalence between the category of triangles and itself, with explicit inverse given by invRotate. Thus rotate and invRotate form an auto-equivalence of the triangle category.
Русский
Поворот задаёт эквивалентность между категорией треугольников и самой собой, причём обратный поворот является обратноэквивалентностью rotate и invRotate образуют автэквивалентность категории треугольников.
LaTeX
$$$\\text{rotate}(C) : \\mathbf{Triangle}(C) \\to \\mathbf{Triangle}(C)$ и $\\text{invRotate}(C) : \\mathbf{Triangle}(C) \\to \\mathbf{Triangle}(C)$ образуют автоэквивалентность: \\( \\text{rotate}(C) \\dashv\\text{invRotate}(C) \\) с естественными изоморфизмами.$$
Lean4
/-- The unit isomorphism of the auto-equivalence of categories `triangleRotation C` of
`Triangle C` given by the rotation of triangles. -/
@[simps!]
def rotCompInvRot : 𝟭 (Triangle C) ≅ rotate C ⋙ invRotate C :=
NatIso.ofComponents fun T => Triangle.isoMk _ _ ((shiftEquiv C (1 : ℤ)).unitIso.app T.obj₁) (Iso.refl _) (Iso.refl _)
