Lean4
/-- Given a family of endomorphisms of `C` which are intertwined by a fully faithful `F : C ⥤ D`
with shift functors on `D`, we can promote that family to shift functors on `C`. -/
def hasShift : HasShift C A :=
hasShiftMk C A
{ F := s
zero := zero hF s i
add := add hF s i
assoc_hom_app := fun m₁ m₂ m₃ X =>
hF.map_injective
(by
have h := shiftFunctorAdd'_assoc_hom_app m₁ m₂ m₃ _ _ (m₁ + m₂ + m₃) rfl rfl rfl (F.obj X)
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd] at h
rw [← cancel_mono ((i m₃).hom.app ((s m₂).obj ((s m₁).obj X)))]
simp only [Functor.comp_obj, Functor.map_comp, map_add_hom_app, Category.assoc, Iso.inv_hom_id_app_assoc,
NatTrans.naturality_assoc, Functor.comp_map, Iso.inv_hom_id_app, Category.comp_id]
erw [(i m₃).hom.naturality]
rw [Functor.comp_map, map_add_hom_app, Functor.map_comp, Functor.map_comp, Iso.inv_hom_id_app_assoc, ←
Functor.map_comp_assoc _ ((i (m₁ + m₂)).inv.app X), Iso.inv_hom_id_app, Functor.map_id, Category.id_comp,
reassoc_of% h, dcongr_arg (fun a => (i a).hom.app X) (add_assoc m₁ m₂ m₃)]
simp [shiftFunctorAdd', eqToHom_map])
zero_add_hom_app := fun n X =>
hF.map_injective
(by
have this := dcongr_arg (fun a => (i a).hom.app X) (zero_add n)
rw [← cancel_mono ((i n).hom.app ((s 0).obj X))]
simp only [comp_obj, map_add_hom_app, this, shiftFunctorAdd_zero_add_hom_app, id_obj, Category.assoc,
eqToHom_trans_assoc, eqToHom_refl, Category.id_comp, Iso.inv_hom_id_app, Category.comp_id, map_comp,
eqToHom_map]
congr 1
erw [(i n).hom.naturality]
simp)
add_zero_hom_app := fun n X =>
hF.map_injective
(by
have := dcongr_arg (fun a => (i a).hom.app X) (add_zero n)
simp [this, ← NatTrans.naturality_assoc, eqToHom_map, shiftFunctorAdd_add_zero_hom_app]) }
