instHasSmallLocalizedHomObjShiftFunctor

English

For every m in M, there exists a SmallLocalizedHom W X (Y⟦m⟧), i.e., shifting the target yields a valid small localized hom.

Русский

Для каждого m из M существует SmallLocalizedHom W X (Y⟦m⟧), то есть сдвиг целевого объекта образует допустимый малый локализованный гомоморф.

LaTeX

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

Lean4

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

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