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 equivalences of categories preserves these notions;
• 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 coseparating;
• 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);
• show that C is WellPowered if it admits small pullbacks and a detector;
• define corresponding typeclasses HasSeparator, HasCoseparator, HasDetector and HasCodetector on categories and prove analogous results for these.

Future work

• We currently don't have any examples yet.

def CategoryTheory.IsSeparating {C : Type u₁} [Category.{v₁, u₁} 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

• CategoryTheory.IsSeparating 𝒢 = ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : G ⟶ X), CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) → f = g

def CategoryTheory.IsCoseparating {C : Type u₁} [Category.{v₁, u₁} 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

• CategoryTheory.IsCoseparating 𝒢 = ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h) → f = g

def CategoryTheory.IsDetecting {C : Type u₁} [Category.{v₁, u₁} 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

• CategoryTheory.IsDetecting 𝒢 = ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, CategoryTheory.CategoryStruct.comp h' f = h) → CategoryTheory.IsIso f

def CategoryTheory.IsCodetecting {C : Type u₁} [Category.{v₁, u₁} 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

• CategoryTheory.IsCodetecting 𝒢 = ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, CategoryTheory.CategoryStruct.comp f h' = h) → CategoryTheory.IsIso f

theorem CategoryTheory.IsSeparating.of_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {𝒢 : Set C} (h : IsSeparating 𝒢) {D : Type u_1} [Category.{u_2, u_1} D] (α : C ≌ D) : IsSeparating (α.functor.obj '' 𝒢)

theorem CategoryTheory.IsCoseparating.of_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {𝒢 : Set C} (h : IsCoseparating 𝒢) {D : Type u_1} [Category.{u_2, u_1} D] (α : C ≌ D) : IsCoseparating (α.functor.obj '' 𝒢)

theorem CategoryTheory.isSeparating_op_iff {C : Type u₁} [Category.{v₁, u₁} C] (𝒢 : Set C) : IsSeparating 𝒢.op ↔ IsCoseparating 𝒢

theorem CategoryTheory.isCoseparating_op_iff {C : Type u₁} [Category.{v₁, u₁} C] (𝒢 : Set C) : IsCoseparating 𝒢.op ↔ IsSeparating 𝒢

theorem CategoryTheory.isCoseparating_unop_iff {C : Type u₁} [Category.{v₁, u₁} C] (𝒢 : Set Cᵒᵖ) : IsCoseparating 𝒢.unop ↔ IsSeparating 𝒢

theorem CategoryTheory.isSeparating_unop_iff {C : Type u₁} [Category.{v₁, u₁} C] (𝒢 : Set Cᵒᵖ) : IsSeparating 𝒢.unop ↔ IsCoseparating 𝒢

theorem CategoryTheory.isDetecting_op_iff {C : Type u₁} [Category.{v₁, u₁} C] (𝒢 : Set C) : IsDetecting 𝒢.op ↔ IsCodetecting 𝒢

theorem CategoryTheory.isCodetecting_op_iff {C : Type u₁} [Category.{v₁, u₁} C] (𝒢 : Set C) : IsCodetecting 𝒢.op ↔ IsDetecting 𝒢

theorem CategoryTheory.isDetecting_unop_iff {C : Type u₁} [Category.{v₁, u₁} C] (𝒢 : Set Cᵒᵖ) : IsDetecting 𝒢.unop ↔ IsCodetecting 𝒢

theorem CategoryTheory.isCodetecting_unop_iff {C : Type u₁} [Category.{v₁, u₁} C] {𝒢 : Set Cᵒᵖ} : IsCodetecting 𝒢.unop ↔ IsDetecting 𝒢

theorem CategoryTheory.IsDetecting.isSeparating {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasEqualizers C] {𝒢 : Set C} (h𝒢 : IsDetecting 𝒢) : IsSeparating 𝒢

theorem CategoryTheory.IsCodetecting.isCoseparating {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasCoequalizers C] {𝒢 : Set C} : IsCodetecting 𝒢 → IsCoseparating 𝒢

theorem CategoryTheory.IsSeparating.isDetecting {C : Type u₁} [Category.{v₁, u₁} C] [Balanced C] {𝒢 : Set C} (h𝒢 : IsSeparating 𝒢) : IsDetecting 𝒢

theorem CategoryTheory.IsDetecting.isIso_iff_of_mono {C : Type u₁} [Category.{v₁, u₁} C] {𝒢 : Set C} (h𝒢 : IsDetecting 𝒢) {X Y : C} (f : X ⟶ Y) [Mono f] : IsIso f ↔ ∀ s ∈ 𝒢, Function.Surjective ((coyoneda.obj (Opposite.op s)).map f)

theorem CategoryTheory.IsCodetecting.isIso_iff_of_epi {C : Type u₁} [Category.{v₁, u₁} C] {𝒢 : Set C} (h𝒢 : IsCodetecting 𝒢) {X Y : C} (f : X ⟶ Y) [Epi f] : IsIso f ↔ ∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op)

theorem CategoryTheory.IsCoseparating.isCodetecting {C : Type u₁} [Category.{v₁, u₁} C] [Balanced C] {𝒢 : Set C} : IsCoseparating 𝒢 → IsCodetecting 𝒢

theorem CategoryTheory.isDetecting_iff_isSeparating {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasEqualizers C] [Balanced C] (𝒢 : Set C) : IsDetecting 𝒢 ↔ IsSeparating 𝒢

theorem CategoryTheory.isCodetecting_iff_isCoseparating {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasCoequalizers C] [Balanced C] {𝒢 : Set C} : IsCodetecting 𝒢 ↔ IsCoseparating 𝒢

theorem CategoryTheory.IsSeparating.mono {C : Type u₁} [Category.{v₁, u₁} C] {𝒢 : Set C} (h𝒢 : IsSeparating 𝒢) {ℋ : Set C} (h𝒢ℋ : 𝒢 ⊆ ℋ) : IsSeparating ℋ

theorem CategoryTheory.IsCoseparating.mono {C : Type u₁} [Category.{v₁, u₁} C] {𝒢 : Set C} (h𝒢 : IsCoseparating 𝒢) {ℋ : Set C} (h𝒢ℋ : 𝒢 ⊆ ℋ) : IsCoseparating ℋ

theorem CategoryTheory.IsDetecting.mono {C : Type u₁} [Category.{v₁, u₁} C] {𝒢 : Set C} (h𝒢 : IsDetecting 𝒢) {ℋ : Set C} (h𝒢ℋ : 𝒢 ⊆ ℋ) : IsDetecting ℋ

theorem CategoryTheory.IsCodetecting.mono {C : Type u₁} [Category.{v₁, u₁} C] {𝒢 : Set C} (h𝒢 : IsCodetecting 𝒢) {ℋ : Set C} (h𝒢ℋ : 𝒢 ⊆ ℋ) : IsCodetecting ℋ

theorem CategoryTheory.thin_of_isSeparating_empty {C : Type u₁} [Category.{v₁, u₁} C] (h : IsSeparating ∅) : Quiver.IsThin C

theorem CategoryTheory.isSeparating_empty_of_thin {C : Type u₁} [Category.{v₁, u₁} C] [Quiver.IsThin C] : IsSeparating ∅

theorem CategoryTheory.thin_of_isCoseparating_empty {C : Type u₁} [Category.{v₁, u₁} C] (h : IsCoseparating ∅) : Quiver.IsThin C

theorem CategoryTheory.isCoseparating_empty_of_thin {C : Type u₁} [Category.{v₁, u₁} C] [Quiver.IsThin C] : IsCoseparating ∅

theorem CategoryTheory.groupoid_of_isDetecting_empty {C : Type u₁} [Category.{v₁, u₁} C] (h : IsDetecting ∅) {X Y : C} (f : X ⟶ Y) : IsIso f

theorem CategoryTheory.isDetecting_empty_of_groupoid {C : Type u₁} [Category.{v₁, u₁} C] [∀ {X Y : C} (f : X ⟶ Y), IsIso f] : IsDetecting ∅

theorem CategoryTheory.groupoid_of_isCodetecting_empty {C : Type u₁} [Category.{v₁, u₁} C] (h : IsCodetecting ∅) {X Y : C} (f : X ⟶ Y) : IsIso f

theorem CategoryTheory.isCodetecting_empty_of_groupoid {C : Type u₁} [Category.{v₁, u₁} C] [∀ {X Y : C} (f : X ⟶ Y), IsIso f] : IsCodetecting ∅

theorem CategoryTheory.isSeparating_iff_epi {C : Type u₁} [Category.{v₁, u₁} C] (𝒢 : Set C) [∀ (A : C), Limits.HasCoproduct fun (f : (G : ↑𝒢) × (↑G ⟶ A)) => ↑f.fst] : IsSeparating 𝒢 ↔ ∀ (A : C), Epi (Limits.Sigma.desc Sigma.snd)

theorem CategoryTheory.isCoseparating_iff_mono {C : Type u₁} [Category.{v₁, u₁} C] (𝒢 : Set C) [∀ (A : C), Limits.HasProduct fun (f : (G : ↑𝒢) × (A ⟶ ↑G)) => ↑f.fst] : IsCoseparating 𝒢 ↔ ∀ (A : C), Mono (Limits.Pi.lift Sigma.snd)

theorem CategoryTheory.hasInitial_of_isCoseparating {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasLimitsOfSize.{w, w, v₁, u₁} C] {𝒢 : Set C} [Small.{w, u₁} ↑𝒢] (h𝒢 : IsCoseparating 𝒢) : Limits.HasInitial C

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₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} Cᵒᵖ] [WellPowered.{w, v₁, u₁} Cᵒᵖ] [Limits.HasColimitsOfSize.{w, w, v₁, u₁} C] {𝒢 : Set C} [Small.{w, u₁} ↑𝒢] (h𝒢 : IsSeparating 𝒢) : Limits.HasTerminal C

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₁} [Category.{v₁, u₁} C] {𝒢 : Set C} (h𝒢 : IsDetecting 𝒢) {X : C} (P Q : Subobject X) (h₁ : P ≤ Q) (h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f) : P = Q

