English
The map of φ under shiftFunctor on Opposite category is given by a standard naturality of the shift iso, i.e., the shift functor on the opposite category decomposes through the iso hom and inv components with the opposite of φ\, unop.
Русский
Перенос отображения φ через shiftFunctor на Opposite распадается через естественность изоморфизма сдвига, то есть сдвиг на противоположной стороне распадается через гом и инв компоненты с противоположным φ, unop.
LaTeX
$$$ (\\text{shiftFunctor } C^{op} n).\\mathrm{map} \\\\; \\phi = (\\text{shiftFunctorOpIso } C n m h) .\\mathrm{hom.app} K \\\\; \\gg ((\\text{shiftFunctor } C m).map \\phi.unop).op \\\\; \\gg (\\text{shiftFunctorOpIso } C n m h).inv.app L $$$
Lean4
theorem shiftFunctor_op_map (n m : ℤ) (hnm : n + m = 0) {K L : Cᵒᵖ} (φ : K ⟶ L) :
(shiftFunctor Cᵒᵖ n).map φ =
(shiftFunctorOpIso C n m hnm).hom.app K ≫
((shiftFunctor C m).map φ.unop).op ≫ (shiftFunctorOpIso C n m hnm).inv.app L :=
(NatIso.naturality_2 (shiftFunctorOpIso C n m hnm) φ).symm
