From f18a5b78cc0d84c2263ae5eb53f7cf3a3b1160ad Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 12 Sep 2026 11:06:02 +0200 Subject: [PATCH 1/8] strengthen result about cartesian closed categories --- database/data/category-implications/cartesian closed.yaml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/database/data/category-implications/cartesian closed.yaml b/database/data/category-implications/cartesian closed.yaml index 7566380ce..7d143bc56 100644 --- a/database/data/category-implications/cartesian closed.yaml +++ b/database/data/category-implications/cartesian closed.yaml @@ -7,13 +7,13 @@ - finite products proof: This holds by definition. -- id: ccc_consequence +- id: lcc_consequence assumptions: - - cartesian closed + - locally cartesian closed - initial object conclusions: - strict initial object - proof: See the nLab. + proof: Assume that $\C$ is locally cartesian closed and $0 \in \C$ is an initial object. The slice category $\C / 0$ has a zero object, the identity of $0$. By assumption, it is also cartesian closed. But a cartesian closed category with a zero object is trivial, since for every object $A$ we have $A \cong A \times 1 \cong A \times 0 \cong 0$, where the last step uses that $A \times -$ is a left adjoint and hence preserves the initial object. Since $\C / 0$ is trivial, every morphism $X \to 0$ is an isomorphism. - id: ccc_cartesian_filtered_colimits assumptions: From e647b05f286b5e23eaa0c91d91e8bc740e3c7512 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 12 Sep 2026 11:42:37 +0200 Subject: [PATCH 2/8] add the category of large families of sets which are mostly singletons --- .cspell.json | 4 +- database/data/categories/Set.yaml | 1 + .../data/categories/Set_family_mostly_1.yaml | 119 ++++++++++++++++++ database/data/categories/SetxSet.yaml | 1 + database/data/categories/Vect_family.yaml | 2 + shared/structure.history.json | 3 +- 6 files changed, 128 insertions(+), 2 deletions(-) create mode 100644 database/data/categories/Set_family_mostly_1.yaml diff --git a/.cspell.json b/.cspell.json index 86828c3d0..fad69e540 100644 --- a/.cspell.json +++ b/.cspell.json @@ -22,7 +22,8 @@ "cech", "Unif", "noiso", - "coprod" + "coprod", + "isbell" ], "words": [ "abelian", @@ -321,6 +322,7 @@ "subbasic", "subbasis", "subcollection", + "subcollections", "subconjugated", "subcover", "subfunctor", diff --git a/database/data/categories/Set.yaml b/database/data/categories/Set.yaml index 7c11f77f7..0876748c7 100644 --- a/database/data/categories/Set.yaml +++ b/database/data/categories/Set.yaml @@ -19,6 +19,7 @@ related: - Setne - Set_arrow - Set_disc + - Set_family_mostly_1 satisfied_properties: - property: locally small diff --git a/database/data/categories/Set_family_mostly_1.yaml b/database/data/categories/Set_family_mostly_1.yaml new file mode 100644 index 000000000..2595f4c44 --- /dev/null +++ b/database/data/categories/Set_family_mostly_1.yaml @@ -0,0 +1,119 @@ +id: Set_family_mostly_1 +name: category of large families of sets which are mostly singletons +notation: $\Set^{(I)}_1$ +objects: 'families of sets $X = (X_i)_{i \in I}$ such that $S(X) \coloneqq \{i \in I : X_i \not\cong 1\}$ is essentially small (i.e., isomorphic to a set), where $I$ is a fixed collection that is not essentially small' +morphisms: families of maps +description: We have added this category solely as an example of a cartesian closed category without a generating collection, but it also satisfies some other interesting combinations of properties. It is a full subcategory of the product category $\Set^I$, which exists even when $I$ is merely a collection; see Foundations. +nlab_link: null + +tags: + - set theory + +related: + - Set + - SetxSet + - Set_disc_Ab + - Vect_family + +satisfied_properties: + - property: locally essentially small + proof: For two families $X$ and $Y$, the collection $\Hom(X,Y) = \prod_{i \in I} \Hom(X_i,Y_i)$ is isomorphic to $\prod_{i \in S(Y)} \Hom(X_i,Y_i)$, which is essentially small since $S(Y)$ and each $\Hom(X_i,Y_i)$ are essentially small. + + - property: complete + proof: 'Since $\Set$ is complete, the product category $\Set^I$ is complete with pointwise limits. (The size of the index collection does not matter.) Thus, it only remains to check that $\Set^{(I)}_1$ is closed under limits, which are small by convention. Let $D : \J \to \Set^{(I)}_1$ be a small diagram and let $L$ be its limit in $\Set^I$. Thus, $L_i = \lim_{j \in \J} D(j)_i$. Consider the collection $\bigcup_{j \in \J} S(D(j))$, which is essentially small. For any index $i$ outside this collection, we have $L_i \cong \lim_{j \in \J} 1 \cong 1$. Thus, $S(L) \subseteq \bigcup_{j \in \J} S(D(j))$, and hence $S(L)$ is essentially small.' + + - property: locally cartesian closed + proof: >- + First of all, $\Set$ is locally cartesian closed, i.e. each slice $\Set / X$ is cartesian closed, with exponentials + $$\textstyle [Y \to X, Z \to X] = \coprod_{x \in X} \Hom(Y_x,Z_x),$$ + where $Y_x$ denotes the fiber of $Y \to X$ over $x \in X$. It follows formally that, for every collection $I$, also $\Set^I$ is locally cartesian closed, with exponentials + $$\textstyle [Y \to X, Z \to X]_i = \coprod_{x \in X_i} \Hom((Y_i)_x,(Z_i)_x).$$ + Thus, if $X_i \cong 1$ and $Z_i \cong 1$, then $[Y \to X, Z \to X]_i \cong 1$. In other words, + $$S([Y \to X, Z \to X]) \subseteq S(X) \cup S(Z).$$ + In particular, if $S(X)$ and $S(Z)$ are essentially small, then $S([Y \to X, Z \to X])$ is also essentially small. Thus, if $X \in \Set^{(I)}_1$, then the full subcategory $\Set^{(I)}_1 / X$ of $\Set^I / X$ is closed under exponentials and is therefore also cartesian closed. + + - property: connected colimits + proof: 'Since $\Set$ is cocomplete, the product category $\Set^I$ is also cocomplete with pointwise colimits. It suffices to prove that $\Set^{(I)}_1$ is closed under connected colimits, which are small by convention. Let $D : \J \to \Set^{(I)}_1$ be a small connected diagram and let $C$ be its colimit in $\Set^I$. Thus, $C_i = \colim_{j \in \J} D(j)_i$. Consider the collection $\bigcup_{j \in \J} S(D(j))$, which is essentially small. For any index $i$ outside this collection, we have $C_i \cong \colim_{j \in \J} 1 \cong 1$, where the last step uses the fact that $\J$ is connected. Thus, $S(C) \subseteq \bigcup_{j \in \J} S(D(j))$, and hence $S(C)$ is essentially small.' + + - property: exact filtered colimits + proof: We already know that the category has connected, hence filtered, colimits, and that it has finite limits. These (co)limits are defined pointwise. Hence, the claim follows from the corresponding property of $\Set$. + + - property: mono-regular + proof: We claim that every monomorphism $X \to Y$ is the equalizer of its cokernel pair $Y \rightrightarrows Y \sqcup_X Y$. This is because every component $X_i \to Y_i$ is injective (see the classification of monomorphisms below), the statement holds in $\Set$, and equalizers and pushouts are constructed pointwise. + + - property: well-copowered + proof: The epimorphisms $X \to Y$ are precisely the morphisms that are pointwise surjective (see below). If $X_i \to Y_i$ is surjective and $X_i \cong 1$, then also $Y_i \cong 1$. It follows that the collection $\Quot(X) \cong \prod_{i \in S(X)} \Quot(X_i)$ is essentially small. + + - property: effective congruences + proof: Let $R \rightrightarrows X$ be a congruence in $\Set^{(I)}_1$. We claim that it is the kernel pair of its coequalizer $X \twoheadrightarrow X/R$. This certainly holds in $\Set$, and for every $i \in I$, the pair $R_i \rightrightarrows X_i$ is a congruence in $\Set$. Therefore, the claim follows since kernel pairs (in fact, all limits) and coequalizers (in fact, all connected colimits) are constructed pointwise. + + - property: effective cocongruences + proof: Let $X \rightrightarrows R$ be a cocongruence in $\Set^{(I)}_1$. We claim that it is the cokernel pair of its equalizer $E \hookrightarrow X$. This certainly holds in $\Set$, and for every $i \in I$, the pair $X_i \rightrightarrows R_i$ is a cocongruence in $\Set$. Therefore, the claim follows since cokernel pairs (in fact, all connected colimits) and equalizers (in fact, all limits) are constructed pointwise. + +unsatisfied_properties: + - property: skeletal + proof: This is trivial. + + - property: semi-strongly connected + proof: This is because $\Set \times \Set$ can be embedded into $\Set^{(I)}_1$ by extending each pair of sets with singletons, and we know that $\Set \times \Set$ is not semi-strongly connected. + + - property: locally small + proof: The proof is identical to the proof for $\Vect^{(I)}$. However, this result is not relevant for category theory; only the fact that the category is locally essentially small matters. + references: + - Vect_family_not_locally_small + + - property: binary copowers + proof: >- + We first observe that each evaluation functor $\ev_i : \Set^{(I)}_1 \to \Set$ is cocontinuous. This is because it has a right adjoint, which maps a set $T$ to the family $\widetilde{T}$ defined by $\widetilde{T}_i = T$ and $\widetilde{T}_j = 1$ for indices $j \neq i$. + It follows that the inclusion functor $\Set^{(I)}_1 \hookrightarrow \Set^I$ is cocontinuous. In particular, a coproduct $X+Y$ exists in $\Set^{(I)}_1$ if and only if the pointwise coproduct $X+Y$ belongs to $\Set^{(I)}_1$. But this almost never happens. For example, if $X=Y=1$, then $S(1+1) = I$, which is not essentially small. Thus, the coproduct $1+1$ does not exist. + label: Set_family_mostly_1_colimits + + - property: natural numbers object + proof: 'Assume that $(N,z,s)$ is a natural numbers object. Since $z : 1 \to N$ is a morphism consisting of maps $z_i : 1 \to N_i$, we have $N_i \neq \varnothing$ for every $i \in I$. By Lemma 2 here, the coproduct $1 + N$ exists, and we have $N \cong 1 + N$. We have seen above that coproducts, if they exist, must be computed pointwise. Thus, for every $i \in I$, the set $N_i \cong 1 + N_i$ has at least $2$ elements. Hence, $S(N) = I$, which is not essentially small.' + references: + - Set_family_mostly_1_colimits + + - property: cofiltered-limit-stable epimorphisms + proof: Take some index $i \in I$ and consider the embedding $\Set \to \Set^{(I)}_1$, $T \mapsto \widetilde{T}$, defined by $\widetilde{T}_i = T$ and $\widetilde{T}_j = 1$ for indices $j \neq i$. This embedding is faithful and preserves limits and epimorphisms. Thus, by Lemma 2 here, the claim follows from the fact that epimorphisms in $\Set$ are not stable under cofiltered limits. + + - property: Malcev + proof: Again, we use the embedding $\Set \to \Set^{(I)}_1$, $T \mapsto \widetilde{T}$, which extends a set by singletons. Take any set $X$ with a non-symmetric reflexive relation $R \hookrightarrow X \times X$. Then $\widetilde{R} \hookrightarrow \widetilde{X} \times \widetilde{X}$ is a non-symmetric reflexive relation. + + - property: disjoint finite products + proof: Take some index $i \in I$ and consider the embedding $\Set \to \Set^{(I)}_1$, $T \mapsto \widetilde{T}$, defined by $\widetilde{T}_i = T$ and $\widetilde{T}_j = 1$ for indices $j \neq i$. This embedding preserves products (in fact, it is right adjoint to $\ev_i$, as noted above). Take a non-empty set $T$. The projection $T \times \varnothing \to T$ is not surjective. It follows that the projection $\widetilde{T} \times \widetilde{\varnothing} \to \widetilde{T}$ is not an epimorphism, using the description of epimorphisms below. + references: + - Set_family_mostly_1_colimits + + - property: well-powered + proof: The collection $\Sub(1)$ is isomorphic to the collection of essentially small subcollections of $I$. In fact, if $J \subseteq I$ is an essentially small subcollection, we define $X \subseteq 1$ by $X_i = \varnothing$ for $i \in J$ and $X_i = 1$ for $i \notin J$. Every subobject of $1$ has this form. Since for every $i \in I$ the collection $\{i\} \subseteq I$ is essentially small, we conclude that $\Sub(1)$ is not essentially small. + + - property: concretizable + proof: >- + We will show that Isbell's condition for concretizability fails. For every object $X$ there is a unique span $1 \leftarrow X \rightarrow 1$, where $1$ is the terminal object. A cospan $1 \xrightarrow{u} Y \xleftarrow{v} 1$ corresponds to a family of elements $u_i, v_i \in Y_i$ for $i \in I$. The span commutes with the cospan if and only if, for every $i \in I$, the diagram + $$\begin{CD} + X_i @>>> 1 \\ + @VVV @VV{v_i}V \\ + 1 @>>{u_i}> Y_i + \end{CD}$$ + commutes. In other words, we must have + $$X_i \neq \varnothing \implies u_i = v_i.$$ + In particular, if we define $V(X) \coloneqq \{i \in I : X_i = \varnothing\}$, then $V(X)=V(X')$ implies that the spans for $X$ and $X'$ are equivalent, i.e., they commute with the same cospans. The converse also holds. To prove this, assume that the spans for $X$ and $X'$ are equivalent and that $i \in V(X)$. To show that $i \in V(X')$, consider the family $Y$ defined by $Y_i = \{1,2\}$ and $Y_j = \{\ast\}$ for $j \neq i$. Define $u,v : 1 \rightrightarrows Y$ by $u_i = 1$ and $v_i = 2$, and by taking the unique value for all indices $j \neq i$. Since $X_i = \varnothing$ and $u_j = v_j$ for all $j \neq i$, we see that the span for $X$ commutes with the cospan $(u,v)$. By assumption, the span for $X'$ also commutes with that cospan. Since $u_i \neq v_i$, this implies that $X'_i = \varnothing$. + + We have thus fully characterized the equivalence classes of spans $1 \leftarrow X \rightarrow 1$. For every $i \in I$, there is a family $X^i$ with $V(X^i) = \{i\}$, for example, $X^i_i = \varnothing$ and $X^i_j = \{\ast\}$ for $j \neq i$. For $i \neq i'$, the spans for $X^i$ and $X^{i'}$ are not equivalent since $V(X^i) \neq V(X^{i'})$. We conclude that the collection of equivalence classes is not essentially small. + +special_objects: + terminal object: + description: family of singleton sets + products: + description: pointwise direct products + +special_morphisms: + isomorphisms: + description: families of bijective maps + proof: This is trivial. + monomorphisms: + description: families of injective maps + proof: 'The non-trivial direction follows from the observation that each evaluation functor $\ev_i : \Set^{(I)}_1 \to \Set$ is continuous by the pointwise description of limits, and hence preserves monomorphisms.' + epimorphisms: + description: families of surjective maps + proof: 'The non-trivial direction follows from the observation that each evaluation functor $\ev_i : \Set^{(I)}_1 \to \Set$ preserves connected colimits by the pointwise description of connected colimits, and hence preserves pushouts and, consequently, epimorphisms.' diff --git a/database/data/categories/SetxSet.yaml b/database/data/categories/SetxSet.yaml index 03fe11f14..fc8446ab0 100644 --- a/database/data/categories/SetxSet.yaml +++ b/database/data/categories/SetxSet.yaml @@ -13,6 +13,7 @@ related: - Set - Set_arrow - Sh(X) + - Set_family_mostly_1 satisfied_properties: - property: locally small diff --git a/database/data/categories/Vect_family.yaml b/database/data/categories/Vect_family.yaml index e8e33d7eb..874b586f5 100644 --- a/database/data/categories/Vect_family.yaml +++ b/database/data/categories/Vect_family.yaml @@ -13,6 +13,7 @@ related: - Vect - Set_disc_Ab - Vect_large + - Set_family_mostly_1 satisfied_properties: - property: cocomplete @@ -43,6 +44,7 @@ unsatisfied_properties: Disclaimer: This result and its proof are not relevant for category theory and also depend on implementation details of set theory. Only the fact that the category is locally essentially small matters. The collection $\Hom(0,0)$ is not a set, since otherwise its unique element, the $I$-indexed family of identities $\id_0 : 0 \to 0$, would also be a set. But this is modelled as the collection of Kuratowski pairs $(i,\id_0) = \{\{i\},\{i,\id_0\}\}$ for $i \in I$. Since $I$ is not a set, this is not a set. + label: Vect_family_not_locally_small - property: generator proof: Assume that a generator $G$ exists. Since $\supp(G)$ is essentially small, but $I$ is not, we may pick $i \in I \setminus \supp(G)$. Consider the family $V$ with $\supp(V)=\{i\}$ and $V_i = K$. Then $V \neq 0$, but $\Hom(G,V) \cong \Hom(G_i,V_i) = 0$. diff --git a/shared/structure.history.json b/shared/structure.history.json index 552b39244..246ec31ea 100644 --- a/shared/structure.history.json +++ b/shared/structure.history.json @@ -194,5 +194,6 @@ "TransSeqAb": "2026-09-08", "Vect_c": "2026-09-09", "Vect_large": "2026-09-09", - "Vect_family": "2026-09-11" + "Vect_family": "2026-09-11", + "Set_family_mostly_1": "2026-09-12" } From 7f6b42aeb316a7b86ff9785097b05dbb95456b55 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 12 Sep 2026 12:00:37 +0200 Subject: [PATCH 3/8] add product categories to foundations page --- content/foundations.md | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/content/foundations.md b/content/foundations.md index 5f40e9d8f..b19e66a6b 100644 --- a/content/foundations.md +++ b/content/foundations.md @@ -72,6 +72,16 @@ For example, the category of sets $\Set$ has $\Ob(\Set) = \SetColl$, the collect Collections are the objects of a hypercategory $\Set^+$. +## Product categories + +If $(\C_i)_{i \in I}$ is a collection of categories, we can define their product $\prod_{i \in I} \C_i$ by +$$\textstyle \Ob(\prod_{i \in I} \C_i) = \prod_{i \in I} \Ob(\C_i)$$ +and +$$\textstyle \Hom(X,Y) = \prod_{i \in I} \Hom(X_i,Y_i).$$ +Identities and compositions are defined pointwise. This construction works for any collection $I$ because collections are closed under products; $I$ does not need to be small. The size of $I$ only matters if we want to determine whether the product is locally small: if $I$ is (essentially) small and each $\C_i$ is locally (essentially) small, then $\prod_{i \in I} \C_i$ is locally (essentially) small. If $I$ is not essentially small, the product is usually not locally essentially small. + +In particular, if $\C$ is a single category and $I$ is any collection, we can construct the product category $\C^I$, whose objects are $I$-indexed families of objects in $\C$. This is in fact an example of a functor category $[I_{\disc},\C]$, which we describe next. + ## Functors A _functor_ $F : \C \to \D$ between two categories (or small categories, or hypercategories) is defined as usual; it consists of maps @@ -83,7 +93,7 @@ Small categories and functors form the category $\Cat$ of small categories, whic If $F,G : \C \rightrightarrows \D$ are two functors, a morphism $F \to G$ (a _natural transformation_) is defined as a map $\Ob(\C) \to \Mor(\D)$ satisfying the usual naturality condition. These morphisms form a collection $\Hom(F,G)$. -If $\C, \D$ are categories, we can construct the functor category $[\C, \D]$ as usual. There is no set-theoretic issue, since collections behave like sets. If $\C$ is small and $\D$ is locally small, then $[\C, \D]$ is locally small. This extra assumption on $\C$ is one of many indications that categories should not be assumed locally small by default. For example, one could not even form the category of endofunctors of a general category under such a restriction, and hence no category of monads. +If $\C, \D$ are categories, we can therefore construct the functor category $[\C, \D]$ as usual, whose objects are functors and whose morphisms are morphisms of functors. There is no set-theoretic issue, since collections behave like sets. If $\C$ is small and $\D$ is locally small, then $[\C, \D]$ is locally small. This extra assumption on $\C$ is one of many indications that categories should not be assumed locally small by default. For example, one could not even form the category of endofunctors of a general category under such a restriction, and hence no category of monads. It is better to state explicitly when the assumption of being locally small is needed. From f90f1363085e2b3f64b5b2f561607f726430b9dd Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 12 Sep 2026 12:12:28 +0200 Subject: [PATCH 4/8] rename Set_disc_Ab to Ab_family and change its notation and name; change notation of SeqAb --- database/data/categories/Ab.yaml | 2 +- .../{Set_disc_Ab.yaml => Ab_family.yaml} | 27 +++++++++---------- database/data/categories/SeqAb.yaml | 8 +++--- .../data/categories/Set_family_mostly_1.yaml | 2 +- database/data/categories/TransSeqAb.yaml | 2 +- database/data/categories/Vect_family.yaml | 2 +- database/data/categories/Vect_large.yaml | 2 +- database/data/categories/Z.yaml | 2 +- database/data/categories/grAb.yaml | 2 +- .../category-implications/accessible.yaml | 2 +- shared/structure.history.json | 2 +- 11 files changed, 25 insertions(+), 28 deletions(-) rename database/data/categories/{Set_disc_Ab.yaml => Ab_family.yaml} (57%) diff --git a/database/data/categories/Ab.yaml b/database/data/categories/Ab.yaml index 87d7494f0..d0310d66f 100644 --- a/database/data/categories/Ab.yaml +++ b/database/data/categories/Ab.yaml @@ -20,7 +20,7 @@ related: - TorsFreeAb - grAb - SeqAb - - Set_disc_Ab + - Ab_family - TransSeqAb satisfied_properties: [] diff --git a/database/data/categories/Set_disc_Ab.yaml b/database/data/categories/Ab_family.yaml similarity index 57% rename from database/data/categories/Set_disc_Ab.yaml rename to database/data/categories/Ab_family.yaml index 2131fe5b3..8e04d7698 100644 --- a/database/data/categories/Set_disc_Ab.yaml +++ b/database/data/categories/Ab_family.yaml @@ -1,9 +1,9 @@ -id: Set_disc_Ab -name: category of set-indexed families of abelian groups -notation: $[\Set_{\disc},\Ab]$ -objects: families of abelian groups $(A_X)_{X \in \SetColl}$ indexed by all sets +id: Ab_family +name: category of large families of abelian groups +notation: $\Ab^I$ +objects: families of abelian groups $(A_i)_{i \in I}$ indexed by a collection $I$ that is not essentially small morphisms: families of homomorphisms -description: This functor category $[\Set_{\disc},\Ab] \cong \Ab^{\SetColl}$ is a larger variant of $\grAb = [\IZ_{\disc}, \Ab]$. Instead of $\Set_{\disc}$, we may take any other large discrete category. It does not appear in practice, but we have added it because of its interesting combinations of properties. For example, it shows that a Grothendieck abelian category is not necessarily locally small. For some background on why this functor category is well-defined, see Foundations. +description: This is the product category $\Ab^I = \prod_{i \in I} \Ab$, or equivalently, the functor category $[I_{\disc},\Ab]$. For some background on why this product category is well-defined even though $I$ is a collection, see Foundations. This category is a larger variant of $\grAb = \Ab^{\IZ}$. The properties do not depend on the specific choice of $I$, but to make things concrete, one might take $I = \SetColl$, the collection of all sets. The category does not appear in practice, but we have added it because of its interesting combinations of properties. For example, it shows that a Grothendieck abelian category is not necessarily locally essentially small or well-powered. nlab_link: null tags: @@ -11,16 +11,13 @@ tags: related: - Ab - - Z - - Set_disc - grAb - TransSeqAb - - Vect_large - Vect_family satisfied_properties: - property: preadditive - proof: This property is immediately inherited from $\Ab$, because we may define the preadditive structure pointwise via $(f+g)_X \coloneqq f_X + g_X$. Note that for two families $A,B$, the collection $\Hom(A,B)$ is a possibly large abelian group, which is compatible with our definition of a preadditive category. + proof: This property is immediately inherited from $\Ab$, because we may define the preadditive structure pointwise via $(f+g)_i \coloneqq f_i + g_i$. Note that for two families $A,B$, the collection $\Hom(A,B)$ is a possibly large abelian group, which is compatible with our definition of a preadditive category. - property: cocomplete proof: This property is immediately inherited from $\Ab$. Colimits are defined pointwise. @@ -38,20 +35,20 @@ satisfied_properties: proof: This property is immediately inherited from $\Ab$. - property: generator - proof: We know that $\Ab$ has a cogenerator $G$, for example $G = \IZ$. Then the constant family $(G)_{X \in \SetColl}$ is a generator of $[\Set_{\disc},\Ab]$. + proof: We know that $\Ab$ has a cogenerator $G$, for example $G = \IZ$. Then the constant family $(G)_{i \in I}$ is a generator of $\Ab^I$. - property: cogenerator - proof: We know that $\Ab$ has a cogenerator $Q$, for example $Q = \IQ / \IZ$. Then the constant family $(Q)_{X \in \SetColl}$ is a cogenerator of $[\Set_{\disc},\Ab]$. + proof: We know that $\Ab$ has a cogenerator $Q$, for example $Q = \IQ / \IZ$. Then the constant family $(Q)_{i \in I}$ is a cogenerator of $\Ab^I$. unsatisfied_properties: - property: skeletal proof: This is trivial. - property: split abelian - 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. + proof: Since there is an exact embedding $\Ab \to \Ab^I$ 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 essentially small. + proof: The collection of subobjects of the constant family $(\IZ/2)_{i \in I}$ identifies with the collection $P(I)$, which is not essentially small. special_objects: initial object: @@ -69,7 +66,7 @@ special_morphisms: proof: This is trivial. monomorphisms: description: families of injective homomorphisms - proof: The category is abelian and hence has kernels, constructed pointwise. Thus, a homomorphism $f = (f_X)_{X \in \SetColl}$ is a monomorphism if and only if $\ker(f_X) = 0$ for all $X$, i.e. each $f_X$ is a monomorphism. + proof: The category is abelian and hence has kernels, constructed pointwise. Thus, a homomorphism $f = (f_i)_{i \in I}$ is a monomorphism if and only if $\ker(f_i) = 0$ for all $i$, i.e. each $f_i$ is a monomorphism. epimorphisms: description: families of surjective homomorphisms - proof: The category is abelian and hence has cokernels, constructed pointwise. Thus, a homomorphism $f = (f_X)_{X \in \SetColl}$ is an epimorphism if and only if $\coker(f_X) = 0$ for all $X$, i.e. each $f_X$ is an epimorphism. + proof: The category is abelian and hence has cokernels, constructed pointwise. Thus, a homomorphism $f = (f_i)_{i \in I}$ is an epimorphism if and only if $\coker(f_i) = 0$ for all $i$, i.e. each $f_i$ is an epimorphism. diff --git a/database/data/categories/SeqAb.yaml b/database/data/categories/SeqAb.yaml index 57f4269f7..c42c5c9d4 100644 --- a/database/data/categories/SeqAb.yaml +++ b/database/data/categories/SeqAb.yaml @@ -1,9 +1,9 @@ id: SeqAb name: category of sequences of abelian groups -notation: $\Ab^{(\IN,\leq)}$ +notation: $[(\IN,\leq),\Ab]$ objects: sequences of abelian groups $A_0 \to A_1 \to A_2 \to \cdots$ morphisms: commutative diagrams -description: This is the special case of the category of $\IN$-graded modules over the $\IN$-graded ring $\IZ[T]$ with $\deg(T)=1$. It can also be viewed as the category of functors from the category of natural numbers $(\IN,\leq)$ to $\Ab$. Thus, most (but not all) properties are inherited from $\Ab$. A notable difference is that $\Ab^{(\IN,\leq)}$ is not one-sorted finitary algebraic. +description: This is the special case of the category of $\IN$-graded modules over the $\IN$-graded ring $\IZ[T]$ with $\deg(T)=1$. It can also be viewed as the category of functors from the category of natural numbers $(\IN,\leq)$ to $\Ab$. Thus, most (but not all) properties are inherited from $\Ab$. A notable difference is that $[(\IN,\leq),\Ab]$ is not one-sorted finitary algebraic. nlab_link: null parent: grMod_G(R) @@ -21,13 +21,13 @@ satisfied_properties: [] unsatisfied_properties: - property: split abelian - proof: 'This follows directly from the fact that $\Ab$ is not split abelian: it identifies with the full subcategory of $\Ab^{(\IN,\leq)}$ consisting of sequences concentrated in degree $0$.' + proof: 'This follows directly from the fact that $\Ab$ is not split abelian: it identifies with the full subcategory of $[(\IN,\leq),\Ab]$ consisting of sequences concentrated in degree $0$.' - property: one-sorted finitary algebraic proof: >- The proof is similar to the one for $\grAb$, which is the special case in which all transition maps are zero. We will show that there is no finitely presentable generator. - First, notice that $\Ab^{(\IN,\leq)}$ is the category of models of the many-sorted algebraic theory with one sort $S_n$ for each $n \in \IN$, one unary operation $T : S_n \to S_{n+1}$ for each $n \in \IN$, and the theory of an abelian group on each $S_n$. The free algebra on one generator of sort $S_n$ is the object $P[n]$ defined by + First, notice that $[(\IN,\leq),\Ab]$ is the category of models of the many-sorted algebraic theory with one sort $S_n$ for each $n \in \IN$, one unary operation $T : S_n \to S_{n+1}$ for each $n \in \IN$, and the theory of an abelian group on each $S_n$. The free algebra on one generator of sort $S_n$ is the object $P[n]$ defined by $$0 \to \cdots \to 0 \to \IZ \xrightarrow{\id} \IZ \xrightarrow{\id} \cdots,$$ which starts in degree $n$ and remains constant in all degrees $\geq n$. By Theorem 3.12 in Adamek-Rosicky, every finitely presentable object $A$ is a quotient of a finite direct sum of objects $P[n]$. It follows that there is some $N \in \IN$ such that the map $A_n \to A_{n+1}$ is surjective for every $n \geq N$ (in fact, much more is true, but this is sufficient here). But then every homomorphism $A \to P[N+1]$ is zero, as can be seen from a diagram chase in $$\begin{CD} diff --git a/database/data/categories/Set_family_mostly_1.yaml b/database/data/categories/Set_family_mostly_1.yaml index 2595f4c44..ac6aab0e4 100644 --- a/database/data/categories/Set_family_mostly_1.yaml +++ b/database/data/categories/Set_family_mostly_1.yaml @@ -12,7 +12,7 @@ tags: related: - Set - SetxSet - - Set_disc_Ab + - Ab_family - Vect_family satisfied_properties: diff --git a/database/data/categories/TransSeqAb.yaml b/database/data/categories/TransSeqAb.yaml index 3088f332e..e79a9c916 100644 --- a/database/data/categories/TransSeqAb.yaml +++ b/database/data/categories/TransSeqAb.yaml @@ -13,7 +13,7 @@ related: - Ab - On - SeqAb - - Set_disc_Ab + - Ab_family - Vect_large satisfied_properties: diff --git a/database/data/categories/Vect_family.yaml b/database/data/categories/Vect_family.yaml index 874b586f5..89115e037 100644 --- a/database/data/categories/Vect_family.yaml +++ b/database/data/categories/Vect_family.yaml @@ -11,7 +11,7 @@ tags: related: - Vect - - Set_disc_Ab + - Ab_family - Vect_large - Set_family_mostly_1 diff --git a/database/data/categories/Vect_large.yaml b/database/data/categories/Vect_large.yaml index 80806b099..ea0c061a9 100644 --- a/database/data/categories/Vect_large.yaml +++ b/database/data/categories/Vect_large.yaml @@ -19,7 +19,7 @@ tags: related: - Vect - TransSeqAb - - Set_disc_Ab + - Ab_family - FinVect - Vect_family diff --git a/database/data/categories/Z.yaml b/database/data/categories/Z.yaml index d151ff343..0de7f788e 100644 --- a/database/data/categories/Z.yaml +++ b/database/data/categories/Z.yaml @@ -13,7 +13,7 @@ tags: related: - Sch_R - Set - - Set_disc_Ab + - Ab_family satisfied_properties: - property: complete diff --git a/database/data/categories/grAb.yaml b/database/data/categories/grAb.yaml index 35d7a0619..1631ae6c5 100644 --- a/database/data/categories/grAb.yaml +++ b/database/data/categories/grAb.yaml @@ -13,7 +13,7 @@ related: - Ab - SeqAb - Ch(Ab) - - Set_disc_Ab + - Ab_family satisfied_properties: [] diff --git a/database/data/category-implications/accessible.yaml b/database/data/category-implications/accessible.yaml index 68e726d2f..f218678d7 100644 --- a/database/data/category-implications/accessible.yaml +++ b/database/data/category-implications/accessible.yaml @@ -112,7 +112,7 @@ See Deriving Auslander's formula, Cor. 5.2, or Sheafifiable homotopy model categories, Prop. 3.10. - Remark: The assumption that the category is locally essentially small is necessary (and is implicit in most of the literature), as the example $[\Set_{\disc},\Ab]$ shows (see here). + Remark: The assumption that the category is locally essentially small is necessary (and is implicit in most of the literature), as the example $\Ab^I$ for large $I$ shows (see here). - id: algebraic_implies_lfp assumptions: diff --git a/shared/structure.history.json b/shared/structure.history.json index 246ec31ea..cd16541ac 100644 --- a/shared/structure.history.json +++ b/shared/structure.history.json @@ -190,7 +190,7 @@ "Pos_noiso": "2026-09-05", "Free_fg(ZxZ)": "2026-09-06", "Set_disc": "2026-09-07", - "Set_disc_Ab": "2026-09-07", + "Ab_family": "2026-09-07", "TransSeqAb": "2026-09-08", "Vect_c": "2026-09-09", "Vect_large": "2026-09-09", From 2d79c9601507c030747f09ac64db5513d6fd06fc Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 12 Sep 2026 13:18:55 +0200 Subject: [PATCH 5/8] add the category of large families of sets which are mostly empty --- database/data/categories/Set.yaml | 1 + .../data/categories/Set_family_mostly_0.yaml | 120 ++++++++++++++++++ .../data/categories/Set_family_mostly_1.yaml | 3 +- database/data/categories/SetxSet.yaml | 1 + database/data/categories/Vect_family.yaml | 1 + shared/structure.history.json | 3 +- 6 files changed, 127 insertions(+), 2 deletions(-) create mode 100644 database/data/categories/Set_family_mostly_0.yaml diff --git a/database/data/categories/Set.yaml b/database/data/categories/Set.yaml index 0876748c7..220ab008f 100644 --- a/database/data/categories/Set.yaml +++ b/database/data/categories/Set.yaml @@ -19,6 +19,7 @@ related: - Setne - Set_arrow - Set_disc + - Set_family_mostly_0 - Set_family_mostly_1 satisfied_properties: diff --git a/database/data/categories/Set_family_mostly_0.yaml b/database/data/categories/Set_family_mostly_0.yaml new file mode 100644 index 000000000..ac826c280 --- /dev/null +++ b/database/data/categories/Set_family_mostly_0.yaml @@ -0,0 +1,120 @@ +id: Set_family_mostly_0 +name: category of large families of sets which are mostly empty +notation: $\Set^{(I)}_0$ +objects: 'families of sets $X = (X_i)_{i \in I}$ such that $\supp(X) \coloneqq \{i \in I : X_i \neq \varnothing\}$ is essentially small (i.e., isomorphic to a set), where $I$ is a fixed collection that is not essentially small' +morphisms: families of maps +description: We have added this category solely as an example of a locally cartesian closed category without a generating collection. It is a full subcategory of the product category $\Set^I$, which exists even when $I$ is merely a collection; see Foundations. Most properties are immediately inherited from $\Set$, but there is no terminal object. There are also many differences between this category and its variant $\Set^{(I)}_1$. +nlab_link: null + +tags: + - set theory + +related: + - Set + - SetxSet + - Ab_family + - Vect_family + - Set_family_mostly_1 + +satisfied_properties: + - property: locally essentially small + proof: For two families $X$ and $Y$, the collection $\Hom(X,Y) = \prod_{i \in I} \Hom(X_i,Y_i)$ is isomorphic to $\prod_{i \in \supp(X)} \Hom(X_i,Y_i)$, which is essentially small since $\supp(X)$ and each $\Hom(X_i,Y_i)$ are essentially small. + check_redundancy: false + + - property: concretizable + proof: The functor $\Set^{(I)}_0 \to \Set^+$, $X \mapsto \coprod_{i \in I} X_i$ is faithful. Since $\coprod_{i \in I} X_i \cong \coprod_{i \in \supp(X)} X_i$ is essentially small, it yields a faithful functor $\Set^{(I)}_0 \to \Set$. + + - property: cocomplete + proof: 'Since $\Set$ is cocomplete, the product category $\Set^I$ is cocomplete with pointwise colimits. (The size of the index collection does not matter.) Thus, it only remains to check that $\Set^{(I)}_0$ is closed under colimits, which are small by convention. Let $D : \J \to \Set^{(I)}_0$ be a small diagram and let $C$ be its colimit in $\Set^I$. Thus, $C_i = \colim_{j \in \J} D(j)_i$. Consider the collection $\bigcup_{j \in \J} \supp(D(j))$, which is essentially small. For any index $i$ outside this collection, we have $C_i \cong \colim_{j \in \J} 0 \cong 0$. Thus, $\supp(C) \subseteq \bigcup_{j \in \J} \supp(D(j))$, and hence $\supp(C)$ is essentially small.' + check_redundancy: false + + - property: connected limits + proof: 'In fact, all non-empty limits exist. Since $\Set$ is complete, the product category $\Set^I$ is also complete with pointwise limits. It suffices to prove that $\Set^{(I)}_0$ is closed under non-empty limits, which are small by convention. Let $D : \J \to \Set^{(I)}_0$ be a small non-empty diagram and let $L$ be its limit in $\Set^I$. Thus, $L_i = \lim_{j \in \J} D(j)_i$. Consider the collection $\bigcup_{j \in \J} \supp(D(j))$, which is essentially small. For any index $i$ outside this collection, we have $L_i \cong \lim_{j \in \J} 0 \cong 0$, where the last step uses the fact that $\J$ is non-empty. Thus, $\supp(L) \subseteq \bigcup_{j \in \J} \supp(D(j))$, and hence $\supp(L)$ is essentially small.' + label: Set_family_mostly_0_non_empty_limits + check_redundancy: false + + - property: binary products + proof: We have just proved that non-empty limits exist. Concretely, we have $(X \times Y)_i = X_i \times Y_i$ with $\supp(X \times Y) = \supp(X) \cap \supp(Y)$. + references: + - Set_family_mostly_0_non_empty_limits + + - property: infinitary extensive + proof: Since $\Set$ is infinitary extensive, $\Set^I$ is also infinitary extensive. We can now apply Lemma 11 here to the inclusion functor $\Set^{(I)}_0 \hookrightarrow \Set^I$. + + - property: locally cartesian closed + proof: >- + First of all, $\Set$ is locally cartesian closed, i.e. each slice $\Set / X$ is cartesian closed, with exponentials + $$\textstyle [Y \to X, Z \to X] = \coprod_{x \in X} \Hom(Y_x,Z_x),$$ + where $Y_x$ denotes the fiber of $Y \to X$ over $x \in X$. It follows formally that, for every collection $I$, $\Set^I$ is also locally cartesian closed, with exponentials + $$\textstyle [Y \to X, Z \to X]_i = \coprod_{x \in X_i} \Hom((Y_i)_x,(Z_i)_x).$$ + We see + $$\supp([Y \to X, Z \to X]) \subseteq \supp(X).$$ + In particular, if $\supp(X)$ is essentially small, then $\supp([Y \to X, Z \to X])$ is also essentially small. Thus, if $X \in \Set^{(I)}_0$, then the full subcategory $\Set^{(I)}_0 / X$ of $\Set^I / X$ is closed under exponentials and is therefore also cartesian closed. + + - property: epi-regular + proof: We claim that every epimorphism $X \to Y$ is the coequalizer of its kernel pair $X \times_Y X \rightrightarrows X$. This is because every component $X_i \to Y_i$ is surjective (see the classification of epimorphisms below), the statement holds in $\Set$, and coequalizers and pullbacks are constructed pointwise. + + - property: filtered-colimit-stable monomorphisms + proof: Since filtered colimits are constructed pointwise and the monomorphisms are precisely the morphisms that are pointwise injective (see below), this property is inherited from $\Set$. + + - property: cocartesian cofiltered limits + proof: This property is inherited from $\Set$ since binary coproducts (in fact, all colimits) and cofiltered limits (in fact, all non-empty limits) are constructed pointwise. + + - property: coregular + proof: It suffices to prove that regular monomorphisms are stable under pushout. This property is clearly inherited from $\Set$. + + - property: well-powered + proof: The monomorphisms $X \to Y$ are precisely the morphisms that are pointwise injective (see below). If $X_i \to Y_i$ is injective and $Y_i = \varnothing$, then also $X_i = \varnothing$. It follows that the collection $\Sub(Y) \cong \prod_{i \in \supp(Y)} \Sub(Y_i)$ is essentially small. + check_redundancy: false + + - property: well-copowered + proof: The epimorphisms $X \to Y$ are precisely the morphisms that are pointwise surjective (see below). If $X_i \to Y_i$ is surjective and $X_i = \varnothing$, then also $Y_i = \varnothing$. It follows that the collection $\Quot(X) \cong \prod_{i \in \supp(X)} \Quot(X_i)$ is essentially small. + + - property: effective congruences + proof: Let $R \rightrightarrows X$ be a congruence in $\Set^{(I)}_0$. We claim that it is the kernel pair of its coequalizer $X \twoheadrightarrow X/R$. This certainly holds in $\Set$, and for every $i \in I$, the pair $R_i \rightrightarrows X_i$ is a congruence in $\Set$. Therefore, the claim follows since kernel pairs (in fact, all connected limits) and coequalizers (in fact, all colimits) are constructed pointwise. + + - property: effective cocongruences + proof: Let $X \rightrightarrows R$ be a cocongruence in $\Set^{(I)}_0$. We claim that it is the cokernel pair of its equalizer $E \hookrightarrow X$. This certainly holds in $\Set$, and for every $i \in I$, the pair $X_i \rightrightarrows R_i$ is a cocongruence in $\Set$. Therefore, the claim follows since cokernel pairs (in fact, all colimits) and equalizers (in fact, all connected limits) are constructed pointwise. + + - property: co-Malcev + proof: Since colimits are constructed pointwise, this property is inherited from $\Set$. + +unsatisfied_properties: + - property: skeletal + proof: This is trivial. + + - property: semi-strongly connected + proof: This is because $\Set \times \Set$ can be embedded into $\Set^{(I)}_0$ by extending each pair of sets with empty sets, and we know that $\Set \times \Set$ is not semi-strongly connected. + + - property: locally small + proof: The proof is identical to the proof for $\Vect^{(I)}$. However, this result is not relevant for category theory; only the fact that the category is locally essentially small matters. + references: + - Vect_family_not_locally_small + + - property: terminal object + proof: Assume that a terminal object $X$ exists. For $i \in I$, define the family $Y$ by $Y_i = \{\ast\}$ and $Y_j = \varnothing$ for $j \neq i$. Then $\supp(Y) = \{i\}$, so $Y$ belongs to $\Set^{(I)}_0$. By assumption, there is a morphism $Y \to X$. In particular, we see that $X_i$ is non-empty. But then $\supp(X) = I$, which is not essentially small. + + - property: cofiltered-limit-stable epimorphisms + proof: Take some index $i \in I$ and consider the embedding $\Set \to \Set^{(I)}_0$, $T \mapsto \widetilde{T}$, defined by $\widetilde{T}_i = T$ and $\widetilde{T}_j = 0$ for indices $j \neq i$. This embedding is faithful and preserves non-empty limits and epimorphisms. Thus, by Lemma 2 here, the claim follows from the fact that epimorphisms in $\Set$ are not stable under cofiltered limits. + + - property: cogenerating collection + proof: Assume that $S$ is a cogenerating collection. In particular, $S$ is essentially small (by definition). Since $\bigcup_{Q \in S} \supp(Q)$ is essentially small, but $I$ is not essentially small, there is some index $i \in I$ with $Q_i = \varnothing$ for all $Q \in S$. Consider the family $X \in \Set^{(I)}_0$ defined by $X_i = \{1,2\}$ and $X_j = \varnothing$ for all $j \neq i$. There are (at least) two morphisms $X \rightrightarrows X$. Thus, there is some $Q \in S$ and some morphism $X \to Q$ that distinguishes them. The component at $i$ is a map $X_i \to Q_i$, which cannot exist since $X_i$ is non-empty and $Q_i$ is empty. + +special_objects: + initial object: + description: family of empty sets + coproducts: + description: pointwise disjoint unions + products: + description: '[non-empty case] pointwise direct products' + +special_morphisms: + isomorphisms: + description: families of bijective maps + proof: This is trivial. + monomorphisms: + description: families of injective maps + proof: 'The non-trivial direction follows from the observation that each evaluation functor $\ev_i : \Set^{(I)}_0 \to \Set$ preserves pullbacks by the pointwise description of pullbacks, and hence preserves monomorphisms.' + epimorphisms: + description: families of surjective maps + proof: 'The non-trivial direction follows from the observation that each evaluation functor $\ev_i : \Set^{(I)}_0 \to \Set$ preserves pushouts by the pointwise description of colimits, and hence preserves epimorphisms.' diff --git a/database/data/categories/Set_family_mostly_1.yaml b/database/data/categories/Set_family_mostly_1.yaml index ac6aab0e4..8d8648291 100644 --- a/database/data/categories/Set_family_mostly_1.yaml +++ b/database/data/categories/Set_family_mostly_1.yaml @@ -3,7 +3,7 @@ name: category of large families of sets which are mostly singletons notation: $\Set^{(I)}_1$ objects: 'families of sets $X = (X_i)_{i \in I}$ such that $S(X) \coloneqq \{i \in I : X_i \not\cong 1\}$ is essentially small (i.e., isomorphic to a set), where $I$ is a fixed collection that is not essentially small' morphisms: families of maps -description: We have added this category solely as an example of a cartesian closed category without a generating collection, but it also satisfies some other interesting combinations of properties. It is a full subcategory of the product category $\Set^I$, which exists even when $I$ is merely a collection; see Foundations. +description: We have added this category solely as an example of a cartesian closed category without a generating collection, but it also satisfies some other interesting combinations of properties. It is a full subcategory of the product category $\Set^I$, which exists even when $I$ is merely a collection; see Foundations. Most properties are immediately inherited from $\Set$, but there is no initial object. There are also many differences between this category and its variant $\Set^{(I)}_0$. nlab_link: null tags: @@ -12,6 +12,7 @@ tags: related: - Set - SetxSet + - Set_family_mostly_0 - Ab_family - Vect_family diff --git a/database/data/categories/SetxSet.yaml b/database/data/categories/SetxSet.yaml index fc8446ab0..c637d1fd6 100644 --- a/database/data/categories/SetxSet.yaml +++ b/database/data/categories/SetxSet.yaml @@ -13,6 +13,7 @@ related: - Set - Set_arrow - Sh(X) + - Set_family_mostly_0 - Set_family_mostly_1 satisfied_properties: diff --git a/database/data/categories/Vect_family.yaml b/database/data/categories/Vect_family.yaml index 89115e037..f26525c44 100644 --- a/database/data/categories/Vect_family.yaml +++ b/database/data/categories/Vect_family.yaml @@ -13,6 +13,7 @@ related: - Vect - Ab_family - Vect_large + - Set_family_mostly_0 - Set_family_mostly_1 satisfied_properties: diff --git a/shared/structure.history.json b/shared/structure.history.json index cd16541ac..4ba91f8f5 100644 --- a/shared/structure.history.json +++ b/shared/structure.history.json @@ -195,5 +195,6 @@ "Vect_c": "2026-09-09", "Vect_large": "2026-09-09", "Vect_family": "2026-09-11", - "Set_family_mostly_1": "2026-09-12" + "Set_family_mostly_1": "2026-09-12", + "Set_family_mostly_0": "2026-09-12" } From 659fa70bd70eff27f5e78975141d169ffbc4d827 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 13 Sep 2026 07:56:26 +0200 Subject: [PATCH 6/8] remove redundant assignments from Z --- database/data/categories/Z.yaml | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/database/data/categories/Z.yaml b/database/data/categories/Z.yaml index 0de7f788e..61d91300c 100644 --- a/database/data/categories/Z.yaml +++ b/database/data/categories/Z.yaml @@ -17,10 +17,10 @@ related: satisfied_properties: - property: complete - proof: This follows immediately from the fact for $\Set$. + proof: This follows immediately from the fact for $\Set$. Limits are constructed pointwise. - property: cocomplete - proof: This follows immediately from the fact for $\Set$. + proof: This follows immediately from the fact for $\Set$. Colimits are constructed pointwise. check_redundancy: false - property: infinitary extensive @@ -35,17 +35,9 @@ satisfied_properties: - property: coregular proof: This follows immediately from the fact for $\Set$. - - property: co-Malcev - proof: This follows immediately from the fact for $\Set$. - check_redundancy: false - - property: effective congruences proof: 'If we have a congruence $E \rightrightarrows X$ in $[\CRing, \Set]$, then evaluating at any commutative ring gives a congruence in $\Set$. Defining $Y$ pointwise to be the quotient of this congruence, we get a morphism of functors $h : X \to Y$, and by this result applied pointwise, the kernel pair of $h$ is $E$.' - - property: effective cocongruences - proof: 'If we have a cocongruence $X\rightrightarrows E$ in $[\CRing, \Set]$, then evaluating at any commutative gives a cocongruence in $\Set$. Defining $Y$ pointwise to be the equalizer of the pair, we get a morphism of functors $h : Y \to X$, and by the dual of this result applied pointwise, the cokernel pair of $h$ is $E$.' - check_redundancy: false - unsatisfied_properties: - property: skeletal proof: This is trivial. From da26df656345a8f07f936811550fe78aba778ead Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 13 Sep 2026 09:15:06 +0200 Subject: [PATCH 7/8] add the category of large families of sets --- content/cogenerators_in_product_categories.md | 2 + database/data/categories/Ab_family.yaml | 1 + database/data/categories/Set.yaml | 3 +- database/data/categories/Set_family.yaml | 73 +++++++++++++++++++ .../data/categories/Set_family_mostly_0.yaml | 3 +- .../data/categories/Set_family_mostly_1.yaml | 3 +- database/data/categories/SetxSet.yaml | 3 +- database/data/categories/Vect_family.yaml | 1 + database/data/categories/Z.yaml | 2 +- shared/structure.history.json | 3 +- 10 files changed, 86 insertions(+), 8 deletions(-) create mode 100644 database/data/categories/Set_family.yaml diff --git a/content/cogenerators_in_product_categories.md b/content/cogenerators_in_product_categories.md index 84551062d..926321feb 100644 --- a/content/cogenerators_in_product_categories.md +++ b/content/cogenerators_in_product_categories.md @@ -5,6 +5,8 @@ description: How to construct a cogenerator in a product category # Cogenerators in product categories +Recall that an object $X$ of a category is called _weakly terminal_ if any object $Y$ admits at least one morphism $Y \to X$. Uniqueness is not required. + ::: Lemma For a family of categories $(\C_i)_{i \in I}$, each having a cogenerator $Q_i$ which is weakly terminal, the object $(Q_i)_{i \in I}$ is a cogenerator in the product category $\prod_{i \in I} \C_i$. ::: diff --git a/database/data/categories/Ab_family.yaml b/database/data/categories/Ab_family.yaml index 8e04d7698..17d7b0fad 100644 --- a/database/data/categories/Ab_family.yaml +++ b/database/data/categories/Ab_family.yaml @@ -14,6 +14,7 @@ related: - grAb - TransSeqAb - Vect_family + - Set_family satisfied_properties: - property: preadditive diff --git a/database/data/categories/Set.yaml b/database/data/categories/Set.yaml index 220ab008f..3aca6674d 100644 --- a/database/data/categories/Set.yaml +++ b/database/data/categories/Set.yaml @@ -19,8 +19,7 @@ related: - Setne - Set_arrow - Set_disc - - Set_family_mostly_0 - - Set_family_mostly_1 + - Set_family satisfied_properties: - property: locally small diff --git a/database/data/categories/Set_family.yaml b/database/data/categories/Set_family.yaml new file mode 100644 index 000000000..98f8e5189 --- /dev/null +++ b/database/data/categories/Set_family.yaml @@ -0,0 +1,73 @@ +id: Set_family +name: category of large families of sets +notation: $\Set^I$ +objects: families of sets $(X_i)_{i \in I}$ indexed by a collection $I$ that is not essentially small +morphisms: families of maps +description: This is the product category $\Set^I = \prod_{i \in I} \Set$, or equivalently, the functor category $[I_{\disc},\Set]$. For some background on why this product category is well-defined even though $I$ is a collection, see Foundations. It is a larger variant of $\Set \times \Set$, and most of its properties are inherited from $\Set$, but it is not locally essentially small. +nlab_link: null + +tags: + - set theory + +related: + - Set + - SetxSet + - Set_family_mostly_0 + - Set_family_mostly_1 + - Vect_family + - Ab_family + - Z + +satisfied_properties: + - property: complete + proof: This follows immediately from the fact that $\Set$ is complete. Limits are constructed pointwise. + + - property: cocomplete + proof: This follows immediately from the fact that $\Set$ is cocomplete. Colimits are constructed pointwise. + check_redundancy: false + + - property: exact filtered colimits + proof: This follows immediately from the corresponding property of $\Set$. + + - property: cartesian closed + proof: This follows immediately from the fact that $\Set$ is cartesian closed. Exponentials are constructed pointwise. + + - property: subobject classifier + proof: Since monomorphisms in $\Set^I$ are families of monomorphisms in $\Set$ (see below) and the set $\{0,1\}$ is a subobject classifier for $\Set$, the family $(\{0,1\})_{i \in I}$ is a subobject classifier for $\Set^I$. + + - property: cogenerator + proof: The set $\{0,1\}$ is a cogenerator of $\Set$, which is weakly terminal. Hence, this lemma implies that the family $(\{0,1\})_{i \in I}$ is a cogenerator of $\Set^I$. + +unsatisfied_properties: + - property: skeletal + proof: This is trivial. + + - property: semi-strongly connected + proof: This is because $\Set \times \Set$ can be embedded into $\Set^I$ by extending each pair of sets with empty sets, and we know that $\Set \times \Set$ is not semi-strongly connected. + + - property: generating collection + proof: 'Assume that there is a generating collection $S$, which is in particular essentially small by convention. For $i \in I$, consider the family $X^i$ defined by $(X^i)_i = \{0,1\}$ and $(X^i)_j = \varnothing$ for $j \neq i$. There are (at least) two morphisms $X^i \rightrightarrows X^i$. Thus, there is some $G^i \in S$ and a morphism $G^i \to X^i$ that distinguishes the two morphisms. This is only possible when $(G^i)_i$ is non-empty, while $(G^i)_j$ is empty for all $j \neq i$. Thus, if we define the support of a family by $\supp(X) \coloneqq \{i \in I : X_i \neq \varnothing\}$, then $\supp(G^i) = \{i\}$. Therefore, using the axiom of choice, we get an injective map $I \to S$, $i \mapsto G^i$. Since $S$ is essentially small, it follows that $I$ is essentially small, which contradicts our assumption on $I$.' + + - property: well-powered + proof: The collection $\Sub(1)$ is isomorphic to the collection $P(I)$ of subcollections of $I$. In fact, if $J \subseteq I$ is a subcollection, we define $X \subseteq 1$ by $X_i = \varnothing$ for $i \in J$ and $X_i = 1$ for $i \notin J$. Every subobject of $1$ has this form. Since $P(I)$ is not essentially small (there is an injective map $I \hookrightarrow P(I)$), we conclude that $\Sub(1)$ is not essentially small. + +special_objects: + initial object: + description: family of empty sets + terminal object: + description: family of singleton sets + coproducts: + description: pointwise defined disjoint unions + products: + description: pointwise defined direct products + +special_morphisms: + isomorphisms: + description: families of bijective maps + proof: This is trivial. + monomorphisms: + description: families of injective maps + proof: 'The non-trivial direction follows from the observation that each evaluation functor $\ev_i : \Set^I \to \Set$ preserves pullbacks by the pointwise description of limits, and hence preserves monomorphisms.' + epimorphisms: + description: families of surjective maps + proof: 'The non-trivial direction follows from the observation that each evaluation functor $\ev_i : \Set^I \to \Set$ preserves pushouts by the pointwise description of colimits, and hence preserves epimorphisms.' diff --git a/database/data/categories/Set_family_mostly_0.yaml b/database/data/categories/Set_family_mostly_0.yaml index ac826c280..4fe2b325c 100644 --- a/database/data/categories/Set_family_mostly_0.yaml +++ b/database/data/categories/Set_family_mostly_0.yaml @@ -3,7 +3,7 @@ name: category of large families of sets which are mostly empty notation: $\Set^{(I)}_0$ objects: 'families of sets $X = (X_i)_{i \in I}$ such that $\supp(X) \coloneqq \{i \in I : X_i \neq \varnothing\}$ is essentially small (i.e., isomorphic to a set), where $I$ is a fixed collection that is not essentially small' morphisms: families of maps -description: We have added this category solely as an example of a locally cartesian closed category without a generating collection. It is a full subcategory of the product category $\Set^I$, which exists even when $I$ is merely a collection; see Foundations. Most properties are immediately inherited from $\Set$, but there is no terminal object. There are also many differences between this category and its variant $\Set^{(I)}_1$. +description: We have added this category solely as an example of a locally cartesian closed category without a generating collection. It is a full subcategory of the product category $\Set^I$. Most properties are immediately inherited from $\Set$, but there is no terminal object. There are also many differences between this category and its variant $\Set^{(I)}_1$. nlab_link: null tags: @@ -12,6 +12,7 @@ tags: related: - Set - SetxSet + - Set_family - Ab_family - Vect_family - Set_family_mostly_1 diff --git a/database/data/categories/Set_family_mostly_1.yaml b/database/data/categories/Set_family_mostly_1.yaml index 8d8648291..53701d63b 100644 --- a/database/data/categories/Set_family_mostly_1.yaml +++ b/database/data/categories/Set_family_mostly_1.yaml @@ -3,7 +3,7 @@ name: category of large families of sets which are mostly singletons notation: $\Set^{(I)}_1$ objects: 'families of sets $X = (X_i)_{i \in I}$ such that $S(X) \coloneqq \{i \in I : X_i \not\cong 1\}$ is essentially small (i.e., isomorphic to a set), where $I$ is a fixed collection that is not essentially small' morphisms: families of maps -description: We have added this category solely as an example of a cartesian closed category without a generating collection, but it also satisfies some other interesting combinations of properties. It is a full subcategory of the product category $\Set^I$, which exists even when $I$ is merely a collection; see Foundations. Most properties are immediately inherited from $\Set$, but there is no initial object. There are also many differences between this category and its variant $\Set^{(I)}_0$. +description: We have added this category solely as an example of a cartesian closed category without a generating collection, but it also satisfies some other interesting combinations of properties. It is a full subcategory of the product category $\Set^I$. Most properties are immediately inherited from $\Set$, but there is no initial object. There are also many differences between this category and its variant $\Set^{(I)}_0$. nlab_link: null tags: @@ -13,6 +13,7 @@ related: - Set - SetxSet - Set_family_mostly_0 + - Set_family - Ab_family - Vect_family diff --git a/database/data/categories/SetxSet.yaml b/database/data/categories/SetxSet.yaml index c637d1fd6..b05d16184 100644 --- a/database/data/categories/SetxSet.yaml +++ b/database/data/categories/SetxSet.yaml @@ -13,8 +13,7 @@ related: - Set - Set_arrow - Sh(X) - - Set_family_mostly_0 - - Set_family_mostly_1 + - Set_family satisfied_properties: - property: locally small diff --git a/database/data/categories/Vect_family.yaml b/database/data/categories/Vect_family.yaml index f26525c44..f3194fe30 100644 --- a/database/data/categories/Vect_family.yaml +++ b/database/data/categories/Vect_family.yaml @@ -15,6 +15,7 @@ related: - Vect_large - Set_family_mostly_0 - Set_family_mostly_1 + - Set_family satisfied_properties: - property: cocomplete diff --git a/database/data/categories/Z.yaml b/database/data/categories/Z.yaml index 61d91300c..ebd566efe 100644 --- a/database/data/categories/Z.yaml +++ b/database/data/categories/Z.yaml @@ -13,7 +13,7 @@ tags: related: - Sch_R - Set - - Ab_family + - Set_family satisfied_properties: - property: complete diff --git a/shared/structure.history.json b/shared/structure.history.json index 4ba91f8f5..a7b4673e0 100644 --- a/shared/structure.history.json +++ b/shared/structure.history.json @@ -196,5 +196,6 @@ "Vect_large": "2026-09-09", "Vect_family": "2026-09-11", "Set_family_mostly_1": "2026-09-12", - "Set_family_mostly_0": "2026-09-12" + "Set_family_mostly_0": "2026-09-12", + "Set_family": "2026-09-13" } From 2be5aaa950fa3faafb0186bfdf0bcf995589db53 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 13 Sep 2026 09:29:40 +0200 Subject: [PATCH 8/8] rename Vect_family to Vect_family_mostly_0 --- database/data/categories/Ab_family.yaml | 2 +- database/data/categories/Set_family.yaml | 2 +- database/data/categories/Set_family_mostly_0.yaml | 6 +++--- database/data/categories/Set_family_mostly_1.yaml | 6 +++--- database/data/categories/Vect.yaml | 2 +- .../{Vect_family.yaml => Vect_family_mostly_0.yaml} | 8 ++++---- database/data/categories/Vect_large.yaml | 2 +- shared/structure.history.json | 2 +- 8 files changed, 15 insertions(+), 15 deletions(-) rename database/data/categories/{Vect_family.yaml => Vect_family_mostly_0.yaml} (97%) diff --git a/database/data/categories/Ab_family.yaml b/database/data/categories/Ab_family.yaml index 17d7b0fad..2a9e07776 100644 --- a/database/data/categories/Ab_family.yaml +++ b/database/data/categories/Ab_family.yaml @@ -13,7 +13,7 @@ related: - Ab - grAb - TransSeqAb - - Vect_family + - Vect_family_mostly_0 - Set_family satisfied_properties: diff --git a/database/data/categories/Set_family.yaml b/database/data/categories/Set_family.yaml index 98f8e5189..52b1ad0ea 100644 --- a/database/data/categories/Set_family.yaml +++ b/database/data/categories/Set_family.yaml @@ -14,7 +14,7 @@ related: - SetxSet - Set_family_mostly_0 - Set_family_mostly_1 - - Vect_family + - Vect_family_mostly_0 - Ab_family - Z diff --git a/database/data/categories/Set_family_mostly_0.yaml b/database/data/categories/Set_family_mostly_0.yaml index 4fe2b325c..e7af16b91 100644 --- a/database/data/categories/Set_family_mostly_0.yaml +++ b/database/data/categories/Set_family_mostly_0.yaml @@ -14,7 +14,7 @@ related: - SetxSet - Set_family - Ab_family - - Vect_family + - Vect_family_mostly_0 - Set_family_mostly_1 satisfied_properties: @@ -88,9 +88,9 @@ unsatisfied_properties: proof: This is because $\Set \times \Set$ can be embedded into $\Set^{(I)}_0$ by extending each pair of sets with empty sets, and we know that $\Set \times \Set$ is not semi-strongly connected. - property: locally small - proof: The proof is identical to the proof for $\Vect^{(I)}$. However, this result is not relevant for category theory; only the fact that the category is locally essentially small matters. + proof: The proof is identical to the proof for $\Vect^{(I)}$. However, this result is not relevant for category theory; only the fact that the category is locally essentially small matters. references: - - Vect_family_not_locally_small + - Vect_family_mostly_0_not_locally_small - property: terminal object proof: Assume that a terminal object $X$ exists. For $i \in I$, define the family $Y$ by $Y_i = \{\ast\}$ and $Y_j = \varnothing$ for $j \neq i$. Then $\supp(Y) = \{i\}$, so $Y$ belongs to $\Set^{(I)}_0$. By assumption, there is a morphism $Y \to X$. In particular, we see that $X_i$ is non-empty. But then $\supp(X) = I$, which is not essentially small. diff --git a/database/data/categories/Set_family_mostly_1.yaml b/database/data/categories/Set_family_mostly_1.yaml index 53701d63b..f44224039 100644 --- a/database/data/categories/Set_family_mostly_1.yaml +++ b/database/data/categories/Set_family_mostly_1.yaml @@ -15,7 +15,7 @@ related: - Set_family_mostly_0 - Set_family - Ab_family - - Vect_family + - Vect_family_mostly_0 satisfied_properties: - property: locally essentially small @@ -60,9 +60,9 @@ unsatisfied_properties: proof: This is because $\Set \times \Set$ can be embedded into $\Set^{(I)}_1$ by extending each pair of sets with singletons, and we know that $\Set \times \Set$ is not semi-strongly connected. - property: locally small - proof: The proof is identical to the proof for $\Vect^{(I)}$. However, this result is not relevant for category theory; only the fact that the category is locally essentially small matters. + proof: The proof is identical to the proof for $\Vect^{(I)}$. However, this result is not relevant for category theory; only the fact that the category is locally essentially small matters. references: - - Vect_family_not_locally_small + - Vect_family_mostly_0_not_locally_small - property: binary copowers proof: >- diff --git a/database/data/categories/Vect.yaml b/database/data/categories/Vect.yaml index 620a41c97..34ec987fd 100644 --- a/database/data/categories/Vect.yaml +++ b/database/data/categories/Vect.yaml @@ -17,7 +17,7 @@ related: - FreeAb - Vect_c - Vect_large - - Vect_family + - Vect_family_mostly_0 satisfied_properties: - property: split abelian diff --git a/database/data/categories/Vect_family.yaml b/database/data/categories/Vect_family_mostly_0.yaml similarity index 97% rename from database/data/categories/Vect_family.yaml rename to database/data/categories/Vect_family_mostly_0.yaml index f3194fe30..71c59e680 100644 --- a/database/data/categories/Vect_family.yaml +++ b/database/data/categories/Vect_family_mostly_0.yaml @@ -1,5 +1,5 @@ -id: Vect_family -name: category of large families of vector spaces with small support +id: Vect_family_mostly_0 +name: category of large families of vector spaces which are mostly zero notation: $\Vect^{(I)}_K$ objects: 'families of vector spaces $V = (V_i)_{i \in I}$ over a field $K$ whose support $\supp(V) \coloneqq \{i \in I : V_i \neq 0\}$ is essentially small (i.e., isomorphic to a set), where $I$ is a fixed collection that is not essentially small' morphisms: families of linear maps @@ -32,7 +32,7 @@ satisfied_properties: proof: This follows easily from the fact that $\Vect_K$ has exact filtered colimits. - property: well-powered - proof: The subobjects of $V$ are given by the families $W$ with $W_i \subseteq V_i$ for all $i \in I$. In particular, $\supp(W) \subseteq \supp(V)$. Hence, the collection of subobjects is small. + proof: The subobjects of $V$ are given by the families $W$ with $W_i \subseteq V_i$ for all $i \in I$. In particular, $\supp(W) \subseteq \supp(V)$. Hence, the collection of subobjects is essentially small. - property: concretizable proof: The functor $\Vect^{(I)}_K \to \Vect_K$, $(V_i)_{i \in I} \mapsto \bigoplus_{i \in I} V_i$ is well-defined (since we may discard all indices $i$ for which $V_i=0$) and faithful. Since $\Vect_K$ is concretizable, so is $\Vect^{(I)}_K$. @@ -46,7 +46,7 @@ unsatisfied_properties: Disclaimer: This result and its proof are not relevant for category theory and also depend on implementation details of set theory. Only the fact that the category is locally essentially small matters. The collection $\Hom(0,0)$ is not a set, since otherwise its unique element, the $I$-indexed family of identities $\id_0 : 0 \to 0$, would also be a set. But this is modelled as the collection of Kuratowski pairs $(i,\id_0) = \{\{i\},\{i,\id_0\}\}$ for $i \in I$. Since $I$ is not a set, this is not a set. - label: Vect_family_not_locally_small + label: Vect_family_mostly_0_not_locally_small - property: generator proof: Assume that a generator $G$ exists. Since $\supp(G)$ is essentially small, but $I$ is not, we may pick $i \in I \setminus \supp(G)$. Consider the family $V$ with $\supp(V)=\{i\}$ and $V_i = K$. Then $V \neq 0$, but $\Hom(G,V) \cong \Hom(G_i,V_i) = 0$. diff --git a/database/data/categories/Vect_large.yaml b/database/data/categories/Vect_large.yaml index ea0c061a9..52b615b06 100644 --- a/database/data/categories/Vect_large.yaml +++ b/database/data/categories/Vect_large.yaml @@ -21,7 +21,7 @@ related: - TransSeqAb - Ab_family - FinVect - - Vect_family + - Vect_family_mostly_0 satisfied_properties: - property: preadditive diff --git a/shared/structure.history.json b/shared/structure.history.json index a7b4673e0..f0b21c7aa 100644 --- a/shared/structure.history.json +++ b/shared/structure.history.json @@ -194,7 +194,7 @@ "TransSeqAb": "2026-09-08", "Vect_c": "2026-09-09", "Vect_large": "2026-09-09", - "Vect_family": "2026-09-11", + "Vect_family_mostly_0": "2026-09-11", "Set_family_mostly_1": "2026-09-12", "Set_family_mostly_0": "2026-09-12", "Set_family": "2026-09-13"