mathlib3 documentation

category_theory.generator

Separating and detecting sets #

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

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, see has_colimits_of_has_limits_of_is_coseparating.

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, see has_limits_of_has_colimits_of_is_separating.

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