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.

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.

    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.

      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.

        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๐’ขโ„‹ : ๐’ข โŠ† โ„‹) :

          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 : C), G โˆˆ ๐’ข โ†’ โˆ€ {f : G โŸถ X}, CategoryTheory.Subobject.Factors Q f โ†’ CategoryTheory.Subobject.Factors P 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.

          Instances For

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

            Instances For

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

              Instances For

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

                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', 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', 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', 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', CategoryTheory.CategoryStruct.comp f h' = h) โ†’ CategoryTheory.IsIso f