mathlib documentation

category_theory.generator

Separating and detecting sets #

There are several non-equivalent notions of a generator of a category. Here, we consider two of them:

There are, of course, also the dual notions of coseparating and codetecting sets.

Main results #

We

Future work #

def category_theory.is_separating {C : Type u₁} [category_theory.category C] (𝒒 : set C) :
Prop

We say that 𝒒 is a separating set if the functors C(G, -) for G ∈ 𝒒 are collectively faithful, i.e., if h ≫ f = h ≫ g for all h with domain in 𝒒 implies f = g.

Equations
def category_theory.is_coseparating {C : Type u₁} [category_theory.category C] (𝒒 : set C) :
Prop

We say that 𝒒 is a coseparating set if the functors C(-, G) for G ∈ 𝒒 are collectively faithful, i.e., if f ≫ h = g ≫ h for all h with codomain in 𝒒 implies f = g.

Equations
def category_theory.is_detecting {C : Type u₁} [category_theory.category C] (𝒒 : set C) :
Prop

We say that 𝒒 is a detecting set if the functors C(G, -) collectively reflect isomorphisms, i.e., if any h with domain in 𝒒 uniquely factors through f, then f is an isomorphism.

Equations
def category_theory.is_codetecting {C : Type u₁} [category_theory.category C] (𝒒 : set C) :
Prop

We say that 𝒒 is a codetecting set if the functors C(-, G) collectively reflect isomorphisms, i.e., if any h with codomain in G uniquely factors through f, then f is an isomorphism.

Equations
theorem category_theory.is_separating.mono {C : Type u₁} [category_theory.category C] {𝒒 : set C} (h𝒒 : category_theory.is_separating 𝒒) {β„‹ : set C} (h𝒒ℋ : 𝒒 βŠ† β„‹) :
theorem category_theory.is_coseparating.mono {C : Type u₁} [category_theory.category C] {𝒒 : set C} (h𝒒 : category_theory.is_coseparating 𝒒) {β„‹ : set C} (h𝒒ℋ : 𝒒 βŠ† β„‹) :
theorem category_theory.is_detecting.mono {C : Type u₁} [category_theory.category C] {𝒒 : set C} (h𝒒 : category_theory.is_detecting 𝒒) {β„‹ : set C} (h𝒒ℋ : 𝒒 βŠ† β„‹) :
theorem category_theory.is_codetecting.mono {C : Type u₁} [category_theory.category C] {𝒒 : set C} (h𝒒 : category_theory.is_codetecting 𝒒) {β„‹ : set C} (h𝒒ℋ : 𝒒 βŠ† β„‹) :

An ingredient of the proof of the Special Adjoint Functor Theorem: a complete well-powered category with a small coseparating set has an initial object.

In fact, it follows from the Special Adjoint Functor Theorem that C is already cocomplete.

An ingredient of the proof of the Special Adjoint Functor Theorem: a cocomplete well-copowered category with a small separating set has a terminal object.

In fact, it follows from the Special Adjoint Functor Theorem that C is already complete.

theorem category_theory.subobject.eq_of_le_of_is_detecting {C : Type u₁} [category_theory.category C] {𝒒 : set C} (h𝒒 : category_theory.is_detecting 𝒒) {X : C} (P Q : category_theory.subobject X) (h₁ : P ≀ Q) (hβ‚‚ : βˆ€ (G : C), G ∈ 𝒒 β†’ βˆ€ {f : G ⟢ X}, Q.factors f β†’ P.factors f) :
P = Q
theorem category_theory.subobject.inf_eq_of_is_detecting {C : Type u₁} [category_theory.category C] [category_theory.limits.has_pullbacks C] {𝒒 : set C} (h𝒒 : category_theory.is_detecting 𝒒) {X : C} (P Q : category_theory.subobject X) (h : βˆ€ (G : C), G ∈ 𝒒 β†’ βˆ€ {f : G ⟢ X}, P.factors f β†’ Q.factors f) :
P βŠ“ Q = P
theorem category_theory.subobject.eq_of_is_detecting {C : Type u₁} [category_theory.category C] [category_theory.limits.has_pullbacks C] {𝒒 : set C} (h𝒒 : category_theory.is_detecting 𝒒) {X : C} (P Q : category_theory.subobject X) (h : βˆ€ (G : C), G ∈ 𝒒 β†’ βˆ€ {f : G ⟢ X}, P.factors f ↔ Q.factors f) :
P = Q

