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 P : ObjectProperty C is a separating set if the functors C(G, -) for G such that P G are collectively faithful, i.e., if h ≫ f = h ≫ g for all h with domain satisfying P implies f = g.
• We say that P : ObjectProperty C is a detecting set if the functors C(G, -) collectively reflect isomorphisms, i.e., if any h with domain satisfying P 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 ObjectProperty C;
• 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.

Examples

See the files CategoryTheory.Generator.Presheaf and CategoryTheory.Generator.Sheaf.

def CategoryTheory.ObjectProperty.IsSeparating {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) : Prop

We say that P : ObjectProperty C is separating if the functors C(G, -) for G : C such that P G are collectively faithful, i.e., if h ≫ f = h ≫ g for all h with domain in 𝒢 implies f = g.

Equations

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

def CategoryTheory.ObjectProperty.IsCoseparating {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) : Prop

We say that P : ObjectProperty C is coseparating if the functors C(-, G) for G : C such that P G are collectively faithful, i.e., if f ≫ h = g ≫ h for all h with codomain in 𝒢 implies f = g.

Equations

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

def CategoryTheory.ObjectProperty.IsDetecting {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) : Prop

We say that P : ObjectProperty C is detecting if the functors C(G, -) for G : C such that P G collectively reflect isomorphisms, i.e., if any h with domain G that P G uniquely factors through f, then f is an isomorphism.

Equations

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

def CategoryTheory.ObjectProperty.IsCodetecting {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) : Prop

We say that P : ObjectProperty C is codetecting if the functors C(-, G) for G : C such that P G collectively reflect isomorphisms, i.e., if any h with codomain G such that P G uniquely factors through f, then f is an isomorphism.

Equations

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

theorem CategoryTheory.ObjectProperty.IsSeparating.of_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (h : P.IsSeparating) {D : Type u_1} [Category.{u_2, u_1} D] (α : C ≌ D) : (P.strictMap α.functor).IsSeparating

theorem CategoryTheory.ObjectProperty.IsCoseparating.of_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (h : P.IsCoseparating) {D : Type u_1} [Category.{u_2, u_1} D] (α : C ≌ D) : (P.strictMap α.functor).IsCoseparating

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

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

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

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

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

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

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

theorem CategoryTheory.ObjectProperty.isCodetecting_unop_iff {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty Cᵒᵖ) : P.unop.IsCodetecting ↔ P.IsDetecting

theorem CategoryTheory.ObjectProperty.IsDetecting.isSeparating {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} [Limits.HasEqualizers C] (hP : P.IsDetecting) : P.IsSeparating

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

theorem CategoryTheory.ObjectProperty.IsSeparating.isDetecting {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} [Balanced C] (hP : P.IsSeparating) : P.IsDetecting

