English
The inverse of the shift-equivariant bijection between ShiftedHom X Y n and ShiftedHom (op Y) (op X) n sends a morphism f to a morphism from X to Y of degree n with a prescribed unop form; more precisely, opEquiv.symm_apply describes this transformation.
Русский
Обратное отображение биекции между ShiftedHom X Y n и ShiftedHom (op Y) (op X) n переводит морфизм f в морфизм из X в Y степени n с заданной формой через развёртывание противоположного.
LaTeX
$$$\\text{opEquiv}(n)^{-1}(f) = \\text{explicit formula in terms of } f,$$$
Lean4
/-- The bijection `ShiftedHom X Y n ≃ ShiftedHom (Opposite.op Y) (Opposite.op X) n` when
`n : ℤ`, and `X` and `Y` are objects of a category equipped with a shift by `ℤ`. -/
noncomputable def opEquiv (n : ℤ) : ShiftedHom X Y n ≃ ShiftedHom (Opposite.op Y) (Opposite.op X) n :=
Quiver.Hom.opEquiv.trans ((opShiftFunctorEquivalence C n).symm.toAdjunction.homEquiv (Opposite.op Y) (Opposite.op X))
