English
The hom component of the shiftFunctorCompIsoId_hom_app expresses how a morphism f is transported along two consecutive shifts with the appropriate isomorphisms.
Русский
Гом-компонента shiftFunctorCompIsoId_hom_app описывает, как морфизм f переносится сквозь два последовательных сдвига через соответствующие изоморфизмы.
LaTeX
$$$ ((\\mathrm{shiftFunctorCompIsoId} \\ C n m h).hom.app X)\\langle n \\rangle' = (\\mathrm{shiftFunctorCompIsoId} \\ C m n (..)).hom.app (X⟦n⟧) $$$
Lean4
theorem shift_shiftFunctorCompIsoId_hom_app (n m : A) (h : n + m = 0) (X : C) :
((shiftFunctorCompIsoId C n m h).hom.app X)⟦n⟧' =
(shiftFunctorCompIsoId C m n (by rw [← neg_eq_of_add_eq_zero_left h, add_neg_cancel])).hom.app (X⟦n⟧) :=
by
dsimp [shiftFunctorCompIsoId]
simpa only [Functor.map_comp, ← shiftFunctorAdd'_zero_add_inv_app n X, ← shiftFunctorAdd'_add_zero_inv_app n X] using
shiftFunctorAdd'_assoc_inv_app n m n 0 0 n h (by rw [← neg_eq_of_add_eq_zero_left h, add_neg_cancel])
(by rw [h, zero_add]) X