theorem CategoryTheory.ObjectProperty.IsDetecting.isIso_iff_of_mono {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (hP : P.IsDetecting) {X Y : C} (f : X ⟶ Y) [Mono f] : IsIso f ↔ ∀ (G : C), P G → Function.Surjective ((coyoneda.obj (Opposite.op G)).map f)

theorem CategoryTheory.ObjectProperty.IsCodetecting.isIso_iff_of_epi {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (hP : P.IsCodetecting) {X Y : C} (f : X ⟶ Y) [Epi f] : IsIso f ↔ ∀ (G : C), P G → Function.Surjective ((yoneda.obj G).map f.op)

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

theorem CategoryTheory.ObjectProperty.isDetecting_iff_isSeparating {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} [Limits.HasEqualizers C] [Balanced C] : P.IsDetecting ↔ P.IsSeparating

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

theorem CategoryTheory.ObjectProperty.IsSeparating.of_le {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (hP : P.IsSeparating) {Q : ObjectProperty C} (h : P ≤ Q) : Q.IsSeparating

theorem CategoryTheory.ObjectProperty.IsCoseparating.of_le {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (hP : P.IsCoseparating) {Q : ObjectProperty C} (h : P ≤ Q) : Q.IsCoseparating

theorem CategoryTheory.ObjectProperty.IsDetecting.of_le {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (hP : P.IsDetecting) {Q : ObjectProperty C} (h : P ≤ Q) : Q.IsDetecting

theorem CategoryTheory.ObjectProperty.IsCodetecting.of_le {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (h𝒢 : P.IsCodetecting) {Q : ObjectProperty C} (h : P ≤ Q) : Q.IsCodetecting

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

theorem CategoryTheory.ObjectProperty.isSeparating_bot_of_isThin {C : Type u₁} [Category.{v₁, u₁} C] [Quiver.IsThin C] : ⊥.IsSeparating

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

theorem CategoryTheory.ObjectProperty.isCoseparating_bot_of_isThin {C : Type u₁} [Category.{v₁, u₁} C] [Quiver.IsThin C] : ⊥.IsCoseparating

theorem CategoryTheory.ObjectProperty.isGroupoid_of_isDetecting_bot {C : Type u₁} [Category.{v₁, u₁} C] (h : ⊥.IsDetecting) : IsGroupoid C

theorem CategoryTheory.ObjectProperty.isDetecting_bot_of_isGroupoid {C : Type u₁} [Category.{v₁, u₁} C] [IsGroupoid C] : ⊥.IsDetecting

theorem CategoryTheory.ObjectProperty.isGroupoid_of_isCodetecting_bot {C : Type u₁} [Category.{v₁, u₁} C] (h : ⊥.IsCodetecting) : IsGroupoid C

theorem CategoryTheory.ObjectProperty.isCodetecting_bot_of_isGroupoid {C : Type u₁} [Category.{v₁, u₁} C] [IsGroupoid C] : ⊥.IsCodetecting

theorem CategoryTheory.ObjectProperty.IsSeparating.mk_of_exists_epi {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (hP : ∀ (X : C), ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Limits.Cofan s) (x : Limits.IsColimit c) (p : c.pt ⟶ X), Epi p) : P.IsSeparating

theorem CategoryTheory.ObjectProperty.IsCoseparating.mk_of_exists_mono {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (hP : ∀ (X : C), ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Limits.Fan s) (x : Limits.IsLimit c) (j : X ⟶ c.pt), Mono j) : P.IsCoseparating

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.coproductFromFamily {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) (X : C) (i : CostructuredArrow P.ι X) : C

Given P : ObjectProperty C and X : C, this is the map which sends i : CostructuredArrow P.ι X to i.left.obj : C. The coproduct of this family is the source of the morphism P.coproductFrom X.

Equations

• P.coproductFromFamily X i = i.left.obj

@[reducible, inline]

noncomputable abbrev CategoryTheory.ObjectProperty.coproductFrom {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) (X : C) [Limits.HasCoproduct (P.coproductFromFamily X)] : ∐ P.coproductFromFamily X ⟶ X

Given P : ObjectProperty C and X : C, this is the coproduct of all the morphisms Y ⟶ X such that P Y holds.

Equations

• P.coproductFrom X = CategoryTheory.Limits.Sigma.desc fun (i : CategoryTheory.CostructuredArrow P.ι X) => i.hom

@[reducible, inline]

noncomputable abbrev CategoryTheory.ObjectProperty.ιCoproductFrom {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) {X : C} [Limits.HasCoproduct (P.coproductFromFamily X)] {Y : C} (f : Y ⟶ X) (hY : P Y) : Y ⟶ ∐ P.coproductFromFamily X

The inclusion morphisms to ∐ (P.coproductFromFamily X).

Equations

• P.ιCoproductFrom f hY = CategoryTheory.Limits.Sigma.ι (P.coproductFromFamily X) (CategoryTheory.CostructuredArrow.mk f)

theorem CategoryTheory.ObjectProperty.IsSeparating.epi_coproductFrom {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (hP : P.IsSeparating) (X : C) [Limits.HasCoproduct (P.coproductFromFamily X)] : Epi (P.coproductFrom X)

theorem CategoryTheory.ObjectProperty.isSeparating_iff_epi {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) [∀ (X : C), Limits.HasCoproduct (P.coproductFromFamily X)] : P.IsSeparating ↔ ∀ (X : C), Epi (P.coproductFrom X)

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.productToFamily {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) (X : C) (i : StructuredArrow X P.ι) : C

Given P : ObjectProperty C and X : C, this is the map which sends i : StructuredArrow P.ι X to i.right.obj : C. The product of this family is the target of the morphism P.productTo X.

Equations

• P.productToFamily X i = i.right.obj

@[reducible, inline]

noncomputable abbrev CategoryTheory.ObjectProperty.productTo {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) (X : C) [Limits.HasProduct (P.productToFamily X)] : X ⟶ ∏ᶜ P.productToFamily X

Given P : ObjectProperty C and X : C, this is the product of all the morphisms X ⟶ Y such that P Y holds.

Equations

• P.productTo X = CategoryTheory.Limits.Pi.lift fun (i : CategoryTheory.StructuredArrow X P.ι) => i.hom

@[reducible, inline]

noncomputable abbrev CategoryTheory.ObjectProperty.πProductTo {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) {X : C} [Limits.HasProduct (P.productToFamily X)] {Y : C} (f : X ⟶ Y) (hY : P Y) : ∏ᶜ P.productToFamily X ⟶ Y

The projection morphisms from ∏ᶜ (P.productToFamily X).

Equations

• P.πProductTo f hY = CategoryTheory.Limits.Pi.π (P.productToFamily X) (CategoryTheory.StructuredArrow.mk f)

theorem CategoryTheory.ObjectProperty.IsCoseparating.mono_productTo {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (hP : P.IsCoseparating) (X : C) [Limits.HasProduct (P.productToFamily X)] : Mono (P.productTo X)

theorem CategoryTheory.ObjectProperty.isCoseparating_iff_mono {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) [∀ (X : C), Limits.HasProduct (P.productToFamily X)] : P.IsCoseparating ↔ ∀ (X : C), Mono (P.productTo X)

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] {P : ObjectProperty C} [ObjectProperty.Small.{w, v₁, u₁} P] (hP : P.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] {P : ObjectProperty C} [ObjectProperty.Small.{w, v₁, u₁} P] (hP : P.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] {𝒢 : ObjectProperty C} (h𝒢 : 𝒢.IsDetecting) {X : C} (P Q : Subobject X) (h₁ : P ≤ Q) (h₂ : ∀ (G : C), 𝒢 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] {𝒢 : ObjectProperty C} (h𝒢 : 𝒢.IsDetecting) {X : C} (P Q : Subobject X) (h : ∀ (G : C), 𝒢 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] {𝒢 : ObjectProperty C} (h𝒢 : 𝒢.IsDetecting) {X : C} (P Q : Subobject X) (h : ∀ (G : C), 𝒢 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] {𝒢 : ObjectProperty C} [ObjectProperty.Small.{w, v₁, 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_inverseImage_proj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (S : D) (T : Functor C D) {P : ObjectProperty C} (hP : P.IsCoseparating) : (P.inverseImage (proj S T)).IsCoseparating

theorem CategoryTheory.CostructuredArrow.isSeparating_inverseImage_proj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (S : Functor C D) (T : D) {P : ObjectProperty C} (hP : P.IsSeparating) : (P.inverseImage (proj S T)).IsSeparating

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.ObjectProperty.singleton G).IsSeparating

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.ObjectProperty.singleton G).IsCoseparating

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.ObjectProperty.singleton G).IsDetecting

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.ObjectProperty.singleton G).IsCodetecting

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_of_isColimit_cofan {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {β : Type w} {f : β → C} (hf : (ObjectProperty.ofObj f).IsSeparating) {c : Limits.Cofan f} (hc : Limits.IsColimit c) : IsSeparator c.pt

theorem CategoryTheory.isSeparator_iff_of_isColimit_cofan {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {β : Type w} {f : β → C} {c : Limits.Cofan f} (hc : Limits.IsColimit c) : IsSeparator c.pt ↔ (ObjectProperty.ofObj f).IsSeparating

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

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

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.ObjectProperty.IsSeparating.isSeparator_coproduct {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {β : Type w} {f : β → C} [Limits.HasCoproduct f] (hS : (ofObj f).IsSeparating) : 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_of_isLimit_fan {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {β : Type w} {f : β → C} (hf : (ObjectProperty.ofObj f).IsCoseparating) {c : Limits.Fan f} (hc : Limits.IsLimit c) : IsCoseparator c.pt

theorem CategoryTheory.isCoseparator_iff_of_isLimit_fan {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {β : Type w} {f : β → C} {c : Limits.Fan f} (hc : Limits.IsLimit c) : IsCoseparator c.pt ↔ (ObjectProperty.ofObj f).IsCoseparating

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

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

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_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

@[deprecated CategoryTheory.ObjectProperty.IsSeparating (since := "2025-10-06")]

def CategoryTheory.IsSeparating {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) : Prop

Alias of CategoryTheory.ObjectProperty.IsSeparating.

---

We say that P : ObjectProperty C is separating if the functors C(G, -) for G : C such that P G are collectively faithful, i.e., if h ≫ f = h ≫ g for all h with domain in 𝒢 implies f = g.

Equations

• @CategoryTheory.IsSeparating = @CategoryTheory.ObjectProperty.IsSeparating

@[deprecated CategoryTheory.ObjectProperty.IsCoseparating (since := "2025-10-06")]

def CategoryTheory.IsCoseparating {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) : Prop

Alias of CategoryTheory.ObjectProperty.IsCoseparating.

---

We say that P : ObjectProperty C is coseparating if the functors C(-, G) for G : C such that P G are collectively faithful, i.e., if f ≫ h = g ≫ h for all h with codomain in 𝒢 implies f = g.

Equations

• @CategoryTheory.IsCoseparating = @CategoryTheory.ObjectProperty.IsCoseparating

@[deprecated CategoryTheory.ObjectProperty.IsDetecting (since := "2025-10-06")]

def CategoryTheory.IsDetecting {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) : Prop

Alias of CategoryTheory.ObjectProperty.IsDetecting.

---

We say that P : ObjectProperty C is detecting if the functors C(G, -) for G : C such that P G collectively reflect isomorphisms, i.e., if any h with domain G that P G uniquely factors through f, then f is an isomorphism.

Equations

• @CategoryTheory.IsDetecting = @CategoryTheory.ObjectProperty.IsDetecting

@[deprecated CategoryTheory.ObjectProperty.IsCodetecting (since := "2025-10-06")]

def CategoryTheory.IsCodetecting {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) : Prop

Alias of CategoryTheory.ObjectProperty.IsCodetecting.

---

We say that P : ObjectProperty C is codetecting if the functors C(-, G) for G : C such that P G collectively reflect isomorphisms, i.e., if any h with codomain G such that P G uniquely factors through f, then f is an isomorphism.

Equations

• @CategoryTheory.IsCodetecting = @CategoryTheory.ObjectProperty.IsCodetecting

@[deprecated CategoryTheory.ObjectProperty.IsSeparating.of_equivalence (since := "2025-10-06")]

theorem CategoryTheory.IsSeparating.of_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (h : P.IsSeparating) {D : Type u_1} [Category.{u_2, u_1} D] (α : C ≌ D) : (P.strictMap α.functor).IsSeparating

Alias of CategoryTheory.ObjectProperty.IsSeparating.of_equivalence.

@[deprecated CategoryTheory.ObjectProperty.IsCoseparating.of_equivalence (since := "2025-10-06")]

theorem CategoryTheory.IsCoseparating.of_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (h : P.IsCoseparating) {D : Type u_1} [Category.{u_2, u_1} D] (α : C ≌ D) : (P.strictMap α.functor).IsCoseparating

Alias of CategoryTheory.ObjectProperty.IsCoseparating.of_equivalence.

@[deprecated CategoryTheory.ObjectProperty.isSeparating_op_iff (since := "2025-10-06")]

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

Alias of CategoryTheory.ObjectProperty.isSeparating_op_iff.

@[deprecated CategoryTheory.ObjectProperty.isCoseparating_op_iff (since := "2025-10-06")]

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

Alias of CategoryTheory.ObjectProperty.isCoseparating_op_iff.

@[deprecated CategoryTheory.ObjectProperty.isSeparating_op_iff (since := "2025-10-06")]

theorem CategoryTheory.isSeparating_unop_iff {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) : P.op.IsSeparating ↔ P.IsCoseparating

Alias of CategoryTheory.ObjectProperty.isSeparating_op_iff.

@[deprecated CategoryTheory.ObjectProperty.isCoseparating_op_iff (since := "2025-10-06")]

theorem CategoryTheory.isCoseparating_unop_iff {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) : P.op.IsCoseparating ↔ P.IsSeparating

Alias of CategoryTheory.ObjectProperty.isCoseparating_op_iff.

@[deprecated CategoryTheory.ObjectProperty.isDetecting_op_iff (since := "2025-10-06")]

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

Alias of CategoryTheory.ObjectProperty.isDetecting_op_iff.

@[deprecated CategoryTheory.ObjectProperty.isCodetecting_op_iff (since := "2025-10-06")]

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

Alias of CategoryTheory.ObjectProperty.isCodetecting_op_iff.

@[deprecated CategoryTheory.ObjectProperty.isDetecting_op_iff (since := "2025-10-06")]

theorem CategoryTheory.isDetecting_unop_iff {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) : P.op.IsDetecting ↔ P.IsCodetecting

Alias of CategoryTheory.ObjectProperty.isDetecting_op_iff.

@[deprecated CategoryTheory.ObjectProperty.isCodetecting_op_iff (since := "2025-10-06")]

theorem CategoryTheory.isCodetecting_unop_iff {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) : P.op.IsCodetecting ↔ P.IsDetecting

Alias of CategoryTheory.ObjectProperty.isCodetecting_op_iff.

@[deprecated CategoryTheory.ObjectProperty.IsDetecting.isSeparating (since := "2025-10-06")]

theorem CategoryTheory.IsDetecting.isSeparating {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} [Limits.HasEqualizers C] (hP : P.IsDetecting) : P.IsSeparating

Alias of CategoryTheory.ObjectProperty.IsDetecting.isSeparating.

@[deprecated CategoryTheory.ObjectProperty.IsCodetecting.isCoseparating (since := "2025-10-06")]

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

Alias of CategoryTheory.ObjectProperty.IsCodetecting.isCoseparating.

@[deprecated CategoryTheory.ObjectProperty.IsSeparating.isDetecting (since := "2025-10-06")]

theorem CategoryTheory.IsSeparating.isDetecting {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} [Balanced C] (hP : P.IsSeparating) : P.IsDetecting

Alias of CategoryTheory.ObjectProperty.IsSeparating.isDetecting.

@[deprecated CategoryTheory.ObjectProperty.IsDetecting.isIso_iff_of_mono (since := "2025-10-06")]

theorem CategoryTheory.IsDetecting.isIso_iff_of_mono {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (hP : P.IsDetecting) {X Y : C} (f : X ⟶ Y) [Mono f] : IsIso f ↔ ∀ (G : C), P G → Function.Surjective ((coyoneda.obj (Opposite.op G)).map f)

Alias of CategoryTheory.ObjectProperty.IsDetecting.isIso_iff_of_mono.

@[deprecated CategoryTheory.ObjectProperty.IsCodetecting.isIso_iff_of_epi (since := "2025-10-06")]

theorem CategoryTheory.IsCodetecting.isIso_iff_of_epi {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (hP : P.IsCodetecting) {X Y : C} (f : X ⟶ Y) [Epi f] : IsIso f ↔ ∀ (G : C), P G → Function.Surjective ((yoneda.obj G).map f.op)

Alias of CategoryTheory.ObjectProperty.IsCodetecting.isIso_iff_of_epi.

@[deprecated CategoryTheory.ObjectProperty.IsCoseparating.isCodetecting (since := "2025-10-06")]

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

Alias of CategoryTheory.ObjectProperty.IsCoseparating.isCodetecting.

@[deprecated CategoryTheory.ObjectProperty.isDetecting_iff_isSeparating (since := "2025-10-06")]

theorem CategoryTheory.isDetecting_iff_isSeparating {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} [Limits.HasEqualizers C] [Balanced C] : P.IsDetecting ↔ P.IsSeparating

Alias of CategoryTheory.ObjectProperty.isDetecting_iff_isSeparating.

@[deprecated CategoryTheory.ObjectProperty.isCodetecting_iff_isCoseparating (since := "2025-10-06")]

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

Alias of CategoryTheory.ObjectProperty.isCodetecting_iff_isCoseparating.

@[deprecated CategoryTheory.ObjectProperty.IsSeparating.of_le (since := "2025-10-06")]

theorem CategoryTheory.IsSeparating.mono {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (hP : P.IsSeparating) {Q : ObjectProperty C} (h : P ≤ Q) : Q.IsSeparating

Alias of CategoryTheory.ObjectProperty.IsSeparating.of_le.

@[deprecated CategoryTheory.ObjectProperty.IsCoseparating.of_le (since := "2025-10-06")]

theorem CategoryTheory.IsCoseparating.mono {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (hP : P.IsCoseparating) {Q : ObjectProperty C} (h : P ≤ Q) : Q.IsCoseparating

Alias of CategoryTheory.ObjectProperty.IsCoseparating.of_le.

@[deprecated CategoryTheory.ObjectProperty.IsDetecting.of_le (since := "2025-10-06")]

theorem CategoryTheory.IsDetecting.mono {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (hP : P.IsDetecting) {Q : ObjectProperty C} (h : P ≤ Q) : Q.IsDetecting

Alias of CategoryTheory.ObjectProperty.IsDetecting.of_le.

@[deprecated CategoryTheory.ObjectProperty.IsCodetecting.of_le (since := "2025-10-06")]

theorem CategoryTheory.IsCodetecting.mono {C : Type u₁} [Category.{v₁, u₁} C] {P : ObjectProperty C} (h𝒢 : P.IsCodetecting) {Q : ObjectProperty C} (h : P ≤ Q) : Q.IsCodetecting

Alias of CategoryTheory.ObjectProperty.IsCodetecting.of_le.

@[deprecated CategoryTheory.ObjectProperty.isThin_of_isSeparating_bot (since := "2025-10-06")]

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

Alias of CategoryTheory.ObjectProperty.isThin_of_isSeparating_bot.

@[deprecated CategoryTheory.ObjectProperty.isSeparating_bot_of_isThin (since := "2025-10-06")]

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

Alias of CategoryTheory.ObjectProperty.isSeparating_bot_of_isThin.

@[deprecated CategoryTheory.ObjectProperty.isThin_of_isCoseparating_bot (since := "2025-10-06")]

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

Alias of CategoryTheory.ObjectProperty.isThin_of_isCoseparating_bot.

@[deprecated CategoryTheory.ObjectProperty.isCoseparating_bot_of_isThin (since := "2025-10-06")]

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

Alias of CategoryTheory.ObjectProperty.isCoseparating_bot_of_isThin.

@[deprecated CategoryTheory.ObjectProperty.isGroupoid_of_isDetecting_bot (since := "2025-10-06")]

theorem CategoryTheory.groupoid_of_isDetecting_empty {C : Type u₁} [Category.{v₁, u₁} C] (h : ⊥.IsDetecting) : IsGroupoid C

Alias of CategoryTheory.ObjectProperty.isGroupoid_of_isDetecting_bot.

@[deprecated CategoryTheory.ObjectProperty.isDetecting_bot_of_isGroupoid (since := "2025-10-06")]

theorem CategoryTheory.isDetecting_empty_of_groupoid {C : Type u₁} [Category.{v₁, u₁} C] [IsGroupoid C] : ⊥.IsDetecting

Alias of CategoryTheory.ObjectProperty.isDetecting_bot_of_isGroupoid.

@[deprecated CategoryTheory.ObjectProperty.isGroupoid_of_isCodetecting_bot (since := "2025-10-06")]

theorem CategoryTheory.groupoid_of_isCodetecting_empty {C : Type u₁} [Category.{v₁, u₁} C] (h : ⊥.IsCodetecting) : IsGroupoid C

Alias of CategoryTheory.ObjectProperty.isGroupoid_of_isCodetecting_bot.

@[deprecated CategoryTheory.ObjectProperty.isCodetecting_bot_of_isGroupoid (since := "2025-10-06")]

theorem CategoryTheory.isCodetecting_empty_of_groupoid {C : Type u₁} [Category.{v₁, u₁} C] [IsGroupoid C] : ⊥.IsCodetecting

Alias of CategoryTheory.ObjectProperty.isCodetecting_bot_of_isGroupoid.

@[deprecated CategoryTheory.ObjectProperty.isSeparating_iff_epi (since := "2025-10-07")]

theorem CategoryTheory.isSeparating_iff_epi {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) [∀ (X : C), Limits.HasCoproduct (P.coproductFromFamily X)] : P.IsSeparating ↔ ∀ (X : C), Epi (P.coproductFrom X)

Alias of CategoryTheory.ObjectProperty.isSeparating_iff_epi.

@[deprecated CategoryTheory.ObjectProperty.isCoseparating_iff_mono (since := "2025-10-07")]

theorem CategoryTheory.isCoseparating_iff_mono {C : Type u₁} [Category.{v₁, u₁} C] (P : ObjectProperty C) [∀ (X : C), Limits.HasProduct (P.productToFamily X)] : P.IsCoseparating ↔ ∀ (X : C), Mono (P.productTo X)

Alias of CategoryTheory.ObjectProperty.isCoseparating_iff_mono.

@[deprecated CategoryTheory.ObjectProperty.IsSeparating.isSeparator_coproduct (since := "2025-10-07")]

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

Alias of CategoryTheory.ObjectProperty.IsSeparating.isSeparator_coproduct.

@[deprecated CategoryTheory.StructuredArrow.isCoseparating_inverseImage_proj (since := "2025-10-07")]

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) {P : ObjectProperty C} (hP : P.IsCoseparating) : (P.inverseImage (proj S T)).IsCoseparating

Alias of CategoryTheory.StructuredArrow.isCoseparating_inverseImage_proj.

@[deprecated CategoryTheory.CostructuredArrow.isSeparating_inverseImage_proj (since := "2025-10-07")]

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) {P : ObjectProperty C} (hP : P.IsSeparating) : (P.inverseImage (proj S T)).IsSeparating

Alias of CategoryTheory.CostructuredArrow.isSeparating_inverseImage_proj.