# mathlibdocumentation

category_theory.abelian.generator

# 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 #

theorem category_theory.abelian.has_injective_coseparator {C : Type u} (G : C) (hG : category_theory.is_separator G) :
∃ (G : C),
theorem category_theory.abelian.has_projective_separator {C : Type u} (G : C)  :
∃ (G : C),