Separators in preadditive categories

This file contains characterizations of separating sets and objects that are valid in all preadditive categories.

theorem CategoryTheory.Preadditive.isSeparating_iff {C : Type u} [Category.{v, u} C] [Preadditive C] (P : ObjectProperty C) : P.IsSeparating ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C), P G → ∀ (h : G ⟶ X), CategoryStruct.comp h f = 0) → f = 0

theorem CategoryTheory.Preadditive.isCoseparating_iff {C : Type u} [Category.{v, u} C] [Preadditive C] (P : ObjectProperty C) : P.IsCoseparating ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C), P G → ∀ (h : Y ⟶ G), CategoryStruct.comp f h = 0) → f = 0

theorem CategoryTheory.Preadditive.isSeparator_iff {C : Type u} [Category.{v, u} C] [Preadditive C] (G : C) : IsSeparator G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ X), CategoryStruct.comp h f = 0) → f = 0

theorem CategoryTheory.Preadditive.isCoseparator_iff {C : Type u} [Category.{v, u} C] [Preadditive C] (G : C) : IsCoseparator G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : Y ⟶ G), CategoryStruct.comp f h = 0) → f = 0

theorem CategoryTheory.isSeparator_iff_faithful_preadditiveCoyoneda {C : Type u} [Category.{v, u} C] [Preadditive C] (G : C) : IsSeparator G ↔ (preadditiveCoyoneda.obj (Opposite.op G)).Faithful

theorem CategoryTheory.isSeparator_iff_faithful_preadditiveCoyonedaObj {C : Type u} [Category.{v, u} C] [Preadditive C] (G : C) : IsSeparator G ↔ (preadditiveCoyonedaObj G).Faithful

theorem CategoryTheory.isCoseparator_iff_faithful_preadditiveYoneda {C : Type u} [Category.{v, u} C] [Preadditive C] (G : C) : IsCoseparator G ↔ (preadditiveYoneda.obj G).Faithful

theorem CategoryTheory.isCoseparator_iff_faithful_preadditiveYonedaObj {C : Type u} [Category.{v, u} C] [Preadditive C] (G : C) : IsCoseparator G ↔ (preadditiveYonedaObj G).Faithful