English
When the shift parameter m0 is zero, mk₀_W m0 is mapped to ShiftedHom.mk₀ m0 with L.map f, showing compatibility with the base functor.
Русский
При m0 = 0 отображение mk₀_W m0 переходит к ShiftedHom.mk₀ m0 через L.map, демонстрируя совместимость с базовым функтором.
LaTeX
$$$\mathrm{equiv}\,W\,L\big(\mathrm{SmallShiftedHom.mk₀}\,W\,m_0\,\mathrm{hm}_0\,f\big) = \mathrm{ShiftedHom.mk₀}\,m_0\,\mathrm{hm}_0\,(L.map f)$$$
Lean4
/-- The bijection `SmallShiftedHom.{w} W X Y m ≃ ShiftedHom (L.obj X) (L.obj Y) m`
for all `m : M`, and `X` and `Y` in `C` when `L : C ⥤ D` is a localization functor for
`W : MorphismProperty C` such that the category `D` is equipped with a shift by `M`
and `L` commutes with the shifts. -/
noncomputable def equiv [HasSmallLocalizedShiftedHom.{w} W M X Y] {m : M} :
SmallShiftedHom.{w} W X Y m ≃ ShiftedHom (L.obj X) (L.obj Y) m :=
(SmallHom.equiv W L).trans ((L.commShiftIso m).app Y).homToEquiv
