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.Functor.Faithful (CategoryTheory.preadditiveCoyoneda.obj (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.Functor.Faithful (CategoryTheory.preadditiveYoneda.obj G)