invRotateInvRotateInvRotateIso — Mathlib

English

The inverse of rotating triangles three times backwards is isomorphic to shifting by -1.

Русский

Обратный тройному повороту треугольников назад эквивалентен сдвигу на −1.

LaTeX

$$$\\operatorname{invRotate} C \\;\\cong\\; \\operatorname{rotate} C \\; ⋙ \\operatorname{rotate} C \\; ⋙ \\operatorname{Triangle.shiftFunctor} C (-1)$$$

Lean4

/-- Rotating triangles three times backwards identifies with the shift by `-1`. -/
noncomputable def invRotateInvRotateInvRotateIso :
    invRotate C ⋙ invRotate C ⋙ invRotate C ≅ Triangle.shiftFunctor C (-1) :=
  NatIso.ofComponents
    (fun T =>
      Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp) (by simp)
        (by
          dsimp [shiftFunctorCompIsoId]
          simp [shiftFunctorComm_eq C _ _ _ (add_neg_cancel (1 : ℤ))]))
    (by cat_disch)

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