Commit 2024-06-03 18:57 d6ea8fe0

feat(CategoryTheory/Shift): functors from a category to a category with a shift (#12607) Given a category C, and a category D equipped with a shift by a monoid A, we define a structure SingleFunctors C D A which contains the data of functors functor a : C ⥤ D for all a : A and isomorphisms shiftIso n a a' h : functor a' ⋙ shiftFunctor D n ≅ functor a whenever n + a = a'. These isomorphisms should satisfy certain compatibilities with respect to the shift on D.