mathlib3 documentation

category_theory.preadditive.generator

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

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

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

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

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)

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)