Commit 2023-09-04 15:04 80b90ea7

View on Github →

feat: the induced shift on the target category of a functor (#6652) When a functor F : C ⥤ D satisfies a suitable condition, this PR constructs a shift on the category D from a shift on the category C.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Shift/Induced.lean

added def CategoryTheory.Functor.CommShift.ofInduced

added theorem CategoryTheory.Functor.commShiftIso_eq_ofInduced

added theorem CategoryTheory.HasShift.Induced.add_hom_app_obj

added theorem CategoryTheory.HasShift.Induced.add_inv_app_obj

added theorem CategoryTheory.HasShift.Induced.zero_hom_app_obj

added theorem CategoryTheory.HasShift.Induced.zero_inv_app_obj

added theorem CategoryTheory.shiftFunctorAdd_hom_app_obj_of_induced

added theorem CategoryTheory.shiftFunctorAdd_inv_app_obj_of_induced

added theorem CategoryTheory.shiftFunctorZero_hom_app_obj_of_induced

added theorem CategoryTheory.shiftFunctorZero_inv_app_obj_of_induced

added theorem CategoryTheory.shiftFunctor_of_induced