theorem CategoryTheory.Subobject.inf_eq_of_isDetecting {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {𝒢 : Set C} (h𝒢 : IsDetecting 𝒢) {X : C} (P Q : Subobject X) (h : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, P.Factors f → Q.Factors f) : P ⊓ Q = P

theorem CategoryTheory.Subobject.eq_of_isDetecting {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {𝒢 : Set C} (h𝒢 : IsDetecting 𝒢) {X : C} (P Q : Subobject X) (h : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, P.Factors f ↔ Q.Factors f) : P = Q

theorem CategoryTheory.wellPowered_of_isDetecting {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {𝒢 : Set C} [Small.{w, u₁} ↑𝒢] [LocallySmall.{w, v₁, u₁} C] (h𝒢 : IsDetecting 𝒢) : WellPowered.{w, v₁, u₁} C

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

theorem CategoryTheory.StructuredArrow.isCoseparating_proj_preimage {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (S : D) (T : Functor C D) {𝒢 : Set C} (h𝒢 : IsCoseparating 𝒢) : IsCoseparating ((proj S T).obj ⁻¹' 𝒢)

theorem CategoryTheory.CostructuredArrow.isSeparating_proj_preimage {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (S : Functor C D) (T : D) {𝒢 : Set C} (h𝒢 : IsSeparating 𝒢) : IsSeparating ((proj S T).obj ⁻¹' 𝒢)

def CategoryTheory.IsSeparator {C : Type u₁} [Category.{v₁, u₁} C] (G : C) : Prop

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

Equations

• CategoryTheory.IsSeparator G = CategoryTheory.IsSeparating {G}

def CategoryTheory.IsCoseparator {C : Type u₁} [Category.{v₁, u₁} C] (G : C) : Prop

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

Equations

• CategoryTheory.IsCoseparator G = CategoryTheory.IsCoseparating {G}

def CategoryTheory.IsDetector {C : Type u₁} [Category.{v₁, u₁} C] (G : C) : Prop

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

Equations

• CategoryTheory.IsDetector G = CategoryTheory.IsDetecting {G}

def CategoryTheory.IsCodetector {C : Type u₁} [Category.{v₁, u₁} C] (G : C) : Prop

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

Equations

• CategoryTheory.IsCodetector G = CategoryTheory.IsCodetecting {G}

theorem CategoryTheory.IsSeparator.of_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {G : C} (h : IsSeparator G) (α : C ≌ D) : IsSeparator (α.functor.obj G)

theorem CategoryTheory.IsCoseparator.of_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {G : C} (h : IsCoseparator G) (α : C ≌ D) : IsCoseparator (α.functor.obj G)

theorem CategoryTheory.isSeparator_op_iff {C : Type u₁} [Category.{v₁, u₁} C] (G : C) : IsSeparator (Opposite.op G) ↔ IsCoseparator G

theorem CategoryTheory.isCoseparator_op_iff {C : Type u₁} [Category.{v₁, u₁} C] (G : C) : IsCoseparator (Opposite.op G) ↔ IsSeparator G

theorem CategoryTheory.isCoseparator_unop_iff {C : Type u₁} [Category.{v₁, u₁} C] (G : Cᵒᵖ) : IsCoseparator (Opposite.unop G) ↔ IsSeparator G

theorem CategoryTheory.isSeparator_unop_iff {C : Type u₁} [Category.{v₁, u₁} C] (G : Cᵒᵖ) : IsSeparator (Opposite.unop G) ↔ IsCoseparator G

theorem CategoryTheory.isDetector_op_iff {C : Type u₁} [Category.{v₁, u₁} C] (G : C) : IsDetector (Opposite.op G) ↔ IsCodetector G

theorem CategoryTheory.isCodetector_op_iff {C : Type u₁} [Category.{v₁, u₁} C] (G : C) : IsCodetector (Opposite.op G) ↔ IsDetector G

theorem CategoryTheory.isCodetector_unop_iff {C : Type u₁} [Category.{v₁, u₁} C] (G : Cᵒᵖ) : IsCodetector (Opposite.unop G) ↔ IsDetector G

theorem CategoryTheory.isDetector_unop_iff {C : Type u₁} [Category.{v₁, u₁} C] (G : Cᵒᵖ) : IsDetector (Opposite.unop G) ↔ IsCodetector G

theorem CategoryTheory.IsDetector.isSeparator {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasEqualizers C] {G : C} : IsDetector G → IsSeparator G

theorem CategoryTheory.IsCodetector.isCoseparator {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasCoequalizers C] {G : C} : IsCodetector G → IsCoseparator G

theorem CategoryTheory.IsSeparator.isDetector {C : Type u₁} [Category.{v₁, u₁} C] [Balanced C] {G : C} : IsSeparator G → IsDetector G

theorem CategoryTheory.IsCoseparator.isCodetector {C : Type u₁} [Category.{v₁, u₁} C] [Balanced C] {G : C} : IsCoseparator G → IsCodetector G

theorem CategoryTheory.isSeparator_def {C : Type u₁} [Category.{v₁, u₁} C] (G : C) : IsSeparator G ↔ ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), CategoryStruct.comp h f = CategoryStruct.comp h g) → f = g

theorem CategoryTheory.IsSeparator.def {C : Type u₁} [Category.{v₁, u₁} C] {G : C} : IsSeparator G → ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), CategoryStruct.comp h f = CategoryStruct.comp h g) → f = g

theorem CategoryTheory.isCoseparator_def {C : Type u₁} [Category.{v₁, u₁} C] (G : C) : IsCoseparator G ↔ ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), CategoryStruct.comp f h = CategoryStruct.comp g h) → f = g

theorem CategoryTheory.IsCoseparator.def {C : Type u₁} [Category.{v₁, u₁} C] {G : C} : IsCoseparator G → ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), CategoryStruct.comp f h = CategoryStruct.comp g h) → f = g

