# 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.

@[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⟧

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
@[simp]
theorem CategoryTheory.Pretriangulated.rotate_map_hom₁ (C : Type u) :
∀ {X Y : } (f : X Y), ().hom₁ = f.hom₂
@[simp]
@[simp]
theorem CategoryTheory.Pretriangulated.rotate_map_hom₃ (C : Type u) :
∀ {X Y : } (f : X Y), ().hom₃ = ().map f.hom₁
@[simp]
theorem CategoryTheory.Pretriangulated.rotate_map_hom₂ (C : Type u) :
∀ {X Y : } (f : X Y), ().hom₂ = f.hom₃

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

Instances For
@[simp]
theorem CategoryTheory.Pretriangulated.invRotate_map_hom₃ (C : Type u) :
∀ {X Y : } (f : X Y), ().hom₃ = f.hom₂
@[simp]
theorem CategoryTheory.Pretriangulated.invRotate_map_hom₂ (C : Type u) :
∀ {X Y : } (f : X Y), ().hom₂ = f.hom₁
@[simp]
@[simp]
theorem CategoryTheory.Pretriangulated.invRotate_map_hom₁ (C : Type u) :
∀ {X Y : } (f : X Y), ().hom₁ = ().map f.hom₃

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

Instances For
@[simp]
theorem CategoryTheory.Pretriangulated.rotCompInvRot_hom_app_hom₂ {C : Type u} [] :
(CategoryTheory.Pretriangulated.rotCompInvRot.hom.app X).hom₂ =
@[simp]
theorem CategoryTheory.Pretriangulated.rotCompInvRot_inv_app_hom₂ {C : Type u} [] :
(CategoryTheory.Pretriangulated.rotCompInvRot.inv.app X).hom₂ =
@[simp]
theorem CategoryTheory.Pretriangulated.rotCompInvRot_hom_app_hom₁ {C : Type u} [] :
(CategoryTheory.Pretriangulated.rotCompInvRot.hom.app X).hom₁ = (CategoryTheory.shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).inv.app X.obj₁
@[simp]
theorem CategoryTheory.Pretriangulated.rotCompInvRot_inv_app_hom₃ {C : Type u} [] :
(CategoryTheory.Pretriangulated.rotCompInvRot.inv.app X).hom₃ =
@[simp]
theorem CategoryTheory.Pretriangulated.rotCompInvRot_hom_app_hom₃ {C : Type u} [] :
(CategoryTheory.Pretriangulated.rotCompInvRot.hom.app X).hom₃ =
@[simp]
theorem CategoryTheory.Pretriangulated.rotCompInvRot_inv_app_hom₁ {C : Type u} [] :
(CategoryTheory.Pretriangulated.rotCompInvRot.inv.app X).hom₁ = (CategoryTheory.shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom.app X.obj₁

The unit isomorphism of the auto-equivalence of categories triangleRotation C of Triangle C given by the rotation of triangles.

Instances For
@[simp]
theorem CategoryTheory.Pretriangulated.invRotCompRot_hom_app_hom₂ {C : Type u} [] :
(CategoryTheory.Pretriangulated.invRotCompRot.hom.app X).hom₂ =
@[simp]
theorem CategoryTheory.Pretriangulated.invRotCompRot_hom_app_hom₃ {C : Type u} [] :
(CategoryTheory.Pretriangulated.invRotCompRot.hom.app X).hom₃ = (CategoryTheory.shiftFunctorCompIsoId C (-1) 1 (_ : -1 + 1 = 0)).hom.app X.obj₃
@[simp]
theorem CategoryTheory.Pretriangulated.invRotCompRot_inv_app_hom₁ {C : Type u} [] :
(CategoryTheory.Pretriangulated.invRotCompRot.inv.app X).hom₁ =
@[simp]
theorem CategoryTheory.Pretriangulated.invRotCompRot_hom_app_hom₁ {C : Type u} [] :
(CategoryTheory.Pretriangulated.invRotCompRot.hom.app X).hom₁ =
@[simp]
theorem CategoryTheory.Pretriangulated.invRotCompRot_inv_app_hom₃ {C : Type u} [] :
(CategoryTheory.Pretriangulated.invRotCompRot.inv.app X).hom₃ = (CategoryTheory.shiftFunctorCompIsoId C (-1) 1 (_ : -1 + 1 = 0)).inv.app X.obj₃
@[simp]
theorem CategoryTheory.Pretriangulated.invRotCompRot_inv_app_hom₂ {C : Type u} [] :
(CategoryTheory.Pretriangulated.invRotCompRot.inv.app X).hom₂ =

The counit isomorphism of the auto-equivalence of categories triangleRotation C of Triangle C given by the rotation of triangles.

Instances For
@[simp]
theorem CategoryTheory.Pretriangulated.triangleRotation_unitIso (C : Type u) [] :
().unitIso = CategoryTheory.Pretriangulated.rotCompInvRot
@[simp]
@[simp]
theorem CategoryTheory.Pretriangulated.triangleRotation_counitIso (C : Type u) [] :
().counitIso = CategoryTheory.Pretriangulated.invRotCompRot
@[simp]

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

Instances For