# 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
noncomputable def category_theory.triangulated.triangle.inv_rotate {C : Type u}  :

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]
theorem category_theory.triangulated.rotate_obj (C : Type u)  :
@[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
Instances for category_theory.triangulated.rotate
@[simp]
noncomputable def category_theory.triangulated.inv_rotate (C : Type u)  :

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

Equations
Instances for category_theory.triangulated.inv_rotate
@[simp]
theorem category_theory.triangulated.inv_rotate_map (C : Type u) (_x _x_1 : category_theory.triangulated.triangle C) (f : _x _x_1) :
noncomputable def category_theory.triangulated.to_inv_rotate_rotate {C : Type u} [∀ (n : ), ]  :

There is a natural map from a triangle to the inv_rotate of its rotate.

Equations
@[simp]
theorem category_theory.triangulated.to_inv_rotate_rotate_hom₂ {C : Type u} [∀ (n : ), ]  :
@[simp]
theorem category_theory.triangulated.to_inv_rotate_rotate_hom₃ {C : Type u} [∀ (n : ), ]  :
@[simp]
theorem category_theory.triangulated.to_inv_rotate_rotate_hom₁ {C : Type u} [∀ (n : ), ]  :
@[simp]
noncomputable def category_theory.triangulated.rot_comp_inv_rot_hom {C : Type u} [∀ (n : ), ] :

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

Equations
noncomputable def category_theory.triangulated.from_inv_rotate_rotate {C : Type u} [∀ (n : ), ]  :

There is a natural map from the inv_rotate of the rotate of a triangle to itself.

Equations
@[simp]
theorem category_theory.triangulated.from_inv_rotate_rotate_hom₁ {C : Type u} [∀ (n : ), ]  :
@[simp]
theorem category_theory.triangulated.from_inv_rotate_rotate_hom₂ {C : Type u} [∀ (n : ), ]  :
@[simp]
theorem category_theory.triangulated.from_inv_rotate_rotate_hom₃ {C : Type u} [∀ (n : ), ]  :
@[simp]
noncomputable def category_theory.triangulated.rot_comp_inv_rot_inv {C : Type u} [∀ (n : ), ] :

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]
noncomputable def category_theory.triangulated.rot_comp_inv_rot {C : Type u} [∀ (n : ), ] :

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]
theorem category_theory.triangulated.from_rotate_inv_rotate_hom₂ {C : Type u} [∀ (n : ), ]  :
@[simp]
theorem category_theory.triangulated.from_rotate_inv_rotate_hom₃ {C : Type u} [∀ (n : ), ]  :
@[simp]
theorem category_theory.triangulated.from_rotate_inv_rotate_hom₁ {C : Type u} [∀ (n : ), ]  :
noncomputable def category_theory.triangulated.from_rotate_inv_rotate {C : Type u} [∀ (n : ), ]  :

There is a natural map from the rotate of the inv_rotate of a triangle to itself.

Equations
@[simp]
noncomputable def category_theory.triangulated.inv_rot_comp_rot_hom {C : Type u} [∀ (n : ), ] :

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]
theorem category_theory.triangulated.to_rotate_inv_rotate_hom₃ {C : Type u} [∀ (n : ), ]  :
@[simp]
theorem category_theory.triangulated.to_rotate_inv_rotate_hom₁ {C : Type u} [∀ (n : ), ]  :
@[simp]
theorem category_theory.triangulated.to_rotate_inv_rotate_hom₂ {C : Type u} [∀ (n : ), ]  :
noncomputable def category_theory.triangulated.to_rotate_inv_rotate {C : Type u} [∀ (n : ), ]  :

There is a natural map from a triangle to the rotate of its inv_rotate.

Equations
@[simp]
noncomputable def category_theory.triangulated.inv_rot_comp_rot_inv {C : Type u} [∀ (n : ), ] :

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

Equations
noncomputable def category_theory.triangulated.inv_rot_comp_rot {C : Type u} [∀ (n : ), ] :

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]
noncomputable def category_theory.triangulated.triangle_rotation (C : Type u) [∀ (n : ), ] :

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

Equations
@[simp]
@[simp]
@[simp]
@[simp]
@[protected, instance]
noncomputable def category_theory.triangulated.rotate.category_theory.is_equivalence {C : Type u} [∀ (n : ), ] :
Equations
@[protected, instance]
noncomputable def category_theory.triangulated.inv_rotate.category_theory.is_equivalence {C : Type u} [∀ (n : ), ] :
Equations