English
When transporting a sum zero identity through a composition of functors with shift structure, the composed hom component is described by transporting via commShiftIso and the iso for the sum.
Русский
При переносе тождества нулевого суммирования через композицию функторов с сдвиговой структурой, гомкомпонент композиции задаётся через перенос через commShiftIso и изоморфизм суммы.
LaTeX
$$$ F.map ((shiftFunctorCompIsoId C a b h).hom.app X) = (F.commShiftIso b).hom.app (X⟦a⟧) ≫ ((F.commShiftIso a).hom.app X)⟦b⟧' ≫ (shiftFunctorCompIsoId D a b h).hom.app (F.obj X) $$$
Lean4
@[simp, reassoc]
theorem map_shiftFunctorCompIsoId_hom_app [F.CommShift A] (X : C) (a b : A) (h : a + b = 0) :
F.map ((shiftFunctorCompIsoId C a b h).hom.app X) =
(F.commShiftIso b).hom.app (X⟦a⟧) ≫
((F.commShiftIso a).hom.app X)⟦b⟧' ≫ (shiftFunctorCompIsoId D a b h).hom.app (F.obj X) :=
by
dsimp [shiftFunctorCompIsoId]
have eq := NatTrans.congr_app (congr_arg Iso.hom (F.commShiftIso_add' h)) X
simp only [commShiftIso_zero, comp_obj, CommShift.isoZero_hom_app, CommShift.isoAdd'_hom_app] at eq
rw [← cancel_epi (F.map ((shiftFunctorAdd' C a b 0 h).hom.app X)), ← reassoc_of% eq, F.map_comp]
simp only [Iso.inv_hom_id_app, id_obj, Category.comp_id, ← F.map_comp_assoc, Iso.hom_inv_id_app, F.map_id,
Category.id_comp]
