Documentation

Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Opposites of functors between pretriangulated categories, #

If F : C ⥤ D is a functor between pretriangulated categories, we prove that F is a triangulated functor if and only if F.op is a triangulated functor. In order to do this, we first show that a CommShift structure on F naturally gives one on F.op (for the shifts on Cᵒᵖ and Dᵒᵖ defined in CategoryTheory.Triangulated.Opposite.Basic), and we then prove that F.mapTriangle.op and F.op.mapTriangle correspond to each other via the equivalences (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ and (Triangle D)ᵒᵖ ≌ Triangle Dᵒᵖ given by CategoryTheory.Pretriangulated.triangleOpEquivalence.

source
noncomputable def CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] :
F.op.CommShift ℤ

If F commutes with shifts, so does F.op, for the shifts chosen on Cᵒᵖ in CategoryTheory.Triangulated.Opposite.Basic.

Equations
    Instances For
      source
      theorem CategoryTheory.Pretriangulated.Opposite.commShift_natTrans_op_int {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] {F : Functor C D} [F.CommShift ℤ] {G : Functor C D} [G.CommShift ℤ] (τ : F ⟶ G) [NatTrans.CommShift τ ℤ] :
      NatTrans.CommShift (NatTrans.op τ) ℤ
      source
      theorem CategoryTheory.Pretriangulated.Opposite.commShift_adjunction_op_int {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [HasShift C ℤ] [HasShift D ℤ] {F : Functor C D} [F.CommShift ℤ] {G : Functor D C} [G.CommShift ℤ] (adj : F ⊣ G) [adj.CommShift ℤ] :
      adj.op.CommShift ℤ
      source
      theorem CategoryTheory.Functor.op_commShiftIso_hom_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n m : ℤ) (h : n + m = 0) :
      (F.op.commShiftIso n).hom.app X = CategoryStruct.comp (F.map ((Pretriangulated.shiftFunctorOpIso C n m h).hom.app X).unop).op (CategoryStruct.comp ((F.commShiftIso m).inv.app (Opposite.unop X)).op ((Pretriangulated.shiftFunctorOpIso D n m h).inv.app (Opposite.op (F.obj (Opposite.unop X)))))
      source
      theorem CategoryTheory.Functor.op_commShiftIso_hom_app_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n m : ℤ) (h : n + m = 0) {Z : Dᵒᵖ} (h✝ : (shiftFunctor Dᵒᵖ n).obj (F.op.obj X) ⟶ Z) :
      CategoryStruct.comp ((F.op.commShiftIso n).hom.app X) h✝ = CategoryStruct.comp (F.map ((Pretriangulated.shiftFunctorOpIso C n m h).hom.app X).unop).op (CategoryStruct.comp ((F.commShiftIso m).inv.app (Opposite.unop X)).op (CategoryStruct.comp ((Pretriangulated.shiftFunctorOpIso D n m h).inv.app (Opposite.op (F.obj (Opposite.unop X)))) h✝))
      source
      theorem CategoryTheory.Functor.op_commShiftIso_inv_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n m : ℤ) (h : n + m = 0) :
      (F.op.commShiftIso n).inv.app X = CategoryStruct.comp ((Pretriangulated.shiftFunctorOpIso D n m h).hom.app (Opposite.op (F.obj (Opposite.unop X)))) (CategoryStruct.comp ((F.commShiftIso m).hom.app (Opposite.unop X)).op (F.map ((Pretriangulated.shiftFunctorOpIso C n m h).inv.app X).unop).op)
      source
      theorem CategoryTheory.Functor.op_commShiftIso_inv_app_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n m : ℤ) (h : n + m = 0) {Z : Dᵒᵖ} (h✝ : F.op.obj ((shiftFunctor Cᵒᵖ n).obj X) ⟶ Z) :
      CategoryStruct.comp ((F.op.commShiftIso n).inv.app X) h✝ = CategoryStruct.comp ((Pretriangulated.shiftFunctorOpIso D n m h).hom.app (Opposite.op (F.obj (Opposite.unop X)))) (CategoryStruct.comp ((F.commShiftIso m).hom.app (Opposite.unop X)).op (CategoryStruct.comp (F.map ((Pretriangulated.shiftFunctorOpIso C n m h).inv.app X).unop).op h✝))
      source
      theorem CategoryTheory.Functor.shift_map_op {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] {X Y : C} (f : X ⟶ Y) (n : ℤ) :
      (shiftFunctor Dᵒᵖ n).map (F.map f).op = CategoryStruct.comp ((F.op.commShiftIso n).inv.app (Opposite.op Y)) (CategoryStruct.comp (F.map ((shiftFunctor Cᵒᵖ n).map f.op).unop).op ((F.op.commShiftIso n).hom.app (Opposite.op X)))
      source
      theorem CategoryTheory.Functor.shift_map_op_assoc {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] {X Y : C} (f : X ⟶ Y) (n : ℤ) {Z : Dᵒᵖ} (h : (shiftFunctor Dᵒᵖ n).obj (Opposite.op (F.obj X)) ⟶ Z) :
      CategoryStruct.comp ((shiftFunctor Dᵒᵖ n).map (F.map f).op) h = CategoryStruct.comp ((F.op.commShiftIso n).inv.app (Opposite.op Y)) (CategoryStruct.comp (F.map ((shiftFunctor Cᵒᵖ n).map f.op).unop).op (CategoryStruct.comp ((F.op.commShiftIso n).hom.app (Opposite.op X)) h))
      source
      theorem CategoryTheory.Functor.map_shift_unop {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] {X Y : Cᵒᵖ} (f : X ⟶ Y) (n : ℤ) :
      F.map ((shiftFunctor Cᵒᵖ n).map f).unop = CategoryStruct.comp ((F.op.commShiftIso n).inv.app Y).unop (CategoryStruct.comp ((shiftFunctor Dᵒᵖ n).map (F.map f.unop).op).unop ((F.op.commShiftIso n).hom.app X).unop)
      source
      theorem CategoryTheory.Functor.map_shift_unop_assoc {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] {X Y : Cᵒᵖ} (f : X ⟶ Y) (n : ℤ) {Z : D} (h : F.obj (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)) ⟶ Z) :
      CategoryStruct.comp (F.map ((shiftFunctor Cᵒᵖ n).map f).unop) h = CategoryStruct.comp ((F.op.commShiftIso n).inv.app Y).unop (CategoryStruct.comp ((shiftFunctor Dᵒᵖ n).map (F.map f.unop).op).unop (CategoryStruct.comp ((F.op.commShiftIso n).hom.app X).unop h))
      source
      theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ) :
      F.map ((Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X).unop = CategoryStruct.comp ((F.commShiftIso n).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X))) (CategoryStruct.comp ((shiftFunctor D n).map ((F.op.commShiftIso n).inv.app X).unop) ((Pretriangulated.opShiftFunctorEquivalence D n).unitIso.hom.app (Opposite.op (F.obj (Opposite.unop X)))).unop)
      source
      theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ) {Z : D} (h : F.obj (Opposite.unop X) ⟶ Z) :
      CategoryStruct.comp (F.map ((Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X).unop) h = CategoryStruct.comp ((F.commShiftIso n).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X))) (CategoryStruct.comp ((shiftFunctor D n).map ((F.op.commShiftIso n).inv.app X).unop) (CategoryStruct.comp ((Pretriangulated.opShiftFunctorEquivalence D n).unitIso.hom.app (Opposite.op (F.obj (Opposite.unop X)))).unop h))
      source
      theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ) :
      F.map ((Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X).unop = CategoryStruct.comp ((Pretriangulated.opShiftFunctorEquivalence D n).unitIso.inv.app (Opposite.op (F.obj (Opposite.unop X)))).unop (CategoryStruct.comp ((shiftFunctor D n).map ((F.op.commShiftIso n).hom.app X).unop) ((F.commShiftIso n).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X))))
      source
      theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ) {Z : D} (h : F.obj (Opposite.unop ((Pretriangulated.opShiftFunctorEquivalence C n).inverse.obj ((Pretriangulated.opShiftFunctorEquivalence C n).functor.obj X))) ⟶ Z) :
      CategoryStruct.comp (F.map ((Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X).unop) h = CategoryStruct.comp ((Pretriangulated.opShiftFunctorEquivalence D n).unitIso.inv.app (Opposite.op (F.obj (Opposite.unop X)))).unop (CategoryStruct.comp ((shiftFunctor D n).map ((F.op.commShiftIso n).hom.app X).unop) (CategoryStruct.comp ((F.commShiftIso n).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X))) h))
      source
      theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ) :
      F.map ((Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app X).unop = CategoryStruct.comp ((Pretriangulated.opShiftFunctorEquivalence D n).counitIso.hom.app (Opposite.op (F.obj (Opposite.unop X)))).unop (CategoryStruct.comp ((shiftFunctor Dᵒᵖ n).map ((F.commShiftIso n).inv.app (Opposite.unop X)).op).unop ((F.op.commShiftIso n).hom.app (Opposite.op ((shiftFunctor C n).obj (Opposite.unop X)))).unop)
      source
      theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ) {Z : D} (h : F.obj (Opposite.unop ((Pretriangulated.opShiftFunctorEquivalence C n).functor.obj ((Pretriangulated.opShiftFunctorEquivalence C n).inverse.obj X))) ⟶ Z) :
      CategoryStruct.comp (F.map ((Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app X).unop) h = CategoryStruct.comp ((Pretriangulated.opShiftFunctorEquivalence D n).counitIso.hom.app (Opposite.op (F.obj (Opposite.unop X)))).unop (CategoryStruct.comp ((shiftFunctor Dᵒᵖ n).map ((F.commShiftIso n).inv.app (Opposite.unop X)).op).unop (CategoryStruct.comp ((F.op.commShiftIso n).hom.app (Opposite.op ((shiftFunctor C n).obj (Opposite.unop X)))).unop h))
      source
      theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ) :
      F.map ((Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X).unop = CategoryStruct.comp ((F.op.commShiftIso n).inv.app (Opposite.op ((shiftFunctor C n).obj (Opposite.unop X)))).unop (CategoryStruct.comp ((shiftFunctor Dᵒᵖ n).map ((F.commShiftIso n).hom.app (Opposite.unop X)).op).unop ((Pretriangulated.opShiftFunctorEquivalence D n).counitIso.inv.app (Opposite.op (F.obj (Opposite.unop X)))).unop)
      source
      theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ) {Z : D} (h : F.obj (Opposite.unop X) ⟶ Z) :
      CategoryStruct.comp (F.map ((Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X).unop) h = CategoryStruct.comp ((F.op.commShiftIso n).inv.app (Opposite.op ((shiftFunctor C n).obj (Opposite.unop X)))).unop (CategoryStruct.comp ((shiftFunctor Dᵒᵖ n).map ((F.commShiftIso n).hom.app (Opposite.unop X)).op).unop (CategoryStruct.comp ((Pretriangulated.opShiftFunctorEquivalence D n).counitIso.inv.app (Opposite.op (F.obj (Opposite.unop X)))).unop h))
      source
      noncomputable def CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (T : Pretriangulated.Triangle C) :
      (Pretriangulated.triangleOpEquivalence D).functor.obj (Opposite.op (F.mapTriangle.obj T)) ≅ F.op.mapTriangle.obj ((Pretriangulated.triangleOpEquivalence C).functor.obj (Opposite.op T))

      If F : C ⥤ D commutes with shifts, this expresses the compatibility of F.mapTriangle with the equivalences Pretriangulated.triangleOpEquivalence on C and D.

      Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₃ {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (T : Pretriangulated.Triangle C) :
          (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp T).inv.hom₃ = CategoryStruct.id (Opposite.op (F.obj T.obj₁))
          source
          @[simp]
          theorem CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₁ {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (T : Pretriangulated.Triangle C) :
          (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp T).inv.hom₁ = CategoryStruct.id (Opposite.op (F.obj T.obj₃))
          source
          @[simp]
          theorem CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₁ {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (T : Pretriangulated.Triangle C) :
          (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp T).hom.hom₁ = CategoryStruct.id (Opposite.op (F.obj T.obj₃))
          source
          @[simp]
          theorem CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₂ {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (T : Pretriangulated.Triangle C) :
          (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp T).inv.hom₂ = CategoryStruct.id (Opposite.op (F.obj T.obj₂))
          source
          @[simp]
          theorem CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₂ {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (T : Pretriangulated.Triangle C) :
          (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp T).hom.hom₂ = CategoryStruct.id (Opposite.op (F.obj T.obj₂))
          source
          @[simp]
          theorem CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₃ {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (T : Pretriangulated.Triangle C) :
          (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp T).hom.hom₃ = CategoryStruct.id (Opposite.op (F.obj T.obj₁))
          source
          noncomputable def CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctor {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] :
          F.mapTriangle.op.comp (Pretriangulated.triangleOpEquivalence D).functor ≅ (Pretriangulated.triangleOpEquivalence C).functor.comp F.op.mapTriangle

          If F : C ⥤ D commutes with shifts, this expresses the compatibility of F.mapTriangle with the equivalences Pretriangulated.triangleOpEquivalence on C and D.

          Equations
            Instances For
              source
              noncomputable instance CategoryTheory.Functor.instCatCommSqOppositeTriangleOpMapTriangleFunctorTriangleOpEquivalence {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] :
              CatCommSq F.mapTriangle.op (Pretriangulated.triangleOpEquivalence C).functor (Pretriangulated.triangleOpEquivalence D).functor F.op.mapTriangle

              If F : C ⥤ D commutes with shifts, this is the 2-commutative square of categories CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctor.

              Equations
                source
                noncomputable instance CategoryTheory.Functor.instCatCommSqTriangleOppositeMapTriangleOpInverseTriangleOpEquivalence {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] :
                CatCommSq F.op.mapTriangle (Pretriangulated.triangleOpEquivalence C).inverse (Pretriangulated.triangleOpEquivalence D).inverse F.mapTriangle.op

                Vertical inverse of the 2-commutative square of CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctor.

                Equations
                  source
                  noncomputable def CategoryTheory.Functor.opMapTriangleCompTriangleOpEquivalenceInverse {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] :
                  F.op.mapTriangle.comp (Pretriangulated.triangleOpEquivalence D).inverse ≅ (Pretriangulated.triangleOpEquivalence C).inverse.comp F.mapTriangle.op

                  If F : C ⥤ D commutes with shifts, this expresses the compatibility of F.mapTriangle with the equivalences Pretriangulated.triangleOpEquivalence on C and D.

                  Equations
                    Instances For
                      source
                      theorem CategoryTheory.Pretriangulated.Opposite.functor_isTriangulated_op {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [F.IsTriangulated] :
                      F.op.IsTriangulated

                      If F is triangulated, so is F.op.

                      source
                      theorem CategoryTheory.Functor.isTriangulated_of_op {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [F.op.IsTriangulated] :
                      F.IsTriangulated

                      If F.op is triangulated, so is F.

                      source
                      theorem CategoryTheory.Functor.op_isTriangulated_iff {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] :
                      F.op.IsTriangulated ↔ F.IsTriangulated

                      F is triangulated if and only if F.op is triangulated.