From a159b6b0b5aa271b4d494d0e7f7453016fa27493 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 10 Sep 2026 23:23:45 +0200 Subject: [PATCH 1/3] consistent usage of essentially small collections --- content/comphaus_copresentable.md | 2 +- content/foundations.md | 26 ++++++++++++------- content/free-cocompletion.md | 6 ++--- content/functors_on_discrete_categories.md | 2 +- content/isbell_concreteness.md | 4 +-- content/missing_cogenerator.md | 2 +- content/nice-and-small-presheaves.md | 4 +-- database/data/categories/CAlg(R).yaml | 2 +- database/data/categories/Cat.yaml | 2 +- database/data/categories/Haus.yaml | 2 +- database/data/categories/Mono.yaml | 2 +- database/data/categories/SemiGrp.yaml | 4 +-- database/data/categories/Set_disc_Ab.yaml | 2 +- database/data/categories/Vect_large.yaml | 10 +++---- database/data/categories/Z.yaml | 2 +- .../cocompletion-discrete-pair-join.yaml | 2 +- .../category-implications/accessible.yaml | 4 +-- .../category-implications/generators.yaml | 2 +- database/data/category-implications/size.yaml | 2 +- database/data/category-implications/thin.yaml | 2 +- .../data/category-properties/accessible.yaml | 2 +- .../aleph1-accessible.yaml | 2 +- .../category-properties/cogenerating set.yaml | 2 +- .../data/category-properties/coproducts.yaml | 2 +- .../data/category-properties/cosifted.yaml | 2 +- .../data/category-properties/cototal.yaml | 2 +- .../directed colimits.yaml | 2 +- .../category-properties/directed limits.yaml | 2 +- .../essentially small.yaml | 2 +- .../extremal cogenerating set.yaml | 2 +- .../extremal cogenerator.yaml | 2 +- .../extremal generating set.yaml | 2 +- .../extremal generator.yaml | 2 +- .../finitely accessible.yaml | 2 +- .../generalized variety.yaml | 2 +- .../category-properties/generating set.yaml | 2 +- .../locally essentially small.yaml | 4 +-- .../category-properties/locally small.yaml | 2 +- .../category-properties/multi-algebraic.yaml | 2 +- .../multi-initial object.yaml | 2 +- .../multi-terminal object.yaml | 2 +- .../data/category-properties/products.yaml | 2 +- database/data/category-properties/sifted.yaml | 2 +- database/data/category-properties/small.yaml | 2 +- database/data/category-properties/total.yaml | 2 +- .../category-properties/well-copowered.yaml | 2 +- .../category-properties/well-powered.yaml | 2 +- .../category-properties/wide pullbacks.yaml | 3 ++- .../category-properties/wide pushouts.yaml | 3 ++- .../data/functor-properties/cocontinuous.yaml | 2 +- .../data/functor-properties/continuous.yaml | 2 +- .../data/functors/simple_group_probing.yaml | 4 +-- 52 files changed, 82 insertions(+), 72 deletions(-) diff --git a/content/comphaus_copresentable.md b/content/comphaus_copresentable.md index c888aa060..53faddbb2 100644 --- a/content/comphaus_copresentable.md +++ b/content/comphaus_copresentable.md @@ -98,7 +98,7 @@ followed by $$\Hom_{\CompHaus}({-}, [0,1]) : \CompHaus^{\op} \to \Set.$$ The first automatically preserves $\aleph_1$-filtered colimits (and in fact all colimits) since it has a right adjoint. The second one preserves $\aleph_1$-filtered colimits by the previous lemma. -Alternately, applying the general framework of Lawvere theories shows that $\CompHaus^{\op}$ is equivalent to the category of functors $\T \to \Set$ preserving countable products, where $\T$ is the full subcategory of $\CompHaus$ of all spaces $[0,1]^A$ where $A$ is countable. Note that $\T$ is essentially small. We thus reproduce a result from [Isb82](#references) which also provides a nice description of a small set of generators of the operations of the $\aleph_0$-ary algebraic theory. A more recent treatment in [MR17](#references) refines this by providing a nice axiomatization of the relations of that theory. +Alternately, applying the general framework of Lawvere theories shows that $\CompHaus^{\op}$ is equivalent to the category of functors $\T \to \Set$ preserving countable products, where $\T$ is the full subcategory of $\CompHaus$ of all spaces $[0,1]^A$ where $A$ is countable. Note that $\T$ is essentially small. We thus reproduce a result from [Isb82](#references) which also provides a nice description of a set of generators of the operations of the $\aleph_0$-ary algebraic theory. A more recent treatment in [MR17](#references) refines this by providing a nice axiomatization of the relations of that theory. ::: ## References diff --git a/content/foundations.md b/content/foundations.md index 8f44b40ff..ae571fe6a 100644 --- a/content/foundations.md +++ b/content/foundations.md @@ -27,13 +27,21 @@ Just imagine three copies of ZFC embedded into each other, each representing a " visualization of three levels of size -The levels are not defined by cardinality alone. For example, $\{\SetColl\}$ is a collection with just one element, but it is not a set (since otherwise $\SetColl$ would be a set). In particular, not every finite collection is a set. However, every finite collection is isomorphic to a set. - In our framework, there is no way to group all hypercollections into a single mathematical object; for this, one would need a third Grothendieck universe $\SetColl^{++}$, but such a grouping is usually not required. -A family $(X_i)_{i \in I}$ of collections is called _small_ when its index collection is a set. +## Essentially small, finite, and countable collections + +Let us call a collection $X$ _essentially small_ if it is isomorphic to a set $S$, i.e., if there is a bijection between $X$ and $S$. For most parts of category theory, $X$ can then simply be replaced with $S$ and assumed to be small itself, i.e., a set. + +For example, the collection $\{\SetColl\}$ is not small, but essentially small, since it is isomorphic to the set $\{0\}$. This shows that the three levels are not defined by cardinality alone. + +If a collection $X$ admits a surjective map from a set $S$, then it is also essentially small, since by the axiom of choice $X$ is isomorphic to a subset of $S$. + +A family of collections $(X_i)_{i \in I}$ is called _small_ when $I$ is a set. In this case, the collection of its elements $\{X_i : i \in I\}$ is essentially small. Every essentially small collection has this form. -A collection is called _countable_ if it admits a surjective map from $\IN$. In particular, every finite collection is countable. +A collection is called _finite_ if it is isomorphic to $\{1,\dotsc,n\}$ for some $n \in \IN$. In particular, every finite collection is essentially small. However, a finite collection is not necessarily small, as the example $\{\SetColl\}$ shows. + +A collection is called _countable_ if it admits a surjective map from the set of natural numbers $\IN$. In particular, every finite collection is countable, and every countable collection is essentially small. ## Categories @@ -52,7 +60,9 @@ of collections (and hence a collection itself). We write $\Ob(\C) \coloneqq O$ a When $f \in \Mor(\C)$ is a morphism with $s(f) = X$ and $t(f) = Y$, we write $$f : X \to Y.$$ -We write $\Hom(X,Y)$ or $\Mor(X,Y)$ for the collection of such morphisms. This collection need not be a set. If it is a set for all $X,Y$, the category is called _locally small_. +We write $\Hom(X,Y)$ or $\Mor(X,Y)$ for the collection of such morphisms. + +The collection $\Hom(X,Y)$ need not be a set. If it is a set for all $X,Y$, the category is called _locally small_. If $\Hom(X,Y)$ is essentially small (isomorphic to a set) for all $X,Y$, the category is called _locally essentially small_. When a morphism $f : X \to Y$ happens to be uniquely determined, it will be written as $!_{X,Y}$ or even just $!$. @@ -77,6 +87,8 @@ If $\C, \D$ are categories, we can construct the functor category $[\C, \D]$ as It is better to state explicitly when the assumption of being locally small is needed. +Equivalences of categories are defined [as usual](https://en.wikipedia.org/wiki/Equivalence_of_categories). A category is _essentially small_ if it is equivalent to a small category. A collection $X$ is essentially small if and only if the associated discrete category $X_{\disc}$ (which has only identity morphisms) is essentially small. In this sense, the two notions are compatible. + ## Representable Functors If $\C$ is any category and $A \in \C$, we have the Hom-functor @@ -97,10 +109,6 @@ Unless stated otherwise, we consider only small diagrams and hence small limits There are special types of limits, such as equalizers, products, and cofiltered limits, and their duals, such as coequalizers, coproducts, and filtered colimits. By convention, products and coproducts are indexed by a set, not a collection (unless stated otherwise). Filtered colimits are indexed by a small filtered category (unless stated otherwise). -## Well-powered categories - -If $A$ is an object of a category, the collection of all monomorphisms $B \to A$ need not be a set. If, for every $A$, there exists a small family of such monomorphisms such that every monomorphism $B \to A$ is isomorphic over $A$ to one in the family, then the category is called _well-powered_. The dual notion of being _well-copowered_ is defined using epimorphisms $A \to B$. Every small category is well-powered, but there are many well-powered categories that are not small and not even equivalent to a small category. - ## Conclusion There is much more to say about set-theoretic foundations for category theory (in fact, many papers have been written on the subject, and the approach developed above is just _one_ of [many](https://xkcd.com/927/) approaches), but this suffices for the purposes of _CatDat_. diff --git a/content/free-cocompletion.md b/content/free-cocompletion.md index d13cc5c9c..7701e4aa4 100644 --- a/content/free-cocompletion.md +++ b/content/free-cocompletion.md @@ -11,7 +11,7 @@ that are _small_. This condition can be described in many equivalent ways: 1. $F$ is a small colimit of representable functors. 2. There is a small category $\I$ such that $F$ is the left Kan extension of a presheaf on $\I$ along a functor $\I \to \C$. -3. There is small subcategory $\I \subseteq \C$ such that $F$ is the left Kan extension of its restriction to $\I$. +3. There is an essentially small subcategory $\I \subseteq \C$ such that $F$ is the left Kan extension of its restriction to $\I$. 4. The category of elements $\int F$ is [finally small](https://ncatlab.org/nlab/show/finally+small). Here, the objects of $\int F$ are pairs $(X,a)$, where $X \in \C$ and $a \in F(X)$, and a morphism $(X,a) \to (Y,b)$ is a morphism $f : X \to Y$ with $F(f)(b) = a$. The equivalence of the conditions (1), (2), (3) is proven as Proposition 4.83 in Kelly's book [Basic Concepts of Enriched Category Theory](http://www.tac.mta.ca/tac/reprints/articles/10/tr10.html). The implication (1) $\implies$ (4) is proven as Proposition 3.7 in Kan Extensions are Partial Colimits by Perrone-Tholen (but there must be earlier references). The implication (4) $\implies$ (1) follows from the [co-Yoneda Lemma](https://ncatlab.org/nlab/show/co-Yoneda+lemma) @@ -175,9 +175,9 @@ where $E \coloneqq \eq(F \rightrightarrows G)$ is the objectwise defined equaliz We view the pushout $P \coloneqq F \sqcup_E F$ as the union of two copies $F_1,F_2$ of $F$ with $F_1 \cap F_2 = E$. In particular, we regard $E,F_1,F_2$ as sub-presheaves of $P$. For a morphism $f$ in $\C$, we write $f^*$ instead of $P(f)$. -Since $P \cong G$ is small, its category of elements $\int P$ has a finally small subcategory $\K$. Let $K \subseteq \Ob(\C)$ be the set of objects that appear in $\K$. We claim that +Since $P \cong G$ is small, its category of elements $\int P$ has an essentially small final subcategory $\K$. Let $K \subseteq \Ob(\C)$ be the collection of objects that appear in $\K$. We claim that $$\{(A,a) : A \in K, \, a \in E(A)\}$$ -is a weakly terminal set in $\int E$, which is equivalent to saying that the canonical morphism +is a weakly terminal essentially small collection in $\int E$, which is equivalent to saying that the canonical morphism $$\textstyle \coprod_{A \in K,\, a \in E(A)} \Hom(-,A) \to E$$ is an epimorphism of presheaves, as required. diff --git a/content/functors_on_discrete_categories.md b/content/functors_on_discrete_categories.md index 5514064eb..55da32655 100644 --- a/content/functors_on_discrete_categories.md +++ b/content/functors_on_discrete_categories.md @@ -24,7 +24,7 @@ Let $\S$ be a non-trivial inhabited discrete category. Then a functor $F : \S \t ::: Proof Assume first that $F$ is continuous. An object $X$ is subterminal if and only if $X \times X$ exists and the diagonal $X \to X \times X$ is an isomorphism. Thus, every functor preserving binary products preserves subterminal objects. Since every object in a discrete category is subterminal, it follows that each $F(s) \in \C$ is subterminal. -Conversely, assume that each $F(s) \in \C$ is subterminal. To show that $F$ is continuous, let $D : \I \to \S$ be a (small) diagram admitting a universal cone $(s \to D(i))_{i \in \I}$. Then $D(i) = s$ for all $i \in \I$, and each morphism $s \to D(i)$ is the identity. Since $\S$ has no terminal object (otherwise, $\S$ would be trivial), $\I$ is inhabited. We need to show that $(\id_{F(s)} : F(s) \to F(s))_{i \in \I}$ is a universal cone in $\C$. This follows immediately from $F(s)$ being subterminal: for a family of morphisms $X \to F(s)$ indexed by $\I$, all morphisms must be equal, and there is one such morphism since $\I$ is inhabited. +Conversely, assume that each $F(s) \in \C$ is subterminal. To show that $F$ is continuous, let $D : \I \to \S$ be a diagram admitting a universal cone $(s \to D(i))_{i \in \I}$. Then $D(i) = s$ for all $i \in \I$, and each morphism $s \to D(i)$ is the identity. Since $\S$ has no terminal object (otherwise, $\S$ would be trivial), $\I$ is inhabited. We need to show that $(\id_{F(s)} : F(s) \to F(s))_{i \in \I}$ is a universal cone in $\C$. This follows immediately from $F(s)$ being subterminal: for a family of morphisms $X \to F(s)$ indexed by $\I$, all morphisms must be equal, and there is one such morphism since $\I$ is inhabited. ::: Remark that in a thin category, every object is subterminal. Of course, Lemma 2 can also be dualized: A functor on a non-trivial inhabited discrete category is cocontinuous if and only if each object in its image is "co-subterminal". Here, an object $X$ is co-subterminal if any two morphisms with domain $X$ are equal (see [MSE/1092122](https://math.stackexchange.com/questions/1092122) for a discussion of the terminology). diff --git a/content/isbell_concreteness.md b/content/isbell_concreteness.md index b7d8c807b..29319cfec 100644 --- a/content/isbell_concreteness.md +++ b/content/isbell_concreteness.md @@ -19,7 +19,7 @@ $$ commutes. We say that two spans over $(A,B)$ are _equivalent_ if they commute with exactly the same cospans. -The _Isbell condition_ says that, for each pair of objects $A,B$, the collection of equivalence classes of spans over $(A,B)$ is isomorphic to a set. Equivalently, there must be a set of selected spans over $(A,B)$ such that every span over $(A,B)$ is equivalent to one of the selected spans. +The _Isbell condition_ says that, for each pair of objects $A,B$, the collection of equivalence classes of spans over $(A,B)$ is essentially small. Equivalently, there must be a set of selected spans over $(A,B)$ such that every span over $(A,B)$ is equivalent to one of the selected spans. ::: Lemma Every concretizable category satisfies the Isbell condition. @@ -38,7 +38,7 @@ for $x \in U(X)$. Then the span commutes with the cospan if and only if $$U(a')(u) = U(b')(v)$$ for every $(u,v) \in P_{a,b}$. Thus, whether a span commutes with a given cospan depends only on the subset $P_{a,b}$. -Call a subset of $U(A) \times U(B)$ _realizable_ if it is of the form $P_{a,b}$ for some span $(a,b)$. Since $U(A) \times U(B)$ is a set, there is a set of realizable subsets. As we have just seen, the map that sends a realizable subset $P_{a,b}$ to the equivalence class of $(a,b)$ is well-defined, and it is clearly surjective. Hence, the collection of equivalence classes of spans over $(A,B)$ is isomorphic to a set. +Call a subset of $U(A) \times U(B)$ _realizable_ if it is of the form $P_{a,b}$ for some span $(a,b)$. Since $U(A) \times U(B)$ is a set, there is a set of realizable subsets. As we have just seen, the map that sends a realizable subset $P_{a,b}$ to the equivalence class of $(a,b)$ is well-defined, and it is clearly surjective. Hence, the collection of equivalence classes of spans over $(A,B)$ is essentially small. ::: ## References diff --git a/content/missing_cogenerator.md b/content/missing_cogenerator.md index ac3b7675d..36a1fee90 100644 --- a/content/missing_cogenerator.md +++ b/content/missing_cogenerator.md @@ -18,5 +18,5 @@ Then $\C$ does not have a cogenerator. Moreover, $\C$ is not cototal. ::: Proof Assume that there is a cogenerator $Y$. By assumption (2) there is an object $X \in \F$ such that $U(X)$ is larger than $U(Y)$ (w.r.t. cardinalities). Since $0,\id_X : X \rightrightarrows X$ are distinct, there is a morphism $f : X \to Y$ with $f \neq 0$. But then $U(f) : U(X) \to U(Y)$ is injective by assumption (1), which contradicts our choice of $X$. -Now assume that $\C$ is cototal. Using the axiom of choice, we may assume that for each small cardinal $\kappa$, there is at most one element $X \in \F$ such that $\card(U(X)) = \kappa$. Treating $\F$ as a discrete diagram in $\C$, assumption (1) implies that for any object $Y$ of $\C$, the collection of cocones $\F \to Y$ is bijective with a set, since the maps $X \to Y$ with $\card(U(X)) > \card(U(Y))$ must all be zero in such a cocone. Therefore, by G. M. Kelly, A survey of totality for enriched and ordinary categories, Thm. 5.6 (namely the implication (i) $\Rightarrow$ (iii)), $\C$ must have a coproduct $Y$ of all elements of $\F$. But then by assumption (2), there exists $X \in \F$ such that $\card(U(X)) > \card(U(Y))$; and since $\C$ is pointed, the coprojection $X \to Y$ must be split monic and therefore non-zero. Using assumption (1), we get a contradiction. +Now assume that $\C$ is cototal. Using the axiom of choice, we may assume that for each small cardinal $\kappa$, there is at most one element $X \in \F$ such that $\card(U(X)) = \kappa$. Treating $\F$ as a discrete diagram in $\C$, assumption (1) implies that for any object $Y$ of $\C$, the collection of cocones $\F \to Y$ is essentially small, since the maps $X \to Y$ with $\card(U(X)) > \card(U(Y))$ must all be zero in such a cocone. Therefore, by G. M. Kelly, A survey of totality for enriched and ordinary categories, Thm. 5.6 (namely the implication (i) $\Rightarrow$ (iii)), $\C$ must have a coproduct $Y$ of all elements of $\F$. But then by assumption (2), there exists $X \in \F$ such that $\card(U(X)) > \card(U(Y))$; and since $\C$ is pointed, the coprojection $X \to Y$ must be split monic and therefore non-zero. Using assumption (1), we get a contradiction. ::: diff --git a/content/nice-and-small-presheaves.md b/content/nice-and-small-presheaves.md index dcc5a4312..b4a84cdd9 100644 --- a/content/nice-and-small-presheaves.md +++ b/content/nice-and-small-presheaves.md @@ -34,9 +34,9 @@ A presheaf $F$ on $\C$ is small if and only if it is nice. ::: ::: Proof -The collection of nice presheaves is clearly closed under small colimits of presheaves, since colimits commute with colimits and colimits of presheaves are computed objectwise. Furthermore, we have seen above that representable presheaves are nice. It follows that every small presheaf is nice. +The collection of nice presheaves is clearly closed under colimits of presheaves, since colimits commute with colimits and colimits of presheaves are computed objectwise. Furthermore, we have seen above that representable presheaves are nice. It follows that every small presheaf is nice. -Conversely, assume that $F$ is a nice presheaf and choose an exceptional set $S_F$. To show that $F$ is small, we will show that its category of elements $\int F$ has a small final subcategory. Let $\D$ be the full subcategory of $\int F$ consisting of the objects +Conversely, assume that $F$ is a nice presheaf and choose an exceptional set $S_F$. To show that $F$ is small, we will show that its category of elements $\int F$ has an essentially small final subcategory. Let $\D$ be the full subcategory of $\int F$ consisting of the objects - $(A,a)$ for $a \in F(A)$, - $(B,b)$ for $b \in F(B)$, diff --git a/database/data/categories/CAlg(R).yaml b/database/data/categories/CAlg(R).yaml index 840932f19..ad6ebd199 100644 --- a/database/data/categories/CAlg(R).yaml +++ b/database/data/categories/CAlg(R).yaml @@ -85,7 +85,7 @@ unsatisfied_properties: proof: >- This proof will be similar to the proof of this lemma. To start, for each infinite cardinal $\kappa \ge \card(U(R))$, choose a field $F_\kappa$ of cardinality $\kappa$ including a quotient field of $R$. (For example, fix some such quotient field $R / \m$ and then let $F_\kappa$ be the extension of $R / \m$ by $\kappa$ many indeterminates.) We first claim that for any commutative $R$-algebra $A$ with $\kappa > \card(U(A))$, there is exactly one $R$-algebra homomorphism $\varphi : R \times F_\kappa \to A$, which can be described as the projection $R \times F_\kappa \to R$ followed by the unique morphism $R \to A$. To see this, note that for any other such morphism $\varphi$, we must have $\varphi(0, 1) \ne 0$. It follows that the rng homomorphism $F_\kappa \to A$ formed by composing $F_\kappa \to R \times F_\kappa$, $x \mapsto (0, x)$, with $\varphi$ is non-zero, and it is therefore injective since $F_\kappa$ was chosen to be a field. This gives a contradiction. - It follows that for any commutative $R$-algebra $A$, the set of cocones $R \times F_\kappa \to A$ from the discrete diagram on $R \times F_\kappa$ is bijective to a set. On the other hand, we claim that $\CAlg(R)$ has no coproduct of all $R \times F_\kappa$. This will imply that $\CAlg(R)$ is not cototal, by G. M. Kelly, A survey of totality for enriched and ordinary categories, Thm. 5.6 (namely the contrapositive of the implication (i) $\Rightarrow$ (iii)). To see this, suppose we had such a coproduct $A$, and choose a cardinal $\kappa$ greater than $\max(\card(U(A)), \card(U(R)), \aleph_0)$. Then the coprojection $R \times F_\kappa \to A$ would be split injective, where we can construct the splitting $A \to R\times F_\kappa$ such that the $\kappa$ component is the identity, whereas for $\lambda \ne \kappa$, the $\lambda$ component is given by the projection $R \times F_\lambda \to R$ composed with the unique morphism $R \to R \times F_\kappa$. However, from this injection, we would get $\card(A) \ge \card(R \times F_\kappa) = \kappa$, giving a contradiction. + It follows that for any commutative $R$-algebra $A$, the collection of cocones $R \times F_\kappa \to A$ from the discrete diagram on $R \times F_\kappa$ is essentially small. On the other hand, we claim that $\CAlg(R)$ has no coproduct of all $R \times F_\kappa$. This will imply that $\CAlg(R)$ is not cototal, by G. M. Kelly, A survey of totality for enriched and ordinary categories, Thm. 5.6 (namely the contrapositive of the implication (i) $\Rightarrow$ (iii)). To see this, suppose we had such a coproduct $A$, and choose a cardinal $\kappa$ greater than $\max(\card(U(A)), \card(U(R)), \aleph_0)$. Then the coprojection $R \times F_\kappa \to A$ would be split injective, where we can construct the splitting $A \to R\times F_\kappa$ such that the $\kappa$ component is the identity, whereas for $\lambda \ne \kappa$, the $\lambda$ component is given by the projection $R \times F_\lambda \to R$ composed with the unique morphism $R \to R \times F_\kappa$. However, from this injection, we would get $\card(A) \ge \card(R \times F_\kappa) = \kappa$, giving a contradiction. label: calg_not_cototal special_objects: diff --git a/database/data/categories/Cat.yaml b/database/data/categories/Cat.yaml index 2552d19e7..9e8c71c96 100644 --- a/database/data/categories/Cat.yaml +++ b/database/data/categories/Cat.yaml @@ -92,7 +92,7 @@ unsatisfied_properties: - property: cototal proof: >- - For each infinite cardinal $\kappa$, choose a simple group $G_\kappa$ of cardinality $\kappa$ (such as the alternating group on $\kappa$). Now consider the large span diagram $1 \dottedrightrightarrows B G_\kappa$. Then for any small category $\C$, the collection of cocones $1 \dottedrightrightarrows B G_\kappa \to \C$ is bijective with a set: to form any such cocone, we must first choose the object $X$ of $\C$ which is the image of the object of $1$. Then, we must choose the morphisms $G_\kappa \to \End_{\C}(X)$; but for $\kappa > \card(\End_{\C}(X))$, the corresponding morphism must be zero. + For each infinite cardinal $\kappa$, choose a simple group $G_\kappa$ of cardinality $\kappa$ (such as the alternating group on $\kappa$). Now consider the large span diagram $1 \dottedrightrightarrows B G_\kappa$. Then for any small category $\C$, the collection of cocones $1 \dottedrightrightarrows B G_\kappa \to \C$ is essentially small: to form any such cocone, we must first choose the object $X$ of $\C$ which is the image of the object of $1$. Then, we must choose the morphisms $G_\kappa \to \End_{\C}(X)$; but for $\kappa > \card(\End_{\C}(X))$, the corresponding morphism must be zero. On the other hand, we claim that $1 \dottedrightrightarrows B G_\kappa$ does not have a pushout in $\Cat$; by G. M. Kelly, A survey of totality for enriched and ordinary categories, Thm. 5.6 (namely the contrapositive of the implication (i) $\Rightarrow$ (iii)), this will imply that $\Cat$ is not cototal. To see this, suppose we have a pushout $\C$ of $1 \dottedrightrightarrows B G_\kappa$, and choose a cardinal $\lambda > \card(\Mor(\C))$ (which is possible since $\C$ is a small category). Then the coprojection $i_\lambda : B G_\lambda \to \C$ must be split monic, since we can construct a cocone $1 \dottedrightrightarrows B G_\kappa \to B G_\lambda$ in which $B G_\kappa \to B G_\lambda$ corresponds to the zero map for $\kappa \ne \lambda$, and in which $B G_\lambda \to B G_\lambda$ is the identity. It follows that if $X$ is the image in $\C$ of the object of $B G_\lambda$ under $i_\lambda$, then $i_\lambda$ induces an injective map $G_\lambda \to \End_{\C}(X)$. This gives a contradiction since $\lambda > \card(\End_{\C}(X))$ and $G_\lambda$ has cardinality $\lambda$. label: cat_not_cototal diff --git a/database/data/categories/Haus.yaml b/database/data/categories/Haus.yaml index 8ff38d0e5..b07f581a6 100644 --- a/database/data/categories/Haus.yaml +++ b/database/data/categories/Haus.yaml @@ -91,7 +91,7 @@ unsatisfied_properties: - property: cototal # cspell: disable-next-line proof: >- - For each cardinal $\kappa$, let $Q_\kappa$ be the product of all Hausdorff topological spaces whose underlying set is a non-empty subset of $\kappa$. By a theorem of Herrlich (Wann sind alle stetigen Abbildungen in Y konstant. Math. Z. 90 (1965): 152-154. EUMDL), there is a regular Hausdorff space $X_\kappa$ with at least two points such that every continuous map $X_\kappa \to Q_\kappa$ is constant. (Note that the result there applies for general $T_1$ spaces $Q$, not just for $Q_\kappa$ as constructed above. In the reference, the author only states that $X_\kappa$ is regular, but actually, $X_\kappa$ is regular and $T_1$, hence Hausdorff.) Choose a base point $x_\kappa \in X_\kappa$ for each $\kappa$. We can form a large span diagram $1 \dottedrightrightarrows X_\kappa$ where each morphism $1 \to X_\kappa$ corresponds to $x_\kappa$. Then for any Hausdorff space $Y$, the collection of cocones $1 \dottedrightrightarrows X_\kappa \to Y$ is bijective to a set: We must first choose $y \in Y$ corresponding to the morphism $1 \to Y$. Then for each $\kappa \ge \card(U(Y))$, $Y$ is homeomorphic to one of the spaces in the product forming $Q_\kappa$. Therefore, there is a morphism $Y \to Q_\kappa$ splitting the projection map $Q_\kappa \to Y$. It follows that the map $X_\kappa \to Y$ is constant, and in fact it must be the constant map with image $y$. + For each cardinal $\kappa$, let $Q_\kappa$ be the product of all Hausdorff topological spaces whose underlying set is a non-empty subset of $\kappa$. By a theorem of Herrlich (Wann sind alle stetigen Abbildungen in Y konstant. Math. Z. 90 (1965): 152-154. EUMDL), there is a regular Hausdorff space $X_\kappa$ with at least two points such that every continuous map $X_\kappa \to Q_\kappa$ is constant. (Note that the result there applies for general $T_1$ spaces $Q$, not just for $Q_\kappa$ as constructed above. In the reference, the author only states that $X_\kappa$ is regular, but actually, $X_\kappa$ is regular and $T_1$, hence Hausdorff.) Choose a base point $x_\kappa \in X_\kappa$ for each $\kappa$. We can form a large span diagram $1 \dottedrightrightarrows X_\kappa$ where each morphism $1 \to X_\kappa$ corresponds to $x_\kappa$. Then for any Hausdorff space $Y$, the collection of cocones $1 \dottedrightrightarrows X_\kappa \to Y$ is essentially small: We must first choose $y \in Y$ corresponding to the morphism $1 \to Y$. Then for each $\kappa \ge \card(U(Y))$, $Y$ is homeomorphic to one of the spaces in the product forming $Q_\kappa$. Therefore, there is a morphism $Y \to Q_\kappa$ splitting the projection map $Q_\kappa \to Y$. It follows that the map $X_\kappa \to Y$ is constant, and in fact it must be the constant map with image $y$. On the other hand, we claim that $1 \dottedrightrightarrows X_\kappa$ does not have a pushout in $\Haus$; by G. M. Kelly, A survey of totality for enriched and ordinary categories, Thm. 5.6 (namely the contrapositive of the implication (i) $\Rightarrow$ (iii)), this will imply that $\Haus$ is not cototal. To see this, suppose we had a pushout $Y$, and let $\lambda \coloneqq \card(U(Y))$. Then the coprojection $X_\lambda \to Y$ is split monic, since we can construct a cocone $1 \dottedrightrightarrows X_\kappa \to X_\lambda$ where the map $X_\kappa \to X_\lambda$ is the constant map with image $x_\lambda$ when $\kappa \ne \lambda$, and the map $X_\lambda \to X_\lambda$ is the identity. But similarly to the previous paragraph, we can show any morphism $X_\lambda \to Y$ must be constant, giving a contradiction since $X_\lambda$ has at least two points. diff --git a/database/data/categories/Mono.yaml b/database/data/categories/Mono.yaml index c5548cd55..67f0aacdc 100644 --- a/database/data/categories/Mono.yaml +++ b/database/data/categories/Mono.yaml @@ -81,7 +81,7 @@ satisfied_properties: $$\colim_{i\in\I} \Hom((1,1), (X_i,X_i')) \to \Hom((1,1), \colim_{i\in\I} (X_i,X_i'))$$ is surjective. To see it is injective, use the fact that the unique morphism $(1, 0) \to (1, 1)$ is an epimorphism (see below), and we have already seen that the corresponding function for $(1,0)$ is injective. - Therefore, any finite coproduct of $(1, 0)$ and $(1, 1)$ is finitely presentable; this means any object of the form $([n], [m])$ with $m, n \in \IN$ and $m \le n$ is finitely presentable. All such objects form a small set. Moreover, any object $(X,X')$ of $\Mono$ is a filtered colimit of the subobjects $(F, F \cap X')$ where $F$ is a finite subset of $X$, and each $(F, F \cap X')$ is isomorphic to some $([n], [m])$. + Therefore, any finite coproduct of $(1, 0)$ and $(1, 1)$ is finitely presentable; this means any object of the form $([n], [m])$ with $m, n \in \IN$ and $m \le n$ is finitely presentable. All such objects form a set. Moreover, any object $(X,X')$ of $\Mono$ is a filtered colimit of the subobjects $(F, F \cap X')$ where $F$ is a finite subset of $X$, and each $(F, F \cap X')$ is isomorphic to some $([n], [m])$. - property: co-Malcev proof: >- diff --git a/database/data/categories/SemiGrp.yaml b/database/data/categories/SemiGrp.yaml index f1c698fc9..e78e5b834 100644 --- a/database/data/categories/SemiGrp.yaml +++ b/database/data/categories/SemiGrp.yaml @@ -33,7 +33,7 @@ satisfied_properties: $$\textstyle \alpha : \lim_i B_i + \lim_i C_i \to \lim_i (B_i + C_i)$$ is an isomorphism, i.e. bijective. The underlying set of the coproduct $B_i + C_i$ is identified with the disjoint union of sets of the form $$B_i \times C_i \times B_i \times \cdots \times C_i$$ - with any positive product length, starting and ending either with $B_i$ or $C_i$. Moreover, $\lim_i$ commutes with arbitrary coproducts in $\Set$, and of course also with products. This shows that $\alpha$ is bijective. + with any positive product length, starting and ending either with $B_i$ or $C_i$. Moreover, $\lim_i$ commutes with coproducts in $\Set$, and of course also with products. This shows that $\alpha$ is bijective. unsatisfied_properties: - property: skeletal @@ -68,7 +68,7 @@ unsatisfied_properties: - property: cototal proof: >- - The proof is similar to the proof for $\Cat$. For each infinite cardinal $\kappa$, let $G_\kappa$ be a simple group of cardinality $\kappa$ (such as the alternating group on $\kappa$). We can then form the large span diagram $1 \dottedrightrightarrows G_\kappa$ in $\SemiGrp$. For every semigroup $A$, the collection of cocones $1 \dottedrightrightarrows G_\kappa \to A$ is bijective to a set: for every such cocone, we must first choose an idempotent $e$ of $A$ corresponding to the map $1 \to A$. Then, whenever $\kappa > \card(U(A))$, where $U(-)$ denotes the underlying set, for $f_\kappa : G_\kappa \to A$ in the cocone, we see + The proof is similar to the proof for $\Cat$. For each infinite cardinal $\kappa$, let $G_\kappa$ be a simple group of cardinality $\kappa$ (such as the alternating group on $\kappa$). We can then form the large span diagram $1 \dottedrightrightarrows G_\kappa$ in $\SemiGrp$. For every semigroup $A$, the collection of cocones $1 \dottedrightrightarrows G_\kappa \to A$ is essentially small: for every such cocone, we must first choose an idempotent $e$ of $A$ corresponding to the map $1 \to A$. Then, whenever $\kappa > \card(U(A))$, where $U(-)$ denotes the underlying set, for $f_\kappa : G_\kappa \to A$ in the cocone, we see $$N \coloneqq \{g \in G_\kappa : f_\kappa(g) = e\}$$ is a normal subgroup of $G_\kappa$. It must be non-trivial since otherwise $f_\kappa$ would induce an injective group homomorphism from $G_\kappa$ to a group contained in $A$. Therefore, $N$ is all of $G_\kappa$, so $f_\kappa$ is the constant map with image $e$. diff --git a/database/data/categories/Set_disc_Ab.yaml b/database/data/categories/Set_disc_Ab.yaml index 21ead93fe..d2f220e88 100644 --- a/database/data/categories/Set_disc_Ab.yaml +++ b/database/data/categories/Set_disc_Ab.yaml @@ -50,7 +50,7 @@ unsatisfied_properties: proof: Since there is an exact embedding $\Ab \to [\Set_{\disc},\Ab]$ which inserts an abelian group at some index, this follows from the fact that $\Ab$ is not split abelian. - property: well-powered - proof: The collection of subobjects of the constant family $(\IZ/2)_{X \in \SetColl}$ identifies with the collection $P(\SetColl)$, which is not isomorphic to a set. + proof: The collection of subobjects of the constant family $(\IZ/2)_{X \in \SetColl}$ identifies with the collection $P(\SetColl)$, which is not essentially small. special_objects: initial object: diff --git a/database/data/categories/Vect_large.yaml b/database/data/categories/Vect_large.yaml index c7cf73b88..baaa19609 100644 --- a/database/data/categories/Vect_large.yaml +++ b/database/data/categories/Vect_large.yaml @@ -6,9 +6,9 @@ morphisms: $K$-linear maps description: >- Recall from our foundations that we work with sets ("small sets") and collections ("large sets"). A large field $K$ is a collection equipped with a field structure. Concrete examples are $\IQ(X_\alpha : \alpha \in \OnColl)$ and the field of nimbers $\On_2$. There is a well-behaved hypercategory $\Vect_K$ of large vector spaces over $K$, which are collections equipped with a suitable algebraic structure. (See the linked article on foundations for the definition of a hypercategory.) Since collections and sets behave mostly the same (both satisfy the ZFC-axioms), it has analogous properties to its small counterpart: it is a split abelian, finitary algebraic hypercategory, and every object is isomorphic to $K^{\oplus X}$ for a collection $X$. - In this entry, we consider the full sub-hypercategory $\Vect^s_K$ of $\Vect_K$ consisting of the large vector spaces that are isomorphic to $K^{\oplus X}$ for a set $X$. Equivalently, a small basis exists. The relationship between $\Vect^s_K$ and $\Vect_K$ is similar to that between $\FinVect_K$ and $\Vect_K$. However, $\Vect^s_K$ is not self-dual, which breaks the analogy. + In this entry, we consider the full sub-hypercategory $\Vect^s_K$ of $\Vect_K$ consisting of the large vector spaces that are isomorphic to $K^{\oplus X}$ for a set $X$. The relationship between $\Vect^s_K$ and $\Vect_K$ is similar to that between $\FinVect_K$ and $\Vect_K$. However, $\Vect^s_K$ is not self-dual, which breaks the analogy. - However, $\Vect^s_K$ is not a category as defined in our foundations, because the totality of its objects is not a collection. Even the totality of trivial large vector spaces is not a collection, analogous to the fact that the collection of trivial vector spaces is not a set. However, the totality of objects of $\Vect^s_K$ is in bijection with the collection of sets, so $\Vect^s_K$ is equivalent (as a hypercategory) to a category. This category has sets as objects and (not necessarily finite) column-finite matrices over $K$ as morphisms. Formally, we need to work with this category to stay within our framework, but it is easier and more natural to work with $\Vect^s_K$ instead, in particular when studying its properties. To decide all properties, we assume that $K$ is not bijective to a set. + However, $\Vect^s_K$ is not a category as defined in our foundations, because the totality of its objects is not a collection. Even the totality of trivial large vector spaces is not a collection, analogous to the fact that the collection of trivial vector spaces is not a set. However, the totality of objects of $\Vect^s_K$ is in bijection with the collection of sets, so $\Vect^s_K$ is equivalent (as a hypercategory) to a category. This category has sets as objects and (not necessarily finite) column-finite matrices over $K$ as morphisms. Formally, we need to work with this category to stay within our framework, but it is easier and more natural to work with $\Vect^s_K$ instead, in particular when studying its properties. To decide all properties, we assume that $K$ is not essentially small. This category does not appear in practice, but it provides an example of a Grothendieck abelian category that is not complete, which is impossible in the locally small case. @@ -28,7 +28,7 @@ satisfied_properties: check_redundancy: false # the many redundancies are caused by "split abelian" which is not atomic yet - property: coproducts - proof: The hypercategory $\Vect_K$ has large coproducts given by direct sums. The sub-hypercategory $\Vect^s_K$ is closed under small coproducts because for a small family of sets $(X_i)_{i \in I}$ also their disjoint union $S \coloneqq \coprod_{i \in I} X_i$ is a set and $\bigoplus_{i \in I} K^{\oplus X_i} \cong K^{\oplus S}$. + proof: The hypercategory $\Vect_K$ has large coproducts given by direct sums. The sub-hypercategory $\Vect^s_K$ is closed under coproducts because for a family of sets $(X_i)_{i \in I}$ also their disjoint union $S \coloneqq \coprod_{i \in I} X_i$ is a set and $\bigoplus_{i \in I} K^{\oplus X_i} \cong K^{\oplus S}$. check_redundancy: false - property: coequalizers @@ -63,7 +63,7 @@ satisfied_properties: proof: Since $K$ is a cogenerator of $\Vect_K$ that is contained in $\Vect^s_K$, it is a cogenerator of $\Vect^s_K$. - property: exact filtered colimits - proof: Since the inclusion functor $\Vect^s_K \hookrightarrow \Vect_K$ is exact, preserves small colimits, and is fully faithful, this follows from the corresponding fact for $\Vect_K$ (where finite limits even commute with large filtered colimits). + proof: Since the inclusion functor $\Vect^s_K \hookrightarrow \Vect_K$ is exact, preserves colimits, and is fully faithful, this follows from the corresponding fact for $\Vect_K$ (where finite limits even commute with large filtered colimits). - property: well-powered proof: In contrast to the other properties mentioned before, this does not follow from the hypercategory $\Vect_K$, since the subobjects of a large vector space merely form a collection. Instead, notice that the subobjects of $K^{\oplus X}$, where $X$ is a set, are isomorphic to $K^{\oplus Y}$ for subsets $Y \subseteq X$ (see our proof for equalizers). Since the subsets of $X$ form a set, the subobjects form a set. @@ -90,7 +90,7 @@ unsatisfied_properties: Consider the subset $L \subseteq K^{\IN}$ consisting of the sequences $$(1,\lambda,\lambda^2,\dotsc)$$ - for $\lambda \in K$. Every finite subset of $L$ is linearly independent: for $n$ distinct elements $\lambda_1,\dotsc,\lambda_n$, the truncated sequences $(1,\lambda_i,\dotsc,\lambda_i^{n-1})$ are linearly independent by the Vandermonde determinant. Thus, $L$ is linearly independent. Equivalently, there is a monomorphism $K^{\oplus L} \hookrightarrow K^{\IN} \cong K^{\oplus X}$. Hence there is an injective map $L \hookrightarrow X$. But then $L \cong K$ would be bijective to a set, contradicting our choice of $K$. + for $\lambda \in K$. Every finite subset of $L$ is linearly independent: for $n$ distinct elements $\lambda_1,\dotsc,\lambda_n$, the truncated sequences $(1,\lambda_i,\dotsc,\lambda_i^{n-1})$ are linearly independent by the Vandermonde determinant. Thus, $L$ is linearly independent. Equivalently, there is a monomorphism $K^{\oplus L} \hookrightarrow K^{\IN} \cong K^{\oplus X}$. Hence there is an injective map $L \hookrightarrow X$. But then $L \cong K$ would be essentially small, contradicting our choice of $K$. special_objects: initial object: diff --git a/database/data/categories/Z.yaml b/database/data/categories/Z.yaml index d622d3523..d151ff343 100644 --- a/database/data/categories/Z.yaml +++ b/database/data/categories/Z.yaml @@ -65,7 +65,7 @@ unsatisfied_properties: proof: 'There are functors $F,G : \CRing \rightrightarrows \Set$ such that $\Hom(F,G)$ is not essentially small, see MO/390611 for example. Now if the exponential $[F,G] : \CRing \to \Set$ exists, we get $[F,G](\IZ) \cong \Hom(\Hom(\IZ,-),[F,G])$ by Yoneda, which simplifies to $\Hom(1,[F,G]) \cong \Hom(1 \times F,G) \cong \Hom(F,G)$, a contradiction.' - property: well-powered - proof: 'Consider the functor $F$ from MO/390611 for example. The collection of subobjects of $F$ is not isomorphic to a set: for each infinite cardinal $\kappa$, simply cut off the construction of $F$ at $\kappa$. This yields a different subobject for each $\kappa$.' + proof: 'Consider the functor $F$ from MO/390611 for example. The collection of subobjects of $F$ is not essentially small: for each infinite cardinal $\kappa$, simply cut off the construction of $F$ at $\kappa$. This yields a different subobject for each $\kappa$.' - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to [\CRing, \Set]$ that maps a set to its constant functor. diff --git a/database/data/categories/cocompletion-discrete-pair-join.yaml b/database/data/categories/cocompletion-discrete-pair-join.yaml index c03469db9..144f6fae8 100644 --- a/database/data/categories/cocompletion-discrete-pair-join.yaml +++ b/database/data/categories/cocompletion-discrete-pair-join.yaml @@ -80,7 +80,7 @@ unsatisfied_properties: - property: well-powered references: - terminal_presheaf_small - proof: We already know that the terminal presheaf $1$ is small. For every set $X$, the unique morphism $\Hom(-,X) \to 1$ is a monomorphism since $X$ is subterminal in $\C$ (in fact, any morphism with codomain $X$ is the identity). For different sets $X,X'$ we have $\Hom(-,X) \not\cong \Hom(-,X')$ since there is not even a morphism $X \to X'$ in $\C$. This shows that $\Sub(1)$ is not small. + proof: We already know that the terminal presheaf $1$ is small. For every set $X$, the unique morphism $\Hom(-,X) \to 1$ is a monomorphism since $X$ is subterminal in $\C$ (in fact, any morphism with codomain $X$ is the identity). For different sets $X,X'$ we have $\Hom(-,X) \not\cong \Hom(-,X')$ since there is not even a morphism $X \to X'$ in $\C$. This shows that $\Sub(1)$ is not essentially small. - property: well-copowered proof: >- diff --git a/database/data/category-implications/accessible.yaml b/database/data/category-implications/accessible.yaml index 471d2f019..8e05ac6cb 100644 --- a/database/data/category-implications/accessible.yaml +++ b/database/data/category-implications/accessible.yaml @@ -61,8 +61,8 @@ - accessible conclusions: - extremal generating set - # TODO: refactor this once we add the property "has small dense subcategory" - proof: The set appearing in the definition of a $\kappa$-accessible category gives a small dense full subcategory, which is in particular an extremal generating set. + # TODO: refactor this once we add the property "has (ess.) small dense subcategory" + proof: The set appearing in the definition of a $\kappa$-accessible category gives an essentially small dense full subcategory, which is in particular an extremal generating set. - id: accessible_well-powered assumptions: diff --git a/database/data/category-implications/generators.yaml b/database/data/category-implications/generators.yaml index 0f3b00626..3c6d2ea1c 100644 --- a/database/data/category-implications/generators.yaml +++ b/database/data/category-implications/generators.yaml @@ -79,4 +79,4 @@ $$f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$$ is an injective function between finite sets of equal cardinality, and therefore is also a bijection. By the assumption that $S$ is an extremal generating set, we thus have $f$ is an isomorphism. - This shows that the collection of isomorphism classes of objects of $X$ is in bijection with a set. Together with the assumption that the category is locally finite, this implies the category is essentially small. + This shows that the collection of isomorphism classes of objects of $X$ is essentially small, i.e. isomorphic to a set. Together with the assumption that the category is locally finite, this implies the category is essentially small. diff --git a/database/data/category-implications/size.yaml b/database/data/category-implications/size.yaml index d549163c1..6148bae1c 100644 --- a/database/data/category-implications/size.yaml +++ b/database/data/category-implications/size.yaml @@ -67,7 +67,7 @@ - concretizable conclusions: - locally essentially small - proof: 'If $U : \C \to \Set$ is a faithful functor, for every pair of objects $A,B$, the collection $\Hom(A,B)$ embeds into the set $\Hom(U(A),U(B))$, so that it is isomorphic to a set.' + proof: 'If $U : \C \to \Set$ is a faithful functor, for every pair of objects $A,B$, the collection $\Hom(A,B)$ embeds into the set $\Hom(U(A),U(B))$, so that it is essentially small.' - id: generating_set_concrete assumptions: diff --git a/database/data/category-implications/thin.yaml b/database/data/category-implications/thin.yaml index 192bd5760..d1e320797 100644 --- a/database/data/category-implications/thin.yaml +++ b/database/data/category-implications/thin.yaml @@ -136,7 +136,7 @@ - thin conclusions: - cocomplete - proof: The supremum of a subset in a (small) preordered set is the infimum of the set of upper bounds. + proof: The supremum of a subset in a preordered set is the infimum of the set of upper bounds. - id: thin_implies_regular assumptions: diff --git a/database/data/category-properties/accessible.yaml b/database/data/category-properties/accessible.yaml index 9754d2ded..dd4ef47f3 100644 --- a/database/data/category-properties/accessible.yaml +++ b/database/data/category-properties/accessible.yaml @@ -1,6 +1,6 @@ id: accessible relation: is -description: Let $\kappa$ be a regular cardinal. A category is $\kappa$-accessible if it has $\kappa$-filtered colimits and there is a (small) set $G$ of $\kappa$-presentable objects such that every object is a $\kappa$-filtered colimit of objects in $G$. A category is accessible if it is $\kappa$-accessible for some regular cardinal $\kappa$. +description: Let $\kappa$ be a regular cardinal. A category is $\kappa$-accessible if it has $\kappa$-filtered colimits and there is an essentially small collection $G$ of $\kappa$-presentable objects such that every object is a $\kappa$-filtered colimit of objects in $G$. A category is accessible if it is $\kappa$-accessible for some regular cardinal $\kappa$. nlab_link: https://ncatlab.org/nlab/show/accessible+category dual: coaccessible invariant_under_equivalences: true diff --git a/database/data/category-properties/aleph1-accessible.yaml b/database/data/category-properties/aleph1-accessible.yaml index 8b1ce5d47..1d55c82f0 100644 --- a/database/data/category-properties/aleph1-accessible.yaml +++ b/database/data/category-properties/aleph1-accessible.yaml @@ -1,6 +1,6 @@ id: ℵ₁-accessible relation: is -description: This is the special case of the notion of a $\kappa$-accessible category, where $\kappa = \aleph_1$ is the first uncountable cardinal. Concretely, a category is $\aleph_1$-accessible when it has $\aleph_1$-filtered colimits and there is a small set $G$ of $\aleph_1$-presentable objects such that every object is a $\aleph_1$-filtered colimit of objects in $G$. +description: This is the special case of the notion of a $\kappa$-accessible category, where $\kappa = \aleph_1$ is the first uncountable cardinal. Concretely, a category is $\aleph_1$-accessible when it has $\aleph_1$-filtered colimits and there is an essentially small collection $G$ of $\aleph_1$-presentable objects such that every object is a $\aleph_1$-filtered colimit of objects in $G$. nlab_link: https://ncatlab.org/nlab/show/accessible+category dual: null invariant_under_equivalences: true diff --git a/database/data/category-properties/cogenerating set.yaml b/database/data/category-properties/cogenerating set.yaml index b202f1053..031d1b6ab 100644 --- a/database/data/category-properties/cogenerating set.yaml +++ b/database/data/category-properties/cogenerating set.yaml @@ -3,7 +3,7 @@ relation: has a description: >- A set of objects $S$ is called a cogenerating set if for every pair of parallel morphisms $f,g : A \rightrightarrows B$, $f = g$ holds if and only if for every morphism $h : B \to Q$ with $Q \in S$ we have $h \circ f = h \circ g$. Equivalently, the functor $(\Hom(-,Q))_{Q \in S} : \C^{\op} \to (\Set^+)^S$ is faithful. This property refers to the existence of a cogenerating set. - In a locally essentially small category with small products, it is also equivalent to the condition that the canonical morphism + In a locally essentially small category with products, it is also equivalent to the condition that the canonical morphism $$A \to \textstyle\prod_{Q\in S} \prod_{f\in\Hom(A,Q)} Q$$ is a monomorphism for every object $A$. nlab_link: https://ncatlab.org/nlab/show/cogenerator diff --git a/database/data/category-properties/coproducts.yaml b/database/data/category-properties/coproducts.yaml index c44fd5754..7ce44d52b 100644 --- a/database/data/category-properties/coproducts.yaml +++ b/database/data/category-properties/coproducts.yaml @@ -1,6 +1,6 @@ id: coproducts relation: has -description: 'Given a family of objects $(A_i)_{i \in I}$, a coproduct $\coprod_{i \in I} A_i$ is defined as an object with morphisms $i_i : A_i \to \coprod_{i \in I} A_i$ satisfying the following universal property: For every object $T$ and every family of morphisms $(f_i : A_i \to T)_{i \in I}$ there is a unique morphism $f : \coprod_{i \in I} A_i \to T$ such that $f \circ i_i = f_i$ for all $i \in I$. This property refers to the existence of small coproducts, i.e., coproducts of small families of objects.' +description: 'Given a family of objects $(A_i)_{i \in I}$, a coproduct $\coprod_{i \in I} A_i$ is defined as an object with morphisms $i_i : A_i \to \coprod_{i \in I} A_i$ satisfying the following universal property: For every object $T$ and every family of morphisms $(f_i : A_i \to T)_{i \in I}$ there is a unique morphism $f : \coprod_{i \in I} A_i \to T$ such that $f \circ i_i = f_i$ for all $i \in I$. We say that a category has coproducts if every small family $(A_i)_{i \in I}$ (i.e., $I$ is a set) has a coproduct.' nlab_link: https://ncatlab.org/nlab/show/coproduct dual: products invariant_under_equivalences: true diff --git a/database/data/category-properties/cosifted.yaml b/database/data/category-properties/cosifted.yaml index 4ccf56f35..e2f90ee5e 100644 --- a/database/data/category-properties/cosifted.yaml +++ b/database/data/category-properties/cosifted.yaml @@ -1,6 +1,6 @@ id: cosifted relation: is -description: 'A category $\C$ is cosifted if it is inhabited and the diagonal functor $\Delta : \C \to \C \times \C$ is initial, i.e. if it is non-empty and for any two objects $X,Y \in \C$ the category of spans $$X \leftarrow Z \rightarrow Y$$ is connected. Equivalently, a small category $\C$ is cosifted if $\colim : \Set^{{\C}^\op} \to \Set$ preserves finite products. This property is a weaker notion than being cofiltered.' +description: 'A category $\C$ is cosifted if it is inhabited and the diagonal functor $\Delta : \C \to \C \times \C$ is initial, i.e. if it is non-empty and for any two objects $X,Y \in \C$ the category of spans $$X \leftarrow Z \rightarrow Y$$ is connected. A small category $\C$ is cosifted if and only if $\colim : \Set^{{\C}^\op} \to \Set$ preserves finite products. This property is a weaker notion than being cofiltered.' nlab_link: https://ncatlab.org/nlab/show/sifted+category dual: sifted invariant_under_equivalences: true diff --git a/database/data/category-properties/cototal.yaml b/database/data/category-properties/cototal.yaml index a9e58b504..a80469742 100644 --- a/database/data/category-properties/cototal.yaml +++ b/database/data/category-properties/cototal.yaml @@ -7,7 +7,7 @@ description: >- $$y : \C^{\op} \to [\C, \Set]$$ has a left adjoint.
  • Every discrete opfibration $X : \I \to \C$ (with $\I$ not necessarily essentially small) whose fibers are bijective to sets has a limit in $\C$. (Recall that $X$ is a discrete opfibration if for every morphism $f : X_i \to Y$ in $\C$ there exists a unique $\alpha : i \to j$ in $\I$ such that $X_\alpha = f$.)
    • -
  • Let $X : \I \to \C$ be a diagram (with $\I$ not necessarily essentially small) such that for each object $Y$ of $\C$, the collection of connected components of the comma category $X \downarrow Y$ is bijective to a set. Then $X$ has a limit in $\C$.
    • +
  • Let $X : \I \to \C$ be a diagram (with $\I$ not necessarily essentially small) such that for each object $Y$ of $\C$, the collection of connected components of the comma category $X \downarrow Y$ is essentially small, i.e. bijective to a set. Then $X$ has a limit in $\C$.
    • The equivalence is proven as Thm. 5.2 and 5.5 in G. M. Kelly, A survey of totality for enriched and ordinary categories. diff --git a/database/data/category-properties/directed colimits.yaml b/database/data/category-properties/directed colimits.yaml index 5bc2d7e9d..c8969e359 100644 --- a/database/data/category-properties/directed colimits.yaml +++ b/database/data/category-properties/directed colimits.yaml @@ -1,6 +1,6 @@ id: directed colimits relation: has -description: A category has directed colimits if it has colimits of diagrams indexed by directed (small) posets. This is actually equivalent to having filtered colimits. Directed colimits are (somewhat confusingly) also known as inverse limits. +description: A category has directed colimits if it has colimits of diagrams indexed by directed posets. This is actually equivalent to having filtered colimits. Directed colimits are (somewhat confusingly) also known as inverse limits. nlab_link: https://ncatlab.org/nlab/show/directed+colimit dual: directed limits invariant_under_equivalences: true diff --git a/database/data/category-properties/directed limits.yaml b/database/data/category-properties/directed limits.yaml index 3249354a9..07a30cb6a 100644 --- a/database/data/category-properties/directed limits.yaml +++ b/database/data/category-properties/directed limits.yaml @@ -1,6 +1,6 @@ id: directed limits relation: has -description: A category has directed limits if it has limits of diagrams indexed by codirected (small) posets. This is actually equivalent to having cofiltered limits. +description: A category has directed limits if it has limits of diagrams indexed by codirected posets. This is actually equivalent to having cofiltered limits. nlab_link: https://ncatlab.org/nlab/show/directed+limit dual: directed colimits invariant_under_equivalences: true diff --git a/database/data/category-properties/essentially small.yaml b/database/data/category-properties/essentially small.yaml index 41da16023..7b5a61556 100644 --- a/database/data/category-properties/essentially small.yaml +++ b/database/data/category-properties/essentially small.yaml @@ -1,6 +1,6 @@ id: essentially small relation: is -description: A category is essentially small when it is equivalent to a small category. In particular, there is a set of objects such that every object is isomorphic to an object in this set. In contrast to the property of being small, being essentially small is invariant under equivalences of categories. +description: A category is essentially small when it is equivalent to a small category. Equivalently, it is locally essentially small and its collection of objects is essentially small (isomorphic to a set). See here for the set-theoretic foundation of category theory we are working with. In contrast to the property of being small, being essentially small is invariant under equivalences of categories. nlab_link: https://ncatlab.org/nlab/show/small+category dual: essentially small invariant_under_equivalences: true diff --git a/database/data/category-properties/extremal cogenerating set.yaml b/database/data/category-properties/extremal cogenerating set.yaml index f1acbce8c..36acf17cf 100644 --- a/database/data/category-properties/extremal cogenerating set.yaml +++ b/database/data/category-properties/extremal cogenerating set.yaml @@ -3,7 +3,7 @@ relation: has an description: >- A set of objects $S$ is called an extremal cogenerating set if it is a cogenerating set and for every morphism $f : A \to B$, $f$ is an isomorphism if and only if for every object $Q \in S$ we have ${-}\circ f : \Hom(B, Q) \to \Hom(A, Q)$ is a bijection. Equivalently, the functor $(\Hom(-,Q))_{Q \in S} : \C^{\op} \to (\Set^+)^S$ is faithful and conservative. This property refers to the existence of an extremal cogenerating set. - In a locally essentially small category with small products, it is also equivalent to the condition that the canonical morphism + In a locally essentially small category with products, it is also equivalent to the condition that the canonical morphism $$\textstyle A \to \prod_{Q\in S} \prod_{f\in\Hom(A,Q)} Q$$ is an extremal monomorphism for every object $A$, explaining the terminology (see Prop. 5.3 at the nLab). nlab_link: https://ncatlab.org/nlab/show/separator diff --git a/database/data/category-properties/extremal cogenerator.yaml b/database/data/category-properties/extremal cogenerator.yaml index ef53ecd9f..9b512e98e 100644 --- a/database/data/category-properties/extremal cogenerator.yaml +++ b/database/data/category-properties/extremal cogenerator.yaml @@ -3,7 +3,7 @@ relation: has an description: >- An object $Q$ of a category is called an extremal cogenerator if it is a cogenerator and for every morphism $f : A \to B$, if ${-}\circ f : \Hom(B,Q)\to\Hom(A,Q)$ is a bijection, then $f$ is an isomorphism. Equivalently, the functor $\Hom(-,Q) : \C^{\op} \to \Set^+$ is faithful and conservative. This property refers to the existence of an extremal cogenerator. - In a locally essentially small category with small products, it is also equivalent to the condition that the canonical morphism + In a locally essentially small category with products, it is also equivalent to the condition that the canonical morphism $$\textstyle A \to \prod_{f\in\Hom(A,Q)} Q$$ is an extremal monomorphism for every object $A$, explaining the terminology (see Prop. 5.3 at the nLab). diff --git a/database/data/category-properties/extremal generating set.yaml b/database/data/category-properties/extremal generating set.yaml index beb4151d9..253508f5f 100644 --- a/database/data/category-properties/extremal generating set.yaml +++ b/database/data/category-properties/extremal generating set.yaml @@ -3,7 +3,7 @@ relation: has an description: >- A set of objects $S$ is called an extremal generating set if it is a generating set and for every morphism $f : A \to B$, $f$ is an isomorphism if and only if for every object $G \in S$ we have $f \circ {-} : \Hom(G, A) \to \Hom(G, B)$ is a bijection. Equivalently, the functor $(\Hom(G,-))_{G \in S} : \C \to (\Set^+)^S$ is faithful and conservative. This property refers to the existence of an extremal generating set. - In a locally essentially small category with small coproducts, it is also equivalent to the condition that the canonical morphism + In a locally essentially small category with coproducts, it is also equivalent to the condition that the canonical morphism $$\textstyle\bigsqcup_{G\in S} \bigsqcup_{f\in\Hom(G,A)} G \to A$$ is an extremal epimorphism for every object $A$, explaining the terminology (see Prop. 5.3 at the nLab). nlab_link: https://ncatlab.org/nlab/show/separator diff --git a/database/data/category-properties/extremal generator.yaml b/database/data/category-properties/extremal generator.yaml index 086b3fe22..7a0d2a87c 100644 --- a/database/data/category-properties/extremal generator.yaml +++ b/database/data/category-properties/extremal generator.yaml @@ -3,7 +3,7 @@ relation: has an description: >- An object $G$ of a category is called an extremal generator if it is a generator and for every morphism $f : A \to B$, if $f\circ{-} : \Hom(G,A)\to\Hom(G,B)$ is a bijection, then $f$ is an isomorphism. Equivalently, the functor $\Hom(G,-) : \C \to \Set^+$ is faithful and conservative. This property refers to the existence of an extremal generator. - In a locally essentially small category with small coproducts, it is also equivalent to the condition that the canonical morphism + In a locally essentially small category with coproducts, it is also equivalent to the condition that the canonical morphism $$\textstyle\bigsqcup_{f\in\Hom(G,A)} G \to A$$ is an extremal epimorphism for every object $A$, explaining the terminology (see Prop. 5.3 at the nLab). diff --git a/database/data/category-properties/finitely accessible.yaml b/database/data/category-properties/finitely accessible.yaml index 66945f526..6df331fde 100644 --- a/database/data/category-properties/finitely accessible.yaml +++ b/database/data/category-properties/finitely accessible.yaml @@ -1,6 +1,6 @@ id: finitely accessible relation: is -description: A category is finitely accessible if it has filtered colimits and there is a (small) set $G$ of finitely presentable objects such that every object is a filtered colimit of objects in $G$. +description: A category is finitely accessible if it has filtered colimits and there is an essentially small collection $G$ of finitely presentable objects such that every object is a filtered colimit of objects in $G$. nlab_link: https://ncatlab.org/nlab/show/accessible+category dual: null invariant_under_equivalences: true diff --git a/database/data/category-properties/generalized variety.yaml b/database/data/category-properties/generalized variety.yaml index b68412999..d8cdaaaf0 100644 --- a/database/data/category-properties/generalized variety.yaml +++ b/database/data/category-properties/generalized variety.yaml @@ -1,6 +1,6 @@ id: generalized variety relation: is a -description: A category is a generalized variety if it has sifted colimits and there is a (small) set $G$ of strongly finitely presentable objects such that every object is a sifted colimit of objects from $G$. Generalized varieties are like locally strongly finitely presentable categories but without colimits. The relation is similar as between finitely accessible and locally finitely presentable categories. This notion is defined in [AR01, Def. 3.6]. +description: A category is a generalized variety if it has sifted colimits and there is an essentially small collection $G$ of strongly finitely presentable objects such that every object is a sifted colimit of objects from $G$. Generalized varieties are like locally strongly finitely presentable categories but without colimits. The relation is similar as between finitely accessible and locally finitely presentable categories. This notion is defined in [AR01, Def. 3.6]. nlab_link: null dual: null invariant_under_equivalences: true diff --git a/database/data/category-properties/generating set.yaml b/database/data/category-properties/generating set.yaml index 7f847d270..96baa6a30 100644 --- a/database/data/category-properties/generating set.yaml +++ b/database/data/category-properties/generating set.yaml @@ -3,7 +3,7 @@ relation: has a description: >- A set of objects $S$ is called a generating set if for every pair of parallel morphisms $f,g : A \rightrightarrows B$, $f = g$ holds if and only if for every morphism $h : G \to A$ with $G \in S$ we have $f \circ h = g \circ h$. Equivalently, the functor $(\Hom(G,-))_{G \in S} : \C \to (\Set^+)^S$ is faithful. This property refers to the existence of a generating set. - In a locally essentially small category with small coproducts, it is also equivalent to the condition that the canonical morphism + In a locally essentially small category with coproducts, it is also equivalent to the condition that the canonical morphism $$\textstyle\bigsqcup_{G\in S} \bigsqcup_{f\in\Hom(G,A)} G \to A$$ is an epimorphism for every object $A$. nlab_link: https://ncatlab.org/nlab/show/separator diff --git a/database/data/category-properties/locally essentially small.yaml b/database/data/category-properties/locally essentially small.yaml index 9cbc23ed0..8a845f2ce 100644 --- a/database/data/category-properties/locally essentially small.yaml +++ b/database/data/category-properties/locally essentially small.yaml @@ -1,8 +1,8 @@ id: locally essentially small relation: is description: >- - A category is locally essentially small when for every pair of objects $A,B$ the collection of morphisms $A \to B$ is isomorphic to a set; see here for the set-theoretic foundation of category theory we are working with. - A category is locally essentially small if and only if it is equivalent to a locally small category. In contrast to being locally small, this condition is invariant under equivalences of categories. This is why we have added it to the database. For instance, every algebraic category is locally essentially small, but not necessarily locally small. This indicates that this is the "right" notion to work with. + A category is locally essentially small when for every pair of objects $A,B$ the collection $\Hom(A,B)$ of morphisms $A \to B$ is essentially small, i.e. isomorphic to a set; see here for the set-theoretic foundation of category theory we are working with. + A category is locally essentially small if and only if it is equivalent to a locally small category. In contrast to being locally small, this condition is invariant under equivalences of categories. This is why we have added it to the database. For instance, every algebraic category is locally essentially small, but not necessarily locally small. This indicates that, from a structural perspective, this is the right notion to work with. nlab_link: null dual: locally essentially small invariant_under_equivalences: true diff --git a/database/data/category-properties/locally small.yaml b/database/data/category-properties/locally small.yaml index ee222525b..68b78a74b 100644 --- a/database/data/category-properties/locally small.yaml +++ b/database/data/category-properties/locally small.yaml @@ -1,6 +1,6 @@ id: locally small relation: is -description: A category is locally small when for every pair of objects $A,B$ the collection of morphisms $A \to B$ is a set; see here for the set-theoretic foundation of category theory we are working with. +description: A category is locally small when for every pair of objects $A,B$ the collection $\Hom(A,B)$ of morphisms $A \to B$ is a set. See here for the set-theoretic foundation of category theory we are working with. nlab_link: https://ncatlab.org/nlab/show/locally+small+category dual: locally small invariant_under_equivalences: false diff --git a/database/data/category-properties/multi-algebraic.yaml b/database/data/category-properties/multi-algebraic.yaml index 0596c18c5..ef676b343 100644 --- a/database/data/category-properties/multi-algebraic.yaml +++ b/database/data/category-properties/multi-algebraic.yaml @@ -3,7 +3,7 @@ relation: is description: >- A category is multi-algebraic if it satisfies one of the following equivalent conditions:
      -
    1. It is a multi-cocomplete generalized variety, that is, it has multi-colimits and sifted colimits of all small diagrams, and there is a (small) set $G$ of strongly finitely presentable objects such that every object is a sifted colimit of objects from $G$.
      2. +
    2. It is a multi-cocomplete generalized variety, that is, it has multi-colimits, sifted colimits, and there is an essentially small collection $G$ of strongly finitely presentable objects such that every object is a sifted colimit of objects from $G$.
    3. It is equivalent to the category of models of a small (finite product, coproduct)-sketch, shortly small FPC-sketch.
    4. It is equivalent to the category of multi-finite-product-preserving functors to $\Set$ from a small category with multi-finite-products (multi-algebraic theory). Here, multi-finite-products means multi-limits of finite discrete diagrams.
    5. It is equivalent to the category of models of a small multi-finite-product sketch.
      6. diff --git a/database/data/category-properties/multi-initial object.yaml b/database/data/category-properties/multi-initial object.yaml index e7ff72968..6ebe6b740 100644 --- a/database/data/category-properties/multi-initial object.yaml +++ b/database/data/category-properties/multi-initial object.yaml @@ -1,6 +1,6 @@ id: multi-initial object relation: has a -description: A category has a multi-initial object if the empty diagram has a multi-colimit. That is, there is a small family of objects $(X_i)_{i \in I}$ such that for every object $Y$ there is a unique index $i \in I$ with a unique morphism $X_i \to Y$. A category has a multi-initial object if and only if the collection of all connected components is isomorphic to a set, and each connected component has a initial object. +description: A category has a multi-initial object if the empty diagram has a multi-colimit. That is, there is an essentially small collection of objects $\I$ such that for every object $Y$ there is a unique object $X \in \I$ with a unique morphism $X \to Y$. A category has a multi-initial object if and only if the collection of its connected components is essentially small and each connected component has an initial object. nlab_link: https://ncatlab.org/nlab/show/multilimit dual: multi-terminal object invariant_under_equivalences: true diff --git a/database/data/category-properties/multi-terminal object.yaml b/database/data/category-properties/multi-terminal object.yaml index 9b633fbbb..a00a337b2 100644 --- a/database/data/category-properties/multi-terminal object.yaml +++ b/database/data/category-properties/multi-terminal object.yaml @@ -1,6 +1,6 @@ id: multi-terminal object relation: has a -description: A category has a multi-terminal object if the empty diagram has a multi-limit. That is, there is a small family of objects $(X_i)_{i \in I}$ such that for every object $Y$ there is a unique index $i \in I$ with a unique morphism $Y \to X_i$. A category has a multi-terminal object if and only if the collection of all connected components is isomorphic to a set, and each connected component has a terminal object. +description: A category has a multi-terminal object if the empty diagram has a multi-limit. That is, there is an essentially small collection of objects $\I$ such that for every object $Y$ there is a unique object $X \in \I$ with a unique morphism $Y \to X$. A category has a multi-terminal object if and only if the collection of its connected components is essentially small and each connected component has a terminal object. nlab_link: https://ncatlab.org/nlab/show/multilimit dual: multi-initial object invariant_under_equivalences: true diff --git a/database/data/category-properties/products.yaml b/database/data/category-properties/products.yaml index 568862b80..d5fa7f150 100644 --- a/database/data/category-properties/products.yaml +++ b/database/data/category-properties/products.yaml @@ -1,6 +1,6 @@ id: products relation: has -description: 'Given a family of objects $(A_i)_{i \in I}$, a product $\prod_{i \in I} A_i$ is defined as an object with morphisms $p_i : \prod_{i \in I} A_i \to A_i$ satisfying the following universal property: For every object $T$ and every family of morphisms $(f_i : T \to A_i)_{i \in I}$ there is a unique morphism $f : T \to \prod_{i \in I} A_i$ such that $p_i \circ f = f_i$ for all $i \in I$. This property refers to the existence of small products, i.e., products of small families of objects.' +description: 'Given a family of objects $(A_i)_{i \in I}$, a product $\prod_{i \in I} A_i$ is defined as an object with morphisms $p_i : \prod_{i \in I} A_i \to A_i$ satisfying the following universal property: For every object $T$ and every family of morphisms $(f_i : T \to A_i)_{i \in I}$ there is a unique morphism $f : T \to \prod_{i \in I} A_i$ such that $p_i \circ f = f_i$ for all $i \in I$. We say that a category has products if every small family $(A_i)_{i \in I}$ (i.e., $I$ is a set) has a product.' nlab_link: https://ncatlab.org/nlab/show/cartesian+product dual: coproducts invariant_under_equivalences: true diff --git a/database/data/category-properties/sifted.yaml b/database/data/category-properties/sifted.yaml index ee62667b2..ff02d40bf 100644 --- a/database/data/category-properties/sifted.yaml +++ b/database/data/category-properties/sifted.yaml @@ -3,7 +3,7 @@ relation: is description: >- A category $\C$ is sifted if it is inhabited and the diagonal functor $\Delta : \C \to \C \times \C$ is final, i.e. if it is non-empty and for any two objects $X,Y \in \C$ the category of cospans $$X \rightarrow Z \leftarrow Y$$ - is connected. Equivalently, a small category $\C$ is sifted if $\colim : \Set^{\C} \to \Set$ preserves finite products. This property is a weaker notion than being filtered. + is connected. A small category $\C$ is sifted if and only if $\colim : \Set^{\C} \to \Set$ preserves finite products. This property is a weaker notion than being filtered. nlab_link: https://ncatlab.org/nlab/show/sifted+category dual: cosifted invariant_under_equivalences: true diff --git a/database/data/category-properties/small.yaml b/database/data/category-properties/small.yaml index f136c9a7c..3478aba13 100644 --- a/database/data/category-properties/small.yaml +++ b/database/data/category-properties/small.yaml @@ -1,6 +1,6 @@ id: small relation: is -description: A category is small when the collection of objects and the collection of morphisms are sets, i.e. small. +description: A category is small when the collection of objects and the collection of morphisms are sets, i.e. small. See here for the set-theoretic foundation of category theory we are working with. nlab_link: https://ncatlab.org/nlab/show/small+category dual: small invariant_under_equivalences: false diff --git a/database/data/category-properties/total.yaml b/database/data/category-properties/total.yaml index 5023fd42f..ef8a19706 100644 --- a/database/data/category-properties/total.yaml +++ b/database/data/category-properties/total.yaml @@ -7,7 +7,7 @@ description: >- $$y : \C \to [\C^{\op}, \Set]$$ has a left adjoint. For a concrete example of how such a left adjoint could look, see here.
    6. Every discrete fibration $X : \I \to \C$ (with $\I$ not necessarily essentially small) whose fibers are bijective to sets has a colimit in $\C$. (Recall that $X$ is a discrete fibration if for every morphism $f : Y \to X_i$ in $\C$ there exists a unique $\alpha : j \to i$ in $\I$ such that $X_\alpha = f$.)
      7. -
    7. Let $X : \I \to \C$ be a diagram (with $\I$ not necessarily essentially small) such that for each object $Y$ of $\C$, the collection of connected components of the comma category $Y \downarrow X$ is bijective to a set. Then $X$ has a colimit in $\C$.
      8. +
    8. Let $X : \I \to \C$ be a diagram (with $\I$ not necessarily essentially small) such that for each object $Y$ of $\C$, the collection of connected components of the comma category $Y \downarrow X$ is essentially small. Then $X$ has a colimit in $\C$.
    The equivalence is proven as Thm. 5.2 and 5.5 in G. M. Kelly, A survey of totality for enriched and ordinary categories. diff --git a/database/data/category-properties/well-copowered.yaml b/database/data/category-properties/well-copowered.yaml index 33692a16f..77cb15842 100644 --- a/database/data/category-properties/well-copowered.yaml +++ b/database/data/category-properties/well-copowered.yaml @@ -1,6 +1,6 @@ id: well-copowered relation: is -description: A category is well-copowered if the collection of quotients of any object is isomorphic to a set. +description: A category is well-copowered if the collection of quotients of any object is essentially small. Equivalently, for every object $X$, there is a small family of epimorphisms $(X \twoheadrightarrow Y_i)_{i \in I}$ (i.e., $I$ is a set) such that every epimorphism $X \twoheadrightarrow Y$ is isomorphic to some epimorphism in the family. nlab_link: https://ncatlab.org/nlab/show/well-powered+category dual: well-powered invariant_under_equivalences: true diff --git a/database/data/category-properties/well-powered.yaml b/database/data/category-properties/well-powered.yaml index 204ccb550..9b7daa71f 100644 --- a/database/data/category-properties/well-powered.yaml +++ b/database/data/category-properties/well-powered.yaml @@ -1,6 +1,6 @@ id: well-powered relation: is -description: A category is well-powered if the collection of subobjects of any object is isomorphic to a set. +description: A category is well-powered if the collection of subobjects of any object is essentially small. Equivalently, for every object $X$, there is a small family of monomorphisms $(Y_i \hookrightarrow X)_{i \in I}$ (i.e., $I$ is a set) such that every monomorphism $Y \hookrightarrow X$ is isomorphic to some monomorphism in the family. nlab_link: https://ncatlab.org/nlab/show/well-powered+category dual: well-copowered invariant_under_equivalences: true diff --git a/database/data/category-properties/wide pullbacks.yaml b/database/data/category-properties/wide pullbacks.yaml index 22fdf3495..8b74ffb2c 100644 --- a/database/data/category-properties/wide pullbacks.yaml +++ b/database/data/category-properties/wide pullbacks.yaml @@ -1,12 +1,13 @@ id: wide pullbacks relation: has -description: A category $\C$ has wide pullbacks if for every object $S$ the slice category $\C/S$ has arbitrary small products. +description: A category $\C$ has wide pullbacks if for every object $S$ the slice category $\C/S$ has products. nlab_link: https://ncatlab.org/nlab/show/wide+pullback dual: wide pushouts invariant_under_equivalences: true related: - pullbacks + - products tags: - limits diff --git a/database/data/category-properties/wide pushouts.yaml b/database/data/category-properties/wide pushouts.yaml index e85776b1e..9845001bf 100644 --- a/database/data/category-properties/wide pushouts.yaml +++ b/database/data/category-properties/wide pushouts.yaml @@ -1,12 +1,13 @@ id: wide pushouts relation: has -description: A category $\C$ has wide pushouts if for every object $S$ the coslice category $S/\C$ has arbitrary small coproducts. +description: A category $\C$ has wide pushouts if for every object $S$ the coslice category $S/\C$ has coproducts. nlab_link: https://ncatlab.org/nlab/show/wide+pushout dual: wide pullbacks invariant_under_equivalences: true related: - pushouts + - coproducts tags: - colimits diff --git a/database/data/functor-properties/cocontinuous.yaml b/database/data/functor-properties/cocontinuous.yaml index dd421a093..d003455f8 100644 --- a/database/data/functor-properties/cocontinuous.yaml +++ b/database/data/functor-properties/cocontinuous.yaml @@ -1,6 +1,6 @@ id: cocontinuous relation: is -description: A functor is cocontinuous when it preserves all small colimits. +description: A functor is cocontinuous when it preserves colimits (which are assumed to be small unless otherwise stated). nlab_link: https://ncatlab.org/nlab/show/cocontinuous+functor invariant_under_equivalences: true dual: continuous diff --git a/database/data/functor-properties/continuous.yaml b/database/data/functor-properties/continuous.yaml index 235d5e8a7..9c613523e 100644 --- a/database/data/functor-properties/continuous.yaml +++ b/database/data/functor-properties/continuous.yaml @@ -1,6 +1,6 @@ id: continuous relation: is -description: A functor is continuous when it preserves all small limits. +description: A functor is continuous when it preserves limits (which are assumed to be small unless otherwise stated). nlab_link: https://ncatlab.org/nlab/show/continuous+functor invariant_under_equivalences: true dual: cocontinuous diff --git a/database/data/functors/simple_group_probing.yaml b/database/data/functors/simple_group_probing.yaml index 60edf66e0..7445a57c0 100644 --- a/database/data/functors/simple_group_probing.yaml +++ b/database/data/functors/simple_group_probing.yaml @@ -6,9 +6,9 @@ codomain: Set description: >- This functor maps a group $G$ to the collection $$F(G) \coloneqq \textstyle\prod_{\kappa} \Hom(L_\kappa,G),$$ - where $\kappa$ ranges over all infinite cardinals and $L_\kappa$ is an infinite simple group of cardinality $\kappa$; we choose $L_\kappa \coloneqq \Alt_{\fin}(\kappa)$ to make things concrete. For each $G$, the collection $F(G)$ is isomorphic to a set, since for $\kappa > \card(G)$ every homomorphism $L_\kappa \to G$ is trivial. Thus, a more precise definition would be + where $\kappa$ ranges over all infinite cardinals and $L_\kappa$ is an infinite simple group of cardinality $\kappa$; we choose $L_\kappa \coloneqq \Alt_{\fin}(\kappa)$ to make things concrete. For each $G$, the collection $F(G)$ is essentially small, since for $\kappa > \card(G)$ every homomorphism $L_\kappa \to G$ is trivial. Thus, a more precise definition would be $$F(G) \coloneqq \textstyle\prod_{\kappa \leq \card(G)} \Hom(L_\kappa,G),$$ - but the first definition makes it more apparent that $F$ is a functor. + since only then $F(G)$ is actually a set, but the first definition makes it more apparent that $F$ is a functor. This is the canonical example of a continuous functor $\Grp \to \Set$ that is not representable, and not a right adjoint. nlab_link: null left_adjoint: null From a9ad15d5366b994474fcd33d39523e8c8fbab666 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 11 Sep 2026 15:25:25 +0200 Subject: [PATCH 2/3] rename generating set -> generating collection same with the dual and the extremal versions --- content/foundations.md | 4 +-- content/generator_construction.md | 10 +++---- content/missing_cogenerating_collections.md | 19 +++++++++++++ content/missing_cogenerating_sets.md | 19 ------------- content/subcategories.md | 6 ++-- database/data/categories/FiltVect.yaml | 4 +-- database/data/categories/Fld.yaml | 6 ++-- database/data/categories/Fld_0.yaml | 4 +-- database/data/categories/Haus.yaml | 4 +-- database/data/categories/LRS_R.yaml | 2 +- database/data/categories/Meas.yaml | 8 +++--- database/data/categories/Mono.yaml | 2 +- database/data/categories/PreOrd.yaml | 2 +- database/data/categories/Sch_R.yaml | 4 +-- database/data/categories/Set_ff.yaml | 4 +-- database/data/categories/Top.yaml | 8 +++--- database/data/categories/Top_pointed.yaml | 6 ++-- database/data/categories/TorsFreeAb.yaml | 4 +-- database/data/categories/Unif.yaml | 6 ++-- database/data/categories/sSet.yaml | 2 +- .../category-implications/accessible.yaml | 6 ++-- .../data/category-implications/algebraic.yaml | 4 +-- .../disjoint coproducts.yaml | 4 +-- .../category-implications/generators.yaml | 28 +++++++++---------- .../data/category-implications/groupoids.yaml | 8 ++++-- database/data/category-implications/size.yaml | 10 +++---- database/data/category-implications/thin.yaml | 2 +- .../data/category-implications/topos.yaml | 2 +- .../data/category-implications/total.yaml | 2 +- .../cogenerating collection.yaml | 22 +++++++++++++++ .../category-properties/cogenerating set.yaml | 18 ------------ .../data/category-properties/cogenerator.yaml | 7 +++-- .../category-properties/concretizable.yaml | 2 +- .../extremal cogenerating collection.yaml | 19 +++++++++++++ .../extremal cogenerating set.yaml | 18 ------------ .../extremal cogenerator.yaml | 4 +-- .../extremal generating collection.yaml | 19 +++++++++++++ .../extremal generating set.yaml | 18 ------------ .../extremal generator.yaml | 4 +-- .../generating collection.yaml | 23 +++++++++++++++ .../category-properties/generating set.yaml | 19 ------------- .../data/category-properties/generator.yaml | 7 +++-- .../data/functor-implications/adjoints.yaml | 2 +- .../closed.yaml | 2 +- database/scripts/expected-data/Ab.json | 8 +++--- database/scripts/expected-data/Set.json | 8 +++--- database/scripts/expected-data/Top.json | 8 +++--- src/routes/download/+page.svelte | 4 +-- 48 files changed, 210 insertions(+), 192 deletions(-) create mode 100644 content/missing_cogenerating_collections.md delete mode 100644 content/missing_cogenerating_sets.md create mode 100644 database/data/category-properties/cogenerating collection.yaml delete mode 100644 database/data/category-properties/cogenerating set.yaml create mode 100644 database/data/category-properties/extremal cogenerating collection.yaml delete mode 100644 database/data/category-properties/extremal cogenerating set.yaml create mode 100644 database/data/category-properties/extremal generating collection.yaml delete mode 100644 database/data/category-properties/extremal generating set.yaml create mode 100644 database/data/category-properties/generating collection.yaml delete mode 100644 database/data/category-properties/generating set.yaml diff --git a/content/foundations.md b/content/foundations.md index ae571fe6a..5f40e9d8f 100644 --- a/content/foundations.md +++ b/content/foundations.md @@ -31,9 +31,9 @@ In our framework, there is no way to group all hypercollections into a single ma ## Essentially small, finite, and countable collections -Let us call a collection $X$ _essentially small_ if it is isomorphic to a set $S$, i.e., if there is a bijection between $X$ and $S$. For most parts of category theory, $X$ can then simply be replaced with $S$ and assumed to be small itself, i.e., a set. +Let us call a collection $X$ _essentially small_ if it is isomorphic to a set $S$, i.e., if there is a bijection between $X$ and $S$. (An alternative terminology suggested [here](https://ncatlab.org/nlab/show/small+category) is _structurally small_.) For most parts of category theory, $X$ can then simply be replaced with $S$ and assumed to be small itself, i.e., a set. -For example, the collection $\{\SetColl\}$ is not small, but essentially small, since it is isomorphic to the set $\{0\}$. This shows that the three levels are not defined by cardinality alone. +For example, the collection $\{\SetColl\}$ is not small, but essentially small, since it is isomorphic to the set $\{0\}$. This example shows that the three levels are not defined by cardinality alone. It also shows that the elements of a collection are not necessarily sets, which is yet another fundamental difference to classes. If a collection $X$ admits a surjective map from a set $S$, then it is also essentially small, since by the axiom of choice $X$ is isomorphic to a subset of $S$. diff --git a/content/generator_construction.md b/content/generator_construction.md index d0bf28a4d..97d9563be 100644 --- a/content/generator_construction.md +++ b/content/generator_construction.md @@ -1,18 +1,18 @@ --- title: Construction of generators -description: How to construct a generator from a generating set +description: How to construct a generator from a generating collection --- # Construction of generators ::: Lemma -In a category let $S$ be a generating set which is [strongly connected](/category-property/strongly_connected), i.e. between any two objects $G,G' \in S$ there is a morphism $G \to G'$. If the coproduct $U \coloneqq \coprod_{G \in S} G$ exists, then it is a generator. Moreover, if $S$ is an extremal generating set, then $U$ is an extremal generator. +In a category let $S$ be a generating collection which is [strongly connected](/category-property/strongly_connected), i.e. between any two objects $G,G' \in S$ there is a morphism $G \to G'$. If the coproduct $U \coloneqq \coprod_{G \in S} G$ exists, then it is a generator. Moreover, if $S$ is an extremal generating collection, then $U$ is an extremal generator. ::: ::: Proof -We remark that the assumption on $S$ implies that each coprojection $i_G : G \to U$ has a left inverse. Now let $f,g : A \rightrightarrows B$ be two morphisms with $f \circ \bar a = g \circ \bar a$ for all $\bar a : U \to A$. If $G \in S$, any morphism $G \to A$ extends to $U$ by our preliminary remark. Thus, $f \circ a = g \circ a$ holds for all morphisms $a : G \to A$ with $G \in S$. Since $S$ is a generating set, this implies $f = g$. +We remark that the assumption on $S$ implies that each coprojection $i_G : G \to U$ has a left inverse. Now let $f,g : A \rightrightarrows B$ be two morphisms with $f \circ \bar a = g \circ \bar a$ for all $\bar a : U \to A$. If $G \in S$, any morphism $G \to A$ extends to $U$ by our preliminary remark. Thus, $f \circ a = g \circ a$ holds for all morphisms $a : G \to A$ with $G \in S$. Since $S$ is a generating collection, this implies $f = g$. -Similarly, for the case where $S$ is an extremal generating set, suppose we have a morphism $f : A \to B$ such that $f \circ {-} : \Hom(U, A) \to \Hom(U, B)$ is a bijection. In particular, because it is injective and $U$ is a generator, we can conclude that $f$ is a monomorphism, so $f \circ {-} : \Hom(G, A) \to \Hom(G, B)$ is injective for each $G \in S$. Now suppose $b \in \Hom(G, B)$ for $G \in S$. Then $b$ extends to a morphism $\bar b : U \to B$. By assumption, there exists $\bar a : U \to A$ such that $f \circ \bar a = \bar b$. Composing with the coprojection $i_G : G \to U$, we see +Similarly, for the case where $S$ is an extremal generating collection, suppose we have a morphism $f : A \to B$ such that $f \circ {-} : \Hom(U, A) \to \Hom(U, B)$ is a bijection. In particular, because it is injective and $U$ is a generator, we can conclude that $f$ is a monomorphism, so $f \circ {-} : \Hom(G, A) \to \Hom(G, B)$ is injective for each $G \in S$. Now suppose $b \in \Hom(G, B)$ for $G \in S$. Then $b$ extends to a morphism $\bar b : U \to B$. By assumption, there exists $\bar a : U \to A$ such that $f \circ \bar a = \bar b$. Composing with the coprojection $i_G : G \to U$, we see $$f \circ \bar a \circ i_G = \bar b \circ i_G = b.$$ -This shows that $f \circ {-} : \Hom(G, A) \to \Hom(G, B)$ is also surjective for each $G \in S$. Since $S$ is an extremal generating set, this implies $f$ is an isomorphism. +This shows that $f \circ {-} : \Hom(G, A) \to \Hom(G, B)$ is also surjective for each $G \in S$. Since $S$ is an extremal generating collection, this implies $f$ is an isomorphism. ::: diff --git a/content/missing_cogenerating_collections.md b/content/missing_cogenerating_collections.md new file mode 100644 index 000000000..f17e0d41d --- /dev/null +++ b/content/missing_cogenerating_collections.md @@ -0,0 +1,19 @@ +--- +title: Missing cogenerating collections +description: A generalization of the proof that the category of commutative rings has no cogenerating collection. +--- + +# Missing cogenerating collections + +::: Lemma +Let $\C$ be a category with a faithful functor $U: \C \to \Set$. Assume there exists a collection of objects $\F \subseteq \Ob(\C)$ satisfying the following conditions: + +1. For any $X \in \F$ and any non-terminal $Y \in \C$, for every morphism $f: X \to Y$ its underlying map $U(f) : U(X) \to U(Y)$ is injective. +2. For every infinite cardinal number $\kappa$, there exists an object $X \in \F$ such that $\card(U(X)) \geq \kappa$ and such that $X$ has a non-identity endomorphism. + +Then $\C$ does not have a cogenerating collection. +::: + +::: Proof +Assume that there is a cogenerating collection $S$. By assumption (2) there is an object $X \in \F$ such that $U(X)$ is larger than all the $U(Y)$ with $Y \in S$ (w.r.t. cardinalities) and which has a non-identity endomorphism $\sigma : X \to X$. Since $S$ cogenerates, there is a morphism $f : X \to Y$ with $Y \in S$ and $f \sigma \neq f$. For this, $Y$ must be non-terminal. By (1) the map $U(f) : U(X) \to U(Y)$ is injective. This is a contradiction. +::: diff --git a/content/missing_cogenerating_sets.md b/content/missing_cogenerating_sets.md deleted file mode 100644 index 9a97f67ce..000000000 --- a/content/missing_cogenerating_sets.md +++ /dev/null @@ -1,19 +0,0 @@ ---- -title: Missing cogenerating sets -description: A generalization of the proof that the category of commutative rings has no cogenerating set. ---- - -# Missing cogenerating sets - -::: Lemma -Let $\C$ be a category with a faithful functor $U: \C \to \Set$. Assume there exists a collection of objects $\F \subseteq \Ob(\C)$ satisfying the following conditions: - -1. For any $X \in \F$ and any non-terminal $Y \in \C$, for every morphism $f: X \to Y$ its underlying map $U(f) : U(X) \to U(Y)$ is injective. -2. For every infinite cardinal number $\kappa$, there exists an object $X \in \F$ such that $\card(U(X)) \geq \kappa$ and such that $X$ has a non-identity endomorphism. - -Then $\C$ does not have a cogenerating set. -::: - -::: Proof -Assume that there is a cogenerating set $S$. By assumption (2) there is an object $X \in \F$ such that $U(X)$ is larger than all the $U(Y)$ with $Y \in S$ (w.r.t. cardinalities) and which has a non-identity endomorphism $\sigma : X \to X$. Since $S$ cogenerates, there is a morphism $f : X \to Y$ with $Y \in S$ and $f \sigma \neq f$. For this, $Y$ must be non-terminal. By (1) the map $U(f) : U(X) \to U(Y)$ is injective. This is a contradiction. -::: diff --git a/content/subcategories.md b/content/subcategories.md index a7aac4051..2dc04ad8c 100644 --- a/content/subcategories.md +++ b/content/subcategories.md @@ -112,11 +112,11 @@ Here, $UE \rightrightarrows UX$ is a congruence: the map $UE \to UX \times UX$ i ::: ::: Lemma 9 -Let $L$ be a functor which is left adjoint to a faithful functor $U$. Then $L$ preserves generating sets. (Thus in particular, any reflective subcategory of a category with a generating set also has a generating set; and similarly for a single generator.) +Let $L$ be a functor which is left adjoint to a faithful functor $U$. Then $L$ preserves generating collections. (Thus in particular, any reflective subcategory of a category with a generating collection also has a generating collection; and similarly for a single generator.) ::: ::: Proof -If $S$ is a generating set, +If $S$ is a generating collection, $$ \begin{align*} @@ -129,7 +129,7 @@ is a composition of faithful functors, hence faithful. ::: ::: Lemma 10 -Any fully faithful functor reflects extremal generating sets (and therefore, by duality, it also reflects extremal cogenerating sets). In other words, if $U : \C \to \D$ is a fully faithful functor, and $S$ is a set of objects such that $U(S)$ is an extremal generating set of $\D$, then $S$ is an extremal generating set of $\C$. +Any fully faithful functor reflects extremal generating collections (and therefore, by duality, it also reflects extremal cogenerating collections). In other words, if $U : \C \to \D$ is a fully faithful functor, and $S$ is an essentially small collection of objects such that $U(S)$ is an extremal generating collection of $\D$, then $S$ is an extremal generating collection of $\C$. ::: ::: Proof diff --git a/database/data/categories/FiltVect.yaml b/database/data/categories/FiltVect.yaml index 4501bd651..a07b49a25 100644 --- a/database/data/categories/FiltVect.yaml +++ b/database/data/categories/FiltVect.yaml @@ -51,9 +51,9 @@ satisfied_properties: proof: It is straightforward to check that the vector space $K$ equipped with the maximal filtration $F^n(K) \coloneqq K$ is a cogenerator. check_redundancy: false - - property: extremal cogenerating set + - property: extremal cogenerating collection proof: >- - Let $K_n$ denote the vector space $K$ equipped with the filtration such that $F_m(K) = K$ for $m < n$ and $F_m(K) = 0$ for $m \ge n$; and similarly, let $K_\infty$ denote the vector space equipped with the filtration such that $F_m(K) = K$ for each $m$. Then $K_n$ represents the functor mapping $(V, F)$ to $F_n(V)^\perp$, i.e. the space of functionals on $V$ whose kernels contain $F_n(V)$. Also, $K_\infty$ represents the functor sending $(V, F)$ to the dual $V^*$; and the canonical epimorphism $K_\infty \twoheadrightarrow K_n$ corresponds under the Yoneda embedding to the natural inclusion $F_n(V)^\perp \hookrightarrow V^*$. We claim that $\{ K_n : n \in \IZ \} \cup \{ K_\infty \}$ is an extremal cogenerating set of $\FiltVect_K$. + Let $K_n$ denote the vector space $K$ equipped with the filtration such that $F_m(K) = K$ for $m < n$ and $F_m(K) = 0$ for $m \ge n$; and similarly, let $K_\infty$ denote the vector space equipped with the filtration such that $F_m(K) = K$ for each $m$. Then $K_n$ represents the functor mapping $(V, F)$ to $F_n(V)^\perp$, i.e. the space of functionals on $V$ whose kernels contain $F_n(V)$. Also, $K_\infty$ represents the functor sending $(V, F)$ to the dual $V^*$; and the canonical epimorphism $K_\infty \twoheadrightarrow K_n$ corresponds under the Yoneda embedding to the natural inclusion $F_n(V)^\perp \hookrightarrow V^*$. We claim that $\{ K_n : n \in \IZ \} \cup \{ K_\infty \}$ is an extremal cogenerating collection of $\FiltVect_K$. First, the set includes $K_\infty$, which we have already seen above is a cogenerator of $\FiltVect_K$. Now, suppose we have a morphism $f : (V, F) \to (W, G)$ such that $${-} \circ f : \Hom((W, G), K_\infty) \to \Hom((V, F), K_\infty)$$ diff --git a/database/data/categories/Fld.yaml b/database/data/categories/Fld.yaml index 4dd09eb54..22b3c5a1b 100644 --- a/database/data/categories/Fld.yaml +++ b/database/data/categories/Fld.yaml @@ -54,9 +54,9 @@ unsatisfied_properties: - property: generator proof: Assume that $G$ is a generator, say of characteristic $p$. Then for all $q \neq p$, all homomorphisms between two fields of characteristic $q$ would be equal, which is absurd. - - property: cogenerating set - proof: 'We apply this lemma to the collection of fields: Any homomorphism of fields is injective. For every infinite cardinal $\kappa$, the field of rational functions in $\kappa$ variables has cardinality $\geq \kappa$ and a non-trivial automorphism (swapping two variables).' - label: Fld_no_cogenerating_set + - property: cogenerating collection + proof: 'We apply this lemma to the collection of fields: Any homomorphism of fields is injective. For every infinite cardinal $\kappa$, the field of rational functions in $\kappa$ variables has cardinality $\geq \kappa$ and a non-trivial automorphism (swapping two variables).' + label: Fld_no_cogenerating_collection - property: binary powers proof: 'Assume that the product $P \coloneqq \IQ(\sqrt{2}) \times \IQ(\sqrt{2})$ exists. This field is isomorphic to a subfield of $\IQ(\sqrt{2})$, hence $P \cong \IQ$ or $P \cong \IQ(\sqrt{2})$. In the first case, the two projections $P \rightrightarrows \IQ(\sqrt{2})$ must be equal, which means that every two homomorphisms $K \rightrightarrows \IQ(\sqrt{2})$ are equal, which is absurd (take $K = \IQ(\sqrt{2})$ and its two automorphisms). In the second case, the projections induce for every field $K$ a bijection $\Hom(K,\IQ(\sqrt{2})) \cong \Hom(K,\IQ(\sqrt{2}))^2$, which, however, fails for $K = \IQ(\sqrt{2})$: the left-hand side has $2$ elements, while the right-hand side has $4$ elements. A more general result about products in $\Fld$ can be found at MSE/359352.' diff --git a/database/data/categories/Fld_0.yaml b/database/data/categories/Fld_0.yaml index 5a7f4e0b4..db2ad9bff 100644 --- a/database/data/categories/Fld_0.yaml +++ b/database/data/categories/Fld_0.yaml @@ -45,10 +45,10 @@ unsatisfied_properties: - property: semi-strongly connected proof: There is no homomorphism from $\IQ(\sqrt{2})$ to $\IQ(\sqrt{3})$, since a direct calculation shows that $\IQ(\sqrt{3})$ has no element $a$ with $a^2=2$. Similarly, there is no homomorphism from $\IQ(\sqrt{3})$ to $\IQ(\sqrt{2})$. See also MSE/1069387. - - property: cogenerating set + - property: cogenerating collection proof: We can copy the proof from $\Fld$. references: - - Fld_no_cogenerating_set + - Fld_no_cogenerating_collection - property: binary powers proof: We can copy the proof from $\Fld$ that the product $\IQ(\sqrt{2}) \times \IQ(\sqrt{2})$ does not exist. diff --git a/database/data/categories/Haus.yaml b/database/data/categories/Haus.yaml index b07f581a6..267fc7dd4 100644 --- a/database/data/categories/Haus.yaml +++ b/database/data/categories/Haus.yaml @@ -95,10 +95,10 @@ unsatisfied_properties: On the other hand, we claim that $1 \dottedrightrightarrows X_\kappa$ does not have a pushout in $\Haus$; by G. M. Kelly, A survey of totality for enriched and ordinary categories, Thm. 5.6 (namely the contrapositive of the implication (i) $\Rightarrow$ (iii)), this will imply that $\Haus$ is not cototal. To see this, suppose we had a pushout $Y$, and let $\lambda \coloneqq \card(U(Y))$. Then the coprojection $X_\lambda \to Y$ is split monic, since we can construct a cocone $1 \dottedrightrightarrows X_\kappa \to X_\lambda$ where the map $X_\kappa \to X_\lambda$ is the constant map with image $x_\lambda$ when $\kappa \ne \lambda$, and the map $X_\lambda \to X_\lambda$ is the identity. But similarly to the previous paragraph, we can show any morphism $X_\lambda \to Y$ must be constant, giving a contradiction since $X_\lambda$ has at least two points. - - property: extremal generating set + - property: extremal generating collection proof: The proof is the same as the one for $\Top$; there the test spaces we use are of the form $\kappa \sqcup \{ \kappa \}$ and $\kappa + 1$, which are both Hausdorff spaces. references: - - top_no_extremal_generating_set + - top_no_extremal_generating_collection special_objects: initial object: diff --git a/database/data/categories/LRS_R.yaml b/database/data/categories/LRS_R.yaml index 03d2971fe..51c09ea0e 100644 --- a/database/data/categories/LRS_R.yaml +++ b/database/data/categories/LRS_R.yaml @@ -42,7 +42,7 @@ satisfied_properties: $$\iota_{f^*(V)} \circ f^\sharp(V) = \iota_{g^*(V)} \circ g^\sharp(V)$$ for every open subset $V \subseteq Y$. Since $\iota_{f^*(V)} = \iota_{g^*(V)}$ is a monomorphism of sets, we conclude that $f^\sharp(V) = g^\sharp(V)$. Thus, $f^\sharp = g^\sharp$. We have shown $(f,f^\sharp) = (g,g^\sharp)$, as required. - Since $\Set^{\op}$ is concretizable (say, via the contravariant power set functor), and $\Set \times \Set$ is also concretizable (because it is locally small and has a generating set), it follows that $\LRS_R$ is concretizable. + Since $\Set^{\op}$ is concretizable (say, via the contravariant power set functor), and $\Set \times \Set$ is also concretizable (because it is locally small and has a generating collection), it follows that $\LRS_R$ is concretizable. - property: infinitary extensive proof: >- diff --git a/database/data/categories/Meas.yaml b/database/data/categories/Meas.yaml index c324ddc85..fa3c0cbf3 100644 --- a/database/data/categories/Meas.yaml +++ b/database/data/categories/Meas.yaml @@ -68,7 +68,7 @@ satisfied_properties: proof: >- First, take the two-element set $2$ endowed with the trivial $\sigma$-algebra (where only $\varnothing$ and $2$ are measurable), and use that $2$ is a cogenerator for $\Set$ to show that $2$ with the trivial $\sigma$-algebra is a cogenerator for $\Meas$. - Now, we claim that adding the two-element set $2$ endowed with the discrete $\sigma$-algebra (where every subset is measurable) gives an extremal cogenerating set. To see this, suppose we have a morphism $f : (X, \M_X) \to (Y, \M_Y)$ such that $f \circ {-} : \Hom(Y, Q) \to \Hom(X, Q)$ is a bijection if $Q$ is either measurable space. Since $2$ with the trivial $\sigma$-algebra represents taking the power set of the underlying set, and the contravariant power set functor on $\Set$ is conservative, we conclude that $f$ is a bijection on the underlying sets. Also, since $2$ with the discrete $\sigma$-algebra represents the functor $(X, \M_X) \mapsto \M_X$, we see that $f^* : \M_Y \to \M_X$ is also a bijection. This shows that $f$ is an isomorphism of measurable spaces. + Now, we claim that adding the two-element set $2$ endowed with the discrete $\sigma$-algebra (where every subset is measurable) gives an extremal cogenerating collection. To see this, suppose we have a morphism $f : (X, \M_X) \to (Y, \M_Y)$ such that $f \circ {-} : \Hom(Y, Q) \to \Hom(X, Q)$ is a bijection if $Q$ is either measurable space. Since $2$ with the trivial $\sigma$-algebra represents taking the power set of the underlying set, and the contravariant power set functor on $\Set$ is conservative, we conclude that $f$ is a bijection on the underlying sets. Also, since $2$ with the discrete $\sigma$-algebra represents the functor $(X, \M_X) \mapsto \M_X$, we see that $f^* : \M_Y \to \M_X$ is also a bijection. This shows that $f$ is an isomorphism of measurable spaces. Finally, using this result, we conclude that the product of these two measurable spaces with underlying set $2$ is an extremal cogenerator of $\Meas$. references: @@ -149,7 +149,7 @@ unsatisfied_properties: Hence by Theorem 6.5.7 in Bogachev's Measure theory $\Delta_Y \notin \Sigma_Y \otimes \Sigma_Y$. We have identified a non-measurable subset of $Y \times Y$ whose preimage under $f \times f$ is measurable. Therefore, $f \times f$ is not a regular epimorphism. - - property: extremal generating set + - property: extremal generating collection proof: >- The proof is similar to the one for $\Top$. In this case, suppose $\kappa$ is an uncountable regular cardinal. We can then define $\M_\kappa$ to be the collection of subsets $E \subseteq \kappa + 1$ such that there exists an ordinal $\alpha < \kappa$ such that for each $\beta \in [\alpha, \kappa)$, $\beta \in E$ if and only if $\kappa \in E$. This is easily checked to be a $\sigma$-algebra on $\kappa + 1$. Similarly, define $\M_\kappa'$ to be the $\sigma$-algebra generated by $\M_\kappa \cup \{ \{ \kappa \} \}$; this can be described as the set of $E \subseteq \kappa + 1$ such that there exists an ordinal $\alpha < \kappa$ such that for each $\beta, \gamma \in [\alpha, \kappa)$, $\beta \in E$ if and only if $\gamma \in E$. @@ -157,9 +157,9 @@ unsatisfied_properties: $$(\kappa+1, M_\kappa') \to (\kappa+1, \M_\kappa), \, \alpha \mapsto \alpha,$$ which is not an isomorphism, induces a bijection $$\Hom(G, (\kappa + 1, \M_\kappa')) \to \Hom(G, (\kappa + 1, \M_\kappa))$$ - for each $G \in S$, implying that $S$ cannot be an extremal generating set. In fact, if $f : G \to (\kappa + 1, \M_\kappa)$ is a measurable map, since $\kappa$ is regular and $\card(G) < \kappa$, there exists an ordinal $\alpha < \kappa$ which is an upper bound for $\im(f) \cap [0, \kappa)$. Therefore, $f^*(\{\kappa\}) = f^*([\alpha + 1, \kappa])$ is measurable, implying that $f$ factors through $(\kappa + 1, \M_\kappa')$. + for each $G \in S$, implying that $S$ cannot be an extremal generating collection. In fact, if $f : G \to (\kappa + 1, \M_\kappa)$ is a measurable map, since $\kappa$ is regular and $\card(G) < \kappa$, there exists an ordinal $\alpha < \kappa$ which is an upper bound for $\im(f) \cap [0, \kappa)$. Therefore, $f^*(\{\kappa\}) = f^*([\alpha + 1, \kappa])$ is measurable, implying that $f$ factors through $(\kappa + 1, \M_\kappa')$. references: - - top_no_extremal_generating_set + - top_no_extremal_generating_collection - property: infinitary distributive proof: >- diff --git a/database/data/categories/Mono.yaml b/database/data/categories/Mono.yaml index 67f0aacdc..1e2d0b072 100644 --- a/database/data/categories/Mono.yaml +++ b/database/data/categories/Mono.yaml @@ -50,7 +50,7 @@ satisfied_properties: proof: >- Consider the forgetful functor $U : \Mono \to \Set$, $(X, X') \mapsto X$. This has right adjoint $R : \Set \to \Mono$, $X \mapsto (X, X)$. Therefore, by the dual of Lemma 9 here, $R$ preserves cogenerators; and in particular, since $\Set$ has a cogenerator, so does $\Mono$. In other words, $(\{0,1\}, \{0,1\})$ is a cogenerator of $\Mono$. - We now claim that adding $(\{0,1\}, \{1\})$ gives an extremal cogenerating set. To see this, suppose we have $f : (X, X') \to (Y, Y')$ such that ${-} \circ f$ induces bijections of morphisms both to $(\{0,1\}, \{0,1\})$ and to $(\{0,1\}, \{0\})$. Then since the first object represents the functor taking $(X, X')$ to $\Hom_{\Set}(X, \{ 0, 1 \})$, and $\{ 0, 1 \}$ is an extremal cogenerator of $\Set$, the bijection of morphisms for the first object implies that $f$ is a bijection $X \to Y$. On the other hand, the second object represents the functor taking $(X, X')$ to the collection of subsets of $X$ which contain $X'$; and under the Yoneda embedding, the monomorphism $(\{0,1\}, \{1\}) \hookrightarrow (\{0,1\}, \{0,1\})$ corresponds to the natural inclusion $\{ S\in P(X) : X' \subseteq S \} \hookrightarrow P(X)$. Therefore, if $f$ also induces a bijection of morphisms to the second object, then in particular there is a set $S$ with $Y' \subseteq S \subseteq Y$ with $f^*(S) = X'$. However, since $f$ is bijective, we also have $f^*(f_*(X')) = X'$ and $f^* : P(Y) \to P(X)$ is bijective, so $S = f_*(X')$. In other words, + We now claim that adding $(\{0,1\}, \{1\})$ gives an extremal cogenerating collection. To see this, suppose we have $f : (X, X') \to (Y, Y')$ such that ${-} \circ f$ induces bijections of morphisms both to $(\{0,1\}, \{0,1\})$ and to $(\{0,1\}, \{0\})$. Then since the first object represents the functor taking $(X, X')$ to $\Hom_{\Set}(X, \{ 0, 1 \})$, and $\{ 0, 1 \}$ is an extremal cogenerator of $\Set$, the bijection of morphisms for the first object implies that $f$ is a bijection $X \to Y$. On the other hand, the second object represents the functor taking $(X, X')$ to the collection of subsets of $X$ which contain $X'$; and under the Yoneda embedding, the monomorphism $(\{0,1\}, \{1\}) \hookrightarrow (\{0,1\}, \{0,1\})$ corresponds to the natural inclusion $\{ S\in P(X) : X' \subseteq S \} \hookrightarrow P(X)$. Therefore, if $f$ also induces a bijection of morphisms to the second object, then in particular there is a set $S$ with $Y' \subseteq S \subseteq Y$ with $f^*(S) = X'$. However, since $f$ is bijective, we also have $f^*(f_*(X')) = X'$ and $f^* : P(Y) \to P(X)$ is bijective, so $S = f_*(X')$. In other words, $$Y' \subseteq S = f_*(X') \subseteq Y',$$ so $f_*(X') = Y'$. diff --git a/database/data/categories/PreOrd.yaml b/database/data/categories/PreOrd.yaml index 360b6cc7d..6bb21863a 100644 --- a/database/data/categories/PreOrd.yaml +++ b/database/data/categories/PreOrd.yaml @@ -46,7 +46,7 @@ satisfied_properties: proof: >- Endow the set $\{ 0,1 \}$ with the preorder $0 \leq 1$, $1 \leq 0$ (which is not a partial order), and call this object $\{0,1\}_c$. Then every map $P \to \{0,1\}$ is order-preserving. Therefore, $\{0,1\}_c$ represents the functor taking $(P, \le)$ to the power set of $P$. Now since the set $\{ 0,1 \}$ is a cogenerator in $\Set$, it follows that $\{0,1\}_c$ is a cogenerator of $\PreOrd$. - We now claim that $\{0,1\}_c$ together with $\{ 0 < 1 \}$ form an extremal cogenerating set. Thus, suppose we have a morphism $f : P \to Q$ such that ${-} \circ f$ induces a bijection for morphisms both to $\{0,1\}_c$ and to $\{ 0 < 1 \}$. Then since $\{0,1\}$ is an extremal cogenerator in $\Set$, it follows that $f$ is a bijection on the underlying sets. Now, suppose we have $p_1, p_2 \in P$ such that $f(p_1) \le f(p_2)$. Then we can define an increasing function $\varphi : P \to \{0<1\}$ which sends $p \mapsto 1$ if $p_1 \le p$, and $p \mapsto 0$ otherwise. By the assumption on $f$, there is an increasing function $\psi : Q \to \{0<1\}$ such that $\psi \circ f = \varphi$. Since $1 = \psi(f(p_1)) \le \psi(f(p_2))$, it follows that $\varphi(p_2) = 1$, so $p_1 \le p_2$. We conclude that $f$ is an isomorphism. + We now claim that $\{0,1\}_c$ together with $\{ 0 < 1 \}$ form an extremal cogenerating collection. Thus, suppose we have a morphism $f : P \to Q$ such that ${-} \circ f$ induces a bijection for morphisms both to $\{0,1\}_c$ and to $\{ 0 < 1 \}$. Then since $\{0,1\}$ is an extremal cogenerator in $\Set$, it follows that $f$ is a bijection on the underlying sets. Now, suppose we have $p_1, p_2 \in P$ such that $f(p_1) \le f(p_2)$. Then we can define an increasing function $\varphi : P \to \{0<1\}$ which sends $p \mapsto 1$ if $p_1 \le p$, and $p \mapsto 0$ otherwise. By the assumption on $f$, there is an increasing function $\psi : Q \to \{0<1\}$ such that $\psi \circ f = \varphi$. Since $1 = \psi(f(p_1)) \le \psi(f(p_2))$, it follows that $\varphi(p_2) = 1$, so $p_1 \le p_2$. We conclude that $f$ is an isomorphism. Finally, by this result, we can conclude that the product of $\{0,1\}_c$ and $\{0<1\}$ is an extremal cogenerator. diff --git a/database/data/categories/Sch_R.yaml b/database/data/categories/Sch_R.yaml index 7d60a8ee9..2d219b0ea 100644 --- a/database/data/categories/Sch_R.yaml +++ b/database/data/categories/Sch_R.yaml @@ -55,8 +55,8 @@ unsatisfied_properties: - property: semi-strongly connected proof: This is because already the full subcategory of affine $R$-schemes is not semi-strongly connected, because its dual $\CAlg(R)$ is not semi-strongly connected. - - property: generating set - proof: If $S$ is a generating set of $R$-schemes, then the set of affine open subsets of the schemes in $S$ would also be a generating set. This is then also a generating set in the category of affine $R$-schemes, corresponding to a cogenerating set in $\CAlg(R)$, which we know does not exist. + - property: generating collection + proof: If $S$ is a generating collection of $R$-schemes, then the collection of affine opens of the schemes in $S$ would also be a generating collection. This is then also a generating collection of the category of affine $R$-schemes, corresponding to a cogenerating collection of $\CAlg(R)$, which we know does not exist. - property: cokernel pairs proof: Choose a residue field $K$ of $R$. Then the span $\IA^1_K \leftarrow \Spec(K(t)) \rightarrow \IA^1_K$ has no pushout; see MO/9961. diff --git a/database/data/categories/Set_ff.yaml b/database/data/categories/Set_ff.yaml index f9ffe948c..25f593732 100644 --- a/database/data/categories/Set_ff.yaml +++ b/database/data/categories/Set_ff.yaml @@ -90,8 +90,8 @@ unsatisfied_properties: - property: sequential limits proof: Consider the set $[n] \coloneqq \{0,\dotsc,n\}$ for $n \in \IN$. The forgetful functor to $\Set$ is representable (by the singleton set), hence preserves all limits. Thus, if the diagram of truncation maps $\cdots \twoheadrightarrow [2] \twoheadrightarrow [1] \twoheadrightarrow [0]$ has a limit in $\Set_\ff$, its underlying set is isomorphic to the limit taken in $\Set$, which is $\IN \cup \{\infty\}$. But there is no finite-to-one map $\IN \cup \{\infty\} \to [0]$. - - property: cogenerating set - proof: 'Suppose that $S$ is a set of objects of $\Set_\ff$, and let $\kappa$ be an uncountable cardinal greater than $\card(Q)$ for each $Q \in S$. Then for each $Q \in S$, $\Hom(\kappa, Q) = \varnothing$ (or else we would have $\kappa = \card(\kappa) \le \aleph_0 \cdot \card(Q) = \max(\aleph_0, \card(Q)) < \kappa$ giving a contradiction). This makes it impossible for any morphisms from $\kappa$ to an object of $S$ to distinguish the two morphisms $0, 1 : 1 \rightrightarrows \kappa$.' + - property: cogenerating collection + proof: 'Suppose that $S$ is an essentially small collection of objects of $\Set_\ff$, and let $\kappa$ be an uncountable cardinal greater than $\card(Q)$ for each $Q \in S$. Then for each $Q \in S$, $\Hom(\kappa, Q) = \varnothing$ (or else we would have $\kappa = \card(\kappa) \le \aleph_0 \cdot \card(Q) = \max(\aleph_0, \card(Q)) < \kappa$ giving a contradiction). This makes it impossible for any morphisms from $\kappa$ to an object of $S$ to distinguish the two morphisms $0, 1 : 1 \rightrightarrows \kappa$.' special_objects: initial object: diff --git a/database/data/categories/Top.yaml b/database/data/categories/Top.yaml index 84c7e6c5e..7e4b7519f 100644 --- a/database/data/categories/Top.yaml +++ b/database/data/categories/Top.yaml @@ -49,7 +49,7 @@ satisfied_properties: - property: extremal cogenerator proof: >- - Using the dual of Lemma 9 here with $U : \Top \to \Set$ the forgetful functor whose right adjoint is the indiscrete topology functor, and the fact that the two-element set is a cogenerator of $\Set$, we see that the indiscrete two-point space is a cogenerator of $\Top$. We claim that adding the Sierpinski space $S$ makes an extremal cogenerating set. To see this, let $f : X \to Y$ be a continuous function. First, $f$ inducing a bijection of maps to the indiscrete two-point space implies that $f$ is bijective on the underlying sets. Then, $f$ inducing a bijection of maps to the Sierpinski space implies that $f^* : \Open(Y) \to \Open(X)$ is also a bijection. We can then conclude that $f$ is open and therefore a homeomorphism: if $U \subseteq X$ is open, then there is an open subset $V \subseteq Y$ such that $f^*(V) = U$. Therefore, $f_*(U) = f_*(f^*(V)) = V$ is open, where in the last equality we use the fact that $f$ is surjective. + Using the dual of Lemma 9 here with $U : \Top \to \Set$ the forgetful functor whose right adjoint is the indiscrete topology functor, and the fact that the two-element set is a cogenerator of $\Set$, we see that the indiscrete two-point space is a cogenerator of $\Top$. We claim that adding the Sierpinski space $S$ makes an extremal cogenerating collection. To see this, let $f : X \to Y$ be a continuous function. First, $f$ inducing a bijection of maps to the indiscrete two-point space implies that $f$ is bijective on the underlying sets. Then, $f$ inducing a bijection of maps to the Sierpinski space implies that $f^* : \Open(Y) \to \Open(X)$ is also a bijection. We can then conclude that $f$ is open and therefore a homeomorphism: if $U \subseteq X$ is open, then there is an open subset $V \subseteq Y$ such that $f^*(V) = U$. Therefore, $f_*(U) = f_*(f^*(V)) = V$ is open, where in the last equality we use the fact that $f$ is surjective. Now, by this result, we conclude that the product of the indiscrete two-point space and the Sierpinski space is an extremal cogenerator of $\Top$. references: @@ -94,12 +94,12 @@ unsatisfied_properties: proof: 'Consider the indiscrete topological space $I$ on two points. This represents the functor which takes a topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $1 \rightrightarrows I$, where the maps are the two possible functions. However, this cannot be effective: if we have $h : Z\to 1$ which equalizes the two maps, then $Z$ must be empty. But that means the cokernel pair of $h$ is the discrete space on two points.' label: top_no_effective_cocongruences - - property: extremal generating set + - property: extremal generating collection proof: >- - Suppose $S$ is any set of topological spaces, and let $\kappa$ be an infinite regular cardinal greater than $\card(G)$ for every $G \in S$. Equip ordinal numbers with the order topology as usual. We then claim that the canonical continuous bijection $\kappa \sqcup \{ \kappa \} \to \kappa + 1$, which is not a homeomorphism, induces a bijection $\Hom(G, \kappa \sqcup \{ \kappa \}) \to \Hom(G, \kappa + 1)$ for every $G \in S$, showing that $S$ cannot be an extremal generating set. + Suppose $S$ is any set of topological spaces, and let $\kappa$ be an infinite regular cardinal greater than $\card(G)$ for every $G \in S$. Equip ordinal numbers with the order topology as usual. We then claim that the canonical continuous bijection $\kappa \sqcup \{ \kappa \} \to \kappa + 1$, which is not a homeomorphism, induces a bijection $\Hom(G, \kappa \sqcup \{ \kappa \}) \to \Hom(G, \kappa + 1)$ for every $G \in S$, showing that $S$ cannot be an extremal generating collection. To see this, suppose we have a continuous function $f : G \to \kappa + 1$, and consider $T \coloneqq \im(f) \cap \kappa$. Then $T \subseteq \kappa$ and $\card(T) \leq \card(G) < \kappa$. Since $\kappa$ is regular, this implies $\alpha \coloneqq \sup(T) < \kappa$. Therefore, $f^*(\{ \kappa \}) = f^*((\alpha, \kappa])$ is open, showing that $f$ is also continuous as a function $G \to \kappa \sqcup \{ \kappa \}$. - label: top_no_extremal_generating_set + label: top_no_extremal_generating_collection special_objects: initial object: diff --git a/database/data/categories/Top_pointed.yaml b/database/data/categories/Top_pointed.yaml index db00dfea3..a4992191c 100644 --- a/database/data/categories/Top_pointed.yaml +++ b/database/data/categories/Top_pointed.yaml @@ -67,7 +67,7 @@ satisfied_properties: - property: extremal cogenerator proof: >- - It is easily checked that the indiscrete two-point space $\{0,1\}$ with base point $1$ is a cogenerator, using the fact that the pointed set $\{0,1\}$ with base point $1$ is a cogenerator of $\Set_*$. If $S$ is the Sierpinski space on $\{0,1\}$, we claim that adding $(S, 0)$ and $(S, 1)$ gives an extremal cogenerating set. To see this, let $f : X \to Y$ be a continuous function. Then $f$ inducing a bijection on maps to $(\{0,1\},1)$ implies that the underlying function of $f$ is bijective. In particular, because $f$ is injective, we see that for $V$ an open subset of $Y$, $f^*(V)$ contains the base point of $X$ if and only if $V$ contains the base point of $Y$. Also, $f$ inducing a bijection on maps to $(S, 1)$ implies that $f^* : \Open(Y) \to \Open(X)$ is bijective on the open sets containing the base points, and $f$ inducing a bijection on maps to $(S, 0)$ implies that $f^* : \Open(Y) \to \Open(X)$ is bijective on the open sets not containing the base points. From these observations, we can conclude that $f$ is a homeomorphism. + It is easily checked that the indiscrete two-point space $\{0,1\}$ with base point $1$ is a cogenerator, using the fact that the pointed set $\{0,1\}$ with base point $1$ is a cogenerator of $\Set_*$. If $S$ is the Sierpinski space on $\{0,1\}$, we claim that adding $(S, 0)$ and $(S, 1)$ gives an extremal cogenerating collection. To see this, let $f : X \to Y$ be a continuous function. Then $f$ inducing a bijection on maps to $(\{0,1\},1)$ implies that the underlying function of $f$ is bijective. In particular, because $f$ is injective, we see that for $V$ an open subset of $Y$, $f^*(V)$ contains the base point of $X$ if and only if $V$ contains the base point of $Y$. Also, $f$ inducing a bijection on maps to $(S, 1)$ implies that $f^* : \Open(Y) \to \Open(X)$ is bijective on the open sets containing the base points, and $f$ inducing a bijection on maps to $(S, 0)$ implies that $f^* : \Open(Y) \to \Open(X)$ is bijective on the open sets not containing the base points. From these observations, we can conclude that $f$ is a homeomorphism. Now, by this result, we get that the product of these three pointed topological spaces is an extremal cogenerator of $\Top_*$. references: @@ -116,10 +116,10 @@ unsatisfied_properties: references: - top_no_effective_cocongruences - - property: extremal generating set + - property: extremal generating collection proof: 'The proof is similar to the one for $\Top$: if $S$ is a set of pointed topological spaces and $\kappa$ is an infinite regular cardinal greater than $\card(G)$ for every $G\in S$, we show as before that morphisms from $S$ cannot detect the failure of $(\kappa \sqcup \{ \kappa \}, 0) \to (\kappa + 1, 0)$ to be an isomorphism (where as before, we use the standard order topology on both $\kappa$ and $\kappa + 1$).' references: - - top_no_extremal_generating_set + - top_no_extremal_generating_collection special_objects: initial object: diff --git a/database/data/categories/TorsFreeAb.yaml b/database/data/categories/TorsFreeAb.yaml index 1f0b5b6c0..069067af6 100644 --- a/database/data/categories/TorsFreeAb.yaml +++ b/database/data/categories/TorsFreeAb.yaml @@ -42,11 +42,11 @@ satisfied_properties: $$P = (B \times C)/\{(i(a),-f(a)): a \in A\}.$$ It is torsion-free: If $n \in \IZ \setminus \{0\}$ and $n (b,c) = (i(a),-f(a))$, there is some $a' \in A$ with $b = i(a')$ since $B/i(A)$ is torsion-free. It follows $n a' = a$, and then $c = -f(a')$ since $C$ is torsion-free. Thus, $(b,c) = (i(a'),-f(a'))$, which proves our claim. Therefore, $P$ is also the pushout in $\TorsFreeAb$. The homomorphism $j : C \to P$, $j(c) = [0,c]$ is injective (since $\Ab$ is coregular, but a direct proof is also easy), and by the universal property of $P$ its $\Ab$-cokernel is isomorphic to the $\Ab$-cokernel of $i$, which is torsion-free. - - property: extremal cogenerating set + - property: extremal cogenerating collection proof: >- The additive group $\IQ$ is a cogenerator since every torsion-free abelian group $A$ embeds into $A \otimes \IQ$, which is a vector space over $\IQ$, and by linear algebra $K$ is a cogenerator in the category of vector spaces over $K$. - We claim that $S \coloneqq \{\IQ\} \cup \{\IZ_p : p \text{~prime}\}$ is an extremal cogenerating set, where $\IZ_p$ is the additive group of the $p$-adic integers. To establish this, we will show that for any torsion-free group $G$, the canonical morphism $\alpha : G \to \prod_{Q\in S} \prod_{f\in\Hom(G,Q)} Q$ is in fact a regular monomorphism, and therefore an extremal monomorphism. By equivalent condition (4) in the characterization below of regular monomorphisms, this is equivalent to showing $\alpha$ is injective, and whenever we have $x\in G$ and prime $p$ such that $\alpha(x)$ is $p$-divisible in the product, then $x$ is $p$-divisible in $G$. From the above, including $\IQ$ in $S$ is already sufficient to make $\alpha$ a monomorphism, i.e. an injective homomorphism. + We claim that $S \coloneqq \{\IQ\} \cup \{\IZ_p : p \text{~prime}\}$ is an extremal cogenerating collection, where $\IZ_p$ is the additive group of the $p$-adic integers. To establish this, we will show that for any torsion-free group $G$, the canonical morphism $\alpha : G \to \prod_{Q\in S} \prod_{f\in\Hom(G,Q)} Q$ is in fact a regular monomorphism, and therefore an extremal monomorphism. By equivalent condition (4) in the characterization below of regular monomorphisms, this is equivalent to showing $\alpha$ is injective, and whenever we have $x\in G$ and prime $p$ such that $\alpha(x)$ is $p$-divisible in the product, then $x$ is $p$-divisible in $G$. From the above, including $\IQ$ in $S$ is already sufficient to make $\alpha$ a monomorphism, i.e. an injective homomorphism. We will prove the second part of this condition by establishing the contrapositive for each prime $p$; thus, suppose we have $x\in G$ which is not $p$-divisible. Let $\{y_i : i \in I\}$ be a subset of $G$ including $x = y_{i_0}$ whose images in $G / pG$ form a basis for this $\IZ / p \IZ$-vector space. We will now prove by induction that for each $n$, $G / p^n G$ is a free $\IZ / p^n \IZ$-module with basis given by the images of $y_i$. The base case $n=1$ is true by assumption. Now for the inductive step from $n$ to $n+1$, for $g \in G$ we can find $a_i \in \IZ$ (all but finitely many equal to zero) such that $g \in \sum_{i\in I} a_i y_i + p^n G$. Since $G$ is torsion-free, there exists a unique $h$ such that $g = \sum_{i\in I} a_i y_i + p^n h$. Now projecting $h$ into $G / pG$, we can find $b_i \in \IZ$ such that $h \in \sum_{i\in I} b_i y_i + pG$. Hence, $g \in \sum_{i\in I} (a_i + p^n b_i) y_i + p^{n+1} G$. The uniqueness of the coefficients up to congruence modulo $p^{n+1}$ follows from the fact that there are unique choices of $a_i$ with $0 \le a_i < p^n$, and then the $b_i$ are unique up to congruence modulo $p$. diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml index afecfd969..5c32c2160 100644 --- a/database/data/categories/Unif.yaml +++ b/database/data/categories/Unif.yaml @@ -132,7 +132,7 @@ unsatisfied_properties: Choose any sequence of positive numbers $\varepsilon_n > 0$ converging to $0$. Then $\coprod_{n \in \IN} U_{\varepsilon_n}$ is an entourage of $\coprod_{n \in \IN} [0,1]$. Its image in $[0,1] \times \IN$ consists of all $((r,n),(s,m))$ such that $n=m$ and $|r-s| < \varepsilon_n$. Assume, for a contradiction, that this set is an entourage of the product. Then it contains $(p_1 \times p_1)^*(U_\delta) \cap (p_2 \times p_2)^*(\Delta_{\IN})$ for some $\delta > 0$. In other words, $|r-s| < \delta$ implies $|r-s| < \varepsilon_n$ for all $n \in \IN$ and $r,s \in [0,1]$. Taking $s=0$ and $r=\delta/2$, we see that the sequence $(\varepsilon_n)$ is bounded below by $\delta/2$, contradicting the assumption that it converges to $0$. - - property: extremal generating set + - property: extremal generating collection proof: >- The proof is very similar to $\Top$. Let $S$ be a set of uniform spaces. Let $\kappa$ be an infinite regular cardinal strictly greater than $\card(G)$ for every $G \in S$. Equip the ordinal $\kappa + 1$ with the order topology. As a compact Hausdorff space, it admits a unique compatible uniform structure (Theorem 8.3.13 in Engelking's General Topology). We equip the subset $\kappa$ with the induced uniform structure and the set $\kappa \sqcup \{\kappa\}$ with the coproduct uniform structure. Then the evident bijection $$\kappa \sqcup \{\kappa\} \to \kappa + 1$$ @@ -140,9 +140,9 @@ unsatisfied_properties: $$\Hom(G,\kappa \sqcup \{\kappa\}) \to \Hom(G,\kappa + 1),$$ which is clearly injective, is even bijective. To this end, let $f : G \to \kappa + 1$ be a uniform map. Since $\card(G) < \kappa$ and $\kappa$ is regular, $\im(f) \cap \kappa$ is bounded above by some ordinal $\alpha < \kappa$. Therefore, $f$ factors through the uniform subspace $X \coloneqq [0,\alpha] \cup \{\kappa\}$ of $\kappa + 1$. The underlying topological space of $X$ is compact Hausdorff and decomposes as a coproduct of $[0,\alpha]$ and $\{\kappa\}$. Because of the uniqueness of uniform structures, $X$ itself also decomposes as a coproduct of these spaces. In particular, $X$ is a uniform subspace of $\kappa \sqcup \{\kappa\}$. Hence, $f : G \to \kappa \sqcup \{\kappa\}$ is also a uniform map. references: - - top_no_extremal_generating_set + - top_no_extremal_generating_collection - - property: extremal cogenerating set + - property: extremal cogenerating collection proof: >- Let $S$ be a set of uniform spaces. Let $\kappa$ be an infinite regular cardinal strictly greater than $\card(G)$ for every $G \in S$. Let $X$ be a set of cardinality $\kappa$. Let $X_d$ be the discrete uniform space with underlying set $X$, and let $X_r$ be the uniform space with underlying set $X$ whose entourages are precisely those sets $U \subseteq X \times X$ that contain an equivalence relation $R$ on $X$ such that $\card(X/R) < \kappa$. The axioms of a uniform structure are easy to check. Notice that $X_r$ is not discrete, since otherwise $\Delta_X$ would be an entourage, but $\card(X/\Delta_X) = \card(X) = \kappa$. Thus, the identity map $X \to X$ lifts to a bijective uniform map diff --git a/database/data/categories/sSet.yaml b/database/data/categories/sSet.yaml index 45a04bfdc..a59445b88 100644 --- a/database/data/categories/sSet.yaml +++ b/database/data/categories/sSet.yaml @@ -26,7 +26,7 @@ satisfied_properties: proof: Let $X,Y$ be two simplicial sets. Assume that $X_0$ is empty. Then $X_n$ is empty for all $n$ since there is a morphism $[0] \to [n]$, hence a map $X_n \to X_0$. So there is a morphism $X \to Y$ for trivial reasons. If $X_0$ is non-empty, pick an element. By the Yoneda Lemma it corresponds to a morphism $\Delta^0 \to X$. Since $\Delta^0 = 1$ is terminal, there is a morphism $Y \to \Delta^0$, and these compose to a morphism $Y \to X$. - property: generator - proof: 'Let $\Delta^n \coloneqq \Hom([n],-)$ be the standard $n$-simplex for $n \geq 0$. The set $\{\Delta^n : n \geq 0\}$ is a generating set by the Yoneda Lemma. For all $n,m$ there is a morphism $[n] \to [m]$ in $\Delta$ and hence a morphism $\Delta^m \to \Delta^n$ in $\sSet$. Then by this lemma the coproduct $\coprod_{n \geq 0} \Delta^n$ is a generator in $\sSet$.' + proof: 'Let $\Delta^n \coloneqq \Hom([n],-)$ be the standard $n$-simplex for $n \geq 0$. The set $\{\Delta^n : n \geq 0\}$ is a generating collection by the Yoneda Lemma. For all $n,m$ there is a morphism $[n] \to [m]$ in $\Delta$ and hence a morphism $\Delta^m \to \Delta^n$ in $\sSet$. Then by this lemma the coproduct $\coprod_{n \geq 0} \Delta^n$ is a generator in $\sSet$.' - property: finitary algebraic proof: This follows from the fact that every category of presheaves on a small category is locally strongly finitely presentable, and hence finitary algebraic. Alternatively, we can use the simplicial identities to construct an $\IN$-sorted finitary algebraic theory (with unary operations only) whose models are precisely the simplicial sets. diff --git a/database/data/category-implications/accessible.yaml b/database/data/category-implications/accessible.yaml index 8e05ac6cb..68e726d2f 100644 --- a/database/data/category-implications/accessible.yaml +++ b/database/data/category-implications/accessible.yaml @@ -40,7 +40,7 @@ - finitely accessible conclusions: - filtered-colimit-stable monomorphisms - proof: 'Let $\C$ be a finitely accessible category and let $G$ be a set of finitely presentable objects which generates $\C$ under filtered colimits. Consider $G$ as a full subcategory and consider the restricted Yoneda embedding $\C \hookrightarrow [G^{\op},\Set]$. It preserves filtered colimits (essentially by the definition of a finitely presentable object) and all limits, in particular monomorphisms. It also reflects monomorphisms since $G$ is a generating set. Therefore, since $\Set$ and hence the functor category has filtered-colimit-stable monomorphisms, this is also true for $\C$.' + proof: 'Let $\C$ be a finitely accessible category and let $G$ be an essentially small collection of finitely presentable objects which generates $\C$ under filtered colimits. Consider $G$ as a full subcategory and consider the restricted Yoneda embedding $\C \hookrightarrow [G^{\op},\Set]$. It preserves filtered colimits (essentially by the definition of a finitely presentable object) and all limits, in particular monomorphisms. It also reflects monomorphisms since $G$ is a generating collection. Therefore, since $\Set$ and hence the functor category has filtered-colimit-stable monomorphisms, this is also true for $\C$.' - id: locally_finitely_presentable_raise assumptions: @@ -60,9 +60,9 @@ assumptions: - accessible conclusions: - - extremal generating set + - extremal generating collection # TODO: refactor this once we add the property "has (ess.) small dense subcategory" - proof: The set appearing in the definition of a $\kappa$-accessible category gives an essentially small dense full subcategory, which is in particular an extremal generating set. + proof: The collection appearing in the definition of a $\kappa$-accessible category gives an essentially small dense full subcategory, which is in particular an extremal generating collection. - id: accessible_well-powered assumptions: diff --git a/database/data/category-implications/algebraic.yaml b/database/data/category-implications/algebraic.yaml index 2d907a732..c16702f92 100644 --- a/database/data/category-implications/algebraic.yaml +++ b/database/data/category-implications/algebraic.yaml @@ -53,14 +53,14 @@ proof: >- Let $\C$ be a finitely accessible left cancellative category. The proof of this result shows that every sifted diagram $\I \to \C$ factors through the preorder reflection of $\I$, and hence reduces to a filtered diagram. Since $\C$ has filtered colimits, it therefore also has sifted colimits. It follows that every functor on $\C$ preserving filtered colimits automatically preserves sifted colimits. In particular, for representable functors this means that every finitely presentable object is automatically strongly finitely presentable. - Now let $G$ be a set of finitely presentable objects in $\C$ generating all objects via filtered colimits. The claim follows because every filtered colimit is sifted and the objects in $G$ are strongly finitely presentable. + Now let $G$ be an essentially small collection of finitely presentable objects in $\C$ generating all objects via filtered colimits. The claim follows because every filtered colimit is sifted and the objects in $G$ are strongly finitely presentable. - id: generalized_variety_stable_monos assumptions: - generalized variety conclusions: - filtered-colimit-stable monomorphisms - proof: 'Let $\C$ be a generalized variety and let $G$ be a set of strongly finitely presentable objects which generates $\C$ under sifted colimits. Consider $G$ as a full subcategory of $\C$ and consider the restricted Yoneda embedding $\C \hookrightarrow [G^{\op},\Set]$. It preserves sifted colimits (essentially by the definition of a strongly finitely presentable object) and therefore filtered colimits. It also preserves all limits, in particular monomorphisms, and it reflects monomorphisms since $G$ is a generating set. Therefore, since $\Set$ and hence the functor category has filtered-colimit-stable monomorphisms, this is also true for $\C$.' + proof: 'Let $\C$ be a generalized variety and let $G$ be an essentially small collection of strongly finitely presentable objects which generates $\C$ under sifted colimits. Consider $G$ as a full subcategory of $\C$ and consider the restricted Yoneda embedding $\C \hookrightarrow [G^{\op},\Set]$. It preserves sifted colimits (essentially by the definition of a strongly finitely presentable object) and therefore filtered colimits. It also preserves all limits, in particular monomorphisms, and it reflects monomorphisms since $G$ is a generating collection. Therefore, since $\Set$ and hence the functor category has filtered-colimit-stable monomorphisms, this is also true for $\C$.' - id: multi-algebraic_implies_locally_finitely_multi-presentable assumptions: diff --git a/database/data/category-implications/disjoint coproducts.yaml b/database/data/category-implications/disjoint coproducts.yaml index 5b011e9be..a2b36a4fd 100644 --- a/database/data/category-implications/disjoint coproducts.yaml +++ b/database/data/category-implications/disjoint coproducts.yaml @@ -43,7 +43,7 @@ - id: disjoint_coproduct_cogenerator assumptions: - disjoint coproducts - - cogenerating set + - cogenerating collection conclusions: - cogenerator - proof: 'Assume that $S$ is a cogenerating set and let $Q \coloneqq \coprod_{X \in S} X$. For $X \in S$ we have a monomorphism $i_X : X \to Q$. If $f,g : A \rightrightarrows B$ are two distinct morphisms, there is some $X \in S$ and a morphism $h : B \to X$ with $hf \neq hg$. Hence, $i_X h f \neq i_X h g$. This proves that $Q$ is a cogenerator.' + proof: 'Assume that $S$ is a cogenerating collection and let $Q \coloneqq \coprod_{X \in S} X$. For $X \in S$ we have a monomorphism $i_X : X \to Q$. If $f,g : A \rightrightarrows B$ are two distinct morphisms, there is some $X \in S$ and a morphism $h : B \to X$ with $hf \neq hg$. Hence, $i_X h f \neq i_X h g$. This proves that $Q$ is a cogenerator.' diff --git a/database/data/category-implications/generators.yaml b/database/data/category-implications/generators.yaml index 3c6d2ea1c..316398b40 100644 --- a/database/data/category-implications/generators.yaml +++ b/database/data/category-implications/generators.yaml @@ -1,10 +1,10 @@ -# results on generators and generating sets +# results on generators and generating collections - id: generator_consequence assumptions: - generator conclusions: - - generating set + - generating collection - inhabited proof: This is trivial. @@ -12,15 +12,15 @@ assumptions: - extremal generator conclusions: - - extremal generating set + - extremal generating collection - generator proof: This is trivial. -- id: extremal_generating_set_consequence +- id: extremal_generating_collection_consequence assumptions: - - extremal generating set + - extremal generating collection conclusions: - - generating set + - generating collection proof: This is trivial. - id: generator_balanced_consequence @@ -31,18 +31,18 @@ - extremal generator proof: This is immediate from the fact that any faithful functor out of a balanced category is also conservative (see here). -- id: generating_set_balanced_consequences +- id: generating_collection_balanced_consequence assumptions: - - generating set + - generating collection - balanced conclusions: - - extremal generating set + - extremal generating collection proof: This is immediate from the fact that any faithful functor out of a balanced category is also conservative (see here). - id: generator_via_coproduct assumptions: - coproducts - - generating set + - generating collection - strongly connected conclusions: - generator @@ -51,7 +51,7 @@ - id: extremal_generator_via_coproduct assumptions: - coproducts - - extremal generating set + - extremal generating collection - strongly connected conclusions: - extremal generator @@ -69,14 +69,14 @@ - locally finite - left cancellative - semi-strongly connected - - extremal generating set + - extremal generating collection conclusions: - essentially small proof: >- - Suppose a category $\C$ is locally finite, left cancellative, semi-strongly connected, and has an extremal generating set $S$. We then claim that + Suppose a category $\C$ is locally finite, left cancellative, semi-strongly connected, and has an extremal generating collection $S$. We then claim that $$\Ob(\C) \to \IN^S, \, X \mapsto \bigl(G \mapsto \card(\Hom(G, X))\bigr)$$ is injective on isomorphism classes of $\Ob(\C)$. To see this, suppose two objects $X$ and $Y$ map to the same cardinality tuple. Since $\C$ is semi-strongly connected, we may assume without loss of generality that there is a morphism $f : X \to Y$. Then since $f$ is a monomorphism, for each $G \in S$ we have $$f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$$ - is an injective function between finite sets of equal cardinality, and therefore is also a bijection. By the assumption that $S$ is an extremal generating set, we thus have $f$ is an isomorphism. + is an injective function between finite sets of equal cardinality, and therefore is also a bijection. By the assumption that $S$ is an extremal generating collection, we thus have $f$ is an isomorphism. This shows that the collection of isomorphism classes of objects of $X$ is essentially small, i.e. isomorphic to a set. Together with the assumption that the category is locally finite, this implies the category is essentially small. diff --git a/database/data/category-implications/groupoids.yaml b/database/data/category-implications/groupoids.yaml index e72ac290e..a92ffdde9 100644 --- a/database/data/category-implications/groupoids.yaml +++ b/database/data/category-implications/groupoids.yaml @@ -44,12 +44,14 @@ - extremal generator proof: This is trivial. -- id: groupoid_generating_set +- id: groupoid_generating_collection + # redundant because of "generating_collection_balanced_consequence", + # but we can keep it, because the proof is simpler. assumptions: - groupoid - - generating set + - generating collection conclusions: - - extremal generating set + - extremal generating collection proof: This is trivial. - id: groupoid_with_multi-terminal diff --git a/database/data/category-implications/size.yaml b/database/data/category-implications/size.yaml index 6148bae1c..ffc00bdf1 100644 --- a/database/data/category-implications/size.yaml +++ b/database/data/category-implications/size.yaml @@ -12,11 +12,11 @@ assumptions: - essentially small conclusions: - - extremal generating set + - extremal generating collection - locally essentially small - well-copowered - well-powered - proof: All conclusions are trivial except perhaps that the category has an extremal generating set. For that, let $S$ be a set with one representative of each isomorphism class of objects of the category. Then it is easy to show using the Yoneda Lemma that $S$ is an extremal generating set. + proof: This is trivial. - id: finite_consequence assumptions: @@ -69,10 +69,10 @@ - locally essentially small proof: 'If $U : \C \to \Set$ is a faithful functor, for every pair of objects $A,B$, the collection $\Hom(A,B)$ embeds into the set $\Hom(U(A),U(B))$, so that it is essentially small.' -- id: generating_set_concrete +- id: generating_collection_concrete assumptions: - - generating set + - generating collection - locally essentially small conclusions: - concretizable - proof: 'If $S$ is a generating set of a locally small category $\C$, then by definition the functor $(\Hom(G,-))_{G \in S} : \C \to \Set^S$ is faithful. Furthermore, the functor $\Set^S \to \Set$ mapping $X \mapsto \coprod_{G \in S} X_G$ is faithful. Their composition provides a faithful functor $\C \to \Set$.' + proof: 'If $S$ is a generating collection of a locally small category $\C$, then by definition the functor $(\Hom(G,-))_{G \in S} : \C \to \Set^S$ is faithful. Furthermore, the functor $\Set^S \to \Set$ mapping $X \mapsto \coprod_{G \in S} X_G$ is faithful. Their composition provides a faithful functor $\C \to \Set$.' diff --git a/database/data/category-implications/thin.yaml b/database/data/category-implications/thin.yaml index d1e320797..da5acd9b9 100644 --- a/database/data/category-implications/thin.yaml +++ b/database/data/category-implications/thin.yaml @@ -4,7 +4,7 @@ assumptions: - thin conclusions: - - generating set + - generating collection - locally finite - one-way - equalizers diff --git a/database/data/category-implications/topos.yaml b/database/data/category-implications/topos.yaml index 05a89d3eb..dcffb0a7b 100644 --- a/database/data/category-implications/topos.yaml +++ b/database/data/category-implications/topos.yaml @@ -41,7 +41,7 @@ conclusions: - coproducts - elementary topos - - generating set + - generating collection - locally essentially small proof: See Mac Lane & Moerdijk, Appendix, Prop. 4.4. is_equivalence: true diff --git a/database/data/category-implications/total.yaml b/database/data/category-implications/total.yaml index a65030f82..74cceba46 100644 --- a/database/data/category-implications/total.yaml +++ b/database/data/category-implications/total.yaml @@ -27,7 +27,7 @@ - cocomplete - locally essentially small - well-copowered - - generating set + - generating collection conclusions: - total proof: Since the category is cocomplete and well-copowered, it is epi-cocomplete (meaning that it has wide pushouts of epimorphisms, even of non-small families of epimorphisms). The result then follows from B. J. Day, Further criteria for totality, Thm. 1. diff --git a/database/data/category-properties/cogenerating collection.yaml b/database/data/category-properties/cogenerating collection.yaml new file mode 100644 index 000000000..4900c60e0 --- /dev/null +++ b/database/data/category-properties/cogenerating collection.yaml @@ -0,0 +1,22 @@ +id: cogenerating collection +relation: has a +description: >- + This property refers to the existence of a cogenerating collection. A cogenerating collection of a category $\C$ is a collection of objects $S \subseteq \Ob(\C)$ that is essentially small (i.e., isomorphic to a set) and has the following property: if parallel morphisms $f,g : A \rightrightarrows B$ satisfy $h \circ f = h \circ g$ for every morphism $h : B \to Q$ with $Q \in S$, then $f = g$. Equivalently, the functor + $$(\Hom(-,Q))_{Q \in S} : \C^{\op} \to (\Set^+)^S$$ + is faithful. If $\C$ is locally essentially small and has products, this is also equivalent to the condition that the canonical morphism + $$A \to \textstyle\prod_{Q\in S} \prod_{f\in\Hom(A,Q)} Q$$ + is a monomorphism for every object $A$. + + + The condition that $S$ is essentially small is important since, without it, every category would have a cogenerating collection, namely its collection of all objects. Notice that $S$ is not assumed to be a set "on the nose", since its objects do not need to be sets; see our foundations for more background. This is why we have not adopted the more common terminology of a "cogenerating set". We did not choose "essentially small cogenerating collection" either since it is too cumbersome and diverges too much from the literature. + +nlab_link: https://ncatlab.org/nlab/show/cogenerator +dual: generating collection +invariant_under_equivalences: true + +related: + - cogenerator + - extremal cogenerating collection + +tags: + - size diff --git a/database/data/category-properties/cogenerating set.yaml b/database/data/category-properties/cogenerating set.yaml deleted file mode 100644 index 031d1b6ab..000000000 --- a/database/data/category-properties/cogenerating set.yaml +++ /dev/null @@ -1,18 +0,0 @@ -id: cogenerating set -relation: has a -description: >- - A set of objects $S$ is called a cogenerating set if for every pair of parallel morphisms $f,g : A \rightrightarrows B$, $f = g$ holds if and only if for every morphism $h : B \to Q$ with $Q \in S$ we have $h \circ f = h \circ g$. Equivalently, the functor $(\Hom(-,Q))_{Q \in S} : \C^{\op} \to (\Set^+)^S$ is faithful. This property refers to the existence of a cogenerating set. - - In a locally essentially small category with products, it is also equivalent to the condition that the canonical morphism - $$A \to \textstyle\prod_{Q\in S} \prod_{f\in\Hom(A,Q)} Q$$ - is a monomorphism for every object $A$. -nlab_link: https://ncatlab.org/nlab/show/cogenerator -dual: generating set -invariant_under_equivalences: true - -related: - - cogenerator - - extremal cogenerating set - -tags: - - size diff --git a/database/data/category-properties/cogenerator.yaml b/database/data/category-properties/cogenerator.yaml index 02645b872..d5f5d1db4 100644 --- a/database/data/category-properties/cogenerator.yaml +++ b/database/data/category-properties/cogenerator.yaml @@ -1,12 +1,15 @@ id: cogenerator relation: has a -description: 'An object $Q$ of a category is called a cogenerator if for every pair of parallel morphisms $f,g : A \rightrightarrows B$ the equation $f = g$ holds if for every morphism $h : B \to Q$ we have $h \circ f = h \circ g$. Equivalently, the functor $\Hom(-,Q) : \C^{\op} \to \Set^+$ is faithful. This property refers to the existence of a cogenerator. By definition, $Q$ is a cogenerator if and only if $\{Q\}$ is a cogenerating set.' +description: >- + This property refers to the existence of a cogenerator. An object $Q$ of a category $\C$ is called a cogenerator if for all parallel morphisms $f,g : A \rightrightarrows B$ such that $h \circ f = h \circ g$ for every morphism $h : B \to Q$, we have $f = g$. Equivalently, the functor + $$\Hom(-,Q) : \C^{\op} \to \Set^+$$ + is faithful. By definition, $Q$ is a cogenerator if and only if $\{Q\}$ is a cogenerating collection. nlab_link: https://ncatlab.org/nlab/show/cogenerator dual: generator invariant_under_equivalences: true related: - - cogenerating set + - cogenerating collection - extremal cogenerator tags: diff --git a/database/data/category-properties/concretizable.yaml b/database/data/category-properties/concretizable.yaml index 251f621ee..33f4f92de 100644 --- a/database/data/category-properties/concretizable.yaml +++ b/database/data/category-properties/concretizable.yaml @@ -9,7 +9,7 @@ dual: concretizable invariant_under_equivalences: true related: - - generating set + - generating collection - locally essentially small tags: diff --git a/database/data/category-properties/extremal cogenerating collection.yaml b/database/data/category-properties/extremal cogenerating collection.yaml new file mode 100644 index 000000000..bca930a2e --- /dev/null +++ b/database/data/category-properties/extremal cogenerating collection.yaml @@ -0,0 +1,19 @@ +id: extremal cogenerating collection +relation: has an +description: >- + This property refers to the existence of an extremal cogenerating collection. A collection of objects $S \subseteq \Ob(\C)$ in a category $\C$ is called an extremal cogenerating collection if it is a cogenerating collection and for every morphism $f : A \to B$, $f$ is an isomorphism if and only if for every object $Q \in S$ we have ${-} \circ f : \Hom(B, Q) \to \Hom(A, Q)$ is a bijection. Equivalently, the functor + $(\Hom(-,Q))_{Q \in S} : \C^{\op} \to (\Set^+)^S$ + is faithful and conservative. If $\C$ is locally essentially small and has products, it is also equivalent to the condition that the canonical morphism + $$\textstyle A \to \prod_{Q\in S} \prod_{f\in\Hom(A,Q)} Q$$ + is an extremal monomorphism for every object $A$, explaining the terminology (see Prop. 5.3 at the nLab). The term "extremal cogenerating set" is more common, but within our foundations, the collection $S$ is not necessarily a set; it is just isomorphic to a set. + +nlab_link: https://ncatlab.org/nlab/show/separator +dual: extremal generating collection +invariant_under_equivalences: true + +related: + - extremal cogenerator + - cogenerating collection + +tags: + - size diff --git a/database/data/category-properties/extremal cogenerating set.yaml b/database/data/category-properties/extremal cogenerating set.yaml deleted file mode 100644 index 36acf17cf..000000000 --- a/database/data/category-properties/extremal cogenerating set.yaml +++ /dev/null @@ -1,18 +0,0 @@ -id: extremal cogenerating set -relation: has an -description: >- - A set of objects $S$ is called an extremal cogenerating set if it is a cogenerating set and for every morphism $f : A \to B$, $f$ is an isomorphism if and only if for every object $Q \in S$ we have ${-}\circ f : \Hom(B, Q) \to \Hom(A, Q)$ is a bijection. Equivalently, the functor $(\Hom(-,Q))_{Q \in S} : \C^{\op} \to (\Set^+)^S$ is faithful and conservative. This property refers to the existence of an extremal cogenerating set. - - In a locally essentially small category with products, it is also equivalent to the condition that the canonical morphism - $$\textstyle A \to \prod_{Q\in S} \prod_{f\in\Hom(A,Q)} Q$$ - is an extremal monomorphism for every object $A$, explaining the terminology (see Prop. 5.3 at the nLab). -nlab_link: https://ncatlab.org/nlab/show/separator -dual: extremal generating set -invariant_under_equivalences: true - -related: - - extremal cogenerator - - cogenerating set - -tags: - - size diff --git a/database/data/category-properties/extremal cogenerator.yaml b/database/data/category-properties/extremal cogenerator.yaml index 9b512e98e..412780e95 100644 --- a/database/data/category-properties/extremal cogenerator.yaml +++ b/database/data/category-properties/extremal cogenerator.yaml @@ -7,13 +7,13 @@ description: >- $$\textstyle A \to \prod_{f\in\Hom(A,Q)} Q$$ is an extremal monomorphism for every object $A$, explaining the terminology (see Prop. 5.3 at the nLab). - By definition, $Q$ is an extremal cogenerator if and only if $\{Q\}$ is an extremal cogenerating set. + By definition, $Q$ is an extremal cogenerator if and only if $\{Q\}$ is an extremal cogenerating collection. nlab_link: https://ncatlab.org/nlab/show/separator dual: extremal generator invariant_under_equivalences: true related: - - extremal cogenerating set + - extremal cogenerating collection - cogenerator tags: diff --git a/database/data/category-properties/extremal generating collection.yaml b/database/data/category-properties/extremal generating collection.yaml new file mode 100644 index 000000000..7d2780be1 --- /dev/null +++ b/database/data/category-properties/extremal generating collection.yaml @@ -0,0 +1,19 @@ +id: extremal generating collection +relation: has an +description: >- + This property refers to the existence of an extremal generating collection. A collection of objects $S \subseteq \Ob(\C)$ in a category $\C$ is called an extremal generating collection if it is a generating collection and for every morphism $f : A \to B$, $f$ is an isomorphism if and only if for every object $G \in S$ we have $f \circ {-} : \Hom(G, A) \to \Hom(G, B)$ is a bijection. Equivalently, the functor + $$(\Hom(G,-))_{G \in S} : \C \to (\Set^+)^S$$ + is faithful and conservative. If $\C$ is locally essentially small and has coproducts, it is also equivalent to the condition that the canonical morphism + $$\textstyle\bigsqcup_{G\in S} \bigsqcup_{f\in\Hom(G,A)} G \to A$$ + is an extremal epimorphism for every object $A$, explaining the terminology (see Prop. 5.3 at the nLab). The term "extremal generating set" is more common, but within our foundations, the collection $S$ is not necessarily a set; it is just isomorphic to a set. + +nlab_link: https://ncatlab.org/nlab/show/separator +dual: extremal cogenerating collection +invariant_under_equivalences: true + +related: + - extremal generator + - generating collection + +tags: + - size diff --git a/database/data/category-properties/extremal generating set.yaml b/database/data/category-properties/extremal generating set.yaml deleted file mode 100644 index 253508f5f..000000000 --- a/database/data/category-properties/extremal generating set.yaml +++ /dev/null @@ -1,18 +0,0 @@ -id: extremal generating set -relation: has an -description: >- - A set of objects $S$ is called an extremal generating set if it is a generating set and for every morphism $f : A \to B$, $f$ is an isomorphism if and only if for every object $G \in S$ we have $f \circ {-} : \Hom(G, A) \to \Hom(G, B)$ is a bijection. Equivalently, the functor $(\Hom(G,-))_{G \in S} : \C \to (\Set^+)^S$ is faithful and conservative. This property refers to the existence of an extremal generating set. - - In a locally essentially small category with coproducts, it is also equivalent to the condition that the canonical morphism - $$\textstyle\bigsqcup_{G\in S} \bigsqcup_{f\in\Hom(G,A)} G \to A$$ - is an extremal epimorphism for every object $A$, explaining the terminology (see Prop. 5.3 at the nLab). -nlab_link: https://ncatlab.org/nlab/show/separator -dual: extremal cogenerating set -invariant_under_equivalences: true - -related: - - extremal generator - - generating set - -tags: - - size diff --git a/database/data/category-properties/extremal generator.yaml b/database/data/category-properties/extremal generator.yaml index 7a0d2a87c..1c5f57912 100644 --- a/database/data/category-properties/extremal generator.yaml +++ b/database/data/category-properties/extremal generator.yaml @@ -7,13 +7,13 @@ description: >- $$\textstyle\bigsqcup_{f\in\Hom(G,A)} G \to A$$ is an extremal epimorphism for every object $A$, explaining the terminology (see Prop. 5.3 at the nLab). - By definition, $G$ is an extremal generator if and only if $\{G\}$ is an extremal generating set. + By definition, $G$ is an extremal generator if and only if $\{G\}$ is an extremal generating collection. nlab_link: https://ncatlab.org/nlab/show/separator dual: extremal cogenerator invariant_under_equivalences: true related: - - extremal generating set + - extremal generating collection - generator tags: diff --git a/database/data/category-properties/generating collection.yaml b/database/data/category-properties/generating collection.yaml new file mode 100644 index 000000000..32b55885e --- /dev/null +++ b/database/data/category-properties/generating collection.yaml @@ -0,0 +1,23 @@ +id: generating collection +relation: has a +description: >- + This property refers to the existence of a generating collection. A generating collection of a category $\C$ is a collection of objects $S \subseteq \Ob(\C)$ that is essentially small (i.e., isomorphic to a set) and has the following property: if parallel morphisms $f,g : A \rightrightarrows B$ satisfy $f \circ h = g \circ h$ for every morphism $h : G \to A$ with $G \in S$, then $f = g$. Equivalently, the functor + $$(\Hom(G,-))_{G \in S} : \C \to (\Set^+)^S$$ + is faithful. If $\C$ is locally essentially small and has coproducts, this is also equivalent to the condition that the canonical morphism + $$\textstyle\bigsqcup_{G\in S} \bigsqcup_{f\in\Hom(G,A)} G \to A$$ + is an epimorphism for every object $A$. + + + The condition that $S$ is essentially small is important since, without it, every category would have a generating collection, namely its collection of all objects. Notice that $S$ is not assumed to be a set "on the nose", since its objects do not need to be sets; see our foundations for more background. This is why we have not adopted the more common terminology of a "generating set". We did not choose "essentially small generating collection" either since it is too cumbersome and diverges too much from the literature. + +nlab_link: https://ncatlab.org/nlab/show/separator +dual: cogenerating collection +invariant_under_equivalences: true + +related: + - generator + - extremal generating collection + - concretizable + +tags: + - size diff --git a/database/data/category-properties/generating set.yaml b/database/data/category-properties/generating set.yaml deleted file mode 100644 index 96baa6a30..000000000 --- a/database/data/category-properties/generating set.yaml +++ /dev/null @@ -1,19 +0,0 @@ -id: generating set -relation: has a -description: >- - A set of objects $S$ is called a generating set if for every pair of parallel morphisms $f,g : A \rightrightarrows B$, $f = g$ holds if and only if for every morphism $h : G \to A$ with $G \in S$ we have $f \circ h = g \circ h$. Equivalently, the functor $(\Hom(G,-))_{G \in S} : \C \to (\Set^+)^S$ is faithful. This property refers to the existence of a generating set. - - In a locally essentially small category with coproducts, it is also equivalent to the condition that the canonical morphism - $$\textstyle\bigsqcup_{G\in S} \bigsqcup_{f\in\Hom(G,A)} G \to A$$ - is an epimorphism for every object $A$. -nlab_link: https://ncatlab.org/nlab/show/separator -dual: cogenerating set -invariant_under_equivalences: true - -related: - - generator - - extremal generating set - - concretizable - -tags: - - size diff --git a/database/data/category-properties/generator.yaml b/database/data/category-properties/generator.yaml index 71196236d..940235bfd 100644 --- a/database/data/category-properties/generator.yaml +++ b/database/data/category-properties/generator.yaml @@ -1,12 +1,15 @@ id: generator relation: has a -description: 'An object $G$ of a category is called a generator if for every pair of parallel morphisms $f,g : A \rightrightarrows B$ the equation $f = g$ holds if for every morphism $h : G \to A$ we have $f \circ h = g \circ h$. Equivalently, the functor $\Hom(G,-) : \C \to \Set^+$ is faithful. This property refers to the existence of a generator. By definition, $G$ is a generator if and only if $\{G\}$ is a generating set.' +description: >- + This property refers to the existence of a generator. An object $G$ of a category $\C$ is called a generator if for all parallel morphisms $f,g : A \rightrightarrows B$ such that $f \circ h = g \circ h$ for every morphism $h : G \to A$, we have $f = g$. Equivalently, the functor + $$\Hom(G,-) : \C \to \Set^+$$ + is faithful. By definition, $G$ is a generator if and only if $\{G\}$ is a generating collection. nlab_link: https://ncatlab.org/nlab/show/separator dual: cogenerator invariant_under_equivalences: true related: - - generating set + - generating collection - extremal generator tags: diff --git a/database/data/functor-implications/adjoints.yaml b/database/data/functor-implications/adjoints.yaml index f4957adf1..526e53ed5 100644 --- a/database/data/functor-implications/adjoints.yaml +++ b/database/data/functor-implications/adjoints.yaml @@ -10,7 +10,7 @@ - continuous associated_assumptions: domain: - - cogenerating set + - cogenerating collection - complete - locally essentially small - well-powered diff --git a/database/data/symmetric_monoidal_category_implications/closed.yaml b/database/data/symmetric_monoidal_category_implications/closed.yaml index 6e941a1dc..07552611b 100644 --- a/database/data/symmetric_monoidal_category_implications/closed.yaml +++ b/database/data/symmetric_monoidal_category_implications/closed.yaml @@ -56,7 +56,7 @@ associated_assumptions: underlying_category: - well-copowered - - generating set + - generating collection - locally essentially small conclusions: - closed diff --git a/database/scripts/expected-data/Ab.json b/database/scripts/expected-data/Ab.json index 0f86509e8..6cb04cfe1 100644 --- a/database/scripts/expected-data/Ab.json +++ b/database/scripts/expected-data/Ab.json @@ -8,7 +8,7 @@ "cocomplete": true, "coequalizers": true, "cogenerator": true, - "cogenerating set": true, + "cogenerating collection": true, "complete": true, "connected": true, "semi-strongly connected": true, @@ -33,7 +33,7 @@ "finitely cocomplete": true, "finitely complete": true, "generator": true, - "generating set": true, + "generating collection": true, "Grothendieck abelian": true, "inhabited": true, "initial object": true, @@ -117,9 +117,9 @@ "ℵ₂-small powers": true, "ℵ₂-small copowers": true, "extremal generator": true, - "extremal generating set": true, + "extremal generating collection": true, "extremal cogenerator": true, - "extremal cogenerating set": true, + "extremal cogenerating collection": true, "natural numbers object": true, "kernel pairs": true, "cokernel pairs": true, diff --git a/database/scripts/expected-data/Set.json b/database/scripts/expected-data/Set.json index fd4593e11..34fdebfb0 100644 --- a/database/scripts/expected-data/Set.json +++ b/database/scripts/expected-data/Set.json @@ -9,7 +9,7 @@ "cocomplete": true, "coequalizers": true, "cogenerator": true, - "cogenerating set": true, + "cogenerating collection": true, "complete": true, "connected": true, "semi-strongly connected": true, @@ -35,7 +35,7 @@ "finitely cocomplete": true, "finitely complete": true, "generator": true, - "generating set": true, + "generating collection": true, "infinitary distributive": true, "inhabited": true, "initial object": true, @@ -116,9 +116,9 @@ "pretopos": true, "quasitopos": true, "extremal generator": true, - "extremal generating set": true, + "extremal generating collection": true, "extremal cogenerator": true, - "extremal cogenerating set": true, + "extremal cogenerating collection": true, "kernel pairs": true, "cokernel pairs": true, "equalizers of cokernel pairs": true, diff --git a/database/scripts/expected-data/Top.json b/database/scripts/expected-data/Top.json index 6a8437fc1..36e9a0b10 100644 --- a/database/scripts/expected-data/Top.json +++ b/database/scripts/expected-data/Top.json @@ -5,7 +5,7 @@ "cocomplete": true, "coequalizers": true, "cogenerator": true, - "cogenerating set": true, + "cogenerating collection": true, "complete": true, "connected": true, "semi-strongly connected": true, @@ -27,7 +27,7 @@ "finitely cocomplete": true, "finitely complete": true, "generator": true, - "generating set": true, + "generating collection": true, "infinitary distributive": true, "inhabited": true, "initial object": true, @@ -83,7 +83,7 @@ "ℵ₂-small powers": true, "ℵ₂-small copowers": true, "extremal cogenerator": true, - "extremal cogenerating set": true, + "extremal cogenerating collection": true, "kernel pairs": true, "cokernel pairs": true, "equalizers of cokernel pairs": true, @@ -187,5 +187,5 @@ "regular-quotient-trivial": false, "core-connected": false, "extremal generator": false, - "extremal generating set": false + "extremal generating collection": false } diff --git a/src/routes/download/+page.svelte b/src/routes/download/+page.svelte index 85ccde25b..5b09bd0d6 100644 --- a/src/routes/download/+page.svelte +++ b/src/routes/download/+page.svelte @@ -82,11 +82,11 @@ AND is_satisfied = TRUE;`} From 73027c9f305c4cd9c5c53225c09fb9cfc49d1447 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 10 Sep 2026 19:57:51 +0200 Subject: [PATCH 3/3] parse structure descriptions as content page references --- src/lib/server/fetchers/content.ts | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/src/lib/server/fetchers/content.ts b/src/lib/server/fetchers/content.ts index 6b665f037..7a498eb39 100644 --- a/src/lib/server/fetchers/content.ts +++ b/src/lib/server/fetchers/content.ts @@ -10,7 +10,7 @@ import { db } from '$lib/server/db' import { display_implication } from '../transforms' export function fetch_content_references(content_id: string) { - const structures = db + const structures_via_proofs = db .prepare<[string], StructureShort & { type: StructureType }>( `SELECT DISTINCT s.id, s.name, s.type FROM property_assignments pa @@ -20,11 +20,23 @@ export function fetch_content_references(content_id: string) { ) .all(content_id) + const structures_via_description = db + .prepare<[string], StructureShort & { type: StructureType }>( + `SELECT id, name, type FROM structures + WHERE description LIKE '%/content/' || ? || '%' + ORDER BY lower(id)` + ) + .all(content_id) + + const structures = [...structures_via_proofs, ...structures_via_description] + const structures_by_type: StructureShortDictionary = {} for (const { type, ...structure } of structures) { structures_by_type[type] ??= [] - structures_by_type[type].push(structure) + if (structures_by_type[type].every((s) => s.id != structure.id)) { + structures_by_type[type].push(structure) + } } const properties = db