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.

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
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
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
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