# mathlibdocumentation

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  ───> X⟦1⟧


applying rotate gives a triangle of the form:

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

Equations

Given a triangle of the form:

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


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  ───> X⟦1⟧
│       │       │        │
│a      │b      │c       │a⟦1⟧
V       V       V        V
X' ───> Y' ───> Z' ───> X'⟦1⟧
f'      g'      h'


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

      g        h       -f⟦1⟧
Y  ───> Z  ───>  X⟦1⟧ ───> Y⟦1⟧
│       │         │         │
│b      │c        │a⟦1⟧     │b⟦1⟧'
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  ───> X⟦1⟧
│       │       │        │
│a      │b      │c       │a⟦1⟧
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
@[simp]
@[simp]
theorem category_theory.triangulated.rotate_map {C : Type u} (_x _x_1 : category_theory.triangulated.triangle C) (f : _x _x_1) :

Rotating triangles gives an endofunctor on the category of triangles in C.

Equations
@[simp]

The inverse rotation of triangles gives an endofunctor on the category of triangles in C.

Equations
@[simp]
theorem category_theory.triangulated.inv_rotate_map {C : Type u} (_x _x_1 : category_theory.triangulated.triangle C) (f : _x _x_1) :
@[simp]

There is a natural transformation between the identity functor on triangles in C, and the composition of a rotation with an inverse rotation.

Equations
@[simp]
@[simp]
@[simp]
@[simp]

There is a natural transformation between the composition of a rotation with an inverse rotation on triangles in C, and the identity functor.

Equations
@[simp]
@[simp]
@[simp]

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
@[simp]

There is a natural transformation between the composition of an inverse rotation with a rotation on triangles in C, and the identity functor.

Equations
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]

There is a natural transformation between the identity functor on triangles in C, and the composition of an inverse rotation with a rotation.

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
@[simp]
@[simp]

Rotating triangles gives an auto-equivalence on the category of triangles in C.

Equations
@[simp]
@[simp]
@[simp]
@[simp]