instHasSmallLocalizedHomObjShiftFunctor_1

English

For a morphism property W and a monoid M, for any objects X, Y ∈ C there is a HasSmallLocalizedShiftedHom W M X Y; i.e., shifting X by m yields a localized hom to Y.

Русский

Для свойства морфизмов W и моноида M для любых объектов X, Y ∈ C существует локализованный малый сдвинутый гомоморфизм между X⟨m⟩ и Y.

LaTeX

$$$\forall m \in M,\ HasSmallLocalizedHom\, W\ (X ⟦m⟧)\ Y$$$

Lean4

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

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