The opposite of a triangulated subcategory

In this file, we show that if P : ObjectProperty C is a triangulated subcategory of a pretriangulated category C, then P.op is a triangulated subcategory of Cᵒᵖ.

instance CategoryTheory.ObjectProperty.instIsStableUnderShiftOppositeOpInt {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] (P : ObjectProperty C) [P.IsStableUnderShift ℤ] : P.op.IsStableUnderShift ℤ

instance CategoryTheory.ObjectProperty.instIsStableUnderShiftUnopIntOfOpposite {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] (P : ObjectProperty Cᵒᵖ) [P.IsStableUnderShift ℤ] : P.unop.IsStableUnderShift ℤ

instance CategoryTheory.ObjectProperty.instIsTriangulatedClosed₂OppositeOp {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulatedClosed₂] : P.op.IsTriangulatedClosed₂

instance CategoryTheory.ObjectProperty.instIsTriangulatedClosed₂UnopOfOpposite {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty Cᵒᵖ) [P.IsTriangulatedClosed₂] : P.unop.IsTriangulatedClosed₂

instance CategoryTheory.ObjectProperty.instIsTriangulatedOppositeOp {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulated] : P.op.IsTriangulated

instance CategoryTheory.ObjectProperty.instIsTriangulatedUnopOfOpposite {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty Cᵒᵖ) [P.IsTriangulated] : P.unop.IsTriangulated

theorem CategoryTheory.ObjectProperty.trW_of_op {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulated] {X Y : C} {f : X ⟶ Y} (hf : P.op.trW f.op) : P.trW f

theorem CategoryTheory.ObjectProperty.trW_of_unop {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty Cᵒᵖ) [P.IsTriangulated] {X Y : Cᵒᵖ} {f : X ⟶ Y} (hf : P.unop.trW f.unop) : P.trW f

theorem CategoryTheory.ObjectProperty.trW_op_iff {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulated] {X Y : Cᵒᵖ} {f : X ⟶ Y} : P.op.trW f ↔ P.trW f.unop

theorem CategoryTheory.ObjectProperty.trW_op {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulated] : P.op.trW = P.trW.op