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
  • One or more equations did not get rendered due to their size.
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
    • One or more equations did not get rendered due to their size.
    Instances For
      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
      @[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_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
      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
      • One or more equations did not get rendered due to their size.
      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
        • One or more equations did not get rendered due to their size.
        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
        • One or more equations did not get rendered due to their size.
        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.