English
The counit of the equivalence between rotated and inverse-rotated triangles produces a natural isomorphism to the identity functor on triangles, reflecting the adjoint-like relation between rotation and its inverse.
Русский
Сопряжённая к эквивалентности связь между повернутыми и обратными треугольниками даёт естественную изоморфность к тождественному функтору на треугольниках.
LaTeX
$$$\\text{invRotCompRot} : (\\text{invRotate} \\circ \\text{rotate}) \\cong \\mathrm{Id}_{\\mathbf{Triangle}(C)}$$$
Lean4
/-- The counit isomorphism of the auto-equivalence of categories `triangleRotation C` of
`Triangle C` given by the rotation of triangles. -/
@[simps!]
def invRotCompRot : invRotate C ⋙ rotate C ≅ 𝟭 (Triangle C) :=
NatIso.ofComponents fun T =>
Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) ((shiftEquiv C (1 : ℤ)).counitIso.app T.obj₃)
