A complete abelian category with enough injectives and a separator has an injective coseparator

Future work

• Once we know that Grothendieck categories have enough injectives, we can use this to conclude that Grothendieck categories have an injective coseparator.

References

• [Peter J Freyd, Abelian Categories (Theorem 3.37)][freyd1964abelian]

theorem CategoryTheory.Abelian.has_injective_coseparator {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.EnoughInjectives C] (G : C) (hG : CategoryTheory.IsSeparator G) : ∃ (G : C), CategoryTheory.Injective G ∧ CategoryTheory.IsCoseparator G

theorem CategoryTheory.Abelian.has_projective_separator {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.EnoughProjectives C] (G : C) (hG : CategoryTheory.IsCoseparator G) : ∃ (G : C), CategoryTheory.Projective G ∧ CategoryTheory.IsSeparator G