Lean4
/-- When the target category of a functor `F : C ⥤ D` is equipped with
the induced shift, this is the compatibility of `F` with the shifts on
the categories `C` and `D`. -/
noncomputable def ofInduced :
letI := HasShift.induced F A s i
F.CommShift A :=
by
letI := HasShift.induced F A s i
exact
{ iso := fun a => (i a).symm
zero := by
ext X
dsimp
simp only [isoZero_hom_app, shiftFunctorZero_inv_app_obj_of_induced, ← F.map_comp_assoc, Iso.hom_inv_id_app,
F.map_id, Category.id_comp]
add := fun a b => by
ext X
dsimp
simp only [isoAdd_hom_app, Iso.symm_hom, shiftFunctorAdd_inv_app_obj_of_induced, shiftFunctor_of_induced]
erw [← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id, Category.id_comp, Iso.inv_hom_id_app_assoc, ←
F.map_comp_assoc, Iso.hom_inv_id_app, F.map_id, Category.id_comp] }
