English
The inverse of the rotation of triangles can be expressed using a double rotation and the shift by -1.
Русский
Обратное вращение треугольников может быть выражено через двойной поворот и сдвиг на −1.
LaTeX
$$$\\operatorname{invRotate} C \\cong \\operatorname{rotate} C \\;⋙\\; \\operatorname{rotate} C \\;⋙\\; \\operatorname{Triangle.shiftFunctor} C (-1)$$$
Lean4
/-- The inverse of the rotation of triangles can be expressed using a double
rotation and the shift by `-1`. -/
noncomputable def invRotateIsoRotateRotateShiftFunctorNegOne :
invRotate C ≅ rotate C ⋙ rotate C ⋙ Triangle.shiftFunctor C (-1) :=
calc
invRotate C ≅ invRotate C ⋙ 𝟭 _ := (Functor.rightUnitor _).symm
_ ≅ invRotate C ⋙ Triangle.shiftFunctor C 0 := (Functor.isoWhiskerLeft _ (Triangle.shiftFunctorZero C).symm)
_ ≅ invRotate C ⋙ Triangle.shiftFunctor C 1 ⋙ Triangle.shiftFunctor C (-1) :=
(Functor.isoWhiskerLeft _ (Triangle.shiftFunctorAdd' C 1 (-1) 0 (add_neg_cancel 1)))
_ ≅ invRotate C ⋙ (rotate C ⋙ rotate C ⋙ rotate C) ⋙ Triangle.shiftFunctor C (-1) :=
(Functor.isoWhiskerLeft _ (Functor.isoWhiskerRight (rotateRotateRotateIso C).symm _))
_ ≅ (invRotate C ⋙ rotate C) ⋙ rotate C ⋙ rotate C ⋙ Triangle.shiftFunctor C (-1) :=
(Functor.isoWhiskerLeft _ (Functor.associator _ _ _ ≪≫ Functor.isoWhiskerLeft _ (Functor.associator _ _ _)) ≪≫
(Functor.associator _ _ _).symm)
_ ≅ 𝟭 _ ⋙ rotate C ⋙ rotate C ⋙ Triangle.shiftFunctor C (-1) :=
(Functor.isoWhiskerRight (triangleRotation C).counitIso _)
_ ≅ _ := Functor.leftUnitor _
