preservesFiniteColimits_preadditiveYonedaObj_of_injective

English

The preadditive Yoneda functor on J preserves finite colimits if J is injective.

Русский

Предобеденный Yoneda-функтор на J сохраняет конечные колимиты, если J инъективен.

LaTeX

$$$\mathrm{PreservesFiniteColimits}(\mathrm{preadditiveYonedaObj}(J))$$$

Lean4

/-- The preadditive Yoneda functor on `J` preserves colimits if `J` is injective. -/
instance preservesFiniteColimits_preadditiveYonedaObj_of_injective (J : C) [hP : Injective J] :
    PreservesFiniteColimits (preadditiveYonedaObj J) := by apply Functor.preservesFiniteColimits_of_preservesHomology

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