Fullness of restrictions of preadditiveCoyonedaObj #
In this file we give a sufficient criterion for a restriction of the functor
preadditiveCoyonedaObj G to be full: this is the case if C is an abelian category and G : C
is a projective separator such that every object in the relevant subcategory is a quotient of G.
theorem
CategoryTheory.Abelian.preadditiveCoyonedaObj_map_surjective
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{G : C}
[Projective G]
(hG : IsSeparator G)
{X : C}
(p : G ⟶ X)
[Epi p]
{Y : C}
:
theorem
CategoryTheory.Abelian.full_comp_preadditiveCoyonedaObj
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{D : Type u'}
[Category.{v', u'} D]
(F : Functor D C)
[F.Full]
{G : C}
[Projective G]
(hG : IsSeparator G)
(hG₂ : ∀ (X : D), ∃ (p : G ⟶ F.obj X), Epi p)
:
(F.comp (preadditiveCoyonedaObj G)).Full