Commit 2025-12-12 17:53 6517bcfe
View on Github →feat(CategoryTheory/Triangulated): opOp and unopUnop commute with shifts (#32594)
In this file, we show that if C is a pretriangulated category, then the functors opOp C : C ⥤ Cᵒᵖᵒᵖ and unopUnop C : Cᵒᵖᵒᵖ ⥤ C are triangulated. We also show that the unit and counit isomorphisms of the equivalence opOpEquivalence C : Cᵒᵖᵒᵖ ≌ C are compatible with shifts, which is summarized by the property (opOpEquivalence C).IsTriangulated.