English
The hom component of the shiftFunctorAdd' is expressed as a composition of the corresponding Add' morphisms and the isomorphism shiftFunctorCompIsoId.
Русский
Гом-компонента shiftFunctorAdd' выражается через композицию соответствующих морфизмов Add' и изоморфизм shiftFunctorCompIsoId.
LaTeX
$$$ (\\mathrm{shiftFunctorAdd'} \\ C p' p hp).hom.app X = (\\mathrm{shiftFunctorAdd'} \\ C n' m' p' (..)).hom.app X \\langle p \\rangle' \\\\gg (\\mathrm{shiftFunctorAdd'} \\ C m n p h).hom.app (X⟦n'⟧⟦m'⟧) \\\\gg (\\mathrm{shiftFunctorCompIsoId} \\ C m' m hm).hom.app (X⟦n'⟧)⟦n⟧' \\\\gg (\\mathrm{shiftFunctorCompIsoId} \\ C n' n hn).hom.app X $$$
Lean4
theorem shiftFunctorCompIsoId_add'_hom_app :
(shiftFunctorCompIsoId C p' p hp).hom.app X =
((shiftFunctorAdd' C n' m' p'
(by rw [← add_left_inj p, hp, ← h, add_assoc, ← add_assoc m', hm, zero_add, hn])).hom.app
X)⟦p⟧' ≫
(shiftFunctorAdd' C m n p h).hom.app (X⟦n'⟧⟦m'⟧) ≫
(shiftFunctorCompIsoId C m' m hm).hom.app (X⟦n'⟧)⟦n⟧' ≫ (shiftFunctorCompIsoId C n' n hn).hom.app X :=
by
rw [← cancel_mono ((shiftFunctorCompIsoId C p' p hp).inv.app X), Iso.hom_inv_id_app,
shiftFunctorCompIsoId_add'_inv_app m n p m' n' p' hm hn hp h, Category.assoc, Category.assoc, Category.assoc,
Iso.hom_inv_id_app_assoc, ← Functor.map_comp_assoc, Iso.hom_inv_id_app]
dsimp
rw [Functor.map_id, Category.id_comp, Iso.hom_inv_id_app_assoc, ← Functor.map_comp, Iso.hom_inv_id_app,
Functor.map_id]