A category with pullbacks and a small detecting set is well-powered.

def category_theory.is_separator {C : Type u₁} [category_theory.category C] (G : C) :
Prop

We say that G is a separator if the functor C(G, -) is faithful.

Equations
def category_theory.is_coseparator {C : Type u₁} [category_theory.category C] (G : C) :
Prop

We say that G is a coseparator if the functor C(-, G) is faithful.

Equations
def category_theory.is_detector {C : Type u₁} [category_theory.category C] (G : C) :
Prop

We say that G is a detector if the functor C(G, -) reflects isomorphisms.

Equations
def category_theory.is_codetector {C : Type u₁} [category_theory.category C] (G : C) :
Prop

We say that G is a codetector if the functor C(-, G) reflects isomorphisms.

Equations
theorem category_theory.is_separator_def {C : Type u₁} [category_theory.category C] (G : C) :
category_theory.is_separator G ↔ βˆ€ ⦃X Y : C⦄ (f g : X ⟢ Y), (βˆ€ (h : G ⟢ X), h ≫ f = h ≫ g) β†’ f = g
theorem category_theory.is_separator.def {C : Type u₁} [category_theory.category C] {G : C} :
category_theory.is_separator G β†’ βˆ€ ⦃X Y : C⦄ (f g : X ⟢ Y), (βˆ€ (h : G ⟢ X), h ≫ f = h ≫ g) β†’ f = g
theorem category_theory.is_coseparator_def {C : Type u₁} [category_theory.category C] (G : C) :
category_theory.is_coseparator G ↔ βˆ€ ⦃X Y : C⦄ (f g : X ⟢ Y), (βˆ€ (h : Y ⟢ G), f ≫ h = g ≫ h) β†’ f = g
theorem category_theory.is_coseparator.def {C : Type u₁} [category_theory.category C] {G : C} :
category_theory.is_coseparator G β†’ βˆ€ ⦃X Y : C⦄ (f g : X ⟢ Y), (βˆ€ (h : Y ⟢ G), f ≫ h = g ≫ h) β†’ f = g
theorem category_theory.is_detector_def {C : Type u₁} [category_theory.category C] (G : C) :
category_theory.is_detector G ↔ βˆ€ ⦃X Y : C⦄ (f : X ⟢ Y), (βˆ€ (h : G ⟢ Y), βˆƒ! (h' : G ⟢ X), h' ≫ f = h) β†’ category_theory.is_iso f
theorem category_theory.is_detector.def {C : Type u₁} [category_theory.category C] {G : C} :
category_theory.is_detector G β†’ βˆ€ ⦃X Y : C⦄ (f : X ⟢ Y), (βˆ€ (h : G ⟢ Y), βˆƒ! (h' : G ⟢ X), h' ≫ f = h) β†’ category_theory.is_iso f
theorem category_theory.is_codetector_def {C : Type u₁} [category_theory.category C] (G : C) :
category_theory.is_codetector G ↔ βˆ€ ⦃X Y : C⦄ (f : X ⟢ Y), (βˆ€ (h : X ⟢ G), βˆƒ! (h' : Y ⟢ G), f ≫ h' = h) β†’ category_theory.is_iso f
theorem category_theory.is_codetector.def {C : Type u₁} [category_theory.category C] {G : C} :
category_theory.is_codetector G β†’ βˆ€ ⦃X Y : C⦄ (f : X ⟢ Y), (βˆ€ (h : X ⟢ G), βˆƒ! (h' : Y ⟢ G), f ≫ h' = h) β†’ category_theory.is_iso f