Commit 2024-06-24 08:03 81b12672

View on Github →

feat(CategoryTheory): more API for the commutation of functors with shifts (#13757) In this PR, it is shown that the composition of two functors which commute with shifts also commutes with shifts. The notion of natural transformation which commutes with the shifts is also introduced. This shall be used in the development of the API for the derived category #13742.

Estimated changes

Modified Mathlib/CategoryTheory/Shift/CommShift.lean

added def CategoryTheory.Functor.CommShift.ofIso

added theorem CategoryTheory.Functor.CommShift.ofIso_compatibility

added theorem CategoryTheory.Functor.commShiftIso_comp_hom_app

added theorem CategoryTheory.Functor.commShiftIso_comp_inv_app

added theorem CategoryTheory.NatTrans.CommShift.app_shift

added theorem CategoryTheory.NatTrans.CommShift.comm

added theorem CategoryTheory.NatTrans.CommShift.comm_app

added theorem CategoryTheory.NatTrans.CommShift.of_isIso

added theorem CategoryTheory.NatTrans.CommShift.shift_app

Modified Mathlib/CategoryTheory/Triangulated/Functor.lean

added def CategoryTheory.Functor.mapTriangleCompIso

added def CategoryTheory.Functor.mapTriangleIso