English
In the setting of ShiftSequence.induced with L, F', e', we have the outer iso-zero-hom app relation: (isoZero e M F' e').hom.app (L.obj X) = (e' 0).hom.app X ≫ (isoShiftZero G M).hom.app X ≫ e.inv.app X.
Русский
В рамках индуцированной последовательности сдвигов (ShiftSequence.induced) существует связь для внешнего нулевого изоморфизма: (isoZero e M F' e').hom.app (L.obj X) = (e' 0).hom.app X ≫ (isoShiftZero G M).hom.app X ≫ e.inv.app X.
LaTeX
$$$(\\text{isoZero } e\ M\ F'\\ e').hom.app (L.obj X) = (e' 0).hom.app X \\;\\circ\\; (\\text{isoShiftZero } G M).hom.app X \\;\\circ\\; e.inv.app X$$$
Lean4
@[simp]
theorem shiftFunctorZero_hom_app_obj_of_induced (X : C) :
letI := HasShift.induced F A s i
(shiftFunctorZero D A).hom.app (F.obj X) = (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X) :=
by simp only [ShiftMkCore.shiftFunctorZero_eq, HasShift.Induced.zero_hom_app_obj]
