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.

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
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)

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem CategoryTheory.Pretriangulated.rotCompInvRot_hom_app_hom₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ] [∀ (n : ), (CategoryTheory.shiftFunctor C n).Additive] (X : CategoryTheory.Pretriangulated.Triangle C) :
          (CategoryTheory.Pretriangulated.rotCompInvRot.hom.app X).hom₁ = (CategoryTheory.shiftFunctorCompIsoId C 1 (-1) ).inv.app X.obj₁
          @[simp]
          theorem CategoryTheory.Pretriangulated.rotCompInvRot_inv_app_hom₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ] [∀ (n : ), (CategoryTheory.shiftFunctor C n).Additive] (X : CategoryTheory.Pretriangulated.Triangle C) :
          (CategoryTheory.Pretriangulated.rotCompInvRot.inv.app X).hom₁ = (CategoryTheory.shiftFunctorCompIsoId C 1 (-1) ).hom.app X.obj₁

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem CategoryTheory.Pretriangulated.invRotCompRot_hom_app_hom₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ] [∀ (n : ), (CategoryTheory.shiftFunctor C n).Additive] (X : CategoryTheory.Pretriangulated.Triangle C) :
            (CategoryTheory.Pretriangulated.invRotCompRot.hom.app X).hom₃ = (CategoryTheory.shiftFunctorCompIsoId C (-1) 1 ).hom.app X.obj₃
            @[simp]
            theorem CategoryTheory.Pretriangulated.invRotCompRot_inv_app_hom₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ] [∀ (n : ), (CategoryTheory.shiftFunctor C n).Additive] (X : CategoryTheory.Pretriangulated.Triangle C) :
            (CategoryTheory.Pretriangulated.invRotCompRot.inv.app X).hom₃ = (CategoryTheory.shiftFunctorCompIsoId C (-1) 1 ).inv.app X.obj₃

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For