Commit 2023-09-22 12:58 c97e6da0

View on Github →

feat: the shift on the opposite category (#7324)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Shift/Opposite.lean

Created Mathlib/CategoryTheory/Triangulated/Opposite.lean

added theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app_shift

added theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app_shift

added theorem CategoryTheory.Pretriangulated.shiftFunctorAdd'_op_hom_app

added theorem CategoryTheory.Pretriangulated.shiftFunctorAdd'_op_inv_app

added theorem CategoryTheory.Pretriangulated.shiftFunctorZero_op_hom_app

added theorem CategoryTheory.Pretriangulated.shiftFunctorZero_op_inv_app

added theorem CategoryTheory.Pretriangulated.shiftFunctor_op_map

added theorem CategoryTheory.Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_hom_app

added theorem CategoryTheory.Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_inv_app