theorem CategoryTheory.isDetector_def {C : Type u₁} [Category.{v₁, u₁} C] (G : C) : IsDetector G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, CategoryStruct.comp h' f = h) → IsIso f

theorem CategoryTheory.IsDetector.def {C : Type u₁} [Category.{v₁, u₁} C] {G : C} : IsDetector G → ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, CategoryStruct.comp h' f = h) → IsIso f

theorem CategoryTheory.isCodetector_def {C : Type u₁} [Category.{v₁, u₁} C] (G : C) : IsCodetector G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, CategoryStruct.comp f h' = h) → IsIso f

theorem CategoryTheory.IsCodetector.def {C : Type u₁} [Category.{v₁, u₁} C] {G : C} : IsCodetector G → ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, CategoryStruct.comp f h' = h) → IsIso f

theorem CategoryTheory.isSeparator_iff_faithful_coyoneda_obj {C : Type u₁} [Category.{v₁, u₁} C] (G : C) : IsSeparator G ↔ (coyoneda.obj (Opposite.op G)).Faithful

theorem CategoryTheory.isCoseparator_iff_faithful_yoneda_obj {C : Type u₁} [Category.{v₁, u₁} C] (G : C) : IsCoseparator G ↔ (yoneda.obj G).Faithful

theorem CategoryTheory.isSeparator_iff_epi {C : Type u₁} [Category.{v₁, u₁} C] (G : C) [∀ (A : C), Limits.HasCoproduct fun (x : G ⟶ A) => G] : IsSeparator G ↔ ∀ (A : C), Epi (Limits.Sigma.desc fun (f : G ⟶ A) => f)

