Commit 2024-12-30 18:55 9df7ff0b

View on Github →

feat(CategoryTheory/Triangulated/Opposite): the opposite of a triangulated functor (#20278) A functor between pretriangulated categories is a triangulated functor if and only if its opposite is a triangulated functor.

Estimated changes

Modified Mathlib.lean

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

added theorem CategoryTheory.Functor.isTriangulated_of_op

added theorem CategoryTheory.Functor.isTriangulated_op

added theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop

added theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop

added theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop

added theorem CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop

added theorem CategoryTheory.Functor.map_shift_unop

added theorem CategoryTheory.Functor.op_commShiftIso_hom_app

added theorem CategoryTheory.Functor.op_commShiftIso_inv_app

added theorem CategoryTheory.Functor.op_isTriangulated_iff

added theorem CategoryTheory.Functor.shift_map_op