Separating and detecting sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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.

source

def category_theory.is_separating {C : Type u₁} [category_theory.category 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

category_theory.is_separating 𝒢 = ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g

source

def category_theory.is_coseparating {C : Type u₁} [category_theory.category 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

category_theory.is_coseparating 𝒢 = ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g

source

def category_theory.is_detecting {C : Type u₁} [category_theory.category 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

category_theory.is_detecting 𝒢 = ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ Y), ∃! (h' : G ⟶ X), h' ≫ f = h) → category_theory.is_iso f

source

def category_theory.is_codetecting {C : Type u₁} [category_theory.category 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

category_theory.is_codetecting 𝒢 = ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C), G ∈ 𝒢 → ∀ (h : X ⟶ G), ∃! (h' : Y ⟶ G), f ≫ h' = h) → category_theory.is_iso f

source

theorem category_theory.is_separating_op_iff {C : Type u₁} [category_theory.category C] (𝒢 : set C) :

category_theory.is_separating 𝒢.op ↔ category_theory.is_coseparating 𝒢

source

theorem category_theory.is_coseparating_op_iff {C : Type u₁} [category_theory.category C] (𝒢 : set C) :

category_theory.is_coseparating 𝒢.op ↔ category_theory.is_separating 𝒢

source

theorem category_theory.is_coseparating_unop_iff {C : Type u₁} [category_theory.category C] (𝒢 : set Cᵒᵖ) :

category_theory.is_coseparating 𝒢.unop ↔ category_theory.is_separating 𝒢

source

theorem category_theory.is_separating_unop_iff {C : Type u₁} [category_theory.category C] (𝒢 : set Cᵒᵖ) :

category_theory.is_separating 𝒢.unop ↔ category_theory.is_coseparating 𝒢

source

theorem category_theory.is_detecting_op_iff {C : Type u₁} [category_theory.category C] (𝒢 : set C) :

category_theory.is_detecting 𝒢.op ↔ category_theory.is_codetecting 𝒢

source

theorem category_theory.is_codetecting_op_iff {C : Type u₁} [category_theory.category C] (𝒢 : set C) :

category_theory.is_codetecting 𝒢.op ↔ category_theory.is_detecting 𝒢

source

theorem category_theory.is_detecting_unop_iff {C : Type u₁} [category_theory.category C] (𝒢 : set Cᵒᵖ) :

category_theory.is_detecting 𝒢.unop ↔ category_theory.is_codetecting 𝒢

source

theorem category_theory.is_codetecting_unop_iff {C : Type u₁} [category_theory.category C] {𝒢 : set Cᵒᵖ} :

category_theory.is_codetecting 𝒢.unop ↔ category_theory.is_detecting 𝒢

source

theorem category_theory.is_detecting.is_separating {C : Type u₁} [category_theory.category C] [category_theory.limits.has_equalizers C] {𝒢 : set C} (h𝒢 : category_theory.is_detecting 𝒢) :

category_theory.is_separating 𝒢

source

theorem category_theory.is_codetecting.is_coseparating {C : Type u₁} [category_theory.category C] [category_theory.limits.has_coequalizers C] {𝒢 : set C} :

category_theory.is_codetecting 𝒢 → category_theory.is_coseparating 𝒢

source

theorem category_theory.is_separating.is_detecting {C : Type u₁} [category_theory.category C] [category_theory.balanced C] {𝒢 : set C} (h𝒢 : category_theory.is_separating 𝒢) :

category_theory.is_detecting 𝒢

source

theorem category_theory.is_coseparating.is_codetecting {C : Type u₁} [category_theory.category C] [category_theory.balanced C] {𝒢 : set C} :

category_theory.is_coseparating 𝒢 → category_theory.is_codetecting 𝒢

source

theorem category_theory.is_detecting_iff_is_separating {C : Type u₁} [category_theory.category C] [category_theory.limits.has_equalizers C] [category_theory.balanced C] (𝒢 : set C) :

category_theory.is_detecting 𝒢 ↔ category_theory.is_separating 𝒢

source

theorem category_theory.is_codetecting_iff_is_coseparating {C : Type u₁} [category_theory.category C] [category_theory.limits.has_coequalizers C] [category_theory.balanced C] {𝒢 : set C} :

category_theory.is_codetecting 𝒢 ↔ category_theory.is_coseparating 𝒢

source

theorem category_theory.is_separating.mono {C : Type u₁} [category_theory.category C] {𝒢 : set C} (h𝒢 : category_theory.is_separating 𝒢) {ℋ : set C} (h𝒢ℋ : 𝒢 ⊆ ℋ) :

category_theory.is_separating ℋ

source

theorem category_theory.is_coseparating.mono {C : Type u₁} [category_theory.category C] {𝒢 : set C} (h𝒢 : category_theory.is_coseparating 𝒢) {ℋ : set C} (h𝒢ℋ : 𝒢 ⊆ ℋ) :

category_theory.is_coseparating ℋ

source

theorem category_theory.is_detecting.mono {C : Type u₁} [category_theory.category C] {𝒢 : set C} (h𝒢 : category_theory.is_detecting 𝒢) {ℋ : set C} (h𝒢ℋ : 𝒢 ⊆ ℋ) :

category_theory.is_detecting ℋ

source

theorem category_theory.is_codetecting.mono {C : Type u₁} [category_theory.category C] {𝒢 : set C} (h𝒢 : category_theory.is_codetecting 𝒢) {ℋ : set C} (h𝒢ℋ : 𝒢 ⊆ ℋ) :

category_theory.is_codetecting ℋ

source

theorem category_theory.thin_of_is_separating_empty {C : Type u₁} [category_theory.category C] (h : category_theory.is_separating ∅) :

quiver.is_thin C

source

theorem category_theory.is_separating_empty_of_thin {C : Type u₁} [category_theory.category C] [quiver.is_thin C] :

category_theory.is_separating ∅

source

theorem category_theory.thin_of_is_coseparating_empty {C : Type u₁} [category_theory.category C] (h : category_theory.is_coseparating ∅) :

quiver.is_thin C

source

theorem category_theory.is_coseparating_empty_of_thin {C : Type u₁} [category_theory.category C] [quiver.is_thin C] :

category_theory.is_coseparating ∅

source

theorem category_theory.groupoid_of_is_detecting_empty {C : Type u₁} [category_theory.category C] (h : category_theory.is_detecting ∅) {X Y : C} (f : X ⟶ Y) :

category_theory.is_iso f

source

theorem category_theory.is_detecting_empty_of_groupoid {C : Type u₁} [category_theory.category C] [∀ {X Y : C} (f : X ⟶ Y), category_theory.is_iso f] :

category_theory.is_detecting ∅

source

theorem category_theory.groupoid_of_is_codetecting_empty {C : Type u₁} [category_theory.category C] (h : category_theory.is_codetecting ∅) {X Y : C} (f : X ⟶ Y) :

category_theory.is_iso f

source

theorem category_theory.is_codetecting_empty_of_groupoid {C : Type u₁} [category_theory.category C] [∀ {X Y : C} (f : X ⟶ Y), category_theory.is_iso f] :

category_theory.is_codetecting ∅

source

theorem category_theory.is_separating_iff_epi {C : Type u₁} [category_theory.category C] (𝒢 : set C) [∀ (A : C), category_theory.limits.has_coproduct (λ (f : Σ (G : ↥𝒢), ↑G ⟶ A), ↑(f.fst))] :

category_theory.is_separating 𝒢 ↔ ∀ (A : C), category_theory.epi (category_theory.limits.sigma.desc sigma.snd)

source

theorem category_theory.is_coseparating_iff_mono {C : Type u₁} [category_theory.category C] (𝒢 : set C) [∀ (A : C), category_theory.limits.has_product (λ (f : Σ (G : ↥𝒢), A ⟶ ↑G), ↑(f.fst))] :

category_theory.is_coseparating 𝒢 ↔ ∀ (A : C), category_theory.mono (category_theory.limits.pi.lift sigma.snd)

source

theorem category_theory.has_initial_of_is_coseparating {C : Type u₁} [category_theory.category C] [category_theory.well_powered C] [category_theory.limits.has_limits C] {𝒢 : set C} [small ↥𝒢] (h𝒢 : category_theory.is_coseparating 𝒢) :

category_theory.limits.has_initial 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 has_colimits_of_has_limits_of_is_coseparating.

source

theorem category_theory.has_terminal_of_is_separating {C : Type u₁} [category_theory.category C] [category_theory.well_powered Cᵒᵖ] [category_theory.limits.has_colimits C] {𝒢 : set C} [small ↥𝒢] (h𝒢 : category_theory.is_separating 𝒢) :

category_theory.limits.has_terminal 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 has_limits_of_has_colimits_of_is_separating.

source

theorem category_theory.subobject.eq_of_le_of_is_detecting {C : Type u₁} [category_theory.category C] {𝒢 : 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

source

theorem category_theory.subobject.inf_eq_of_is_detecting {C : Type u₁} [category_theory.category C] [category_theory.limits.has_pullbacks C] {𝒢 : 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

source

theorem category_theory.subobject.eq_of_is_detecting {C : Type u₁} [category_theory.category C] [category_theory.limits.has_pullbacks C] {𝒢 : 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

source

theorem category_theory.well_powered_of_is_detecting {C : Type u₁} [category_theory.category C] [category_theory.limits.has_pullbacks C] {𝒢 : set C} [small ↥𝒢] (h𝒢 : category_theory.is_detecting 𝒢) :

category_theory.well_powered C

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

source

theorem category_theory.structured_arrow.is_coseparating_proj_preimage {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (S : D) (T : C ⥤ D) {𝒢 : set C} (h𝒢 : category_theory.is_coseparating 𝒢) :

category_theory.is_coseparating ((category_theory.structured_arrow.proj S T).obj ⁻¹' 𝒢)

source

theorem category_theory.costructured_arrow.is_separating_proj_preimage {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (S : C ⥤ D) (T : D) {𝒢 : set C} (h𝒢 : category_theory.is_separating 𝒢) :

category_theory.is_separating ((category_theory.costructured_arrow.proj S T).obj ⁻¹' 𝒢)

source

def category_theory.is_separator {C : Type u₁} [category_theory.category C] (G : C) :

Prop

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

Equations

category_theory.is_separator G = category_theory.is_separating {G}

source

def category_theory.is_coseparator {C : Type u₁} [category_theory.category C] (G : C) :

Prop

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

Equations

category_theory.is_coseparator G = category_theory.is_coseparating {G}

source

def category_theory.is_detector {C : Type u₁} [category_theory.category C] (G : C) :

Prop

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

Equations

category_theory.is_detector G = category_theory.is_detecting {G}

source

def category_theory.is_codetector {C : Type u₁} [category_theory.category C] (G : C) :

Prop

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

Equations

category_theory.is_codetector G = category_theory.is_codetecting {G}

source

theorem category_theory.is_separator_op_iff {C : Type u₁} [category_theory.category C] (G : C) :

category_theory.is_separator (opposite.op G) ↔ category_theory.is_coseparator G

source

theorem category_theory.is_coseparator_op_iff {C : Type u₁} [category_theory.category C] (G : C) :

category_theory.is_coseparator (opposite.op G) ↔ category_theory.is_separator G

source

theorem category_theory.is_coseparator_unop_iff {C : Type u₁} [category_theory.category C] (G : Cᵒᵖ) :

category_theory.is_coseparator (opposite.unop G) ↔ category_theory.is_separator G

source

theorem category_theory.is_separator_unop_iff {C : Type u₁} [category_theory.category C] (G : Cᵒᵖ) :

category_theory.is_separator (opposite.unop G) ↔ category_theory.is_coseparator G

source

theorem category_theory.is_detector_op_iff {C : Type u₁} [category_theory.category C] (G : C) :

category_theory.is_detector (opposite.op G) ↔ category_theory.is_codetector G

source

theorem category_theory.is_codetector_op_iff {C : Type u₁} [category_theory.category C] (G : C) :

category_theory.is_codetector (opposite.op G) ↔ category_theory.is_detector G

source

theorem category_theory.is_codetector_unop_iff {C : Type u₁} [category_theory.category C] (G : Cᵒᵖ) :

category_theory.is_codetector (opposite.unop G) ↔ category_theory.is_detector G

source

theorem category_theory.is_detector_unop_iff {C : Type u₁} [category_theory.category C] (G : Cᵒᵖ) :

category_theory.is_detector (opposite.unop G) ↔ category_theory.is_codetector G

source

theorem category_theory.is_detector.is_separator {C : Type u₁} [category_theory.category C] [category_theory.limits.has_equalizers C] {G : C} :

category_theory.is_detector G → category_theory.is_separator G

source

theorem category_theory.is_codetector.is_coseparator {C : Type u₁} [category_theory.category C] [category_theory.limits.has_coequalizers C] {G : C} :

category_theory.is_codetector G → category_theory.is_coseparator G

source

theorem category_theory.is_separator.is_detector {C : Type u₁} [category_theory.category C] [category_theory.balanced C] {G : C} :

category_theory.is_separator G → category_theory.is_detector G

source

theorem category_theory.is_cospearator.is_codetector {C : Type u₁} [category_theory.category C] [category_theory.balanced C] {G : C} :

category_theory.is_coseparator G → category_theory.is_codetector G

source

theorem category_theory.is_separator_def {C : Type u₁} [category_theory.category C] (G : C) :

category_theory.is_separator G ↔ ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g

source

theorem category_theory.is_separator.def {C : Type u₁} [category_theory.category C] {G : C} :

category_theory.is_separator G → ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g

source

theorem category_theory.is_coseparator_def {C : Type u₁} [category_theory.category C] (G : C) :

category_theory.is_coseparator G ↔ ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g

source

theorem category_theory.is_coseparator.def {C : Type u₁} [category_theory.category C] {G : C} :

category_theory.is_coseparator G → ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g

source

theorem category_theory.is_detector_def {C : Type u₁} [category_theory.category C] (G : C) :

category_theory.is_detector G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ Y), ∃! (h' : G ⟶ X), h' ≫ f = h) → category_theory.is_iso f

source

theorem category_theory.is_detector.def {C : Type u₁} [category_theory.category C] {G : C} :

category_theory.is_detector G → ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ Y), ∃! (h' : G ⟶ X), h' ≫ f = h) → category_theory.is_iso f

source

theorem category_theory.is_codetector_def {C : Type u₁} [category_theory.category C] (G : C) :

category_theory.is_codetector G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : X ⟶ G), ∃! (h' : Y ⟶ G), f ≫ h' = h) → category_theory.is_iso f

source

theorem category_theory.is_codetector.def {C : Type u₁} [category_theory.category C] {G : C} :

category_theory.is_codetector G → ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : X ⟶ G), ∃! (h' : Y ⟶ G), f ≫ h' = h) → category_theory.is_iso f

source

theorem category_theory.is_separator_iff_faithful_coyoneda_obj {C : Type u₁} [category_theory.category C] (G : C) :

category_theory.is_separator G ↔ category_theory.faithful (category_theory.coyoneda.obj (opposite.op G))

source

theorem category_theory.is_coseparator_iff_faithful_yoneda_obj {C : Type u₁} [category_theory.category C] (G : C) :

category_theory.is_coseparator G ↔ category_theory.faithful (category_theory.yoneda.obj G)

source

theorem category_theory.is_separator_iff_epi {C : Type u₁} [category_theory.category C] (G : C) [∀ (A : C), category_theory.limits.has_coproduct (λ (f : G ⟶ A), G)] :

category_theory.is_separator G ↔ ∀ (A : C), category_theory.epi (category_theory.limits.sigma.desc (λ (f : G ⟶ A), f))

source

theorem category_theory.is_coseparator_iff_mono {C : Type u₁} [category_theory.category C] (G : C) [∀ (A : C), category_theory.limits.has_product (λ (f : A ⟶ G), G)] :

category_theory.is_coseparator G ↔ ∀ (A : C), category_theory.mono (category_theory.limits.pi.lift (λ (f : A ⟶ G), f))

source

theorem category_theory.is_separator_coprod {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] (G H : C) [category_theory.limits.has_binary_coproduct G H] :

category_theory.is_separator (G ⨿ H) ↔ category_theory.is_separating {G, H}

source

theorem category_theory.is_separator_coprod_of_is_separator_left {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] (G H : C) [category_theory.limits.has_binary_coproduct G H] (hG : category_theory.is_separator G) :

category_theory.is_separator (G ⨿ H)

source

theorem category_theory.is_separator_coprod_of_is_separator_right {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] (G H : C) [category_theory.limits.has_binary_coproduct G H] (hH : category_theory.is_separator H) :

category_theory.is_separator (G ⨿ H)

source

theorem category_theory.is_separator_sigma {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {β : Type w} (f : β → C) [category_theory.limits.has_coproduct f] :

category_theory.is_separator (∐ f) ↔ category_theory.is_separating (set.range f)

source

theorem category_theory.is_separator_sigma_of_is_separator {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {β : Type w} (f : β → C) [category_theory.limits.has_coproduct f] (b : β) (hb : category_theory.is_separator (f b)) :

category_theory.is_separator (∐ f)

source

theorem category_theory.is_coseparator_prod {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] (G H : C) [category_theory.limits.has_binary_product G H] :

category_theory.is_coseparator (G ⨯ H) ↔ category_theory.is_coseparating {G, H}

source

theorem category_theory.is_coseparator_prod_of_is_coseparator_left {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] (G H : C) [category_theory.limits.has_binary_product G H] (hG : category_theory.is_coseparator G) :

category_theory.is_coseparator (G ⨯ H)

source

theorem category_theory.is_coseparator_prod_of_is_coseparator_right {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] (G H : C) [category_theory.limits.has_binary_product G H] (hH : category_theory.is_coseparator H) :

category_theory.is_coseparator (G ⨯ H)

source

theorem category_theory.is_coseparator_pi {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {β : Type w} (f : β → C) [category_theory.limits.has_product f] :

category_theory.is_coseparator (∏ f) ↔ category_theory.is_coseparating (set.range f)

source

theorem category_theory.is_coseparator_pi_of_is_coseparator {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {β : Type w} (f : β → C) [category_theory.limits.has_product f] (b : β) (hb : category_theory.is_coseparator (f b)) :

category_theory.is_coseparator (∏ f)

source

theorem category_theory.is_detector_iff_reflects_isomorphisms_coyoneda_obj {C : Type u₁} [category_theory.category C] (G : C) :

category_theory.is_detector G ↔ category_theory.reflects_isomorphisms (category_theory.coyoneda.obj (opposite.op G))

source

theorem category_theory.is_codetector_iff_reflects_isomorphisms_yoneda_obj {C : Type u₁} [category_theory.category C] (G : C) :

category_theory.is_codetector G ↔ category_theory.reflects_isomorphisms (category_theory.yoneda.obj G)

source

theorem category_theory.well_powered_of_is_detector {C : Type u₁} [category_theory.category C] [category_theory.limits.has_pullbacks C] (G : C) (hG : category_theory.is_detector G) :

category_theory.well_powered C