English
A more explicit shift compatibility formula for a and n, giving an exact expression for equiv of f.shift n a' h in terms of base equiv and shift isos.
Русский
Более явная формула совместимости сдвига для a и n, дающая точное выражение для эквивалентности f.shift n a' h через базовую эквивалентность и изоморфизмы сдвига.
LaTeX
$$$\mathrm{equiv}\,W\,L( f.\mathrm{shift}\ n\ a'\ h) = (L.commShiftIso\ n).hom.app X \circ (\mathrm{equiv}\,W\,L f)^{\langle n \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') :
SmallHom.equiv W L (f.shift n a' h) =
(L.commShiftIso n).hom.app X ≫
(SmallHom.equiv W L f)⟦n⟧' ≫
((L.commShiftIso a).hom.app Y)⟦n⟧' ≫
(shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) ≫ (L.commShiftIso a').inv.app Y :=
by
simp only [shift, SmallHom.equiv_comp, SmallHom.equiv_shift, SmallHom.equiv_mk, assoc, L.commShiftIso_add' h,
Functor.CommShift.isoAdd'_inv_app, Iso.inv_hom_id_app_assoc, ← Functor.map_comp_assoc, Iso.hom_inv_id_app,
Functor.comp_obj, comp_id]
