Lean4
/-- When `F : C ⥤ D` is a functor satisfying suitable technical assumptions,
this is the induced term of type `HasShift D A` deduced from `[HasShift C A]`. -/
noncomputable def induced : HasShift D A :=
hasShiftMk D A
{ F := s
zero := Induced.zero F s i
add := Induced.add F s i
zero_add_hom_app := fun n =>
by
suffices
(Induced.add F s i 0 n).hom = eqToHom (by rw [zero_add]; rfl) ≫ whiskerRight (Induced.zero F s i).inv (s n)
by
intro X
simpa using NatTrans.congr_app this X
apply ((whiskeringLeft C D D).obj F).map_injective
ext X
have eq := dcongr_arg (fun a => (i a).hom.app X) (zero_add n)
dsimp
simp only [Induced.add_hom_app_obj, eq, shiftFunctorAdd_zero_add_hom_app, Functor.map_comp, eqToHom_map,
Category.assoc, eqToHom_trans_assoc, eqToHom_refl, Category.id_comp, eqToHom_app, Induced.zero_inv_app_obj]
erw [← NatTrans.naturality_assoc, Iso.hom_inv_id_app_assoc]
rfl
add_zero_hom_app := fun n =>
by
suffices
(Induced.add F s i n 0).hom = eqToHom (by rw [add_zero]; rfl) ≫ whiskerLeft (s n) (Induced.zero F s i).inv
by
intro X
simpa using NatTrans.congr_app this X
apply ((whiskeringLeft C D D).obj F).map_injective
ext X
dsimp
erw [Induced.add_hom_app_obj, dcongr_arg (fun a => (i a).hom.app X) (add_zero n), ←
cancel_mono ((s 0).map ((i n).hom.app X)), Category.assoc, Category.assoc, Category.assoc, Category.assoc,
Category.assoc, Category.assoc, ← (s 0).map_comp, Iso.inv_hom_id_app, Functor.map_id, Category.comp_id, ←
NatTrans.naturality, Induced.zero_inv_app_obj, shiftFunctorAdd_add_zero_hom_app]
simp [eqToHom_map, eqToHom_app]
assoc_hom_app := fun m₁ m₂ m₃ =>
by
suffices
(Induced.add F s i (m₁ + m₂) m₃).hom ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃) =
eqToHom (by rw [add_assoc]) ≫
(Induced.add F s i m₁ (m₂ + m₃)).hom ≫ whiskerLeft (s m₁) (Induced.add F s i m₂ m₃).hom
by
intro X
simpa using NatTrans.congr_app this X
apply ((whiskeringLeft C D D).obj F).map_injective
ext X
dsimp
have eq := F.congr_map (shiftFunctorAdd'_assoc_hom_app m₁ m₂ m₃ _ _ (m₁ + m₂ + m₃) rfl rfl rfl X)
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd] at eq
simp only [Functor.comp_obj, Functor.map_comp, shiftFunctorAdd', Iso.trans_hom, eqToIso.hom, NatTrans.comp_app,
eqToHom_app, Category.assoc] at eq
rw [← cancel_mono ((s m₃).map ((s m₂).map ((i m₁).hom.app X)))]
simp only [Induced.add_hom_app_obj, Category.assoc, Functor.map_comp]
slice_lhs 4 5 => erw [← Functor.map_comp, Iso.inv_hom_id_app, Functor.map_id]
erw [Category.id_comp]
slice_lhs 6 7 => erw [← Functor.map_comp, ← Functor.map_comp, Iso.inv_hom_id_app, (s m₂).map_id, (s m₃).map_id]
erw [Category.comp_id, ← NatTrans.naturality_assoc, reassoc_of% eq,
dcongr_arg (fun a => (i a).hom.app X) (add_assoc m₁ m₂ m₃).symm]
simp only [Functor.comp_obj, eqToHom_map, eqToHom_app, NatTrans.naturality_assoc, Induced.add_hom_app_obj,
Functor.comp_map, Category.assoc, Iso.inv_hom_id_app_assoc, eqToHom_trans_assoc, eqToHom_refl,
Category.id_comp, Category.comp_id, ← Functor.map_comp, Iso.inv_hom_id_app, Functor.map_id] }
