# mathlib3documentation

category_theory.triangulated.rotate

# Rotate #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[simp]
@[simp]

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

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

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

Equations
Instances for category_theory.pretriangulated.rotate
@[simp]

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

Equations
Instances for category_theory.pretriangulated.inv_rotate
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]

The unit isomorphism of the auto-equivalence of categories triangle_rotation C of triangle C given by the rotation of triangles.

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

The counit isomorphism of the auto-equivalence of categories triangle_rotation C of triangle C given by the rotation of triangles.

Equations
@[simp]
@[simp]

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

Equations
@[simp]
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations