preservesFiniteColimits_preadditiveCoyonedaObj_of_projective

English

If P is projective, the preadditive Co-Yoneda functor at P preserves finite colimits.

Русский

Если P проективен, функтор Coyoneda на P сохраняет конечные колимиты.

LaTeX

$$$ (\text{preadditiveCoyonedaObj}(P)).\mathrm{PreservesFiniteColimits} $$$

Lean4

/-- The preadditive Co-Yoneda functor on `P` preserves finite colimits if `P` is projective. -/
noncomputable instance preservesFiniteColimits_preadditiveCoyonedaObj_of_projective (P : C) [hP : Projective P] :
    PreservesFiniteColimits (preadditiveCoyonedaObj P) := by apply Functor.preservesFiniteColimits_of_preservesHomology

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