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₁} [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_op_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (𝒢 : Set C) : CategoryTheory.IsSeparating (Set.op 𝒢) ↔ CategoryTheory.IsCoseparating 𝒢

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

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

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

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

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

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

theorem CategoryTheory.isCodetecting_unop_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {𝒢 : Set Cᵒᵖ} : CategoryTheory.IsCodetecting (Set.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 : C} {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 : C} {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 : CategoryTheory.Subobject X) (Q : CategoryTheory.Subobject X) (h₁ : P ≤ Q) (h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, CategoryTheory.Subobject.Factors Q f → CategoryTheory.Subobject.Factors P 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 : CategoryTheory.Subobject X) (Q : CategoryTheory.Subobject X) (h : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, CategoryTheory.Subobject.Factors P f → CategoryTheory.Subobject.Factors Q 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 : CategoryTheory.Subobject X) (Q : CategoryTheory.Subobject X) (h : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, CategoryTheory.Subobject.Factors P f ↔ CategoryTheory.Subobject.Factors Q 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_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 G.unop ↔ CategoryTheory.IsSeparator G

theorem CategoryTheory.isSeparator_unop_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : Cᵒᵖ) : CategoryTheory.IsSeparator G.unop ↔ 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 G.unop ↔ CategoryTheory.IsDetector G

theorem CategoryTheory.isDetector_unop_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : Cᵒᵖ) : CategoryTheory.IsDetector G.unop ↔ 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.IsCospearator.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.Faithful (CategoryTheory.coyoneda.obj (Opposite.op G))

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

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 : C) (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 : C) (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 : C) (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 : C) (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 : C) (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 : C) (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.ReflectsIsomorphisms (CategoryTheory.coyoneda.obj (Opposite.op G))

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

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