Commit 2025-12-10 21:53 9e508f58

View on Github →

feat(CategoryTheory): the opposite of a triangulated category is triangulated (#32535)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Shift/Basic.lean

added theorem CategoryTheory.shiftFunctorComm_hom_app_of_add_eq_zero

added theorem CategoryTheory.shiftFunctorComm_inv_app_of_add_eq_zero

Modified Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean

added theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_apply

added theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_left_inv

added theorem CategoryTheory.Pretriangulated.shiftFunctorCompIsoId_op_hom_app

added theorem CategoryTheory.Pretriangulated.shiftFunctorCompIsoId_op_inv_app

added theorem CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalenceSymmHomEquiv_unop

added theorem CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app

Modified Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean

Created Mathlib/CategoryTheory/Triangulated/Opposite/Triangulated.lean

Modified Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean

added theorem CategoryTheory.Pretriangulated.Triangle.shift_distinguished_iff