English
For objects in the shifted category, the opEquiv' of a + b is the appropriate composite of opEquiv' of a and opEquiv' of b with the shift functors and associator as per the additive law.
Русский
Для элементов в категории со сдвигами, opEquiv' при a' = a + b распадается на композицию opEquiv' при a и b совместно со сдвигами и ассоциатором.
LaTeX
$$$$ opEquiv' (n+m) a a'' (hnm) = isoWhiskerLeft \\_ (shiftFunctorAdd' D m n mn hnm) \\llcorner \\cdot (Functor.associator \\_\\_\\_).symm \\llcorner (isoWhiskerRight (F.shiftIso m a' a'' ha') _) \\llcorner F.shiftIso n a a' ha' $$$$
Lean4
theorem opEquiv'_add_symm (n m a a' a'' : ℤ) (ha' : n + a = a') (ha'' : m + a' = a'')
(x : (Opposite.op (Y⟦a⟧) ⟶ (Opposite.op X)⟦m + n⟧)) :
(opEquiv' (m + n) a a'' (by cutsat)).symm x =
(opEquiv' m a' a'' ha'').symm ((opEquiv' n a a' ha').symm (x ≫ (shiftFunctorAdd Cᵒᵖ m n).hom.app _)).op :=
by
simp only [opEquiv'_symm_apply, opEquiv_symm_apply,
opShiftFunctorEquivalence_unitIso_inv_app_eq _ _ _ _ (add_comm n m)]
dsimp
simp only [assoc, Functor.map_comp, ← shiftFunctorAdd'_eq_shiftFunctorAdd, ← NatTrans.naturality_assoc,
shiftFunctorAdd'_assoc_inv_app a n m a' (m + n) a'' (by cutsat) (by cutsat) (by cutsat)]
rfl
