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.

source
def CategoryTheory.Pretriangulated.Triangle.rotate {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (T : Triangle C) :
Triangle C

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
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.Triangle.rotate_mor₁ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (T : Triangle C) :
    T.rotate.mor₁ = T.mor₂
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.Triangle.rotate_mor₃ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (T : Triangle C) :
    T.rotate.mor₃ = -(shiftFunctor C 1).map T.mor₁
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.Triangle.rotate_obj₂ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (T : Triangle C) :
    T.rotate.obj₂ = T.obj₃
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.Triangle.rotate_obj₁ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (T : Triangle C) :
    T.rotate.obj₁ = T.obj₂
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.Triangle.rotate_obj₃ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (T : Triangle C) :
    T.rotate.obj₃ = (shiftFunctor C 1).obj T.obj₁
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.Triangle.rotate_mor₂ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (T : Triangle C) :
    T.rotate.mor₂ = T.mor₃
    source
    def CategoryTheory.Pretriangulated.Triangle.invRotate {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (T : Triangle C) :
    Triangle C

    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
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.Triangle.invRotate_obj₁ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (T : Triangle C) :
      T.invRotate.obj₁ = (shiftFunctor C (-1)).obj T.obj₃
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.Triangle.invRotate_mor₃ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (T : Triangle C) :
      T.invRotate.mor₃ = CategoryStruct.comp T.mor₂ ((shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app T.3)
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.Triangle.invRotate_obj₂ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (T : Triangle C) :
      T.invRotate.obj₂ = T.obj₁
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.Triangle.invRotate_obj₃ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (T : Triangle C) :
      T.invRotate.obj₃ = T.obj₂
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.Triangle.invRotate_mor₂ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (T : Triangle C) :
      T.invRotate.mor₂ = T.mor₁
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.Triangle.invRotate_mor₁ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (T : Triangle C) :
      T.invRotate.mor₁ = -CategoryStruct.comp ((shiftFunctor C (-1)).map T.mor₃) ((shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T.obj₁)
      source
      def CategoryTheory.Pretriangulated.rotate (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] :
      Functor (Triangle C) (Triangle C)

      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
        source
        @[simp]
        theorem CategoryTheory.Pretriangulated.rotate_obj (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (T : Triangle C) :
        (rotate C).obj T = T.rotate
        source
        @[simp]
        theorem CategoryTheory.Pretriangulated.rotate_map_hom₃ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] {X✝ Y✝ : Triangle C} (f : X✝ ⟶ Y✝) :
        ((rotate C).map f).hom₃ = (shiftFunctor C 1).map f.hom₁
        source
        @[simp]
        theorem CategoryTheory.Pretriangulated.rotate_map_hom₁ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] {X✝ Y✝ : Triangle C} (f : X✝ ⟶ Y✝) :
        ((rotate C).map f).hom₁ = f.hom₂
        source
        @[simp]
        theorem CategoryTheory.Pretriangulated.rotate_map_hom₂ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] {X✝ Y✝ : Triangle C} (f : X✝ ⟶ Y✝) :
        ((rotate C).map f).hom₂ = f.hom₃
        source
        def CategoryTheory.Pretriangulated.invRotate (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] :
        Functor (Triangle C) (Triangle C)

        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
          source
          @[simp]
          theorem CategoryTheory.Pretriangulated.invRotate_obj (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] (T : Triangle C) :
          (invRotate C).obj T = T.invRotate
          source
          @[simp]
          theorem CategoryTheory.Pretriangulated.invRotate_map_hom₁ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] {X✝ Y✝ : Triangle C} (f : X✝ ⟶ Y✝) :
          ((invRotate C).map f).hom₁ = (shiftFunctor C (-1)).map f.hom₃
          source
          @[simp]
          theorem CategoryTheory.Pretriangulated.invRotate_map_hom₃ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] {X✝ Y✝ : Triangle C} (f : X✝ ⟶ Y✝) :
          ((invRotate C).map f).hom₃ = f.hom₂
          source
          @[simp]
          theorem CategoryTheory.Pretriangulated.invRotate_map_hom₂ (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] {X✝ Y✝ : Triangle C} (f : X✝ ⟶ Y✝) :
          ((invRotate C).map f).hom₂ = f.hom₁
          source
          def CategoryTheory.Pretriangulated.rotCompInvRot {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] :
          Functor.id (Triangle C) ≅ (rotate C).comp (invRotate C)

          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
            source
            @[simp]
            theorem CategoryTheory.Pretriangulated.rotCompInvRot_hom_app_hom₂ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (X : Triangle C) :
            (rotCompInvRot.hom.app X).hom₂ = CategoryStruct.id X.obj₂
            source
            @[simp]
            theorem CategoryTheory.Pretriangulated.rotCompInvRot_hom_app_hom₃ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (X : Triangle C) :
            (rotCompInvRot.hom.app X).hom₃ = CategoryStruct.id X.obj₃
            source
            @[simp]
            theorem CategoryTheory.Pretriangulated.rotCompInvRot_inv_app_hom₁ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (X : Triangle C) :
            (rotCompInvRot.inv.app X).hom₁ = (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X.obj₁
            source
            @[simp]
            theorem CategoryTheory.Pretriangulated.rotCompInvRot_inv_app_hom₂ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (X : Triangle C) :
            (rotCompInvRot.inv.app X).hom₂ = CategoryStruct.id X.obj₂
            source
            @[simp]
            theorem CategoryTheory.Pretriangulated.rotCompInvRot_inv_app_hom₃ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (X : Triangle C) :
            (rotCompInvRot.inv.app X).hom₃ = CategoryStruct.id X.obj₃
            source
            @[simp]
            theorem CategoryTheory.Pretriangulated.rotCompInvRot_hom_app_hom₁ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (X : Triangle C) :
            (rotCompInvRot.hom.app X).hom₁ = (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app X.obj₁
            source
            def CategoryTheory.Pretriangulated.invRotCompRot {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] :
            (invRotate C).comp (rotate C) ≅ Functor.id (Triangle C)

            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
              source
              @[simp]
              theorem CategoryTheory.Pretriangulated.invRotCompRot_hom_app_hom₁ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (X : Triangle C) :
              (invRotCompRot.hom.app X).hom₁ = CategoryStruct.id X.obj₁
              source
              @[simp]
              theorem CategoryTheory.Pretriangulated.invRotCompRot_inv_app_hom₂ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (X : Triangle C) :
              (invRotCompRot.inv.app X).hom₂ = CategoryStruct.id X.obj₂
              source
              @[simp]
              theorem CategoryTheory.Pretriangulated.invRotCompRot_hom_app_hom₂ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (X : Triangle C) :
              (invRotCompRot.hom.app X).hom₂ = CategoryStruct.id X.obj₂
              source
              @[simp]
              theorem CategoryTheory.Pretriangulated.invRotCompRot_inv_app_hom₁ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (X : Triangle C) :
              (invRotCompRot.inv.app X).hom₁ = CategoryStruct.id X.obj₁
              source
              @[simp]
              theorem CategoryTheory.Pretriangulated.invRotCompRot_hom_app_hom₃ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (X : Triangle C) :
              (invRotCompRot.hom.app X).hom₃ = (shiftFunctorCompIsoId C (-1) 1 ⋯).hom.app X.obj₃
              source
              @[simp]
              theorem CategoryTheory.Pretriangulated.invRotCompRot_inv_app_hom₃ {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] (X : Triangle C) :
              (invRotCompRot.inv.app X).hom₃ = (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app X.obj₃
              source
              def CategoryTheory.Pretriangulated.triangleRotation (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] :
              Triangle C ≌ Triangle C

              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
                source
                @[simp]
                theorem CategoryTheory.Pretriangulated.triangleRotation_inverse (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] :
                (triangleRotation C).inverse = invRotate C
                source
                @[simp]
                theorem CategoryTheory.Pretriangulated.triangleRotation_functor (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] :
                (triangleRotation C).functor = rotate C
                source
                @[simp]
                theorem CategoryTheory.Pretriangulated.triangleRotation_counitIso (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] :
                (triangleRotation C).counitIso = invRotCompRot
                source
                @[simp]
                theorem CategoryTheory.Pretriangulated.triangleRotation_unitIso (C : Type u) [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] :
                (triangleRotation C).unitIso = rotCompInvRot
                source
                instance CategoryTheory.Pretriangulated.instIsEquivalenceTriangleRotate {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] :
                (rotate C).IsEquivalence
                source
                instance CategoryTheory.Pretriangulated.instIsEquivalenceTriangleInvRotate {C : Type u} [Category.{v, u} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] :
                (invRotate C).IsEquivalence