Documentation

Mathlib.CategoryTheory.Generator.Basic

Separating and detecting sets #

There are several non-equivalent notions of a generator of a category. Here, we consider two of them:

There are, of course, also the dual notions of coseparating and codetecting sets.

Main results #

We

Future work #

def CategoryTheory.IsSeparating {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] (๐’ข : Set C) :

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

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
def CategoryTheory.IsDetecting {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] (๐’ข : Set C) :

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

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
theorem CategoryTheory.IsSeparating.of_equivalence {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] {๐’ข : Set C} (h : IsSeparating ๐’ข) {D : Type u_1} [Category.{u_2, u_1} D] (ฮฑ : C โ‰Œ D) :
IsSeparating (ฮฑ.functor.obj '' ๐’ข)
theorem CategoryTheory.IsCoseparating.of_equivalence {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] {๐’ข : Set C} (h : IsCoseparating ๐’ข) {D : Type u_1} [Category.{u_2, u_1} D] (ฮฑ : C โ‰Œ D) :
IsCoseparating (ฮฑ.functor.obj '' ๐’ข)
theorem CategoryTheory.isSeparating_op_iff {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] (๐’ข : Set C) :
IsSeparating ๐’ข.op โ†” IsCoseparating ๐’ข
theorem CategoryTheory.isDetecting_op_iff {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] (๐’ข : Set C) :
IsDetecting ๐’ข.op โ†” IsCodetecting ๐’ข
theorem CategoryTheory.isCodetecting_op_iff {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] (๐’ข : Set C) :
IsCodetecting ๐’ข.op โ†” IsDetecting ๐’ข
theorem CategoryTheory.IsDetecting.isSeparating {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] [Limits.HasEqualizers C] {๐’ข : Set C} (h๐’ข : IsDetecting ๐’ข) :
IsSeparating ๐’ข
theorem CategoryTheory.IsSeparating.isDetecting {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] [Balanced C] {๐’ข : Set C} (h๐’ข : IsSeparating ๐’ข) :
IsDetecting ๐’ข
theorem CategoryTheory.IsDetecting.isIso_iff_of_mono {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] {๐’ข : Set C} (h๐’ข : IsDetecting ๐’ข) {X Y : C} (f : X โŸถ Y) [Mono f] :
IsIso f โ†” โˆ€ s โˆˆ ๐’ข, Function.Surjective ((coyoneda.obj (Opposite.op s)).map f)
theorem CategoryTheory.IsCodetecting.isIso_iff_of_epi {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] {๐’ข : Set C} (h๐’ข : IsCodetecting ๐’ข) {X Y : C} (f : X โŸถ Y) [Epi f] :
IsIso f โ†” โˆ€ s โˆˆ ๐’ข, Function.Surjective ((yoneda.obj s).map f.op)
theorem CategoryTheory.IsCoseparating.isCodetecting {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] [Balanced C] {๐’ข : Set C} :
IsCoseparating ๐’ข โ†’ IsCodetecting ๐’ข
theorem CategoryTheory.IsSeparating.mono {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] {๐’ข : Set C} (h๐’ข : IsSeparating ๐’ข) {โ„‹ : Set C} (h๐’ขโ„‹ : ๐’ข โІ โ„‹) :
IsSeparating โ„‹
theorem CategoryTheory.IsCoseparating.mono {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] {๐’ข : Set C} (h๐’ข : IsCoseparating ๐’ข) {โ„‹ : Set C} (h๐’ขโ„‹ : ๐’ข โІ โ„‹) :
theorem CategoryTheory.IsDetecting.mono {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] {๐’ข : Set C} (h๐’ข : IsDetecting ๐’ข) {โ„‹ : Set C} (h๐’ขโ„‹ : ๐’ข โІ โ„‹) :
IsDetecting โ„‹
theorem CategoryTheory.IsCodetecting.mono {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] {๐’ข : Set C} (h๐’ข : IsCodetecting ๐’ข) {โ„‹ : Set C} (h๐’ขโ„‹ : ๐’ข โІ โ„‹) :
theorem CategoryTheory.isSeparating_iff_epi {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] (๐’ข : Set C) [โˆ€ (A : C), Limits.HasCoproduct fun (f : (G : โ†‘๐’ข) ร— (โ†‘G โŸถ A)) => โ†‘f.fst] :
IsSeparating ๐’ข โ†” โˆ€ (A : C), Epi (Limits.Sigma.desc Sigma.snd)
theorem CategoryTheory.isCoseparating_iff_mono {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] (๐’ข : Set C) [โˆ€ (A : C), Limits.HasProduct fun (f : (G : โ†‘๐’ข) ร— (A โŸถ โ†‘G)) => โ†‘f.fst] :
IsCoseparating ๐’ข โ†” โˆ€ (A : C), Mono (Limits.Pi.lift Sigma.snd)

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.

An ingredient of the proof of the Special Adjoint Functor Theorem: a cocomplete well-copowered category with a small separating set has a terminal object.

In fact, it follows from the Special Adjoint Functor Theorem that C is already complete, see hasLimits_of_hasColimits_of_isSeparating.

theorem CategoryTheory.Subobject.eq_of_le_of_isDetecting {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] {๐’ข : Set C} (h๐’ข : IsDetecting ๐’ข) {X : C} (P Q : Subobject X) (hโ‚ : P โ‰ค Q) (hโ‚‚ : โˆ€ G โˆˆ ๐’ข, โˆ€ {f : G โŸถ X}, Q.Factors f โ†’ P.Factors f) :
P = Q
theorem CategoryTheory.Subobject.inf_eq_of_isDetecting {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] [Limits.HasPullbacks C] {๐’ข : Set C} (h๐’ข : IsDetecting ๐’ข) {X : C} (P Q : Subobject X) (h : โˆ€ G โˆˆ ๐’ข, โˆ€ {f : G โŸถ X}, P.Factors f โ†’ Q.Factors f) :
P โŠ“ Q = P
theorem CategoryTheory.Subobject.eq_of_isDetecting {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] [Limits.HasPullbacks C] {๐’ข : Set C} (h๐’ข : IsDetecting ๐’ข) {X : C} (P Q : Subobject X) (h : โˆ€ G โˆˆ ๐’ข, โˆ€ {f : G โŸถ X}, P.Factors f โ†” Q.Factors f) :
P = Q

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

theorem CategoryTheory.StructuredArrow.isCoseparating_proj_preimage {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] {D : Type uโ‚‚} [Category.{vโ‚‚, uโ‚‚} D] (S : D) (T : Functor C D) {๐’ข : Set C} (h๐’ข : IsCoseparating ๐’ข) :
theorem CategoryTheory.CostructuredArrow.isSeparating_proj_preimage {C : Type uโ‚} [Category.{vโ‚, uโ‚} C] {D : Type uโ‚‚} [Category.{vโ‚‚, uโ‚‚} D] (S : Functor C D) (T : D) {๐’ข : Set C} (h๐’ข : IsSeparating ๐’ข) :

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

Equations

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

Equations

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

Equations

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

Equations
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_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_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)) :

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.

Instances

    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.

    Instances

      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.

      Instances

        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.

        Instances
          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

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

          Equations
          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

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

          Equations