A complete abelian category with enough injectives and a separator has an injective coseparator #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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}
[category_theory.category C]
[category_theory.abelian C]
[category_theory.limits.has_limits C]
[category_theory.enough_injectives C]
(G : C)
(hG : category_theory.is_separator G) :
∃ (G : C), category_theory.injective G ∧ category_theory.is_coseparator G
theorem
category_theory.abelian.has_projective_separator
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
[category_theory.limits.has_colimits C]
[category_theory.enough_projectives C]
(G : C)
(hG : category_theory.is_coseparator G) :
∃ (G : C), category_theory.projective G ∧ category_theory.is_separator G