English
For a fixed n in A, the hom component of the zero-shift functor interacts with shifting by n via a specified composition with the shift-commutation isomorphism.
Русский
Для фиксированного n ∈ A гом-часть нулевого сдвигового функторa взаимодействует с сдвигом на n через заданную композицию с изоморфизмами коммутативности сдвигов.
LaTeX
$$$ (shiftFunctorZero C A).hom.app (X⟦n⟧) = (shiftFunctorComm C n 0).hom.app X ≫ ((shiftFunctorZero C A).inv.app X)⟦n⟧' $$$
Lean4
theorem shiftFunctorZero_hom_app_shift (n : A) :
(shiftFunctorZero C A).hom.app (X⟦n⟧) =
(shiftFunctorComm C n 0).hom.app X ≫ ((shiftFunctorZero C A).hom.app X)⟦n⟧' :=
by
rw [← shiftFunctorAdd'_zero_add_inv_app n X, shiftFunctorComm_eq C n 0 n (add_zero n)]
dsimp
rw [Category.assoc, Iso.hom_inv_id_app, Category.comp_id, shiftFunctorAdd'_add_zero_inv_app]
