English
Let C be a category with shifts indexed by integers. For any X in the opposite category Cᵒᵖ, the hom-component of the zero-shift functor at X factors through the isomorphism shiftFunctorOpIso(C,0,0,0) and the inverse of the zero-shift functor on X.unop, via the opposite.
Русский
Пусть C — категория с переходами по целым числам. Для любого X в противоположной категории C^{op} гом-компонента нулевого сдвига через X распадается через изоморфизм shiftFunctorOpIso(C,0,0,0) и обратный к нулевому сдвигу на X.unop, через противоположность.
LaTeX
$$$ (\\text{shiftFunctorZero}\\; C^{op}\\; \\mathbb{Z}).\\mathrm{hom}.\\mathrm{app}\\; X = (\\text{shiftFunctorOpIso } C\\;0\\;0\\;(\\text{zero\\_add }0)).\\mathrm{hom}.\\mathrm{app}\\; X \\; \\ggg\\; ((\\text{shiftFunctorZero } C\\; \\mathbb{Z}).\\mathrm{inv}.\\mathrm{app}\\; X^{unop}).\\mathrm{op} $$$
Lean4
theorem shiftFunctorZero_op_hom_app (X : Cᵒᵖ) :
(shiftFunctorZero Cᵒᵖ ℤ).hom.app X =
(shiftFunctorOpIso C 0 0 (zero_add 0)).hom.app X ≫ ((shiftFunctorZero C ℤ).inv.app X.unop).op :=
rfl
