Write empty sets, singletons, and two-element sets explicitly

CLAUDE.md

@@ -102,6 +102,7 @@ Writing and notation conventions:
 
 - Write `non-empty`, `non-unital`, `non-expansive` (with a hyphen).
 - Use `\varnothing` (not `\emptyset`), `f : X \to Y` (not `\colon`), and `\coloneqq` (not `:=`).
+- Write concrete sets as `\varnothing`, `\{\ast\}`, `\{0,1\}` (or `\{a,b\}`), never as `0`, `1`, `2`. This also applies to the initial and terminal objects of a specific category (e.g. `x : \{\ast\} \to X` in `\Set`, the trivial category `\1`, or "the terminal object $T$" of a presheaf category). Only abstract initial and terminal objects in statements about arbitrary categories, monoidal units, and the zero and trivial objects of algebra (the zero module $0$, the trivial group $1$) may be called `0` and `1`.
 - Write parallel morphisms as `f,g : A \rightrightarrows B`.
 - Never use one-off font commands such as `\mathcal`, `\mathrm`, `\mathbf`, or `\operatorname` directly. Reuse a macro from [database/data/macros.yaml](database/data/macros.yaml) (e.g. `\IN`, `\Grp`, `\Ab`, `\C`, `\Q`, `\T`) or define a new one there.
 - In displayed formulas containing `\prod` or `\coprod`, add `\textstyle` for the more compact layout, e.g. `$$\textstyle h : A \to \prod_{i \in I} Q_i$$`.

CONTRIBUTING.md

