English
In the same setting, the inv-component of the zero-shift functor on X (X ∈ Cᵒᵖ) is given by the op of the inverse of the hom-component of the zero-shift functor on X.unop composed with the appropriate iso inv, i.e. (shiftFunctorZero Cᵒᵖ ℤ).inv.app X = ((shiftFunctorZero C ℤ).hom.app X.unop).op ≫ (shiftFunctorOpIso C 0 0 (zero_add 0)).inv.app X.
Русский
В той же постановке компонент инверсия нулевого сдвига: (shiftFunctorZero Cᵒᵖ ℤ).inv.app X = ((shiftFunctorZero C ℤ).hom.app X.unop).op \\gg (shiftFunctorOpIso C 0 0 (zero_add 0)).inv.app X.
LaTeX
$$$ (\\text{shiftFunctorZero } C^{op} \\mathbb{Z}).inv.app X = ((\\text{shiftFunctorZero } C \\mathbb{Z}).hom.app X^{unop}).op \\gg (\\text{shiftFunctorOpIso } C 0 0 (0)).inv.app X $$$
Lean4
theorem shiftFunctorZero_op_inv_app (X : Cᵒᵖ) :
(shiftFunctorZero Cᵒᵖ ℤ).inv.app X =
((shiftFunctorZero C ℤ).hom.app X.unop).op ≫ (shiftFunctorOpIso C 0 0 (zero_add 0)).inv.app X :=
by
rw [← cancel_epi ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X), Iso.hom_inv_id_app, shiftFunctorZero_op_hom_app, assoc, ←
op_comp_assoc, Iso.hom_inv_id_app, op_id, id_comp, Iso.hom_inv_id_app]
