# Documentation

Mathlib.CategoryTheory.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 IsSeparating, IsCoseparating, IsDetecting and IsCodetecting 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 IsSeparator, IsCoseparator, IsDetector and IsCodetector 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 HasSeparator C and similar.
def CategoryTheory.IsSeparating {C : Type u₁} [] (𝒢 : Set C) :

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.

Instances For
def CategoryTheory.IsCoseparating {C : Type u₁} [] (𝒢 : Set C) :

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.

Instances For
def CategoryTheory.IsDetecting {C : Type u₁} [] (𝒢 : Set C) :

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.

Instances For
def CategoryTheory.IsCodetecting {C : Type u₁} [] (𝒢 : Set C) :

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.

Instances For
theorem CategoryTheory.isSeparating_op_iff {C : Type u₁} [] (𝒢 : Set C) :
theorem CategoryTheory.isCoseparating_op_iff {C : Type u₁} [] (𝒢 : Set C) :
theorem CategoryTheory.isCoseparating_unop_iff {C : Type u₁} [] (𝒢 : ) :
theorem CategoryTheory.isSeparating_unop_iff {C : Type u₁} [] (𝒢 : ) :
theorem CategoryTheory.isDetecting_op_iff {C : Type u₁} [] (𝒢 : Set C) :
theorem CategoryTheory.isCodetecting_op_iff {C : Type u₁} [] (𝒢 : Set C) :
theorem CategoryTheory.isDetecting_unop_iff {C : Type u₁} [] (𝒢 : ) :
theorem CategoryTheory.isCodetecting_unop_iff {C : Type u₁} [] {𝒢 : } :
theorem CategoryTheory.IsDetecting.isSeparating {C : Type u₁} [] {𝒢 : Set C} (h𝒢 : ) :
theorem CategoryTheory.IsSeparating.isDetecting {C : Type u₁} [] {𝒢 : Set C} (h𝒢 : ) :
theorem CategoryTheory.IsSeparating.mono {C : Type u₁} [] {𝒢 : Set C} (h𝒢 : ) {ℋ : Set C} (h𝒢ℋ : 𝒢 ) :
theorem CategoryTheory.IsCoseparating.mono {C : Type u₁} [] {𝒢 : Set C} (h𝒢 : ) {ℋ : Set C} (h𝒢ℋ : 𝒢 ) :
theorem CategoryTheory.IsDetecting.mono {C : Type u₁} [] {𝒢 : Set C} (h𝒢 : ) {ℋ : Set C} (h𝒢ℋ : 𝒢 ) :
theorem CategoryTheory.IsCodetecting.mono {C : Type u₁} [] {𝒢 : Set C} (h𝒢 : ) {ℋ : Set C} (h𝒢ℋ : 𝒢 ) :
theorem CategoryTheory.groupoid_of_isDetecting_empty {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.isDetecting_empty_of_groupoid {C : Type u₁} [] [∀ {X Y : C} (f : X Y), ] :
theorem CategoryTheory.groupoid_of_isCodetecting_empty {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.isCodetecting_empty_of_groupoid {C : Type u₁} [] [∀ {X Y : C} (f : X Y), ] :
theorem CategoryTheory.isSeparating_iff_epi {C : Type u₁} [] (𝒢 : Set C) [∀ (A : C), CategoryTheory.Limits.HasCoproduct fun f => f.fst] :
∀ (A : C),
theorem CategoryTheory.isCoseparating_iff_mono {C : Type u₁} [] (𝒢 : Set C) [∀ (A : C), CategoryTheory.Limits.HasProduct fun f => f.fst] :
theorem CategoryTheory.hasInitial_of_isCoseparating {C : Type u₁} [] {𝒢 : 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 hasColimits_of_hasLimits_of_isCoseparating.

theorem CategoryTheory.hasTerminal_of_isSeparating {C : Type u₁} [] {𝒢 : Set C} [] (h𝒢 : ) :

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

theorem CategoryTheory.Subobject.eq_of_le_of_isDetecting {C : Type u₁} [] {𝒢 : Set C} (h𝒢 : ) {X : C} (P : ) (Q : ) (h₁ : P Q) (h₂ : ∀ (G : C), G 𝒢∀ {f : G X}, ) :
P = Q
theorem CategoryTheory.Subobject.inf_eq_of_isDetecting {C : Type u₁} [] {𝒢 : Set C} (h𝒢 : ) {X : C} (P : ) (Q : ) (h : ∀ (G : C), G 𝒢∀ {f : G X}, ) :
P Q = P
theorem CategoryTheory.Subobject.eq_of_isDetecting {C : Type u₁} [] {𝒢 : Set C} (h𝒢 : ) {X : C} (P : ) (Q : ) (h : ∀ (G : C), G 𝒢∀ {f : G X}, ) :
P = Q
theorem CategoryTheory.wellPowered_of_isDetecting {C : Type u₁} [] {𝒢 : Set C} [] (h𝒢 : ) :

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

theorem CategoryTheory.StructuredArrow.isCoseparating_proj_preimage {C : Type u₁} [] {D : Type u₂} [] (S : D) (T : ) {𝒢 : Set C} (h𝒢 : ) :
CategoryTheory.IsCoseparating (().toPrefunctor.obj ⁻¹' 𝒢)
theorem CategoryTheory.CostructuredArrow.isSeparating_proj_preimage {C : Type u₁} [] {D : Type u₂} [] (S : ) (T : D) {𝒢 : Set C} (h𝒢 : ) :
CategoryTheory.IsSeparating (().toPrefunctor.obj ⁻¹' 𝒢)
def CategoryTheory.IsSeparator {C : Type u₁} [] (G : C) :

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

Instances For
def CategoryTheory.IsCoseparator {C : Type u₁} [] (G : C) :

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

Instances For
def CategoryTheory.IsDetector {C : Type u₁} [] (G : C) :

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

Instances For
def CategoryTheory.IsCodetector {C : Type u₁} [] (G : C) :

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

Instances For
theorem CategoryTheory.isSeparator_op_iff {C : Type u₁} [] (G : C) :
theorem CategoryTheory.isCoseparator_op_iff {C : Type u₁} [] (G : C) :
theorem CategoryTheory.isDetector_op_iff {C : Type u₁} [] (G : C) :
theorem CategoryTheory.isCodetector_op_iff {C : Type u₁} [] (G : C) :
theorem CategoryTheory.IsDetector.isSeparator {C : Type u₁} [] {G : C} :
theorem CategoryTheory.IsSeparator.isDetector {C : Type u₁} [] {G : C} :
theorem CategoryTheory.isSeparator_def {C : Type u₁} [] (G : C) :
∀ ⦃X Y : C⦄ (f g : X Y), (∀ (h : G X), ) → f = g
theorem CategoryTheory.IsSeparator.def {C : Type u₁} [] {G : C} :
∀ ⦃X Y : C⦄ (f g : X Y), (∀ (h : G X), ) → f = g
theorem CategoryTheory.isCoseparator_def {C : Type u₁} [] (G : C) :
∀ ⦃X Y : C⦄ (f g : X Y), (∀ (h : Y G), ) → f = g
theorem CategoryTheory.IsCoseparator.def {C : Type u₁} [] {G : C} :
∀ ⦃X Y : C⦄ (f g : X Y), (∀ (h : Y G), ) → f = g
theorem CategoryTheory.isDetector_def {C : Type u₁} [] (G : C) :
∀ ⦃X Y : C⦄ (f : X Y), (∀ (h : G Y), ∃! h', ) →
theorem CategoryTheory.IsDetector.def {C : Type u₁} [] {G : C} :
∀ ⦃X Y : C⦄ (f : X Y), (∀ (h : G Y), ∃! h', ) →
theorem CategoryTheory.isCodetector_def {C : Type u₁} [] (G : C) :
∀ ⦃X Y : C⦄ (f : X Y), (∀ (h : X G), ∃! h', ) →
theorem CategoryTheory.IsCodetector.def {C : Type u₁} [] {G : C} :
∀ ⦃X Y : C⦄ (f : X Y), (∀ (h : X G), ∃! h', ) →
theorem CategoryTheory.isSeparator_iff_faithful_coyoneda_obj {C : Type u₁} [] (G : C) :
CategoryTheory.Faithful (CategoryTheory.coyoneda.obj ())
theorem CategoryTheory.isCoseparator_iff_faithful_yoneda_obj {C : Type u₁} [] (G : C) :
CategoryTheory.Faithful (CategoryTheory.yoneda.obj G)
theorem CategoryTheory.isSeparator_iff_epi {C : Type u₁} [] (G : C) [∀ (A : C), CategoryTheory.Limits.HasCoproduct fun x => G] :
theorem CategoryTheory.isCoseparator_iff_mono {C : Type u₁} [] (G : C) [∀ (A : C), CategoryTheory.Limits.HasProduct fun x => G] :
theorem CategoryTheory.isSeparator_coprod {C : Type u₁} [] (G : C) (H : C) :
theorem CategoryTheory.isSeparator_coprod_of_isSeparator_left {C : Type u₁} [] (G : C) (H : C) (hG : ) :
theorem CategoryTheory.isSeparator_coprod_of_isSeparator_right {C : Type u₁} [] (G : C) (H : C) (hH : ) :
theorem CategoryTheory.isSeparator_sigma {C : Type u₁} [] {β : Type w} (f : βC) :
theorem CategoryTheory.isSeparator_sigma_of_isSeparator {C : Type u₁} [] {β : Type w} (f : βC) (b : β) (hb : ) :
theorem CategoryTheory.isCoseparator_prod {C : Type u₁} [] (G : C) (H : C) :
theorem CategoryTheory.isCoseparator_prod_of_isCoseparator_left {C : Type u₁} [] (G : C) (H : C) (hG : ) :
theorem CategoryTheory.isCoseparator_prod_of_isCoseparator_right {C : Type u₁} [] (G : C) (H : C) (hH : ) :
theorem CategoryTheory.isCoseparator_pi {C : Type u₁} [] {β : Type w} (f : βC) :
theorem CategoryTheory.isCoseparator_pi_of_isCoseparator {C : Type u₁} [] {β : Type w} (f : βC) (b : β) (hb : ) :
theorem CategoryTheory.wellPowered_of_isDetector {C : Type u₁} [] (G : C) (hG : ) :