Documentation

Mathlib.CategoryTheory.Triangulated.Rotate

Rotate #

This file adds the ability to rotate triangles and triangle morphisms. It also shows that rotation gives an equivalence on the category of triangles.

If you rotate a triangle, you get another triangle. Given a triangle of the form:

      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧

applying rotate gives a triangle of the form:

      g       h        -f⟦1⟧'
  Y  ───> Z  ───>  X⟦1⟧ ───> Y⟦1⟧
Instances For

    Given a triangle of the form:

          f       g       h
      X  ───> Y  ───> Z  ───> X⟦1⟧
    

    applying invRotate gives a triangle that can be thought of as:

            -h⟦-1⟧'     f       g
      Z⟦-1⟧  ───>  X  ───> Y  ───> Z
    

    (note that this diagram doesn't technically fit the definition of triangle, as Z⟦-1⟧⟦1⟧ is not necessarily equal to Z, but it is isomorphic, by the counitIso of shiftEquiv C 1)

    Instances For