Documentation

Mathlib.CategoryTheory.Generator

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 #

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
Instances For

    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
    Instances For

      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
      Instances For

        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
        Instances For
          theorem CategoryTheory.IsSeparating.mono {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {๐’ข : Set C} (h๐’ข : CategoryTheory.IsSeparating ๐’ข) {โ„‹ : Set C} (h๐’ขโ„‹ : ๐’ข โŠ† โ„‹) :
          theorem CategoryTheory.IsCoseparating.mono {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {๐’ข : Set C} (h๐’ข : CategoryTheory.IsCoseparating ๐’ข) {โ„‹ : Set C} (h๐’ขโ„‹ : ๐’ข โŠ† โ„‹) :
          theorem CategoryTheory.IsDetecting.mono {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {๐’ข : Set C} (h๐’ข : CategoryTheory.IsDetecting ๐’ข) {โ„‹ : Set C} (h๐’ขโ„‹ : ๐’ข โŠ† โ„‹) :
          theorem CategoryTheory.IsCodetecting.mono {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {๐’ข : Set C} (h๐’ข : CategoryTheory.IsCodetecting ๐’ข) {โ„‹ : Set C} (h๐’ขโ„‹ : ๐’ข โŠ† โ„‹) :
          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] :
          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] :

          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โ‚} [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}, Q.Factors f โ†’ P.Factors f) :
          P = Q
          theorem CategoryTheory.Subobject.inf_eq_of_isDetecting {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] [CategoryTheory.Limits.HasPullbacks C] {๐’ข : Set C} (h๐’ข : CategoryTheory.IsDetecting ๐’ข) {X : C} (P : CategoryTheory.Subobject X) (Q : CategoryTheory.Subobject X) (h : โˆ€ G โˆˆ ๐’ข, โˆ€ {f : G โŸถ X}, P.Factors f โ†’ Q.Factors f) :
          P โŠ“ Q = P
          theorem CategoryTheory.Subobject.eq_of_isDetecting {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] [CategoryTheory.Limits.HasPullbacks C] {๐’ข : Set C} (h๐’ข : CategoryTheory.IsDetecting ๐’ข) {X : C} (P : CategoryTheory.Subobject X) (Q : CategoryTheory.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.

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

          Equations
          Instances For

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

            Equations
            Instances For

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

              Equations
              Instances For

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

                Equations
                Instances For
                  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.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