CategoryTheory.IsSeparating.mono
theorem CategoryTheory.IsSeparating.mono :
โ {C : Type uโ} [inst : CategoryTheory.Category.{vโ, uโ} C] {๐ข : Set C},
CategoryTheory.IsSeparating ๐ข โ โ {โ : Set C}, ๐ข โ โ โ CategoryTheory.IsSeparating โ
The theorem `CategoryTheory.IsSeparating.mono` states that, given any category `C` and any set `๐ข` of objects from `C` that is a separating set, then for any other set of objects `โ` from `C` such that `๐ข` is a subset of `โ`, `โ` is also a separating set. Here, a separating set is defined as a set where, if for every object `G` in the set, every morphism `h` from `G` to object `X`, the composite of `h` with morphisms `f` and `g` (both from `X` to `Y`) are the same, then `f` and `g` must be the same morphism. In simpler terms, the theorem is about preserving the property of being a 'separating set' under taking superset in the category theory context.
More concisely: Given a category `C` and a separating set `๐ข` of objects, any larger set `โ` containing `๐ข` is also a separating set.
|
CategoryTheory.isCoseparator_def
theorem CategoryTheory.isCoseparator_def :
โ {C : Type uโ} [inst : 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
The theorem `CategoryTheory.isCoseparator_def` states that, for any category `C` and object `G` in `C`, `G` is a coseparator if and only if for all objects `X` and `Y` in `C` and morphisms `f` and `g` from `X` to `Y`, if for every morphism `h` from `Y` to `G`, the composition of `f` with `h` equals the composition of `g` with `h`, then `f` must be equal to `g`. In simple terms, a coseparator `G` is able to distinguish between any two different morphisms `f` and `g` from `X` to `Y`, by testing them against all morphisms `h` from `Y` to `G`.
More concisely: A object `G` in a category `C` is a coseparator if and only if for all objects `X` and `Y` and morphisms `f` and `g` from `X` to `Y`, if for all morphisms `h` from `Y` to `G`, `hf = hg` implies `f = g`.
|
CategoryTheory.wellPowered_of_isDetecting
theorem CategoryTheory.wellPowered_of_isDetecting :
โ {C : Type uโ} [inst : CategoryTheory.Category.{vโ, uโ} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
{๐ข : Set C} [inst_2 : Small.{vโ, uโ} โ๐ข], CategoryTheory.IsDetecting ๐ข โ CategoryTheory.WellPowered C
The theorem `CategoryTheory.wellPowered_of_isDetecting` states that given any category `C`, if this category has pullbacks and a small detecting set `๐ข`, then the category is well-powered. Here, a detecting set `๐ข` is one where the functors `C(G, -)` collectively reflect isomorphisms -- that is, for any morphism `f` from object `X` to `Y` in the category, if every morphism `h` with domain in `๐ข` uniquely factors through `f`, then `f` is an isomorphism. A category is said to be well-powered if every object has a small skeleton in the category of monomorphisms into it.
More concisely: If a category with small detecting set and pullbacks is such that every morphism factoring uniquely through every morphism in the detecting set is an isomorphism, then the category is well-powered.
|
CategoryTheory.IsCoseparating.mono
theorem CategoryTheory.IsCoseparating.mono :
โ {C : Type uโ} [inst : CategoryTheory.Category.{vโ, uโ} C] {๐ข : Set C},
CategoryTheory.IsCoseparating ๐ข โ โ {โ : Set C}, ๐ข โ โ โ CategoryTheory.IsCoseparating โ
This theorem states that for any category 'C', and a given set '๐ข' that is a coseparating set in the category, any other set 'โ' that contains the set '๐ข' (in the sense that '๐ข' is a subset of 'โ') is also a coseparating set in the category. In other words, if every functor `C(-, G)` for `G โ ๐ข` is collectively faithful, then every functor `C(-, H)` for `H โ โ` is also collectively faithful, provided that '๐ข' is a subset of 'โ'. This theorem is essentially about the preservation of the coseparating property under the operation of taking subsets.
More concisely: If a subset '๐ข' of a category 'C' is a coseparating set and is contained in another set 'โ', then 'โ' is also a coseparating set in 'C'.
|
CategoryTheory.isSeparator_def
theorem CategoryTheory.isSeparator_def :
โ {C : Type uโ} [inst : 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
The theorem `CategoryTheory.isSeparator_def` states that for any category `C` and an object `G` in `C`, `G` is a separator if and only if for all pairs of objects `X` and `Y` in `C` and for any two morphisms `f` and `g` from `X` to `Y`, if for all morphisms `h` from `G` to `X`, the composition of `h` and `f` equals the composition of `h` and `g`, it implies that `f` and `g` are equal. This is essentially stating that a separator in a category is an object such that, given any two morphisms with the same domain and codomain, if their compositions with every morphism from the separator result in the same morphism, then the original two morphisms must be the same.
More concisely: A separator in a category is an object `G` such that for all objects `X` and `Y` and morphisms `f, g : X -> Y`, if for all morphisms `h : G -> X`, `h * f = h * g`, then `f = g`.
|
CategoryTheory.hasTerminal_of_isSeparating
theorem CategoryTheory.hasTerminal_of_isSeparating :
โ {C : Type uโ} [inst : CategoryTheory.Category.{vโ, uโ} C] [inst_1 : CategoryTheory.WellPowered Cแตแต]
[inst_2 : CategoryTheory.Limits.HasColimits C] {๐ข : Set C} [inst_3 : Small.{vโ, uโ} โ๐ข],
CategoryTheory.IsSeparating ๐ข โ CategoryTheory.Limits.HasTerminal C
This theorem is part of the proof for the Special Adjoint Functor Theorem. It states that if a category `C` is cocomplete, well-copowered and has a small separating set `๐ข`, then it must also have a terminal object. The theorem further alludes to the fact that, as a consequence of the Special Adjoint Functor Theorem, `C` is also complete as shown in the theorem `hasLimits_of_hasColimits_of_isSeparating`. In essence, this theorem provides a condition under which a category has a terminal object, which is a key concept in category theory.
More concisely: If a cocomplete, well-copowered category with a small separating set has a terminal object, then it is complete. (The theorem states that under these conditions, the existence of a terminal object implies the completeness of the category.)
|
CategoryTheory.hasInitial_of_isCoseparating
theorem CategoryTheory.hasInitial_of_isCoseparating :
โ {C : Type uโ} [inst : CategoryTheory.Category.{vโ, uโ} C] [inst_1 : CategoryTheory.WellPowered C]
[inst_2 : CategoryTheory.Limits.HasLimits C] {๐ข : Set C} [inst_3 : Small.{vโ, uโ} โ๐ข],
CategoryTheory.IsCoseparating ๐ข โ CategoryTheory.Limits.HasInitial C
This theorem is a component of the proof for the Special Adjoint Functor Theorem. The theorem states that for any category `C`, given that `C` is well-powered, has all limits, and has a small set `๐ข` that is coseparating, then `C` has an initial object. Furthermore, the Special Adjoint Functor Theorem implies that `C` is already cocomplete, as shown by the theorem `hasColimits_of_hasLimits_of_isCoseparating`. In essence, the theorem establishes that certain conditions allow us to guarantee the existence of an initial object in a category.
More concisely: If a well-powered category `C` with a small, coseparating set `๐ข` has all limits, then it has an initial object and is cocomplete.
|
CategoryTheory.IsDetecting.isSeparating
theorem CategoryTheory.IsDetecting.isSeparating :
โ {C : Type uโ} [inst : CategoryTheory.Category.{vโ, uโ} C] [inst_1 : CategoryTheory.Limits.HasEqualizers C]
{๐ข : Set C}, CategoryTheory.IsDetecting ๐ข โ CategoryTheory.IsSeparating ๐ข
The theorem `CategoryTheory.IsDetecting.isSeparating` states that for any category `C` with equalizers, if a set `๐ข` of objects in `C` is a detecting set, then it is also a separating set. In other words, if for any morphisms `f` from `X` to `Y` in `C`, the functors `C(G, -)` for `G โ ๐ข` collectively reflect isomorphisms (i.e., if any `h` with domain in `๐ข` uniquely factors through `f`, then `f` is an isomorphism), then the functors `C(G, -)` for `G โ ๐ข` are collectively faithful (i.e., if `h โซ f = h โซ g` for all `h` with domain in `๐ข`, then `f = g`).
More concisely: If a set of objects in a category with equalizers is detecting, then it is separating. That is, if the functors given by evaluation at each object in the set collectively reflect isomorphisms, then they also collectively preserve compositions of morphisms.
|
CategoryTheory.IsSeparating.isDetecting
theorem CategoryTheory.IsSeparating.isDetecting :
โ {C : Type uโ} [inst : CategoryTheory.Category.{vโ, uโ} C] [inst_1 : CategoryTheory.Balanced C] {๐ข : Set C},
CategoryTheory.IsSeparating ๐ข โ CategoryTheory.IsDetecting ๐ข
This theorem states that for any category `C` that is balanced (meaning that every morphism that factors through an isomorphism is itself an isomorphism), if a set of objects `๐ข` in `C` is separating (meaning the functors `C(G, -)` for `G โ ๐ข` are collectively faithful, i.e., if `h โซ f = h โซ g` for all `h` with domain in `๐ข`, then `f = g`), then `๐ข` is also detecting (meaning the functors `C(G, -)` collectively reflect isomorphisms, i.e., if any `h` with domain in `๐ข` uniquely factors through `f`, then `f` is an isomorphism). In simple terms, in a balanced category, a separating set of objects is also a detecting set.
More concisely: In a balanced category, a separating set of objects is also a detecting set.
|