English
A general shift compatibility formula for f, expressed via equiv_shift, combining shift isomorphisms with SmallHom equivalence.
Русский
Общая формула совместимости сдвига через equiv_shift, объединяющая изоморфизмы сдвига и эквивалентность SmallHom.
LaTeX
$$$\text{equiv}_W L\big( f.\mathrm{shift}\ a' h\big) = (L.commShiftIso a).hom.app X \circ (\mathrm{equiv}\,W\,L f)^{\langle a \rangle} \circ (L.commShiftIso a).inv.app Y$$$
Lean4
theorem equiv_shift {a : M} [HasSmallLocalizedShiftedHom.{w} W M X Y] [HasSmallLocalizedShiftedHom.{w} W M Y Y]
(f : SmallShiftedHom.{w} W X Y a) (n a' : M) (h : a + n = a') :
equiv W L (f.shift n a' h) =
(L.commShiftIso n).hom.app X ≫ (equiv W L f)⟦n⟧' ≫ (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) :=
by
dsimp [equiv]
erw [Iso.homToEquiv_apply, Iso.homToEquiv_apply, equiv_shift']
simp only [Functor.comp_obj, Iso.app_hom, assoc, Iso.inv_hom_id_app, comp_id, Functor.map_comp]
rfl
