Projective objects in abelian categories #
In an abelian category, an object P is projective iff the functor
preadditiveCoyonedaObj (op P) preserves finite colimits.
noncomputable def
CategoryTheory.preservesFiniteColimitsPreadditiveCoyonedaObjOfProjective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
(P : C)
[hP : CategoryTheory.Projective P]
:
The preadditive Co-Yoneda functor on P preserves finite colimits if P is projective.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.projective_of_preservesFiniteColimits_preadditiveCoyonedaObj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
(P : C)
[hP : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveCoyonedaObj (Opposite.op P))]
:
An object is projective if its preadditive Co-Yoneda functor preserves finite colimits.