@@ -179,9 +179,10 @@ As a practical guideline, avoid introducing more than four properties (or four c
 
 1. Write `non-empty`, not `nonempty`. Same for `non-unital`, `non-expansive`, etc.
 2. Use `\varnothing` to display the empty set, not `\emptyset`.
-3. For declarations of functions or morphisms, use `f : X \to Y`, not `f \colon X \to Y`.
-4. For definitions, use `\coloneqq` instead of `:=`.
-5. For LaTeX symbols that are used repeatedly, in particular category-theoretic notation, define a LaTeX macro in [macros.yaml](database/data/macros.yaml).
+3. Write concrete sets explicitly, not as `0`, `1`, `2`: the empty set as `\varnothing`, a singleton as `\{\ast\}`, a two-element set as `\{0,1\}` or `\{a,b\}`, also when they are initial or terminal objects (e.g. `x : \{\ast\} \to X` in `\Set`).
+4. For declarations of functions or morphisms, use `f : X \to Y`, not `f \colon X \to Y`.
+5. For definitions, use `\coloneqq` instead of `:=`.
+6. For LaTeX symbols that are used repeatedly, in particular category-theoretic notation, define a LaTeX macro in [macros.yaml](database/data/macros.yaml).
 
 ### Citations
 

content/congruences_in_rel.md

@@ -12,7 +12,7 @@ $$R_* : P(X) \to P(Y),\, S \mapsto \bigl\{ y\in Y \mid \exists x\in S, (x, y) \i
 is injective, and it is an isomorphism if and only if $R$ is the graph of a bijection $X \to Y$ in $\Set$.
 In particular, we get
 $$i_* : P(E) \to P(X + X) \cong P(X) \times P(X)$$
-which must be injective. It must also preserve arbitrary unions and in particular be inclusion-preserving. From the assumption that $q_1, q_2$ is a congruence, since the functor $(P, {-}_*) : \Rel \to \Set$ is representable by the object 1, we see that $i_*$ must have image given by an equivalence relation $\sim$ on $P(X)$. Note also that since $i_*$ preserves arbitrary unions, we must have that $\sim$ respects arbitrary unions.
+which must be injective. It must also preserve arbitrary unions and in particular be inclusion-preserving. From the assumption that $q_1, q_2$ is a congruence, since the functor $(P, {-}_*) : \Rel \to \Set$ is representable by the object $\{\ast\}$, we see that $i_*$ must have image given by an equivalence relation $\sim$ on $P(X)$. Note also that since $i_*$ preserves arbitrary unions, we must have that $\sim$ respects arbitrary unions.
 
 Since the symmetry morphism $s : E \to E$ satisfies $s^2 = \id$, it must be the graph of an involution $s_0$ on $E$, where $s_0$ is a morphism in $\Set$.
 

content/functors_on_discrete_categories.md

@@ -7,14 +7,14 @@ description: We describe which functors on discrete categories are continuous or
 
 Let $\S$ be a discrete category. Thus, a functor $F : \S \to \C$ is the same as a family of objects $F(s) \in \C$ indexed by the objects $s \in \S$. Here, we want to determine under which conditions $F$ is continuous (or cocontinuous). The case $\S = \varnothing$ is rather boring, which is why we assume from now on that $\S \neq \varnothing$, i.e. that $\S$ is inhabited.
 
-First, we consider the trivial case $\S = 1$.
+First, we consider the trivial case $\S = \1$.
 
 ::: Lemma 1
-Consider the trivial category $1 = \{0\}$ with a unique object $0$. Let $F : 1 \to \C$ be a functor corresponding to an object $F(0) \in \C$. Then $F$ is continuous if and only if $F(0)$ is a terminal object in $\C$.
+Consider the trivial category $\1$ with a unique object $0$. Let $F : \1 \to \C$ be a functor corresponding to an object $F(0) \in \C$. Then $F$ is continuous if and only if $F(0)$ is a terminal object in $\C$.
 :::
 
 ::: Proof
-If $F$ is continuous, it preserves terminal objects. Since $0 \in 1$ is terminal, it follows that $F(0) \in \C$ is terminal. Conversely, suppose that $F(0) \in \C$ is terminal. Then $F$ is continuous: for every index category $\I$, there is a unique diagram $D : \I \to 1$, namely $D(i) = 0$ and $D(i \to j) = \id_0$. Its limit is $0$, with the universal cone $(\id_0 : 0 \to D(i))_{i \in \I}$. We need to show that $(\id_{F(0)} : F(0) \to F(0))_{i \in \I}$ is a universal cone in $\C$. This is easy to see using that $F(0)$ is terminal.
+If $F$ is continuous, it preserves terminal objects. Since $0 \in \1$ is terminal, it follows that $F(0) \in \C$ is terminal. Conversely, suppose that $F(0) \in \C$ is terminal. Then $F$ is continuous: for every index category $\I$, there is a unique diagram $D : \I \to \1$, namely $D(i) = 0$ and $D(i \to j) = \id_0$. Its limit is $0$, with the universal cone $(\id_0 : 0 \to D(i))_{i \in \I}$. We need to show that $(\id_{F(0)} : F(0) \to F(0))_{i \in \I}$ is a universal cone in $\C$. This is easy to see using that $F(0)$ is terminal.
 :::
 
 ::: Lemma 2

content/thin_algebraic_categories.md

@@ -12,11 +12,11 @@ Evaluate later if we want to remove it.
 -->
 
 ::: Lemma
-Let $\C$ be a [thin](/category-property/thin) and [one-sorted finitary algebraic](/category-property/one-sorted_finitary_algebraic) category. Then $\C \simeq 1$ or $\C \simeq I$, where $I$ is the walking morphism.
+Let $\C$ be a [thin](/category-property/thin) and [one-sorted finitary algebraic](/category-property/one-sorted_finitary_algebraic) category. Then $\C \simeq \1$ or $\C \simeq I$, where $I$ is the walking morphism.
 :::
 
 ::: Proof
-Let $F : \Set \to \C$ denote the free algebra functor. Every object $A \in \C$ admits a regular epimorphism $F(X) \twoheadrightarrow A$ for some set $X$. But since $\C$ is thin, every regular epimorphism must be an isomorphism. Thus, $A \cong F(X)$. Also, $F(X)$ is a coproduct of copies of $F(1)$, which means it is either the initial object $0$ or $F(1)$ itself (since $\C$ is thin). If $F(1) \cong 0$, then every object is isomorphic to the initial object $0$, and hence $\C$ is trivial. If not, then $\C$ has exactly two objects up to isomorphism, $0$ and $F(1)$; there is a morphism $0 \to F(1)$ but no morphism $F(1) \to 0$. Since $\C$ is thin, we conclude $\C \simeq I$.
+Let $F : \Set \to \C$ denote the free algebra functor. Every object $A \in \C$ admits a regular epimorphism $F(X) \twoheadrightarrow A$ for some set $X$. But since $\C$ is thin, every regular epimorphism must be an isomorphism. Thus, $A \cong F(X)$. Also, $F(X)$ is a coproduct of copies of $F(\{\ast\})$, which means it is either the initial object $0$ or $F(\{\ast\})$ itself (since $\C$ is thin). If $F(\{\ast\}) \cong 0$, then every object is isomorphic to the initial object $0$, and hence $\C$ is trivial. If not, then $\C$ has exactly two objects up to isomorphism, $0$ and $F(\{\ast\})$; there is a morphism $0 \to F(\{\ast\})$ but no morphism $F(\{\ast\}) \to 0$. Since $\C$ is thin, we conclude $\C \simeq I$.
 :::
 
 Remark: Another proof is possible by using the Lemma [here](/content/thin_extremal_generator).

database/data/categories/Cat.yaml

@@ -91,9 +91,9 @@ unsatisfied_properties:
   - property: cototal
     # TODO: refactor this once we add "hypercocomplete"
     proof: >-
-      In fact, it is not hypercocomplete. 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.
+      In fact, it is not hypercocomplete. 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$, showing that it is not hypercocomplete. 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$.
+      On the other hand, we claim that $\1 \dottedrightrightarrows B G_\kappa$ does not have a pushout in $\Cat$, showing that it is not hypercocomplete. 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
 
 special_objects:
@@ -112,7 +112,7 @@ special_morphisms:
     proof: This is easy.
   monomorphisms:
     description: faithful functors that are injective on objects
-    proof: 'Faithful functors that are injective on objects are clearly monomorphisms. For the converse, assume that $F : \C \to \D$ is a monomorphic functor. Two objects $A,B \in \C$ with $F(A) = F(B)$ can be regarded as functors $A,B : 1 \rightrightarrows \C$ from the trivial category satisfying $F \circ A = F \circ B$, so that $A = B$. Now assume that $f,g : A \rightrightarrows B$ are morphisms in $\C$ with $F(f) = F(g)$. These can be regarded as functors $f,g : \{ 0 \to 1 \} \rightrightarrows \C$ from the walking morphism category satisfying $F \circ f = F \circ g$, so that $f = g$.'
+    proof: 'Faithful functors that are injective on objects are clearly monomorphisms. For the converse, assume that $F : \C \to \D$ is a monomorphic functor. Two objects $A,B \in \C$ with $F(A) = F(B)$ can be regarded as functors $A,B : \1 \rightrightarrows \C$ from the trivial category satisfying $F \circ A = F \circ B$, so that $A = B$. Now assume that $f,g : A \rightrightarrows B$ are morphisms in $\C$ with $F(f) = F(g)$. These can be regarded as functors $f,g : \{ 0 \to 1 \} \rightrightarrows \C$ from the walking morphism category satisfying $F \circ f = F \circ g$, so that $f = g$.'
   epimorphisms:
     description: 'A functor $F : \C \to \D$ is an epimorphism iff $F$ is surjective on objects and for every morphism $s$ in $\D$ there is a zigzag over $U \coloneqq F(\C)$, meaning morphisms $u_1,\dotsc,u_{m+1} \in U$, $v_1,\dotsc,v_m \in U$, $x_1,\dotsc,x_m \in \D$ and $y_1,\dotsc,y_m \in \D$ such that $s = x_1 u_1$, $u_1 = v_1 y_1$, $x_{i-1} v_{i-1} = x_i u_i$, $u_i y_{i-1} = v_i y_i$, $x_m v_m = u_{m+1}$ and $u_{m+1} y_m = s$.'
     proof: This is an extension of the <a href="https://en.wikipedia.org/wiki/Isbell's_zigzag_theorem">corresponding theorem for monoids</a> and proven by <a href="https://www.jstor.org/stable/2373286">Isbell</a>.

database/data/categories/CompHaus.yaml

@@ -76,7 +76,7 @@ unsatisfied_properties:
 
   - property: parametrized natural numbers object
     proof: >-
-      Let $I \coloneqq [0, 1]$. If a parametrized natural numbers object $(N, z : 1 \to N, s : N \to N)$ existed, then we could iterate the initial conditions $I\to I\times I$, $x \mapsto (x, x)$ and the recursive step function $I\times I \to I \times I$, $(x, y) \mapsto (x, xy)$ to get a continuous function $N \times I \to I \times I$ such that $(s^n(z), x) \mapsto (x, x^n)$ for $x\in I$, $n \in \IN$. The sequence $(s^n(z)) \in N$ has a convergent subnet $(s^{n_\lambda}(z))_{\lambda \in \Lambda}$, say with limit $y$. Thus, for any $x\in I$ and $\lambda \in \Lambda$, we have $(s^{n_\lambda}(z), x) \mapsto (x, x^{n_\lambda})$. Taking limits, we see $(y, x) \mapsto (x, 0)$ if $x \ne 1$ or $(y, x) \mapsto (x, 1)$ if $x = 1$. In other words, $(y, x) \mapsto (x, \delta_{x, 1})$ for all $x\in I$. However, that contradicts the fact that the composition
+      Let $I \coloneqq [0, 1]$. If a parametrized natural numbers object $(N, z : \{\ast\} \to N, s : N \to N)$ existed, then we could iterate the initial conditions $I\to I\times I$, $x \mapsto (x, x)$ and the recursive step function $I\times I \to I \times I$, $(x, y) \mapsto (x, xy)$ to get a continuous function $N \times I \to I \times I$ such that $(s^n(z), x) \mapsto (x, x^n)$ for $x\in I$, $n \in \IN$. The sequence $(s^n(z)) \in N$ has a convergent subnet $(s^{n_\lambda}(z))_{\lambda \in \Lambda}$, say with limit $y$. Thus, for any $x\in I$ and $\lambda \in \Lambda$, we have $(s^{n_\lambda}(z), x) \mapsto (x, x^{n_\lambda})$. Taking limits, we see $(y, x) \mapsto (x, 0)$ if $x \ne 1$ or $(y, x) \mapsto (x, 1)$ if $x = 1$. In other words, $(y, x) \mapsto (x, \delta_{x, 1})$ for all $x\in I$. However, that contradicts the fact that the composition
       $$\begin{align*}
       I & \overset{y \times \id}\longrightarrow N\times I \to I\times I \overset{p_2}\longrightarrow I, \\
       x & \mapsto (y, x) \mapsto (x, \delta_{x,1}) \mapsto \delta_{x,1},

database/data/categories/Euclid_coprod.yaml

@@ -21,7 +21,7 @@ satisfied_properties:
     proof: It is a full subcategory of <a href="/category/Top">$\Top$</a>, which is locally small.
 
   - property: finite products
-    proof: This follows since $\Top$ is infinitary distributive and Euclidean spaces are closed under finite products. Namely, $\IR^0=1$ and $\IR^n \times \IR^m \cong \IR^{n+m}$.
+    proof: This follows since $\Top$ is infinitary distributive and Euclidean spaces are closed under finite products. Namely, $\IR^0 = \{0\}$ and $\IR^n \times \IR^m \cong \IR^{n+m}$.
 
   - property: infinitary extensive
     proof: The <a href="https://ncatlab.org/nlab/show/free+coproduct+completion">free coproduct completion</a> of any category is infinitary extensive; for the finite case see <a href="https://doi.org/10.1016/0022-4049(93)90035-R">Carboni–Lack–Walters</a>, Proposition 2.4.

database/data/categories/FI.yaml

@@ -65,12 +65,12 @@ unsatisfied_properties:
     proof: This is trivial.
 
   - property: cogenerator
-    proof: Let $Q$ be a finite set. When $Q$ is empty, it is clearly no cogenerator. Otherwise, $Q + 1$ has at least two elements, so that there are two different morphisms $1 \rightrightarrows Q + 1$. But there is no morphism $Q + 1 \to Q$ at all. Hence, $Q$ is no cogenerator.
+    proof: Let $Q$ be a finite set. When $Q$ is empty, it is clearly no cogenerator. Otherwise, $Q \sqcup \{\ast\}$ has at least two elements, so that there are two different morphisms $\{\ast\} \rightrightarrows Q \sqcup \{\ast\}$. But there is no morphism $Q \sqcup \{\ast\} \to Q$ at all. Hence, $Q$ is no cogenerator.
 
   - property: binary powers
     proof: >-
-      Assume that two finite sets $X,Y$ have a product $P$ in this category. Elements of $P$ are the same as maps $1 \to P$, and they are automatically injective. Therefore,
-      $$P \cong \Hom(1,P) \cong \Hom(1,X) \times \Hom(1,Y) \cong X \times Y,$$
+      Assume that two finite sets $X,Y$ have a product $P$ in this category. Elements of $P$ are the same as maps $\{\ast\} \to P$, and they are automatically injective. Therefore,
+      $$P \cong \Hom(\{\ast\},P) \cong \Hom(\{\ast\},X) \times \Hom(\{\ast\},Y) \cong X \times Y,$$
       and the projections must agree as well. But they are usually not injective. In particular, the product $X \times X$ never exists when $X$ has $>1$ elements.
 
   - property: sequential colimits

database/data/categories/FS.yaml

@@ -73,7 +73,7 @@ unsatisfied_properties:
     proof: Its core is <a href="/category/B">$\IB$</a>, which we know is not thin.
 
   - property: generator
-    proof: Let $G$ be a finite set. There are at least two morphisms $G + 2 \rightrightarrows 2$, but there is no morphism $G \to G + 2$ at all. Hence, $G$ is not a generator.
+    proof: Let $G$ be a finite set. There are at least two morphisms $G \sqcup \{0,1\} \rightrightarrows \{0,1\}$, but there is no morphism $G \to G \sqcup \{0,1\}$ at all. Hence, $G$ is not a generator.
 
   - property: connected
     proof: 'If $f : \varnothing \to X$ is surjective, then $X = \varnothing$, and if $f : X \to \varnothing$ is any map, then also $X = \varnothing$. This shows that $\{ \varnothing \}$ is a connected component in this category. (The other connected component consists of all non-empty finite sets.)'
@@ -82,7 +82,7 @@ unsatisfied_properties:
     proof: 'Let $X_n \coloneqq \{1,\dotsc,n\}$. We define the truncation $p_n : X_{n+1} \to X_n$ by extending the identity of $X_n$ with $p_n(n+1) \coloneqq n$. Assume the sequence of truncations $\cdots \to X_2 \to X_1$ has a limit $(f_n : X \to X_n)$ in this category. But $f_n$ is surjective, so that $\card(X) \geq n$ for all $n$. Since $X$ is finite, this is a contradiction.'
 
   - property: binary copowers
-    proof: Assume that the copower $X \coloneqq 2+2$ exists. Since we have a surjective map $2 \to X$, the set $X$ has at most $2$ elements. The codiagonal $X \to 2$ shows that $X$ has at least $2$ elements. Thus, $X \cong 2$. For all finite sets $Y$ we get a bijection $\Hom(2,Y) \cong \Hom(2,Y)^2$, in particular the cardinalities are the same. For $Y=2$ this gives the contradiction $2 = 4$.
+    proof: Let $T \coloneqq \{0,1\}$ and assume that the copower $X \coloneqq T + T$ exists. Since we have a surjective map $T \to X$, the set $X$ has at most $2$ elements. The codiagonal $X \to T$ shows that $X$ has at least $2$ elements. Thus, $X \cong T$. For all finite sets $Y$ we get a bijection $\Hom(T,Y) \cong \Hom(T,Y)^2$, in particular the cardinalities are the same. For $Y = T$ this gives the contradiction $2 = 4$.
 
   - property: locally cocartesian coclosed
     proof: >-

database/data/categories/FinSet.yaml

@@ -60,7 +60,7 @@ unsatisfied_properties:
     proof: This is trivial.
 
   - property: natural numbers object
-    proof: By Lemma 2 <a href="/content/natural_numbers_objects">here</a>, if $(N,z,s)$ is a natural numbers object, then $N \cong 1 \sqcup N$. But there is no finite set with this property.
+    proof: By Lemma 2 <a href="/content/natural_numbers_objects">here</a>, if $(N,z,s)$ is a natural numbers object, then $N \cong \{\ast\} \sqcup N$. But there is no finite set with this property.
     label: FinSet_no_NNO
 
 special_objects: