mathlib documentation

category_theory.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  ───> X1

applying rotate gives a triangle of the form:

      g       h        -f1⟧'
  Y  ───> Z  ───>  X1 ───> Y1
Equations

Given a triangle of the form:

      f       g       h
  X  ───> Y  ───> Z  ───> X1

applying inv_rotate 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 counit_iso of shift C)

Equations

You can also rotate a triangle morphism to get a morphism between the two rotated triangles. Given a triangle morphism of the form:

      f       g       h
  X  ───> Y  ───> Z  ───> X1
                        
  a      b      c       a1
  V       V       V        V
  X' ───> Y' ───> Z' ───> X'1
      f'      g'      h'

applying rotate gives a triangle morphism of the form: ⟦⟧

      g        h       -f1
  Y  ───> Z  ───>  X1 ───> Y1
                           
  b      c        a1     b1⟧'
  V       V         V         V
  Y' ───> Z' ───> X'1 ───> Y'1
      g'      h'       -f'1
Equations

Given a triangle morphism of the form:

      f       g       h
  X  ───> Y  ───> Z  ───> X1
                        
  a      b      c       a1
  V       V       V        V
  X' ───> Y' ───> Z' ───> X'1
      f'      g'      h'

applying inv_rotate gives a triangle morphism that can be thought of as:

        -h⟦-1      f         g
  Z⟦-1  ───>  X   ───>  Y   ───>  Z
                                
    c⟦-1⟧'    a        b        c
    V          V         V         V
  Z'⟦-1 ───>  X'  ───>  Y'  ───>  Z'
       -h'⟦-1     f'        g'

(note that this diagram doesn't technically fit the definition of triangle morphism, as Z⟦-1⟧⟦1⟧ is not necessarily equal to Z, and Z'⟦-1⟧⟦1⟧ is not necessarily equal to Z', but they are isomorphic, by the counit_iso of shift C)

Equations

The natural transformations between the identity functor on triangles in C and the composition of a rotation with an inverse rotation are natural isomorphisms (they are isomorphisms in the category of functors).

Equations

The natural transformations between the composition of a rotation with an inverse rotation on triangles in C, and the identity functor on triangles are natural isomorphisms (they are isomorphisms in the category of functors).

Equations