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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (𝒢 : Set C) : CategoryTheory.IsSeparating 𝒢 ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : G ⟶ X), CategoryTheory.CategoryStruct.comp h f = 0) → f = 0

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

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

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

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

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

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

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