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)

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

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