mathlib3 documentation


Separators in preadditive categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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