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.

noncomputable def CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.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.

theorem CategoryTheory.Pretriangulated.Opposite.commShift_natTrans_op_int {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] {F : CategoryTheory.Functor C D} [F.CommShift ℤ] {G : CategoryTheory.Functor C D} [G.CommShift ℤ] (τ : F ⟶ G) [CategoryTheory.NatTrans.CommShift τ ℤ] : CategoryTheory.NatTrans.CommShift (CategoryTheory.NatTrans.op τ) ℤ

theorem CategoryTheory.Pretriangulated.Opposite.commShift_adjunction_op_int {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] {F : CategoryTheory.Functor C D} [F.CommShift ℤ] {G : CategoryTheory.Functor D C} [G.CommShift ℤ] (adj : F ⊣ G) [adj.CommShift ℤ] : adj.op.CommShift ℤ

theorem CategoryTheory.Functor.op_commShiftIso_hom_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n m : ℤ) (h : n + m = 0) : (F.op.commShiftIso n).hom.app X = CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m h).hom.app X).unop).op (CategoryTheory.CategoryStruct.comp ((F.commShiftIso m).inv.app (Opposite.unop X)).op ((CategoryTheory.Pretriangulated.shiftFunctorOpIso D n m h).inv.app (Opposite.op (F.obj (Opposite.unop X)))))

theorem CategoryTheory.Functor.op_commShiftIso_hom_app_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n m : ℤ) (h : n + m = 0) {Z : Dᵒᵖ} (h✝ : (CategoryTheory.shiftFunctor Dᵒᵖ n).obj (F.op.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.op.commShiftIso n).hom.app X) h✝ = CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m h).hom.app X).unop).op (CategoryTheory.CategoryStruct.comp ((F.commShiftIso m).inv.app (Opposite.unop X)).op (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso D n m h).inv.app (Opposite.op (F.obj (Opposite.unop X)))) h✝))

theorem CategoryTheory.Functor.op_commShiftIso_inv_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n m : ℤ) (h : n + m = 0) : (F.op.commShiftIso n).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso D n m h).hom.app (Opposite.op (F.obj (Opposite.unop X)))) (CategoryTheory.CategoryStruct.comp ((F.commShiftIso m).hom.app (Opposite.unop X)).op (F.map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m h).inv.app X).unop).op)

theorem CategoryTheory.Functor.op_commShiftIso_inv_app_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n m : ℤ) (h : n + m = 0) {Z : Dᵒᵖ} (h✝ : F.op.obj ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.op.commShiftIso n).inv.app X) h✝ = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso D n m h).hom.app (Opposite.op (F.obj (Opposite.unop X)))) (CategoryTheory.CategoryStruct.comp ((F.commShiftIso m).hom.app (Opposite.unop X)).op (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m h).inv.app X).unop).op h✝))

theorem CategoryTheory.Functor.shift_map_op {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] {X Y : C} (f : X ⟶ Y) (n : ℤ) : (CategoryTheory.shiftFunctor Dᵒᵖ n).map (F.map f).op = CategoryTheory.CategoryStruct.comp ((F.op.commShiftIso n).inv.app (Opposite.op Y)) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f.op).unop).op ((F.op.commShiftIso n).hom.app (Opposite.op X)))

theorem CategoryTheory.Functor.shift_map_op_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] {X Y : C} (f : X ⟶ Y) (n : ℤ) {Z : Dᵒᵖ} (h : (CategoryTheory.shiftFunctor Dᵒᵖ n).obj (Opposite.op (F.obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Dᵒᵖ n).map (F.map f).op) h = CategoryTheory.CategoryStruct.comp ((F.op.commShiftIso n).inv.app (Opposite.op Y)) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f.op).unop).op (CategoryTheory.CategoryStruct.comp ((F.op.commShiftIso n).hom.app (Opposite.op X)) h))

theorem CategoryTheory.Functor.map_shift_unop {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] {X Y : Cᵒᵖ} (f : X ⟶ Y) (n : ℤ) : F.map ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f).unop = CategoryTheory.CategoryStruct.comp ((F.op.commShiftIso n).inv.app Y).unop (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Dᵒᵖ n).map (F.map f.unop).op).unop ((F.op.commShiftIso n).hom.app X).unop)

theorem CategoryTheory.Functor.map_shift_unop_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] {X Y : Cᵒᵖ} (f : X ⟶ Y) (n : ℤ) {Z : D} (h : F.obj (Opposite.unop ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f).unop) h = CategoryTheory.CategoryStruct.comp ((F.op.commShiftIso n).inv.app Y).unop (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Dᵒᵖ n).map (F.map f.unop).op).unop (CategoryTheory.CategoryStruct.comp ((F.op.commShiftIso n).hom.app X).unop h))

theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ) : F.map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X).unop = CategoryTheory.CategoryStruct.comp ((F.commShiftIso n).hom.app (Opposite.unop ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((F.op.commShiftIso n).inv.app X).unop) ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence D n).unitIso.hom.app (Opposite.op (F.obj (Opposite.unop X)))).unop)

theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ) {Z : D} (h : F.obj (Opposite.unop X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X).unop) h = CategoryTheory.CategoryStruct.comp ((F.commShiftIso n).hom.app (Opposite.unop ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((F.op.commShiftIso n).inv.app X).unop) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence D n).unitIso.hom.app (Opposite.op (F.obj (Opposite.unop X)))).unop h))

theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ) : F.map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X).unop = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence D n).unitIso.inv.app (Opposite.op (F.obj (Opposite.unop X)))).unop (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((F.op.commShiftIso n).hom.app X).unop) ((F.commShiftIso n).inv.app (Opposite.unop ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X))))

theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ) {Z : D} (h : F.obj (Opposite.unop ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).inverse.obj ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).functor.obj X))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X).unop) h = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence D n).unitIso.inv.app (Opposite.op (F.obj (Opposite.unop X)))).unop (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((F.op.commShiftIso n).hom.app X).unop) (CategoryTheory.CategoryStruct.comp ((F.commShiftIso n).inv.app (Opposite.unop ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X))) h))

theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ) : F.map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app X).unop = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence D n).counitIso.hom.app (Opposite.op (F.obj (Opposite.unop X)))).unop (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Dᵒᵖ n).map ((F.commShiftIso n).inv.app (Opposite.unop X)).op).unop ((F.op.commShiftIso n).hom.app (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)))).unop)

theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ) {Z : D} (h : F.obj (Opposite.unop ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).functor.obj ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).inverse.obj X))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app X).unop) h = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence D n).counitIso.hom.app (Opposite.op (F.obj (Opposite.unop X)))).unop (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Dᵒᵖ n).map ((F.commShiftIso n).inv.app (Opposite.unop X)).op).unop (CategoryTheory.CategoryStruct.comp ((F.op.commShiftIso n).hom.app (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)))).unop h))

theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ) : F.map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X).unop = CategoryTheory.CategoryStruct.comp ((F.op.commShiftIso n).inv.app (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)))).unop (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Dᵒᵖ n).map ((F.commShiftIso n).hom.app (Opposite.unop X)).op).unop ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence D n).counitIso.inv.app (Opposite.op (F.obj (Opposite.unop X)))).unop)

theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ) {Z : D} (h : F.obj (Opposite.unop X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X).unop) h = CategoryTheory.CategoryStruct.comp ((F.op.commShiftIso n).inv.app (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)))).unop (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Dᵒᵖ n).map ((F.commShiftIso n).hom.app (Opposite.unop X)).op).unop (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence D n).counitIso.inv.app (Opposite.op (F.obj (Opposite.unop X)))).unop h))

noncomputable def CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) : (CategoryTheory.Pretriangulated.triangleOpEquivalence D).functor.obj (Opposite.op (F.mapTriangle.obj T)) ≅ F.op.mapTriangle.obj ((CategoryTheory.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.

@[simp]

theorem CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₃ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) : (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp T).inv.hom₃ = CategoryTheory.CategoryStruct.id (Opposite.op (F.obj T.obj₁))

@[simp]

theorem CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₁ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) : (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp T).inv.hom₁ = CategoryTheory.CategoryStruct.id (Opposite.op (F.obj T.obj₃))

@[simp]

theorem CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₁ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) : (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp T).hom.hom₁ = CategoryTheory.CategoryStruct.id (Opposite.op (F.obj T.obj₃))

@[simp]

theorem CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₂ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) : (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp T).inv.hom₂ = CategoryTheory.CategoryStruct.id (Opposite.op (F.obj T.obj₂))

@[simp]

theorem CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₂ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) : (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp T).hom.hom₂ = CategoryTheory.CategoryStruct.id (Opposite.op (F.obj T.obj₂))

@[simp]

theorem CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₃ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) : (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp T).hom.hom₃ = CategoryTheory.CategoryStruct.id (Opposite.op (F.obj T.obj₁))

noncomputable def CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctor {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] : F.mapTriangle.op.comp (CategoryTheory.Pretriangulated.triangleOpEquivalence D).functor ≅ (CategoryTheory.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.

noncomputable instance CategoryTheory.Functor.instCatCommSqOppositeTriangleOpMapTriangleFunctorTriangleOpEquivalence {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] : CategoryTheory.CatCommSq F.mapTriangle.op (CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor (CategoryTheory.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

• F.instCatCommSqOppositeTriangleOpMapTriangleFunctorTriangleOpEquivalence = { iso' := F.mapTriangleOpCompTriangleOpEquivalenceFunctor }

noncomputable instance CategoryTheory.Functor.instCatCommSqTriangleOppositeMapTriangleOpInverseTriangleOpEquivalence {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] : CategoryTheory.CatCommSq F.op.mapTriangle (CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse (CategoryTheory.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.

noncomputable def CategoryTheory.Functor.opMapTriangleCompTriangleOpEquivalenceInverse {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] : F.op.mapTriangle.comp (CategoryTheory.Pretriangulated.triangleOpEquivalence D).inverse ≅ (CategoryTheory.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.

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

If F is triangulated, so is F.op.

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

If F.op is triangulated, so is F.

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

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