Commit 2023-12-26 12:09 9d8e41e6

View on Github →

feat(CategoryTheory/Triangulated): Functor.mapTriangle commutes with the shift (#9073) If F : C ⥤ D is an additive functor which commutes with a shift by , then F.mapTriangle : Triangle C ⥤ Triangle D also commutes with the shift.

Estimated changes