projective_of_preservesFiniteColimits_preadditiveCoyonedaObj

English

An object P is projective iff its preadditive Co-Yoneda functor preserves finite colimits.

Русский

Объект P проектен тогда и только тогда, когда его преддобавительный функтор Coyoneda сохраняет конечные колимиты.

LaTeX

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

Lean4

/-- An object is projective if its preadditive Co-Yoneda functor preserves finite colimits. -/
theorem projective_of_preservesFiniteColimits_preadditiveCoyonedaObj (P : C)
    [hP : PreservesFiniteColimits (preadditiveCoyonedaObj P)] : Projective P :=
  by
  rw [projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj]
  have := Functor.preservesHomologyOfExact (preadditiveCoyonedaObj P)
  infer_instance

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