Documentation

Mathlib.CategoryTheory.Preadditive.Generator

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