English
For X,Y,Z with integers n,m, the symm-comp formula expresses how opEquiv' interacts with composition of shifted morphisms.
Русский
Для X,Y,Z и целых n,m формула симметричного компоновки описывает, как opEquiv' взаимодействует с композицией сдвинутых морфизмов.
LaTeX
$$$$ (opEquiv' n a a' h)^{-1}(f \\circ g) = f \\circ (opEquiv' n a a' h)^{-1} (g) $$$$
Lean4
/-- The bijection `ShiftedHom X Y a' ≃ (Opposite.op (Y⟦a⟧) ⟶ (Opposite.op X)⟦n⟧)`
when integers `n`, `a` and `a'` satisfy `n + a = a'`, and `X` and `Y` are objects
of a category equipped with a shift by `ℤ`. -/
noncomputable def opEquiv' (n a a' : ℤ) (h : n + a = a') :
ShiftedHom X Y a' ≃ (Opposite.op (Y⟦a⟧) ⟶ (Opposite.op X)⟦n⟧) :=
((shiftFunctorAdd' C a n a' (by cutsat)).symm.app Y).homToEquiv.symm.trans (opEquiv n)
