mathlib3

ef51d232 - feat(category_theory/shift): restricting shift functors to a subcategory (#13265)

feat(category_theory/shift): restricting shift functors to a subcategory (#13265) Given a family of endomorphisms of `C` which are interwined by a fully faithful `F : C ⥤ D` with shift functors on `D`, we can promote that family to shift functors on `C`. For LTE. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>