instHasSmallLocalizedHomObjShiftFunctor_2

English

There is a family of localized homs for all shifts, namely HasSmallLocalizedHom W X (Y⟦m⟧) for any m in M.

Русский

Существует семейство локализованных гомоморфизмов для всех сдвигов: HasSmallLocalizedHom W X (Y⟦m⟧) для любого m в M.

LaTeX

$$$ \forall X,Y,m:\, HasSmallLocalizedHom\,W\,X\,(Y\langle m \rangle) $$$

Lean4

instance (m m' n : M) : HasSmallLocalizedHom.{w} W (X⟦m⟧⟦m'⟧) (Y⟦n⟧) :=
  (hasSmallLocalizedHom_iff_of_isos W ((shiftFunctorAdd C m m').app X) (Iso.refl (Y⟦n⟧))).1 inferInstance

Похожие утверждения