# mathlibdocumentation

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:

• 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
• = β β¦X Y : Cβ¦ (f : X βΆ Y), (β (G : C), G β π’ β β (h : G βΆ Y), β! (h' : G βΆ X), h' β« f = h) β
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
• = β β¦X Y : Cβ¦ (f : X βΆ Y), (β (G : C), G β π’ β β (h : X βΆ G), β! (h' : Y βΆ G), f β« h' = h) β
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_coseparating_unop_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_codetecting_unop_iff {C : Type uβ} {π’ : set Cα΅α΅} :
theorem category_theory.is_detecting.is_separating {C : Type uβ} {π’ : set C} (hπ’ : category_theory.is_detecting π’) :
theorem category_theory.is_codetecting.is_coseparating {C : Type uβ} {π’ : set C} :
theorem category_theory.is_separating.is_detecting {C : Type uβ} {π’ : set C} (hπ’ : category_theory.is_separating π’) :
theorem category_theory.is_coseparating.is_codetecting {C : Type uβ} {π’ : set C} :
theorem category_theory.is_detecting_iff_is_separating {C : Type uβ} (π’ : set C) :
theorem category_theory.is_codetecting_iff_is_coseparating {C : Type uβ} {π’ : set C} :
theorem category_theory.is_separating.mono {C : Type uβ} {π’ : set C} (hπ’ : category_theory.is_separating π’) {β : set C} (hπ’β : π’ β β) :
theorem category_theory.is_coseparating.mono {C : Type uβ} {π’ : set C} (hπ’ : category_theory.is_coseparating π’) {β : 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} (hπ’ : category_theory.is_codetecting π’) {β : set C} (hπ’β : π’ β β) :
theorem category_theory.thin_of_is_separating_empty {C : Type uβ} (X Y : C) :
theorem category_theory.is_separating_empty_of_thin {C : Type uβ} [β (X Y : C), subsingleton (X βΆ Y)] :
theorem category_theory.thin_of_is_coseparating_empty {C : Type uβ} (X Y : C) :
theorem category_theory.is_coseparating_empty_of_thin {C : Type uβ} [β (X Y : C), subsingleton (X βΆ Y)] :
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))] :
theorem category_theory.has_initial_of_is_coseparating {C : Type uβ} {π’ : set C} [small β₯π’] (hπ’ : category_theory.is_coseparating π’) :

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.

theorem category_theory.has_terminal_of_is_separating {C : Type uβ} {π’ : set C} [small β₯π’] (hπ’ : category_theory.is_separating π’) :

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β} {π’ : 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} (hπ’ : category_theory.is_coseparating π’) :
theorem category_theory.costructured_arrow.is_separating_proj_preimage {C : Type uβ} {D : Type uβ} (S : C β₯€ D) (T : D) {π’ : set C} (hπ’ : category_theory.is_separating π’) :
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_coseparator_unop_iff {C : Type uβ} (G : Cα΅α΅) :
theorem category_theory.is_separator_unop_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_codetector_unop_iff {C : Type uβ} (G : Cα΅α΅) :
theorem category_theory.is_detector_unop_iff {C : Type uβ} (G : Cα΅α΅) :
theorem category_theory.is_detector.is_separator {C : Type uβ} {G : C} :
theorem category_theory.is_codetector.is_coseparator {C : Type uβ} {G : C} :
theorem category_theory.is_separator.is_detector {C : Type uβ} {G : C} :
theorem category_theory.is_cospearator.is_codetector {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_faithful_coyoneda_obj {C : Type uβ} (G : C) :
theorem category_theory.is_coseparator_iff_faithful_yoneda_obj {C : Type uβ} (G : C) :
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)] :
β β (A : C), category_theory.mono (category_theory.limits.pi.lift (Ξ» (f : A βΆ G), f))
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_prod_of_is_coseparator_left {C : Type uβ} (G H : C)  :
theorem category_theory.is_coseparator_prod_of_is_coseparator_right {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)) :
theorem category_theory.well_powered_of_is_detector {C : Type uβ} (G : C) (hG : category_theory.is_detector G) :