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₁} [CategoryTheory.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₁} [CategoryTheory.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₁} [CategoryTheory.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₁} [CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {𝒢 : Set C} (h : CategoryTheory.IsSeparating 𝒢) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (α : C ≌ D) : CategoryTheory.IsSeparating (α.functor.obj '' 𝒢)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem CategoryTheory.hasInitial_of_isCoseparating {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.WellPowered C] [CategoryTheory.Limits.HasLimits C] {𝒢 : Set C} [Small.{v₁, u₁} ↑𝒢] (h𝒢 : CategoryTheory.IsCoseparating 𝒢) : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.WellPowered Cᵒᵖ] [CategoryTheory.Limits.HasColimits C] {𝒢 : Set C} [Small.{v₁, u₁} ↑𝒢] (h𝒢 : CategoryTheory.IsSeparating 𝒢) : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {𝒢 : Set C} (h𝒢 : CategoryTheory.IsDetecting 𝒢) {X : C} (P Q : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {𝒢 : Set C} (h𝒢 : CategoryTheory.IsDetecting 𝒢) {X : C} (P Q : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {𝒢 : Set C} (h𝒢 : CategoryTheory.IsDetecting 𝒢) {X : C} (P Q : CategoryTheory.Subobject X) (h : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, P.Factors f ↔ Q.Factors f) : P = Q

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

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

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

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

def CategoryTheory.IsSeparator {C : Type u₁} [CategoryTheory.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₁} [CategoryTheory.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₁} [CategoryTheory.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₁} [CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : C} (h : CategoryTheory.IsSeparator G) (α : C ≌ D) : CategoryTheory.IsSeparator (α.functor.obj G)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

class CategoryTheory.HasSeparator (C : Type u₁) [CategoryTheory.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), CategoryTheory.IsSeparator G

class CategoryTheory.HasCoseparator (C : Type u₁) [CategoryTheory.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), CategoryTheory.IsCoseparator G

class CategoryTheory.HasDetector (C : Type u₁) [CategoryTheory.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), CategoryTheory.IsDetector G

class CategoryTheory.HasCodetector (C : Type u₁) [CategoryTheory.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), CategoryTheory.IsCodetector G

noncomputable def CategoryTheory.separator (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.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₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.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₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.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₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.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₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.HasSeparator C] : CategoryTheory.IsSeparator (CategoryTheory.separator C)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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