mathlib documentation

category_theory.preadditive.generator

Separators in preadditive categories #

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

source
theorem category_theory.preadditive.is_separating_iff {C : Type u} [category_theory.category C] [category_theory.preadditive C] (š’¢ : set C) :
category_theory.is_separating š’¢ ā†” āˆ€ ā¦ƒX Y : Cā¦„ (f : X āŸ¶ Y), (āˆ€ (G : C), G āˆˆ š’¢ ā†’ āˆ€ (h : G āŸ¶ X), h ā‰« f = 0) ā†’ f = 0
source
theorem category_theory.preadditive.is_coseparating_iff {C : Type u} [category_theory.category C] [category_theory.preadditive C] (š’¢ : set C) :
category_theory.is_coseparating š’¢ ā†” āˆ€ ā¦ƒX Y : Cā¦„ (f : X āŸ¶ Y), (āˆ€ (G : C), G āˆˆ š’¢ ā†’ āˆ€ (h : Y āŸ¶ G), f ā‰« h = 0) ā†’ f = 0
source
theorem category_theory.preadditive.is_separator_iff {C : Type u} [category_theory.category C] [category_theory.preadditive C] (G : C) :
category_theory.is_separator G ā†” āˆ€ ā¦ƒX Y : Cā¦„ (f : X āŸ¶ Y), (āˆ€ (h : G āŸ¶ X), h ā‰« f = 0) ā†’ f = 0
source
theorem category_theory.preadditive.is_coseparator_iff {C : Type u} [category_theory.category C] [category_theory.preadditive C] (G : C) :
category_theory.is_coseparator G ā†” āˆ€ ā¦ƒX Y : Cā¦„ (f : X āŸ¶ Y), (āˆ€ (h : Y āŸ¶ G), f ā‰« h = 0) ā†’ f = 0
source
theorem category_theory.is_separator_iff_faithful_preadditive_coyoneda {C : Type u} [category_theory.category C] [category_theory.preadditive C] (G : C) :
category_theory.is_separator G ā†” category_theory.faithful (category_theory.preadditive_coyoneda.obj (opposite.op G))
source
theorem category_theory.is_separator_iff_faithful_preadditive_coyoneda_obj {C : Type u} [category_theory.category C] [category_theory.preadditive C] (G : C) :
category_theory.is_separator G ā†” category_theory.faithful (category_theory.preadditive_coyoneda_obj (opposite.op G))
source
theorem category_theory.is_coseparator_iff_faithful_preadditive_yoneda {C : Type u} [category_theory.category C] [category_theory.preadditive C] (G : C) :
category_theory.is_coseparator G ā†” category_theory.faithful (category_theory.preadditive_yoneda.obj G)
source
theorem category_theory.is_coseparator_iff_faithful_preadditive_yoneda_obj {C : Type u} [category_theory.category C] [category_theory.preadditive C] (G : C) :
category_theory.is_coseparator G ā†” category_theory.faithful (category_theory.preadditive_yoneda_obj G)