Add three categories of large families of sets

.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",

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$.
 :::

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.
 

database/data/categories/Ab.yaml

@@ -20,7 +20,7 @@ related:
   - TorsFreeAb
   - grAb
   - SeqAb
-  - Set_disc_Ab
+  - Ab_family
   - TransSeqAb
 
 satisfied_properties: []

database/data/categories/Set_disc_Ab.yaml → database/data/categories/Ab_family.yaml

@@ -1,26 +1,24 @@
-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 <a href="/content/foundations">Foundations</a>.
+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 <a href="/content/foundations">Foundations</a>. 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:
   - algebra
 
 related:
   - Ab
-  - Z
-  - Set_disc
   - grAb
   - TransSeqAb
-  - Vect_large
-  - Vect_family
+  - Vect_family_mostly_0
+  - Set_family
 
 satisfied_properties:
   - property: preadditive
-    proof: This property is immediately inherited from <a href="/category/Ab">$\Ab$</a>, 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 <i>possibly large</i> abelian group, which is compatible with our definition of a preadditive category.
+    proof: This property is immediately inherited from <a href="/category/Ab">$\Ab$</a>, 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 <i>possibly large</i> abelian group, which is compatible with our definition of a preadditive category.
 
   - property: cocomplete
     proof: This property is immediately inherited from <a href="/category/Ab">$\Ab$</a>. Colimits are defined pointwise.
@@ -38,20 +36,20 @@ satisfied_properties:
     proof: This property is immediately inherited from <a href="/category/Ab">$\Ab$</a>.
 
   - property: generator
-    proof: We know that <a href="/category/Ab">$\Ab$</a> 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 <a href="/category/Ab">$\Ab$</a> 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 <a href="/category/Ab">$\Ab$</a> 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 <a href="/category/Ab">$\Ab$</a> 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 <a href="/category/Ab">$\Ab$</a> 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 <a href="/category/Ab">$\Ab$</a> 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 +67,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.

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 <a href="/category/grMod_G(R)">category of $\IN$-graded modules</a> over the $\IN$-graded ring $\IZ[T]$ with $\deg(T)=1$. It can also be viewed as the category of functors from the <a href="/category/N">category of natural numbers $(\IN,\leq)$</a> to $\Ab$. Thus, most (but not all) properties are inherited from <a href="/category/Ab">$\Ab$</a>. A notable difference is that $\Ab^{(\IN,\leq)}$ is not one-sorted finitary algebraic.
+description: This is the special case of the <a href="/category/grMod_G(R)">category of $\IN$-graded modules</a> over the $\IN$-graded ring $\IZ[T]$ with $\deg(T)=1$. It can also be viewed as the category of functors from the <a href="/category/N">category of natural numbers $(\IN,\leq)$</a> to $\Ab$. Thus, most (but not all) properties are inherited from <a href="/category/Ab">$\Ab$</a>. 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 <a href="/category/Ab">$\Ab$</a> 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 <a href="/category/Ab">$\Ab$</a> 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 <a href="/category/grAb">$\grAb$</a>, 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 <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, 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}

database/data/categories/Set.yaml

@@ -19,6 +19,7 @@ related:
   - Setne
   - Set_arrow
   - Set_disc
+  - Set_family
 
 satisfied_properties:
   - property: locally small

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 <a href="/content/foundations">Foundations</a>. 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_mostly_0
+  - Ab_family
+  - Z
+
+satisfied_properties:
+  - property: complete
+    proof: This follows immediately from the fact that <a href="/category/Set">$\Set$</a> is complete. Limits are constructed pointwise.
+
+  - property: cocomplete
+    proof: This follows immediately from the fact that <a href="/category/Set">$\Set$</a> is cocomplete. Colimits are constructed pointwise.
+    check_redundancy: false
+
+  - property: exact filtered colimits
+    proof: This follows immediately from the corresponding property of <a href="/category/Set">$\Set$</a>.
+
+  - property: cartesian closed
+    proof: This follows immediately from the fact that <a href="/category/Set">$\Set$</a> 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 <a href="/category/Set">$\Set$</a>, 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, <a href="/content/cogenerators_in_product_categories">this lemma</a> 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 <a href="/category/SetxSet">$\Set \times \Set$</a> 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.'