theorem CategoryTheory.isCoseparator_iff_mono {C : Type u₁} [Category.{v₁, u₁} C] (G : C) [∀ (A : C), Limits.HasProduct fun (x : A ⟶ G) => G] : IsCoseparator G ↔ ∀ (A : C), Mono (Limits.Pi.lift fun (f : A ⟶ G) => f)

theorem CategoryTheory.isSeparator_coprod {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] (G H : C) [Limits.HasBinaryCoproduct G H] : IsSeparator (G ⨿ H) ↔ IsSeparating {G, H}

theorem CategoryTheory.isSeparator_coprod_of_isSeparator_left {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] (G H : C) [Limits.HasBinaryCoproduct G H] (hG : IsSeparator G) : IsSeparator (G ⨿ H)

theorem CategoryTheory.isSeparator_coprod_of_isSeparator_right {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] (G H : C) [Limits.HasBinaryCoproduct G H] (hH : IsSeparator H) : IsSeparator (G ⨿ H)

theorem CategoryTheory.isSeparator_of_isColimit_cofan {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {β : Type w} {f : β → C} (hf : IsSeparating (Set.range f)) {c : Limits.Cofan f} (hc : Limits.IsColimit c) : IsSeparator c.pt

theorem CategoryTheory.isSeparator_sigma {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {β : Type w} (f : β → C) [Limits.HasCoproduct f] : IsSeparator (∐ f) ↔ IsSeparating (Set.range f)

theorem CategoryTheory.IsSeparating.isSeparator_coproduct {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {β : Type w} {f : β → C} [Limits.HasCoproduct f] (hS : IsSeparating (Set.range f)) : IsSeparator (∐ f)

theorem CategoryTheory.isSeparator_sigma_of_isSeparator {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {β : Type w} (f : β → C) [Limits.HasCoproduct f] (b : β) (hb : IsSeparator (f b)) : IsSeparator (∐ f)

theorem CategoryTheory.isCoseparator_prod {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] (G H : C) [Limits.HasBinaryProduct G H] : IsCoseparator (G ⨯ H) ↔ IsCoseparating {G, H}

theorem CategoryTheory.isCoseparator_prod_of_isCoseparator_left {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] (G H : C) [Limits.HasBinaryProduct G H] (hG : IsCoseparator G) : IsCoseparator (G ⨯ H)

theorem CategoryTheory.isCoseparator_prod_of_isCoseparator_right {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] (G H : C) [Limits.HasBinaryProduct G H] (hH : IsCoseparator H) : IsCoseparator (G ⨯ H)

theorem CategoryTheory.isCoseparator_pi {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {β : Type w} (f : β → C) [Limits.HasProduct f] : IsCoseparator (∏ᶜ f) ↔ IsCoseparating (Set.range f)

theorem CategoryTheory.isCoseparator_pi_of_isCoseparator {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {β : Type w} (f : β → C) [Limits.HasProduct f] (b : β) (hb : IsCoseparator (f b)) : IsCoseparator (∏ᶜ f)

theorem CategoryTheory.isDetector_iff_reflectsIsomorphisms_coyoneda_obj {C : Type u₁} [Category.{v₁, u₁} C] (G : C) : IsDetector G ↔ (coyoneda.obj (Opposite.op G)).ReflectsIsomorphisms

theorem CategoryTheory.isCodetector_iff_reflectsIsomorphisms_yoneda_obj {C : Type u₁} [Category.{v₁, u₁} C] (G : C) : IsCodetector G ↔ (yoneda.obj G).ReflectsIsomorphisms

theorem CategoryTheory.wellPowered_of_isDetector {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] (G : C) (hG : IsDetector G) : WellPowered.{v₁, v₁, u₁} C

theorem CategoryTheory.wellPowered_of_isSeparator {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] [Balanced C] (G : C) (hG : IsSeparator G) : WellPowered.{v₁, v₁, u₁} C

class CategoryTheory.HasSeparator (C : Type u₁) [Category.{v₁, u₁} C] : Prop

For a category C and an object G : C, G is a separator of C if the functor C(G, -) is faithful.

While IsSeparator G : Prop is the proposition that G is a separator of C, an HasSeparator C : Prop is the proposition that such a separator exists. Note that HasSeparator C is a proposition. It does not designate a favored separator and merely asserts the existence of one.

• hasSeparator : ∃ (G : C), IsSeparator G

class CategoryTheory.HasCoseparator (C : Type u₁) [Category.{v₁, u₁} C] : Prop

For a category C and an object G : C, G is a coseparator of C if the functor C(-, G) is faithful.

While IsCoseparator G : Prop is the proposition that G is a coseparator of C, an HasCoseparator C : Prop is the proposition that such a coseparator exists. Note that HasCoseparator C is a proposition. It does not designate a favored coseparator and merely asserts the existence of one.

• hasCoseparator : ∃ (G : C), IsCoseparator G

class CategoryTheory.HasDetector (C : Type u₁) [Category.{v₁, u₁} C] : Prop

For a category C and an object G : C, G is a detector of C if the functor C(G, -) reflects isomorphisms.

While IsDetector G : Prop is the proposition that G is a detector of C, an HasDetector C : Prop is the proposition that such a detector exists. Note that HasDetector C is a proposition. It does not designate a favored detector and merely asserts the existence of one.

• hasDetector : ∃ (G : C), IsDetector G

class CategoryTheory.HasCodetector (C : Type u₁) [Category.{v₁, u₁} C] : Prop

For a category C and an object G : C, G is a codetector of C if the functor C(-, G) reflects isomorphisms.

While IsCodetector G : Prop is the proposition that G is a codetector of C, an HasCodetector C : Prop is the proposition that such a codetector exists. Note that HasCodetector C is a proposition. It does not designate a favored codetector and merely asserts the existence of one.

• hasCodetector : ∃ (G : C), IsCodetector G

noncomputable def CategoryTheory.separator (C : Type u₁) [Category.{v₁, u₁} C] [HasSeparator C] : C

Given a category C that has a separator (HasSeparator C), separator C is an arbitrarily chosen separator of C.

Equations

• CategoryTheory.separator C = ⋯.choose

noncomputable def CategoryTheory.coseparator (C : Type u₁) [Category.{v₁, u₁} C] [HasCoseparator C] : C

Given a category C that has a coseparator (HasCoseparator C), coseparator C is an arbitrarily chosen coseparator of C.

Equations

• CategoryTheory.coseparator C = ⋯.choose

noncomputable def CategoryTheory.detector (C : Type u₁) [Category.{v₁, u₁} C] [HasDetector C] : C

Given a category C that has a detector (HasDetector C), detector C is an arbitrarily chosen detector of C.

Equations

• CategoryTheory.detector C = ⋯.choose

noncomputable def CategoryTheory.codetector (C : Type u₁) [Category.{v₁, u₁} C] [HasCodetector C] : C

Given a category C that has a codetector (HasCodetector C), codetector C is an arbitrarily chosen codetector of C.

Equations

• CategoryTheory.codetector C = ⋯.choose

theorem CategoryTheory.isSeparator_separator (C : Type u₁) [Category.{v₁, u₁} C] [HasSeparator C] : IsSeparator (separator C)

theorem CategoryTheory.isDetector_separator (C : Type u₁) [Category.{v₁, u₁} C] [Balanced C] [HasSeparator C] : IsDetector (separator C)

theorem CategoryTheory.isCoseparator_coseparator (C : Type u₁) [Category.{v₁, u₁} C] [HasCoseparator C] : IsCoseparator (coseparator C)

theorem CategoryTheory.isCodetector_coseparator (C : Type u₁) [Category.{v₁, u₁} C] [Balanced C] [HasCoseparator C] : IsCodetector (coseparator C)

theorem CategoryTheory.isDetector_detector (C : Type u₁) [Category.{v₁, u₁} C] [HasDetector C] : IsDetector (detector C)

theorem CategoryTheory.isSeparator_detector (C : Type u₁) [Category.{v₁, u₁} C] [Limits.HasEqualizers C] [HasDetector C] : IsSeparator (detector C)

theorem CategoryTheory.isCodetector_codetector (C : Type u₁) [Category.{v₁, u₁} C] [HasCodetector C] : IsCodetector (codetector C)

theorem CategoryTheory.isCoseparator_codetector (C : Type u₁) [Category.{v₁, u₁} C] [Limits.HasCoequalizers C] [HasCodetector C] : IsCoseparator (codetector C)

theorem CategoryTheory.HasSeparator.hasDetector {C : Type u₁} [Category.{v₁, u₁} C] [Balanced C] [HasSeparator C] : HasDetector C

theorem CategoryTheory.HasDetector.hasSeparator {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasEqualizers C] [HasDetector C] : HasSeparator C

theorem CategoryTheory.HasCoseparator.hasCodetector {C : Type u₁} [Category.{v₁, u₁} C] [Balanced C] [HasCoseparator C] : HasCodetector C

theorem CategoryTheory.HasCodetector.hasCoseparator {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasCoequalizers C] [HasCodetector C] : HasCoseparator C

instance CategoryTheory.HasDetector.wellPowered {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] [HasDetector C] : WellPowered.{v₁, v₁, u₁} C

instance CategoryTheory.HasSeparator.wellPowered {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] [Balanced C] [HasSeparator C] : WellPowered.{v₁, v₁, u₁} C

theorem CategoryTheory.HasSeparator.of_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasSeparator C] (α : C ≌ D) : HasSeparator D

theorem CategoryTheory.HasCoseparator.of_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasCoseparator C] (α : C ≌ D) : HasCoseparator D

@[simp]

theorem CategoryTheory.hasSeparator_op_iff {C : Type u₁} [Category.{v₁, u₁} C] : HasSeparator Cᵒᵖ ↔ HasCoseparator C

@[simp]

theorem CategoryTheory.hasCoseparator_op_iff {C : Type u₁} [Category.{v₁, u₁} C] : HasCoseparator Cᵒᵖ ↔ HasSeparator C

@[simp]

theorem CategoryTheory.hasDetector_op_iff {C : Type u₁} [Category.{v₁, u₁} C] : HasDetector Cᵒᵖ ↔ HasCodetector C

@[simp]

theorem CategoryTheory.hasCodetector_op_iff {C : Type u₁} [Category.{v₁, u₁} C] : HasCodetector Cᵒᵖ ↔ HasDetector C

instance CategoryTheory.HasSeparator.hasCoseparator_op {C : Type u₁} [Category.{v₁, u₁} C] [HasSeparator C] : HasCoseparator Cᵒᵖ

theorem CategoryTheory.HasSeparator.hasCoseparator_of_hasSeparator_op {C : Type u₁} [Category.{v₁, u₁} C] [h : HasSeparator Cᵒᵖ] : HasCoseparator C

instance CategoryTheory.HasCoseparator.hasSeparator_op {C : Type u₁} [Category.{v₁, u₁} C] [HasCoseparator C] : HasSeparator Cᵒᵖ

theorem CategoryTheory.HasCoseparator.hasSeparator_of_hasCoseparator_op {C : Type u₁} [Category.{v₁, u₁} C] [HasCoseparator Cᵒᵖ] : HasSeparator C

instance CategoryTheory.HasDetector.hasCodetector_op {C : Type u₁} [Category.{v₁, u₁} C] [HasDetector C] : HasCodetector Cᵒᵖ

theorem CategoryTheory.HasDetector.hasCodetector_of_hasDetector_op {C : Type u₁} [Category.{v₁, u₁} C] [HasDetector Cᵒᵖ] : HasCodetector C

instance CategoryTheory.HasCodetector.hasDetector_op {C : Type u₁} [Category.{v₁, u₁} C] [HasCodetector C] : HasDetector Cᵒᵖ

theorem CategoryTheory.HasCodetector.hasDetector_of_hasCodetector_op {C : Type u₁} [Category.{v₁, u₁} C] [HasCodetector Cᵒᵖ] : HasDetector C