# mathlib3documentation

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:

• 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.
• 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.

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

## Main results #

We

• define predicates is_separating, is_coseparating, is_detecting and is_codetecting on sets of objects;
• show that separating and coseparating are dual notions;
• show that detecting and codetecting are dual notions;
• show that if C has equalizers, then detecting implies separating;
• show that if C has coequalizers, then codetecting implies separating;
• show that if C is balanced, then separating implies detecting and coseparating implies codetecting;
• show that ∅ is separating if and only if ∅ is coseparating if and only if C is thin;
• show that ∅ is detecting if and only if ∅ is codetecting if and only if C is a groupoid;
• define predicates is_separator, is_coseparator, is_detector and is_codetector as the singleton counterparts to the definitions for sets above and restate the above results in this situation;
• show that G is a separator if and only if coyoneda.obj (op G) is faithful (and the dual);
• show that G is a detector if and only if coyoneda.obj (op G) reflects isomorphisms (and the dual).

## Future work #

• We currently don't have any examples yet.
• We will want typeclasses has_separator C and similar.
def category_theory.is_separating {C : Type u₁} (𝒢 : 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₁} (𝒢 : 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₁} (𝒢 : 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₁} (𝒢 : 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_op_iff {C : Type u₁} (𝒢 : set C) :
theorem category_theory.is_coseparating_op_iff {C : Type u₁} (𝒢 : set C) :
theorem category_theory.is_separating_unop_iff {C : Type u₁} (𝒢 : set Cᵒᵖ) :
theorem category_theory.is_detecting_op_iff {C : Type u₁} (𝒢 : set C) :
theorem category_theory.is_codetecting_op_iff {C : Type u₁} (𝒢 : set C) :
theorem category_theory.is_detecting_unop_iff {C : Type u₁} (𝒢 : set Cᵒᵖ) :
theorem category_theory.is_separating.is_detecting {C : Type u₁} {𝒢 : set C}  :
theorem category_theory.is_separating.mono {C : Type u₁} {𝒢 : set C} {ℋ : set C} (h𝒢ℋ : 𝒢 ℋ) :
theorem category_theory.is_coseparating.mono {C : Type u₁} {𝒢 : set C} {ℋ : set C} (h𝒢ℋ : 𝒢 ℋ) :
theorem category_theory.is_detecting.mono {C : Type u₁} {𝒢 : set C} (h𝒢 : category_theory.is_detecting 𝒢) {ℋ : set C} (h𝒢ℋ : 𝒢 ℋ) :
theorem category_theory.is_codetecting.mono {C : Type u₁} {𝒢 : set C} {ℋ : set C} (h𝒢ℋ : 𝒢 ℋ) :
theorem category_theory.groupoid_of_is_detecting_empty {C : Type u₁} {X Y : C} (f : X Y) :
theorem category_theory.is_detecting_empty_of_groupoid {C : Type u₁} [ {X Y : C} (f : X Y), ] :
theorem category_theory.groupoid_of_is_codetecting_empty {C : Type u₁} {X Y : C} (f : X Y) :
theorem category_theory.is_codetecting_empty_of_groupoid {C : Type u₁} [ {X Y : C} (f : X Y), ] :
theorem category_theory.is_separating_iff_epi {C : Type u₁} (𝒢 : set C) [ (A : C), category_theory.limits.has_coproduct (λ (f : Σ (G : 𝒢), G A), (f.fst))] :
theorem category_theory.is_coseparating_iff_mono {C : Type u₁} (𝒢 : set C) [ (A : C), category_theory.limits.has_product (λ (f : Σ (G : 𝒢), A G), (f.fst))] :

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₁} {𝒢 : 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₁} {𝒢 : 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₁} {𝒢 : 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
theorem category_theory.well_powered_of_is_detecting {C : Type u₁} {𝒢 : set C} [small 𝒢] (h𝒢 : category_theory.is_detecting 𝒢) :

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

theorem category_theory.structured_arrow.is_coseparating_proj_preimage {C : Type u₁} {D : Type u₂} (S : D) (T : C D) {𝒢 : set C}  :
theorem category_theory.costructured_arrow.is_separating_proj_preimage {C : Type u₁} {D : Type u₂} (S : C D) (T : D) {𝒢 : set C}  :
def category_theory.is_separator {C : Type u₁} (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₁} (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₁} (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₁} (G : C) :
Prop

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

Equations
theorem category_theory.is_separator_op_iff {C : Type u₁} (G : C) :
theorem category_theory.is_coseparator_op_iff {C : Type u₁} (G : C) :
theorem category_theory.is_detector_op_iff {C : Type u₁} (G : C) :
theorem category_theory.is_codetector_op_iff {C : Type u₁} (G : C) :
theorem category_theory.is_separator.is_detector {C : Type u₁} {G : C} :
theorem category_theory.is_separator_def {C : Type u₁} (G : C) :
⦃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₁} {G : C} :
⦃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₁} (G : C) :
⦃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₁} {G : C} :
⦃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₁} (G : C) :
⦃X Y : C⦄ (f : X Y), ( (h : G Y), ∃! (h' : G X), h' f = h)
theorem category_theory.is_detector.def {C : Type u₁} {G : C} :
⦃X Y : C⦄ (f : X Y), ( (h : G Y), ∃! (h' : G X), h' f = h)
theorem category_theory.is_codetector_def {C : Type u₁} (G : C) :
⦃X Y : C⦄ (f : X Y), ( (h : X G), ∃! (h' : Y G), f h' = h)
theorem category_theory.is_codetector.def {C : Type u₁} {G : C} :
⦃X Y : C⦄ (f : X Y), ( (h : X G), ∃! (h' : Y G), f h' = h)
theorem category_theory.is_separator_iff_epi {C : Type u₁} (G : C) [ (A : C), category_theory.limits.has_coproduct (λ (f : G A), G)] :
theorem category_theory.is_coseparator_iff_mono {C : Type u₁} (G : C) [ (A : C), category_theory.limits.has_product (λ (f : A G), G)] :
theorem category_theory.is_separator_coprod {C : Type u₁} (G H : C)  :
theorem category_theory.is_separator_sigma {C : Type u₁} {β : Type w} (f : β C)  :
theorem category_theory.is_separator_sigma_of_is_separator {C : Type u₁} {β : Type w} (f : β C) (b : β) (hb : category_theory.is_separator (f b)) :
theorem category_theory.is_coseparator_prod {C : Type u₁} (G H : C)  :
theorem category_theory.is_coseparator_pi {C : Type u₁} {β : Type w} (f : β C)  :
theorem category_theory.is_coseparator_pi_of_is_coseparator {C : Type u₁} {β : Type w} (f : β C) (b : β) (hb : category_theory.is_coseparator (f b)) :