The opposite of a triangulated category is triangulated

The pretriangulated structure on Cᵒᵖ was constructed in the file CategoryTheory.Triangulated.Opposite.Pretriangulated. Here, we show that Cᵒᵖ is triangulated if C is triangulated.

References

• Jean-Louis Verdier, Des catégories dérivées des catégories abéliennes

theorem CategoryTheory.Pretriangulated.Opposite.instIsTriangulatedOpposite (C : Type u_1) [Category.{u_2, u_1} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] : IsTriangulated Cᵒᵖ