diff --git a/CLAUDE.md b/CLAUDE.md
index 555f15bd6..b2f5227f6 100644
--- a/CLAUDE.md
+++ b/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$$`.
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index ee2098002..ba701d399 100644
--- a/CONTRIBUTING.md
+++ b/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
diff --git a/content/congruences_in_rel.md b/content/congruences_in_rel.md
index 5bd5807b9..b79b259e7 100644
--- a/content/congruences_in_rel.md
+++ b/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$.
diff --git a/content/functors_on_discrete_categories.md b/content/functors_on_discrete_categories.md
index 55da32655..74c230b31 100644
--- a/content/functors_on_discrete_categories.md
+++ b/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
diff --git a/content/thin_algebraic_categories.md b/content/thin_algebraic_categories.md
index c83b4569f..19f357101 100644
--- a/content/thin_algebraic_categories.md
+++ b/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).
diff --git a/database/data/categories/Cat.yaml b/database/data/categories/Cat.yaml
index 861621557..40fd17bc3 100644
--- a/database/data/categories/Cat.yaml
+++ b/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 corresponding theorem for monoids and proven by Isbell.
diff --git a/database/data/categories/CompHaus.yaml b/database/data/categories/CompHaus.yaml
index f75a6ddf4..709bc7481 100644
--- a/database/data/categories/CompHaus.yaml
+++ b/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},
diff --git a/database/data/categories/Euclid_coprod.yaml b/database/data/categories/Euclid_coprod.yaml
index b3bcd1526..77f4eb6cb 100644
--- a/database/data/categories/Euclid_coprod.yaml
+++ b/database/data/categories/Euclid_coprod.yaml
@@ -21,7 +21,7 @@ satisfied_properties:
proof: It is a full subcategory of $\Top$, 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 free coproduct completion of any category is infinitary extensive; for the finite case see Carboni–Lack–Walters, Proposition 2.4.
diff --git a/database/data/categories/FI.yaml b/database/data/categories/FI.yaml
index 08a45e382..6d5f5ad0c 100644
--- a/database/data/categories/FI.yaml
+++ b/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
diff --git a/database/data/categories/FS.yaml b/database/data/categories/FS.yaml
index 479c8627a..7c7709532 100644
--- a/database/data/categories/FS.yaml
+++ b/database/data/categories/FS.yaml
@@ -73,7 +73,7 @@ unsatisfied_properties:
proof: Its core is $\IB$, 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: >-
diff --git a/database/data/categories/FinSet.yaml b/database/data/categories/FinSet.yaml
index 34320ae42..3035325aa 100644
--- a/database/data/categories/FinSet.yaml
+++ b/database/data/categories/FinSet.yaml
@@ -60,7 +60,7 @@ unsatisfied_properties:
proof: This is trivial.
- property: natural numbers object
- proof: By Lemma 2 here, 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 here, 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:
diff --git a/database/data/categories/FinSet_odd.yaml b/database/data/categories/FinSet_odd.yaml
index a78849b86..2d3b57f51 100644
--- a/database/data/categories/FinSet_odd.yaml
+++ b/database/data/categories/FinSet_odd.yaml
@@ -80,13 +80,13 @@ unsatisfied_properties:
proof: 'The map $e : \{0,1,2\} \to \{0,1,2\}$, $0 \mapsto 0$, $1 \mapsto 1$, $2 \mapsto 1$ is idempotent and does not split in $\FinSet_{\odd}$, since a splitting $\{0,1,2\} \to X \to \{0,1,2\}$ would also be a splitting in $\FinSet$, making $X$ isomorphic to $\im(e) = \{0,1\}$.'
- property: cofiltered
- proof: 'The maps $0,1 : \{\ast\} \rightrightarrows \{0,1,2\}$ are not equalized by any morphism, since this would amount to a set $X$ in $\FinSet_{\odd}$ such that $! : X \to \{*\}$ factors through $\varnothing$, i.e. $X = \varnothing$, which is not a valid object of $\FinSet_{\odd}$.'
+ proof: 'The maps $0,1 : \{\ast\} \rightrightarrows \{0,1,2\}$ are not equalized by any morphism, since this would amount to a set $X$ in $\FinSet_{\odd}$ such that $! : X \to \{\ast\}$ factors through $\varnothing$, i.e. $X = \varnothing$, which is not a valid object of $\FinSet_{\odd}$.'
- property: binary copowers
proof: A direct proof is possible, but it is best to first establish that the inclusion functor $\FinSet_{\odd} \hookrightarrow \Set$ is cocontinuous. This follows from Lemma 1 here since $\FinSet_{\odd}$ contains the extremal cogenerator $\{0,1,2\}$ of $\Set$. Therefore, binary copowers exist only if $\FinSet_{\odd}$ is closed under binary copowers in $\Set$. But $\{0\} \sqcup \{0\}$ does not have odd cardinality.
- property: natural numbers object
- proof: By Lemma 2 here, 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 here, if $(N,z,s)$ is a natural numbers object, then $N \cong \{\ast\} \sqcup N$. But there is no finite set with this property.
special_objects:
terminal object:
diff --git a/database/data/categories/FinSet_power_3.yaml b/database/data/categories/FinSet_power_3.yaml
index 343519875..d439cf76c 100644
--- a/database/data/categories/FinSet_power_3.yaml
+++ b/database/data/categories/FinSet_power_3.yaml
@@ -71,7 +71,7 @@ unsatisfied_properties:
proof: 'Consider the idempotent map $e : \{0,1,2\} \to \{0,1,2\}$ defined by $e(0)=0$, $e(1)=1$, $e(2)=1$. If it splits in $\FinSet_{3^\bullet}$ as $\{0,1,2\} \to X \to \{0,1,2\}$, this would also be a splitting in $\FinSet$, making $X$ isomorphic to $\im(e)=\{0,1\}$. But then $X$ is not a valid object of $\FinSet_{3^\bullet}$.'
- property: cofiltered
- proof: 'The maps $0,1 : \{\ast\} \rightrightarrows \{0,1,2\}$ are not equalized by any morphism, since this would amount to a set $X$ in $\FinSet_{3^\bullet}$ such that $! : X \to \{*\}$ factors through $\varnothing$, i.e. $X = \varnothing$, but $0$ is not a power of $3$.'
+ proof: 'The maps $0,1 : \{\ast\} \rightrightarrows \{0,1,2\}$ are not equalized by any morphism, since this would amount to a set $X$ in $\FinSet_{3^\bullet}$ such that $! : X \to \{\ast\}$ factors through $\varnothing$, i.e. $X = \varnothing$, but $0$ is not a power of $3$.'
- property: binary copowers
proof: >-
@@ -96,7 +96,7 @@ unsatisfied_properties:
- FinSet_power_3_inclusion_cocontinuous
- property: natural numbers object
- proof: By Lemma 2 here, 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 here, if $(N,z,s)$ is a natural numbers object, then $N \cong \{\ast\} \sqcup N$. But there is no finite set with this property.
special_objects:
terminal object:
diff --git a/database/data/categories/Haus.yaml b/database/data/categories/Haus.yaml
index 05e6ab251..2a3ce2f4b 100644
--- a/database/data/categories/Haus.yaml
+++ b/database/data/categories/Haus.yaml
@@ -63,14 +63,14 @@ unsatisfied_properties:
proof: This is clear since $\Set$ is not Malcev and can be interpreted as the subcategory of discrete spaces (which are Hausdorff).
- property: regular subobject classifier
- proof: Assume that there is a regular subobject classifier $\Omega$. By the classification of regular monomorphisms, we would have an isomorphism between $\Hom(X,\Omega)$ and the set of closed subsets of $X$ for any Hausdorff space $X$. If we take $X = 1$ we see that $\Omega$ has two points. Since $\Omega$ is Hausdorff, $\Omega \cong 1 + 1$ must be discrete. But then $\Hom(X,\Omega)$ is isomorphic to the set of all clopen subsets of $X$, of which there are usually far fewer than closed subsets (consider $X = [0,1]$).
+ proof: Assume that there is a regular subobject classifier $\Omega$. By the classification of regular monomorphisms, we would have an isomorphism between $\Hom(X,\Omega)$ and the set of closed subsets of $X$ for any Hausdorff space $X$. If we take $X = \{\ast\}$, we see that $\Omega$ has two points. Since $\Omega$ is Hausdorff, it must be discrete. But then $\Hom(X,\Omega)$ is isomorphic to the set of all clopen subsets of $X$, of which there are usually far fewer than closed subsets (consider $X = [0,1]$).
label: Haus_no_regular_subobject_classifier
- property: cartesian filtered colimits
proof: 'It is shown in MSE/1255678 that $\IQ \times - : \Top \to \Top$ does not preserve sequential colimits (so that it cannot be a left adjoint). The same example also works in $\Haus$: Surely $\IQ$ is Hausdorff, $X_n$ is Hausdorff, as is their colimit $X$, and the colimit (taken in $\Top$) of the $X_n \times \IQ$ admits a bijective continuous map to a Hausdorff space, therefore is also Hausdorff, meaning it is also the colimit taken in $\Haus$.'
- property: cofiltered-limit-stable epimorphisms
- proof: 'The following is a basic counterexample for sets: The unique maps $\IN_{\geq n} \to 1$ are surjective, but their limit $0 = \bigcap_{n \geq 0} \IN_{\geq n} \to 1$ is not. This also works in $\Haus$ by using discrete topologies. We could also apply a variant of (the dual of) Lemma 2 here to the discrete topology functor $\Set \to \Haus$, which does not preserve all cofiltered limits, but does preserve intersections.'
+ proof: 'The following is a basic counterexample for sets: The unique maps $\IN_{\geq n} \to \{\ast\}$ are surjective, but their limit $\varnothing = \bigcap_{n \geq 0} \IN_{\geq n} \to \{\ast\}$ is not. This also works in $\Haus$ by using discrete topologies. We could also apply a variant of (the dual of) Lemma 2 here to the discrete topology functor $\Set \to \Haus$, which does not preserve all cofiltered limits, but does preserve intersections.'
- property: filtered-colimit-stable monomorphisms
proof: >-
@@ -96,9 +96,9 @@ unsatisfied_properties:
proof: >-
In fact, it is not hypercocomplete. For each cardinal $\kappa$, let $Q_\kappa$ be the product of all Hausdorff topological spaces whose underlying set is a non-empty subset of $\kappa$. By a theorem of Herrlich, there is a regular Hausdorff space $X_\kappa$ with at least two points such that every continuous map $X_\kappa \to Q_\kappa$ is constant. (Note that the result there applies for general $T_1$ spaces $Q$, not just for $Q_\kappa$ as constructed above. In the reference, the author only states that $X_\kappa$ is regular, but actually, $X_\kappa$ is regular and $T_1$, hence Hausdorff.)
- Choose a base point $x_\kappa \in X_\kappa$ for each $\kappa$. We can form a large span diagram $1 \dottedrightrightarrows X_\kappa$ where each morphism $1 \to X_\kappa$ corresponds to $x_\kappa$. Then for any Hausdorff space $Y$, the collection of cocones $1 \dottedrightrightarrows X_\kappa \to Y$ is essentially small: We must first choose $y \in Y$ corresponding to the morphism $1 \to Y$. Then for each $\kappa \ge \card(U(Y))$, $Y$ is homeomorphic to one of the spaces in the product forming $Q_\kappa$. Therefore, there is a morphism $Y \to Q_\kappa$ splitting the projection map $Q_\kappa \to Y$. It follows that the map $X_\kappa \to Y$ is constant, and in fact it must be the constant map with image $y$.
+ Choose a base point $x_\kappa \in X_\kappa$ for each $\kappa$. We can form a large span diagram $\{\ast\} \dottedrightrightarrows X_\kappa$ where each morphism $\{\ast\} \to X_\kappa$ corresponds to $x_\kappa$. Then for any Hausdorff space $Y$, the collection of cocones $\{\ast\} \dottedrightrightarrows X_\kappa \to Y$ is essentially small: We must first choose $y \in Y$ corresponding to the morphism $\{\ast\} \to Y$. Then for each $\kappa \ge \card(U(Y))$, $Y$ is homeomorphic to one of the spaces in the product forming $Q_\kappa$. Therefore, there is a morphism $Y \to Q_\kappa$ splitting the projection map $Q_\kappa \to Y$. It follows that the map $X_\kappa \to Y$ is constant, and in fact it must be the constant map with image $y$.
- On the other hand, we claim that $1 \dottedrightrightarrows X_\kappa$ does not have a pushout in $\Haus$, showing that it is not hypercocomplete. To see this, suppose we had a pushout $Y$, and let $\lambda \coloneqq \card(U(Y))$. Then the coprojection $X_\lambda \to Y$ is split monic, since we can construct a cocone $1 \dottedrightrightarrows X_\kappa \to X_\lambda$ where the map $X_\kappa \to X_\lambda$ is the constant map with image $x_\lambda$ when $\kappa \ne \lambda$, and the map $X_\lambda \to X_\lambda$ is the identity. But similarly to the previous paragraph, we can show any morphism $X_\lambda \to Y$ must be constant, giving a contradiction since $X_\lambda$ has at least two points.
+ On the other hand, we claim that $\{\ast\} \dottedrightrightarrows X_\kappa$ does not have a pushout in $\Haus$, showing that it is not hypercocomplete. To see this, suppose we had a pushout $Y$, and let $\lambda \coloneqq \card(U(Y))$. Then the coprojection $X_\lambda \to Y$ is split monic, since we can construct a cocone $\{\ast\} \dottedrightrightarrows X_\kappa \to X_\lambda$ where the map $X_\kappa \to X_\lambda$ is the constant map with image $x_\lambda$ when $\kappa \ne \lambda$, and the map $X_\lambda \to X_\lambda$ is the identity. But similarly to the previous paragraph, we can show any morphism $X_\lambda \to Y$ must be constant, giving a contradiction since $X_\lambda$ has at least two points.
- property: extremal generating collection
proof: The proof is the same as the one for $\Top$; there the test spaces we use are of the form $\kappa \sqcup \{ \kappa \}$ and $\kappa + 1$, which are both Hausdorff spaces.
diff --git a/database/data/categories/Man.yaml b/database/data/categories/Man.yaml
index 6572969fa..a722dff8f 100644
--- a/database/data/categories/Man.yaml
+++ b/database/data/categories/Man.yaml
@@ -53,7 +53,7 @@ satisfied_properties:
- property: extremal generator
proof: >-
- The $0$-dimensional one-point manifold is a generator since it represents the forgetful functor $\Man \to \Set$. Since we have an epimorphism $\IR \to 1$, we see that $\IR$ is also a generator.
+ The $0$-dimensional one-point manifold is a generator since it represents the forgetful functor $\Man \to \Set$. Since we have an epimorphism $\IR \to \{\ast\}$, we see that $\IR$ is also a generator.
We claim that in fact, $\IR$ is an extremal generator. To see this, suppose we have a smooth map $f : M \to N$ which induces a bijection of smooth curves on $M$ to smooth curves on $N$. By considering constant curves, we must have that $f$ is a bijection on the underlying sets. Now for any point $p \in M$ and any tangent vector $v \in T_{f(p)}(N)$, there exists a smooth curve $\gamma : \IR \to N$ such that $\gamma(0) = f(p)$ and $\gamma'(0) = v$. By the assumption on $f$, there exists a smooth curve $\beta : \IR \to M$ such that $\gamma = f \circ \beta$. By the injectivity of $f$, we must have $\beta(0) = p$, so $\beta'(0) \in T_p(M)$ and $f_*(\beta'(0)) = \gamma'(0) = v$. This shows that $f_* : T_p(M) \to T_{f(p)}(N)$ is surjective, hence $f$ is a submersion whose fibers are singletons. Therefore, by the submersion theorem, $f$ is a local diffeomorphism. Since $f$ is bijective, $f$ must be a diffeomorphism.
diff --git a/database/data/categories/Meas.yaml b/database/data/categories/Meas.yaml
index 040e6a84c..da5942305 100644
--- a/database/data/categories/Meas.yaml
+++ b/database/data/categories/Meas.yaml
@@ -66,11 +66,11 @@ satisfied_properties:
- property: extremal cogenerator
proof: >-
- First, take the two-element set $2$ endowed with the trivial $\sigma$-algebra (where only $\varnothing$ and $2$ are measurable), and use that $2$ is a cogenerator for $\Set$ to show that $2$ with the trivial $\sigma$-algebra is a cogenerator for $\Meas$.
+ First, take the set $\{0,1\}$ endowed with the trivial $\sigma$-algebra (where only $\varnothing$ and $\{0,1\}$ are measurable), and use that $\{0,1\}$ is a cogenerator for $\Set$ to show that $\{0,1\}$ with the trivial $\sigma$-algebra is a cogenerator for $\Meas$.
- Now, we claim that adding the two-element set $2$ endowed with the discrete $\sigma$-algebra (where every subset is measurable) gives an extremal cogenerating collection. To see this, suppose we have a morphism $f : (X, \M_X) \to (Y, \M_Y)$ such that ${-} \circ f : \Hom(Y, Q) \to \Hom(X, Q)$ is a bijection if $Q$ is either measurable space. Since $2$ with the trivial $\sigma$-algebra represents taking the power set of the underlying set, and the contravariant power set functor on $\Set$ is conservative, we conclude that $f$ is a bijection on the underlying sets. Also, since $2$ with the discrete $\sigma$-algebra represents the functor $(X, \M_X) \mapsto \M_X$, we see that $f^* : \M_Y \to \M_X$ is also a bijection. This shows that $f$ is an isomorphism of measurable spaces.
+ Now, we claim that adding the set $\{0,1\}$ endowed with the discrete $\sigma$-algebra (where every subset is measurable) gives an extremal cogenerating collection. To see this, suppose we have a morphism $f : (X, \M_X) \to (Y, \M_Y)$ such that ${-} \circ f : \Hom(Y, Q) \to \Hom(X, Q)$ is a bijection if $Q$ is either measurable space. Since $\{0,1\}$ with the trivial $\sigma$-algebra represents taking the power set of the underlying set, and the contravariant power set functor on $\Set$ is conservative, we conclude that $f$ is a bijection on the underlying sets. Also, since $\{0,1\}$ with the discrete $\sigma$-algebra represents the functor $(X, \M_X) \mapsto \M_X$, we see that $f^* : \M_Y \to \M_X$ is also a bijection. This shows that $f$ is an isomorphism of measurable spaces.
- Finally, using this result, we conclude that the product of these two measurable spaces with underlying set $2$ is an extremal cogenerator of $\Meas$.
+ Finally, using this result, we conclude that the product of these two measurable spaces with underlying set $\{0,1\}$ is an extremal cogenerator of $\Meas$.
references:
- Set_extremal_cogenerator
@@ -140,8 +140,8 @@ unsatisfied_properties:
- property: infinitary distributive
proof: >-
- Let $X$ be a set of cardinality $> 2^{\aleph_0}$. We equip $X$ with the discrete $\sigma$-algebra. If $1$ denotes the singleton space, we therefore have $X \cong \coprod_{x \in X} 1$ in $\Meas$. However, we claim that the canonical bijective measurable map
- $$\textstyle\coprod_{x,y \in X} 1 \to X \times X$$
+ Let $X$ be a set of cardinality $> 2^{\aleph_0}$. We equip $X$ with the discrete $\sigma$-algebra. Therefore, $X \cong \coprod_{x \in X} \{\ast\}$ in $\Meas$. However, we claim that the canonical bijective measurable map
+ $$\textstyle\coprod_{x,y \in X} \{\ast\} \to X \times X$$
is not an isomorphism, i.e. that $X \times X$ does not carry the discrete $\sigma$-algebra. More precisely, we will show that the diagonal $\Delta \subseteq X \times X$ is not measurable. (This is well-known and is remarked for example in Wengenroth, end of Ch. 1, but we include the proof nevertheless.)
Assume that $\Delta \subseteq X \times X$ is measurable. Then (cf. MSE/61617) there is a countable family of rectangles $(A_n \times B_n)_{n \in \IN}$ such that $\Delta \in \sigma(\{A_n \times B_n : n \in \IN\})$. Consider the product of the characteristic functions
@@ -174,7 +174,7 @@ special_morphisms:
proof: For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the terminal object), hence preserves monomorphisms.
epimorphisms:
description: surjective measurable maps
- proof: Use the same proof as for sets, where $2 = \{0,1\}$ is endowed with the trivial $\sigma$-algebra.
+ proof: Use the same proof as for sets, where $\{0,1\}$ is endowed with the trivial $\sigma$-algebra.
regular monomorphisms:
description: embeddings
proof: '(This is the same proof as for $\Top$.) Equalizers are embeddings by their construction. Conversely, if $f : X \to Y$ is an embedding, then $f$ is the equalizer of the two characteristic maps $\chi_Y, \chi_{f(X)} : Y \rightrightarrows \{0,1\}$, where $\{0,1\}$ carries the trivial $\sigma$-algebra.'
diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml
index b9b5ae06a..b9a94d682 100644
--- a/database/data/categories/Met.yaml
+++ b/database/data/categories/Met.yaml
@@ -68,7 +68,7 @@ satisfied_properties:
proof: >-
Let $G$ be the metric space with underlying set $\IR_{\ge 0}$ equipped with the metric where $d(x,y) = 0$ if $x=y$, and otherwise $d(x,y) = x+y$. We claim that $G$ is an extremal generator.
- First, to see that $G$ is a generator, note that the one-point metric space $1$ is a generator since it represents the forgetful functor $\Met \to \Set$ which is faithful. Since we have an epimorphism $! : G \twoheadrightarrow 1$, $G$ is also a generator.
+ First, to see that $G$ is a generator, note that the one-point metric space $\{\ast\}$ is a generator since it represents the forgetful functor $\Met \to \Set$ which is faithful. Since we have an epimorphism $! : G \twoheadrightarrow \{\ast\}$, $G$ is also a generator.
Now, suppose that $f : X \to Y$ is a non-expansive map of metric spaces such that $f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$ is a bijection. By considering constant maps from $G$, we see that $f$ is a bijection on underlying sets. Now suppose we have $x_1, x_2 \in X$ with $d(f(x_1), f(x_2)) = \varepsilon > 0$. Then there is a non-expansive map $\varphi : G \to Y$ which maps $\varepsilon$ to $f(x_2)$ and every other element of $\IR_{\ge 0}$ to $f(x_1)$. Therefore, there is a non-expansive map $\psi : G \to X$ such that $\varphi = f \circ \psi$. Since $f$ is injective on underlying sets, we must have $\psi(\varepsilon) = x_2$ and $\psi(0) = x_1$. Hence,
$$\begin{align*}
@@ -144,7 +144,7 @@ unsatisfied_properties:
label: Met_no_filtered_colimit_stable_monos
- property: natural numbers object
- proof: By Lemma 2 here, if $(N,z,s)$ is a natural numbers object, then $N \cong 1 \sqcup N$. Since there is a map $1 \to N$, we have $N \neq \varnothing$. However, the coproduct of two non-empty metric spaces does not exist; see MSE/1778408.
+ proof: By Lemma 2 here, if $(N,z,s)$ is a natural numbers object, then $N \cong \{\ast\} \sqcup N$. Since there is a map $\{\ast\} \to N$, we have $N \neq \varnothing$. However, the coproduct of two non-empty metric spaces does not exist; see MSE/1778408.
- property: effective congruences
proof: 'Any kernel pair of $h : X \to Z$ in $\Met$ corresponds to a closed subset of $X\times X$. However, there are plenty of non-closed congruences, such as $\Delta \cup (\IQ \times \IQ) \subseteq \IR \times \IR$ with the subspace metric.'
@@ -166,14 +166,14 @@ unsatisfied_properties:
- property: regular subobject classifier
proof: >-
- Assume that $\top : 1 \to \Omega$ is a regular subobject classifier. We can identify $\top$ with a point $\top \in \Omega$, and for every regular monomorphism $Y \hookrightarrow X$ there is a unique non-expansive map $f : X \to \Omega$ such that $f^*(\{\top\}) = Y$ as metric spaces, and hence as topological spaces.
+ Assume that $\top : \{\ast\} \to \Omega$ is a regular subobject classifier. We can identify $\top$ with a point $\top \in \Omega$, and for every regular monomorphism $Y \hookrightarrow X$ there is a unique non-expansive map $f : X \to \Omega$ such that $f^*(\{\top\}) = Y$ as metric spaces, and hence as topological spaces.
- The underlying set of $\Omega$ is identified with $\Hom(1,\Omega) \cong \Sub_{\reg}(1)$. There are two regular subobjects of $1 = \{\ast\}$, namely $\{\ast\} \subseteq \{\ast\}$ and $\varnothing \subseteq \{\ast\}$ (the latter being the equalizer of, say, two maps $\{\ast\} \rightrightarrows \{0,1\}$). Thus, $\Omega$ has exactly two points and is therefore discrete. In particular, $\top : 1 \to \Omega$ is a clopen inclusion. The universal property then implies that every regular monomorphism is a clopen inclusion. But this is not the case: for example, the inclusion $[0,\infty) \hookrightarrow \IR$ is the equalizer of $\id : \IR \to \IR$ and the absolute value function $|{-}| : \IR \to \IR$, where $\IR$ is equipped with the standard metric.
+ The underlying set of $\Omega$ is identified with $\Hom(\{\ast\},\Omega) \cong \Sub_{\reg}(\{\ast\})$. There are two regular subobjects of $\{\ast\}$, namely $\{\ast\} \subseteq \{\ast\}$ and $\varnothing \subseteq \{\ast\}$ (the latter being the equalizer of, say, two maps $\{\ast\} \rightrightarrows \{0,1\}$). Thus, $\Omega$ has exactly two points and is therefore discrete. In particular, $\top : \{\ast\} \to \Omega$ is a clopen inclusion. The universal property then implies that every regular monomorphism is a clopen inclusion. But this is not the case: for example, the inclusion $[0,\infty) \hookrightarrow \IR$ is the equalizer of $\id : \IR \to \IR$ and the absolute value function $|{-}| : \IR \to \IR$, where $\IR$ is equipped with the standard metric.
label: Met_no_regular_subobject_classifier
- property: coaccessible
proof: >-
- Assume that $\Met$ is $\kappa$-coaccessible for a regular cardinal $\kappa$. In particular, every metric space is a limit of $\kappa$-copresentable metric spaces. We claim that every $\kappa$-copresentable metric space has at most one point. Since the forgetful functor $\Met \to \Set$ is representable (by $1$), it preserves limits, so that every limit of such metric spaces also has at most one point. This is a contradiction, since there are metric spaces with two points.
+ Assume that $\Met$ is $\kappa$-coaccessible for a regular cardinal $\kappa$. In particular, every metric space is a limit of $\kappa$-copresentable metric spaces. We claim that every $\kappa$-copresentable metric space has at most one point. Since the forgetful functor $\Met \to \Set$ is representable (by $\{\ast\}$), it preserves limits, so that every limit of such metric spaces also has at most one point. This is a contradiction, since there are metric spaces with two points.
To prove the claim, let $X$ be a $\kappa$-copresentable metric space and $a,b \in X$. We will show that $a = b$. Choose a real number $\delta > 0$ with $d(a,b) \leq \delta$. Fix a set $I$ with $\card(I) \geq \kappa$, and let $P$ be the set of all subsets $S \subseteq I$ with $\card(S) < \kappa$, ordered by inclusion. Since $\kappa$ is regular, a union of fewer than $\kappa$ elements of $P$ belongs to $P$ again, so that $P$ is $\kappa$-directed. For $S \in P$ let $D(S)$ be the set $\{0,1\}^S$ equipped with the metric $d(x,y) \coloneqq \delta$ for $x \neq y$. For $S \subseteq T$ in $P$, the restriction map $D(T) \to D(S)$ is non-expansive. This defines a $\kappa$-cofiltered diagram $D : P^{\op} \to \Met$.
diff --git a/database/data/categories/Met_c.yaml b/database/data/categories/Met_c.yaml
index 9bf98d2a1..8a1360484 100644
--- a/database/data/categories/Met_c.yaml
+++ b/database/data/categories/Met_c.yaml
@@ -58,7 +58,7 @@ satisfied_properties:
proof: 'If $f : X \to Y$ is an epimorphism, then $f(X)$ is dense in $Y$ (see below). Hence, there is an injective map $Y \to X^{\IN}$, which bounds the size of $Y$.'
- property: extremal generator
- proof: 'We claim the metric space $G \coloneqq \{ 1/n : n \in \IN_{> 0} \} \cup \{ 0 \}$, with the metric inherited from $\IR$, is an extremal generator. First, the one-point metric space is a generator since it represents the forgetful functor $\Met_c \to \Set$; and since we have an epimorphism $! : G \to 1$, it follows that $G$ is a generator as well. Now, suppose we have a continuous function $f : X \to Y$ of metric spaces such that $f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$ is a bijection. Then since $G$ is a generator, we can conclude that $f$ is a monomorphism, i.e. injective on the underlying sets. Also, considering a constant function $G \to Y$ with image $y$, we see that $f$ is surjective on the underlying sets. Finally, the fact that $f$ induces a bijection between $\Hom(G, X)$ and $\Hom(G, Y)$ implies that a sequence $(x_n)_{n\in \IN}$ in $X$ has limit $L$ if and only if $(f(x_n))_{n\in \IN}$ has limit $f(L)$ in $Y$. This shows that $f$ is a homeomorphism.'
+ proof: 'We claim the metric space $G \coloneqq \{ 1/n : n \in \IN_{> 0} \} \cup \{ 0 \}$, with the metric inherited from $\IR$, is an extremal generator. First, the one-point metric space is a generator since it represents the forgetful functor $\Met_c \to \Set$; and since we have an epimorphism $! : G \to \{\ast\}$, it follows that $G$ is a generator as well. Now, suppose we have a continuous function $f : X \to Y$ of metric spaces such that $f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$ is a bijection. Then since $G$ is a generator, we can conclude that $f$ is a monomorphism, i.e. injective on the underlying sets. Also, considering a constant function $G \to Y$ with image $y$, we see that $f$ is surjective on the underlying sets. Finally, the fact that $f$ induces a bijection between $\Hom(G, X)$ and $\Hom(G, Y)$ implies that a sequence $(x_n)_{n\in \IN}$ in $X$ has limit $L$ if and only if $(f(x_n))_{n\in \IN}$ has limit $f(L)$ in $Y$. This shows that $f$ is a homeomorphism.'
- property: extremal cogenerator
proof: >-
@@ -95,7 +95,7 @@ unsatisfied_properties:
proof: 'Consider the metric subspace $\{(a,b) \in \IR^2 : a \leq b\}$ of $\IR^2$.'
- property: regular subobject classifier
- proof: 'We recycle the proof from $\Haus$: Assume that there is a regular subobject classifier $\Omega$. By the classification of regular monomorphisms, we would have an isomorphism between $\Hom(X,\Omega)$ and the set of closed subsets of $X$ for any metric space $X$. If we take $X = 1$ we see that $\Omega$ has two points. Since $\Omega$ is Hausdorff, $\Omega \cong 1 + 1$ must be discrete. But then $\Hom(X,\Omega)$ is isomorphic to the set of all clopen subsets of $X$, of which there are usually far fewer than closed subsets (consider $X = [0,1]$).'
+ proof: 'We recycle the proof from $\Haus$: Assume that there is a regular subobject classifier $\Omega$. By the classification of regular monomorphisms, we would have an isomorphism between $\Hom(X,\Omega)$ and the set of closed subsets of $X$ for any metric space $X$. If we take $X = \{\ast\}$, we see that $\Omega$ has two points. Since $\Omega$ is Hausdorff, it must be discrete. But then $\Hom(X,\Omega)$ is isomorphic to the set of all clopen subsets of $X$, of which there are usually far fewer than closed subsets (consider $X = [0,1]$).'
references:
- Haus_no_regular_subobject_classifier
diff --git a/database/data/categories/PMet.yaml b/database/data/categories/PMet.yaml
index 78b4e8419..445958612 100644
--- a/database/data/categories/PMet.yaml
+++ b/database/data/categories/PMet.yaml
@@ -68,7 +68,7 @@ satisfied_properties:
proof: >-
The proof will be similar to the one for $\Met$. Namely, let $G$ be the set $\IR_{\ge 0} \sqcup \{ 0' \}$, equipped with the metric where $d(x,y) = 0$ if $x=y$ and otherwise $d(x,y) = x+y$ for $x, y \in \IR_{\ge 0}$, and $d(x, 0') = d(0', x) = x$ for $x \in \IR_{\ge 0}$. We will show $G$ is an extremal generator for $\PMet$.
- First, to see $G$ is a generator, note that the one-point metric space is a generator since it represents the forgetful functor $\PMet\to \Set$ which is faithful. Since we have an epimorphism $! : G \twoheadrightarrow 1$, $G$ is also a generator.
+ First, to see $G$ is a generator, note that the one-point metric space is a generator since it represents the forgetful functor $\PMet\to \Set$ which is faithful. Since we have an epimorphism $! : G \twoheadrightarrow \{\ast\}$, $G$ is also a generator.
Now, suppose that $f : X \to Y$ is a non-expansive map of pseudo-metric spaces such that $f \circ {-} : \Hom(G, X) \to \Hom(G, Y)$ is a bijection. By considering constant maps from $G$, we see that $f$ is a bijection on underlying sets. Now suppose we have $x_1, x_2 \in X$ with $d(f(x_1), f(x_2)) = \varepsilon \ge 0$. Then there is a non-expansive map $\varphi : G \to Y$ which maps $\varepsilon$ to $f(x_2)$ and every other element of $G$ to $f(x_1)$. Therefore, there is a non-expansive map $\psi : G \to X$ such that $\varphi = f \circ \psi$. Since $f$ is injective on underlying sets, we must have $\psi(\varepsilon) = x_2$ and $\psi(0') = x_1$. Hence,
$$\begin{align*}
@@ -114,10 +114,10 @@ unsatisfied_properties:
proof: The coproduct of two non-empty pseudo-metric spaces does not exist; see MSE/1778408 (the proof also works for pseudo-metric spaces). For example, the copower $\IR \sqcup \IR$ does not exist. We only get coproducts when allowing $\infty$ as a distance.
- property: natural numbers object
- proof: By Lemma 2 here, if $(N,z,s)$ is a natural numbers object, then $N \cong 1 \sqcup N$. Since there is a map $1 \to N$, we have $N \neq \varnothing$. However, the coproduct of two non-empty pseudo-metric spaces does not exist; see MSE/1778408.
+ proof: By Lemma 2 here, if $(N,z,s)$ is a natural numbers object, then $N \cong \{\ast\} \sqcup N$. Since there is a map $\{\ast\} \to N$, we have $N \neq \varnothing$. However, the coproduct of two non-empty pseudo-metric spaces does not exist; see MSE/1778408.
- property: effective cocongruences
- proof: 'The proof is similar to the one for $\Top$: Equip a two-point set with the zero metric; this pseudo-metric space represents the functor taking a pseudo-metric space to the pairs of points with $d(x,y) = 0$. In this case, once you conclude $Z = \varnothing$, the map $h : Z \to 1$ does not have any cokernel pair, since that would have to be a coproduct $1+1$, which does not exist.'
+ proof: 'The proof is similar to the one for $\Top$: Equip a two-point set with the zero metric; this pseudo-metric space represents the functor taking a pseudo-metric space to the pairs of points with $d(x,y) = 0$. In this case, once you conclude $Z = \varnothing$, the map $h : Z \to \{\ast\}$ does not have any cokernel pair, since that would have to be a coproduct $\{\ast\} \sqcup \{\ast\}$, which does not exist.'
references:
- Top_no_effective_cocongruences
diff --git a/database/data/categories/Pos.yaml b/database/data/categories/Pos.yaml
index bfa9cf633..b5392c348 100644
--- a/database/data/categories/Pos.yaml
+++ b/database/data/categories/Pos.yaml
@@ -69,7 +69,7 @@ unsatisfied_properties:
proof: Assume that there is a regular subobject classifier $\Omega$, so that (by the classification of regular monomorphisms) $\Hom(P,\Omega)$ is isomorphic to the set of subsets of $P$. By taking $P = \{0\}$ we see that $\Omega$ has $2$ elements, so that either $\Omega \cong \{0,1\}$ (discrete) or $\Omega \cong \{0 < 1\}$. By taking $P = \{0 < 1\}$ we see that $\Omega$ has four pairs $(x,y)$ with $x \leq y$. But $\{0,1\}$ has only two and $\{0 < 1\}$ has only three such pairs.
- property: cofiltered-limit-stable epimorphisms
- proof: Pick any poset $X$ which has a decreasing sequence of non-empty sets $X = X_0 \supseteq X_1 \supseteq \cdots$ with empty intersection, such as $X_n = \IN_{\geq n}$ with the natural ordering. The unique maps $X_n \to 1$ are surjective, but their limit $\varnothing \to 1$ is not surjective.
+ proof: Pick any poset $X$ which has a decreasing sequence of non-empty sets $X = X_0 \supseteq X_1 \supseteq \cdots$ with empty intersection, such as $X_n = \IN_{\geq n}$ with the natural ordering. The unique maps $X_n \to \{\ast\}$ are surjective, but their limit $\varnothing \to \{\ast\}$ is not surjective.
- property: effective cocongruences
proof: >-
diff --git a/database/data/categories/PreOrd.yaml b/database/data/categories/PreOrd.yaml
index af746df49..aeaced1e7 100644
--- a/database/data/categories/PreOrd.yaml
+++ b/database/data/categories/PreOrd.yaml
@@ -45,7 +45,7 @@ satisfied_properties:
proof: The set $\{0,1\}$ with the chaotic preorder $(0 \leq 1$, $1 \leq 0)$ is a regular subobject classifier since order-preserving maps $P \to \{0,1\}$ correspond to subsets of $P$.
- property: extremal generator
- proof: 'We claim that $\{ 0 < 1 \}$ is an extremal generator. First, the singleton preordered set $1$ is a generator, since it represents the forgetful functor $\PreOrd \to \Set$ which is faithful. Since we have an epimorphism $\{ 0 < 1 \} \to 1$, it follows that $\{ 0 < 1 \}$ is also a generator. Now, suppose we have a morphism $f : P \to Q$ such that $f \circ {-} : \Hom(\{0<1\}, P) \to \Hom(\{0<1\}, Q)$ is a bijection. Then considering constant functions, we can see that $f$ must be a bijection on the underlying sets. Now, suppose we have $p_1, p_2 \in P$ such that $f(p_1) \le f(p_2)$. Then that induces a morphism $\{0<1\} \to Q$ with $0 \mapsto f(p_1), 1 \mapsto f(p_2)$. The corresponding morphism $\{0<1\}\to P$ must send $0\mapsto p_1, 1 \mapsto p_2$, showing that $p_1 \le p_2$. It follows that $f$ is an isomorphism.'
+ proof: 'We claim that $\{ 0 < 1 \}$ is an extremal generator. First, the singleton preordered set $\{\ast\}$ is a generator, since it represents the forgetful functor $\PreOrd \to \Set$ which is faithful. Since we have an epimorphism $\{ 0 < 1 \} \to \{\ast\}$, it follows that $\{ 0 < 1 \}$ is also a generator. Now, suppose we have a morphism $f : P \to Q$ such that $f \circ {-} : \Hom(\{0<1\}, P) \to \Hom(\{0<1\}, Q)$ is a bijection. Then considering constant functions, we can see that $f$ must be a bijection on the underlying sets. Now, suppose we have $p_1, p_2 \in P$ such that $f(p_1) \le f(p_2)$. Then that induces a morphism $\{0<1\} \to Q$ with $0 \mapsto f(p_1), 1 \mapsto f(p_2)$. The corresponding morphism $\{0<1\}\to P$ must send $0\mapsto p_1, 1 \mapsto p_2$, showing that $p_1 \le p_2$. It follows that $f$ is an isomorphism.'
label: PreOrd_extremal_generator
- property: extremal cogenerator
@@ -67,7 +67,7 @@ unsatisfied_properties:
proof: We know that $\Set$ does not have this property. Now use the contrapositive of the dual of Lemma 2 here applied to the functor $\Set \to \PreOrd$ that equips a set with the chaotic preorder.
- property: effective cocongruences
- proof: 'Consider the preordered set $C \coloneqq \{ a, b \}$ with the chaotic preorder. This represents the functor which sends a preordered set to the pairs of elements $x,y$ with $x \le y$ and $y \le x$. Therefore, it defines a cocongruence $1 \rightrightarrows C$, where the maps are the two possible functions. However, this cannot be effective: for any map $h : Z \to 1$ which equalizes the two functions, $Z$ must be empty. But that means the cokernel pair of $h$ is the two-element preordered set with the trivial preorder.'
+ proof: 'Consider the preordered set $C \coloneqq \{ a, b \}$ with the chaotic preorder. This represents the functor which sends a preordered set to the pairs of elements $x,y$ with $x \le y$ and $y \le x$. Therefore, it defines a cocongruence $\{\ast\} \rightrightarrows C$, where the maps are the two possible functions. However, this cannot be effective: for any map $h : Z \to \{\ast\}$ which equalizes the two functions, $Z$ must be empty. But that means the cokernel pair of $h$ is the two-element preordered set with the trivial preorder.'
special_objects:
initial object:
diff --git a/database/data/categories/Quiv_fc.yaml b/database/data/categories/Quiv_fc.yaml
index 97ee12a17..2d5463893 100644
--- a/database/data/categories/Quiv_fc.yaml
+++ b/database/data/categories/Quiv_fc.yaml
@@ -30,8 +30,8 @@ satisfied_properties:
- property: subobject classifier
proof: >-
- The previous proofs show that $\Quiv_{\fc} \subseteq \Quiv$ is closed under finite limits. The subobject classifier $\Omega$ of $\Quiv$ is finite; see nLab for a detailed description. Hence, $\top : 1 \to \Omega$ is a morphism in $\Quiv_{\fc}$. If $X \hookrightarrow Y$ is a monomorphism in $\Quiv_{\fc}$, it is also a monomorphism in $\Quiv$ since the inclusion functor preserves pullbacks. Hence, there is a unique morphism of quivers $Y \to \Omega$ such that
- $$\begin{CD} X @>>> Y \\ @V{!}VV @VVV \\ 1 @>>> \Omega \end{CD}$$
+ The previous proofs show that $\Quiv_{\fc} \subseteq \Quiv$ is closed under finite limits. The subobject classifier $\Omega$ of $\Quiv$ is finite; see nLab for a detailed description. Hence, $\top : T \to \Omega$ is a morphism in $\Quiv_{\fc}$, where $T$ denotes the terminal quiver (having one vertex and one loop). If $X \hookrightarrow Y$ is a monomorphism in $\Quiv_{\fc}$, it is also a monomorphism in $\Quiv$ since the inclusion functor preserves pullbacks. Hence, there is a unique morphism of quivers $Y \to \Omega$ such that
+ $$\begin{CD} X @>>> Y \\ @V{!}VV @VVV \\ T @>>> \Omega \end{CD}$$
is a pullback square in $\Quiv$, i.e. a pullback square in $\Quiv_{\fc}$.
- property: infinitary extensive
diff --git a/database/data/categories/SeqSet.yaml b/database/data/categories/SeqSet.yaml
index b1d55c168..7b48195ef 100644
--- a/database/data/categories/SeqSet.yaml
+++ b/database/data/categories/SeqSet.yaml
@@ -36,13 +36,13 @@ unsatisfied_properties:
- property: generator
proof: >-
- Suppose the category of sequences had a generator. Then, by this result, every subterminal object would be either initial or terminal. However, $0 \to 1 \to 1 \to \cdots$ is a subterminal object which is isomorphic to neither the initial object $0 \to 0 \to 0 \to \cdots$ nor the terminal object $1 \to 1 \to 1 \to \cdots$.
+ Suppose the category of sequences had a generator. Then, by this result, every subterminal object would be either initial or terminal. However, $\varnothing \to \{\ast\} \to \{\ast\} \to \cdots$ is a subterminal object which is isomorphic to neither the initial object $\varnothing \to \varnothing \to \varnothing \to \cdots$ nor the terminal object $\{\ast\} \to \{\ast\} \to \{\ast\} \to \cdots$.
special_objects:
initial object:
- description: the constant sequence $0 \to 0 \to \cdots$
+ description: the constant sequence $\varnothing \to \varnothing \to \cdots$
terminal object:
- description: the constant sequence $1 \to 1 \to \cdots$
+ description: the constant sequence $\{\ast\} \to \{\ast\} \to \cdots$
coproducts:
description: component-wise defined disjoint union
products:
diff --git a/database/data/categories/SeqSet_conn.yaml b/database/data/categories/SeqSet_conn.yaml
index b49849968..99b781742 100644
--- a/database/data/categories/SeqSet_conn.yaml
+++ b/database/data/categories/SeqSet_conn.yaml
@@ -62,7 +62,7 @@ satisfied_properties:
proof: >-
Define the map ("truncated subtraction") $s : \IN \to \IN$ by $s(k) = \max(0,k-1)$. We claim that the sequence
$$\Omega = \bigl(\IN \xrightarrow{s} \IN \xrightarrow{s} \IN \xrightarrow{s} \cdots\bigr)$$
- is a subobject classifier, where $\top : 1 \to \Omega$ is given by the elements $0 \in \IN$ in every degree. Clearly, $\Omega$ is connected. Consider a monomorphism $U \to X$. By the classification of monomorphisms below, we may assume that $U \subseteq X$ is a subsequence, i.e. $U_n \subseteq X_n$ for each $n$, and the transition maps $X_n \to X_{n+1}$ restrict to the transition maps $U_n \to U_{n+1}$.
+ is a subobject classifier, where $\top : T \to \Omega$ is defined on the terminal object $T$, the constant sequence with value $\{\ast\}$, by the elements $0 \in \IN$ in every degree. Clearly, $\Omega$ is connected. Consider a monomorphism $U \to X$. By the classification of monomorphisms below, we may assume that $U \subseteq X$ is a subsequence, i.e. $U_n \subseteq X_n$ for each $n$, and the transition maps $X_n \to X_{n+1}$ restrict to the transition maps $U_n \to U_{n+1}$.
For $x_n \in X_n$, we claim that there is some $k \geq 0$ such that its image $x_{n+k} \in X_{n+k}$ belongs to $U_{n+k}$. In fact, there is some $r \geq 0$ such that an element $u_{n+r} \in U_{n+r}$ exists, and connectedness of $X$ yields some $k \geq r$ such that the image of $u_{n+r}$ in $X_{n+k}$ is equal to $x_{n+k}$. This image belongs to $U_{n+k}$. Therefore, the map
$$\chi_n : X_n \to \IN, \quad x_n \mapsto \min \{k \geq 0 : x_{n+k} \in U_{n+k}\}$$
@@ -74,7 +74,7 @@ satisfied_properties:
\end{CD}$$
commutes. In other words, if $k$ is the smallest number such that $x_{n+k} \in U_{n+k}$, then $s(k)$ is the smallest number $k'$ such that $x_{n+1+k'} \in U_{n+1+k'}$. If $k=0$, then $x_n \in U_n$, hence $x_{n+1} \in U_{n+1}$, so that $k'=0=s(k)$. Now assume $k > 0$, so that $s(k)=k-1$. Then $k'=k-1$, since $x_{n+1+(k-1)} \in U_{n+1+(k-1)}$ and, if $\ell < k-1$, then $\ell+1 < k$, so $x_{n+1+\ell} = x_{n+(\ell+1)} \notin U_{n+(\ell+1)}$ by the definition of $k$.
- Thus, $\chi = (\chi_n) : X \to \Omega$ is a well-defined morphism of sequences. Since $\chi_n^*(\{0\}) = U_n$ for each $n$, the canonical morphism $U \to X \times_{\Omega} 1$ is an isomorphism. It remains to show that $\chi$ is unique with this property.
+ Thus, $\chi = (\chi_n) : X \to \Omega$ is a well-defined morphism of sequences. Since $\chi_n^*(\{0\}) = U_n$ for each $n$, the canonical morphism $U \to X \times_{\Omega} T$ is an isomorphism. It remains to show that $\chi$ is unique with this property.
Let $\alpha : X \to \Omega$ be another morphism of sequences with $\alpha_n^*(\{0\}) = U_n$ for every $n$, and in particular $(\alpha_n)|_{U_n} = 0$. If $x_n \in X_n$ is any element, choose $k \geq 0$ minimal such that $x_{n+k} \in U_{n+k}$, where $x_{n+k}$ denotes the image of $x_n$ as before. We claim that
$$\alpha_n(x_n) = k.$$
@@ -156,7 +156,7 @@ unsatisfied_properties:
- property: binary copowers
proof: >-
- We show that the coproduct $1+1$ does not exist in $[(\IN,\leq),\Set]_{\conn}$, where $1$ denotes the terminal object, the constant sequence with value $\{\ast\}$. Since a morphism $1 \to X$ corresponds to an element of $X_0$, this would amount to a universal connected sequence of sets $X$ equipped with two elements $x,x' \in X_0$. Choose $k \geq 0$ such that their images in $X_k$ coincide. Then, by the universal property, for every connected sequence $Y$ and every pair of elements $y,y' \in Y_0$, their images in $Y_k$ must coincide. A counterexample is the sequence $Y$ defined by
+ We show that the coproduct $T+T$ does not exist in $[(\IN,\leq),\Set]_{\conn}$, where $T$ denotes the terminal object, the constant sequence with value $\{\ast\}$. Since a morphism $T \to X$ corresponds to an element of $X_0$, this would amount to a universal connected sequence of sets $X$ equipped with two elements $x,x' \in X_0$. Choose $k \geq 0$ such that their images in $X_k$ coincide. Then, by the universal property, for every connected sequence $Y$ and every pair of elements $y,y' \in Y_0$, their images in $Y_k$ must coincide. A counterexample is the sequence $Y$ defined by
$$\{0,1\} \xrightarrow{\id} \cdots \xrightarrow{\id} \{0,1\} \xrightarrow{!} \{0\} \xrightarrow{!} \{0\} \xrightarrow{!} \cdots,$$
where $Y_k = \{0,1\}$ and $Y_{k+1}=\{0\}$. It is connected, but the elements $0,1 \in Y_0$ only become equal in $Y_{k+1}$.
Another counterexample is the subobject classifier $\Omega$, whose elements $0,k+1 \in \Omega_0$ become equal only after $k+1$ steps.
@@ -187,7 +187,7 @@ unsatisfied_properties:
- property: natural numbers object
proof: >-
- Assume that a natural numbers object $(N,z,s)$ exists in $[(\IN,\leq),\Set]_{\conn}$. The morphism $z : 1 \to N$ corresponds to an element $z \in N_0$. The functor
+ Assume that a natural numbers object $(N,z,s)$ exists in $[(\IN,\leq),\Set]_{\conn}$. The morphism $z : T \to N$, where $T$ denotes the terminal object, the constant sequence with value $\{\ast\}$, corresponds to an element $z \in N_0$. The functor
$$[(\IN,\leq),\Set]_{\conn} \to \Set, \quad X \mapsto X_0$$
has a right adjoint mapping a set $S$ to the connected sequence
$$S \xrightarrow{!} \{\ast\} \xrightarrow{!} \{\ast\} \xrightarrow{!} \cdots,$$
@@ -195,7 +195,7 @@ unsatisfied_properties:
For every $k \geq 0$ consider the connected sequence $X$ defined by
$$N_0 \xrightarrow{\id} \cdots \xrightarrow{\id} N_0 \xrightarrow{!} \{\ast\} \xrightarrow{!} \{\ast\} \xrightarrow{!} \cdots,$$
- where the singleton sets start at index $k+1$. The element $z \in N_0 = X_0$ induces a morphism $z : 1 \to X$. We define the endomorphism $r : X \to X$ by using the map $s_0 : N_0 \to N_0$ at indices $0,\dotsc,k$ and the unique maps at indices $> k$. Since $(N,z,s)$ is a natural numbers object, there is a unique morphism of sequences $f : N \to X$ such that $f_0(z)=z$ and $r \circ f = f \circ s$. Evaluating this equation at index $0$ yields $s_0 \circ f_0 = f_0 \circ s_0$, so that $f_0 = \id_{N_0}$. Furthermore, naturality of $f : N \to X$ for $0 \to k$ shows that the diagram
+ where the singleton sets start at index $k+1$. The element $z \in N_0 = X_0$ induces a morphism $z : T \to X$. We define the endomorphism $r : X \to X$ by using the map $s_0 : N_0 \to N_0$ at indices $0,\dotsc,k$ and the unique maps at indices $> k$. Since $(N,z,s)$ is a natural numbers object, there is a unique morphism of sequences $f : N \to X$ such that $f_0(z)=z$ and $r \circ f = f \circ s$. Evaluating this equation at index $0$ yields $s_0 \circ f_0 = f_0 \circ s_0$, so that $f_0 = \id_{N_0}$. Furthermore, naturality of $f : N \to X$ for $0 \to k$ shows that the diagram
$$\begin{CD}
N_0 @>{N_{0 \to k}}>> N_k \\
@V{\id}VV @VV{f_k}V \\
diff --git a/database/data/categories/Set.yaml b/database/data/categories/Set.yaml
index 2cc18bd9f..77db3cea7 100644
--- a/database/data/categories/Set.yaml
+++ b/database/data/categories/Set.yaml
@@ -70,7 +70,7 @@ special_morphisms:
proof: This is an elementary fact from set theory.
monomorphisms:
description: injective maps
- proof: 'For the non-trivial direction, if $f : X \to Y$ is a monomorphism of sets and $a,b \in X$ satisfy $f(a) = f(b)$, then $f \circ a = f \circ b$ when we regard $a,b$ as morphisms $a,b : 1 \rightrightarrows X$. Hence, $a = b$. More generally, if $\C$ is a category that admits a faithful and representable functor $U : \C \to \Set$, then the monomorphisms in $\C$ are precisely the morphisms whose $U$-image is injective.'
+ proof: 'For the non-trivial direction, if $f : X \to Y$ is a monomorphism of sets and $a,b \in X$ satisfy $f(a) = f(b)$, then $f \circ a = f \circ b$ when we regard $a,b$ as morphisms $a,b : \{\ast\} \rightrightarrows X$. Hence, $a = b$. More generally, if $\C$ is a category that admits a faithful and representable functor $U : \C \to \Set$, then the monomorphisms in $\C$ are precisely the morphisms whose $U$-image is injective.'
epimorphisms:
description: surjective maps
- proof: 'For the non-trivial direction, if $f : X \to Y$ is an epimorphism of sets, then in particular $f^* : \Hom(Y,2) \to \Hom(X,2)$ is injective, which identifies with $f^* : P(Y) \to P(X)$. Then for all $y \in Y$ we have $f^*(\{y\}) \neq f^*(\varnothing) = \varnothing$, so that $y$ has a preimage.'
+ proof: 'For the non-trivial direction, if $f : X \to Y$ is an epimorphism of sets, then in particular $f^* : \Hom(Y,\{0,1\}) \to \Hom(X,\{0,1\})$ is injective, which identifies with $f^* : P(Y) \to P(X)$. Then for all $y \in Y$ we have $f^*(\{y\}) \neq f^*(\varnothing) = \varnothing$, so that $y$ has a preimage.'
diff --git a/database/data/categories/Set_arrow.yaml b/database/data/categories/Set_arrow.yaml
index 08e10862f..fdf0d94cc 100644
--- a/database/data/categories/Set_arrow.yaml
+++ b/database/data/categories/Set_arrow.yaml
@@ -46,13 +46,13 @@ unsatisfied_properties:
- property: generator
proof: >-
- Suppose $\Set^{\rightarrow}$ had a generator. Then by this result, every subterminal object would be either initial or terminal. However, in fact, $0 \to 1$ is a subterminal object which is isomorphic to neither the initial object $0 \to 0$ nor the terminal object $1 \to 1$.
+ Suppose $\Set^{\rightarrow}$ had a generator. Then by this result, every subterminal object would be either initial or terminal. However, in fact, $\varnothing \to \{\ast\}$ is a subterminal object which is isomorphic to neither the initial object $\varnothing \to \varnothing$ nor the terminal object $\{\ast\} \to \{\ast\}$.
special_objects:
initial object:
- description: the unique function $0 \to 0$
+ description: the unique function $\varnothing \to \varnothing$
terminal object:
- description: the unique function $1 \to 1$
+ description: the unique function $\{\ast\} \to \{\ast\}$
coproducts:
description: component-wise defined disjoint union, equipped with the disjoint union of the functions
products:
@@ -64,7 +64,7 @@ special_morphisms:
proof: This is easy.
monomorphisms:
description: pairs $(\ell, r)$ where $\ell$ and $r$ are both injective
- proof: For the non-trivial direction, use the fact that the domain functor taking an object $(X, Y, f)$ to $X$ and a morphism $(\ell, r)$ to $\ell$ is representable by $1 \to 1$; and moreover, the codomain functor taking an object $(X, Y, f)$ to $Y$ and a morphism $(\ell, r)$ to $r$ is representable by $0 \to 1$.
+ proof: For the non-trivial direction, use the fact that the domain functor taking an object $(X, Y, f)$ to $X$ and a morphism $(\ell, r)$ to $\ell$ is representable by $\{\ast\} \to \{\ast\}$; and moreover, the codomain functor taking an object $(X, Y, f)$ to $Y$ and a morphism $(\ell, r)$ to $r$ is representable by $\varnothing \to \{\ast\}$.
epimorphisms:
description: pairs $(\ell, r)$ where $\ell$ and $r$ are both surjective
proof: For the non-trivial direction, use the fact that the category is epi-regular, so any epimorphism is a coequalizer; and the fact that coequalizers can be calculated component-wise.
diff --git a/database/data/categories/Set_c.yaml b/database/data/categories/Set_c.yaml
index f6f891358..1271489ac 100644
--- a/database/data/categories/Set_c.yaml
+++ b/database/data/categories/Set_c.yaml
@@ -51,7 +51,7 @@ satisfied_properties:
proof: This follows from Lemma 11 here since $\Set$ is countably extensive (even infinitary extensive) and its full subcategory $\Set_\c$ is closed under pullbacks and countable coproducts in $\Set$.
- property: effective congruences
- proof: 'Let $R \rightrightarrows X$ be a congruence in $\Set_\c$. Then using $1$ as a test object, we see that this induces an equivalence relation on $X$. We already know that $\Set$ has effective congruences (as does every topos). Using this result, we see that $R$ is the kernel pair of $X \to (X/R)_{\Set}$ in $\Set$. Also, the quotient $(X/R)_{\Set}$ is countable; and the forgetful functor $\Set_\c \to \Set$ is fully faithful and therefore reflects limits. Thus, we conclude that $R$ is the kernel pair of $X \to (X/R)_{\Set}$ in $\Set_\c$ as well.'
+ proof: 'Let $R \rightrightarrows X$ be a congruence in $\Set_\c$. Then using $\{\ast\}$ as a test object, we see that this induces an equivalence relation on $X$. We already know that $\Set$ has effective congruences (as does every topos). Using this result, we see that $R$ is the kernel pair of $X \to (X/R)_{\Set}$ in $\Set$. Also, the quotient $(X/R)_{\Set}$ is countable; and the forgetful functor $\Set_\c \to \Set$ is fully faithful and therefore reflects limits. Thus, we conclude that $R$ is the kernel pair of $X \to (X/R)_{\Set}$ in $\Set_\c$ as well.'
- property: regular
proof: This follows from Lemma 7 here applied to the inclusion functor $\Set_\c \hookrightarrow \Set$ into the regular category $\Set$ and the description of regular epimorphisms below.
@@ -70,7 +70,7 @@ unsatisfied_properties:
proof: Since the forgetful functor $\Set_\c \to \Set$ is representable, it preserves (countable) products. Therefore, if the power $\{0,1\}^{\IN}$ exists in $\Set_\c$, it must be the ordinary cartesian product, which however is uncountable.
- property: ℵ₂-small copowers
- proof: 'Assume that the copower $X \coloneqq I \otimes 1$ exists in $\Set_\c$. We will prove that $I$ is countable; in particular, $\aleph_1 \otimes 1$ does not exist. The copower is a countable set $X$ with a universal family of elements $(x_i)_{i \in I}$. For every $i \in I$ there is a map $X \to \{0,1\}$ defined by $x_i \mapsto 1$ and $x_j \mapsto 0$ for $j \neq i$. In particular, $x_i \neq x_j$ whenever $i \neq j$. Thus, $x : I \to X$ is an injective map, which proves that $I$ is countable.'
+ proof: 'Assume that the copower $X \coloneqq I \otimes \{\ast\}$ exists in $\Set_\c$. We will prove that $I$ is countable; in particular, $\aleph_1 \otimes \{\ast\}$ does not exist. The copower is a countable set $X$ with a universal family of elements $(x_i)_{i \in I}$. For every $i \in I$ there is a map $X \to \{0,1\}$ defined by $x_i \mapsto 1$ and $x_j \mapsto 0$ for $j \neq i$. In particular, $x_i \neq x_j$ whenever $i \neq j$. Thus, $x : I \to X$ is an injective map, which proves that $I$ is countable.'
- property: ℵ₁-cofiltered limits
proof: >-
@@ -101,4 +101,4 @@ special_morphisms:
proof: For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the terminal object), hence preserves monomorphisms.
epimorphisms:
description: surjective maps
- proof: 'For the non-trivial direction, if $f : X \to Y$ is an epimorphism of countable sets, then in particular $f^* : \Hom(Y,2) \to \Hom(X,2)$ is injective, which identifies with $f^* : P(Y) \to P(X)$. Then for all $y \in Y$ we have $f^*(\{y\}) \neq f^*(\varnothing) = \varnothing$, so that $y$ has a preimage.'
+ proof: 'For the non-trivial direction, if $f : X \to Y$ is an epimorphism of countable sets, then in particular $f^* : \Hom(Y,\{0,1\}) \to \Hom(X,\{0,1\})$ is injective, which identifies with $f^* : P(Y) \to P(X)$. Then for all $y \in Y$ we have $f^*(\{y\}) \neq f^*(\varnothing) = \varnothing$, so that $y$ has a preimage.'
diff --git a/database/data/categories/Set_family.yaml b/database/data/categories/Set_family.yaml
index f469d63af..233a4c959 100644
--- a/database/data/categories/Set_family.yaml
+++ b/database/data/categories/Set_family.yaml
@@ -50,7 +50,7 @@ unsatisfied_properties:
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.
+ proof: Let $T$ be the terminal object, given by $T_i = \{\ast\}$ for all $i \in I$. The collection $\Sub(T)$ is isomorphic to the collection $P(I)$ of subcollections of $I$. In fact, if $J \subseteq I$ is a subcollection, we define $X \subseteq T$ by $X_i = \varnothing$ for $i \in J$ and $X_i = \{\ast\}$ for $i \notin J$. Every subobject of $T$ has this form. Since $P(I)$ is not essentially small (there is an injective map $I \hookrightarrow P(I)$), we conclude that $\Sub(T)$ is not essentially small.
special_objects:
initial object:
diff --git a/database/data/categories/Set_family_mostly_0.yaml b/database/data/categories/Set_family_mostly_0.yaml
index 29d78fd86..96e09e1d5 100644
--- a/database/data/categories/Set_family_mostly_0.yaml
+++ b/database/data/categories/Set_family_mostly_0.yaml
@@ -26,11 +26,11 @@ satisfied_properties:
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.'
+ 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, $C_i$ is a colimit of empty sets and hence empty. 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.'
+ 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, $L_i$ is a limit of empty sets indexed by the non-empty category $\J$ and hence 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
@@ -90,7 +90,7 @@ unsatisfied_properties:
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 the dual of Lemma 2 here, the claim follows from the fact that epimorphisms in $\Set$ are not stable under cofiltered limits.
+ 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 = \varnothing$ for indices $j \neq i$. This embedding is faithful and preserves non-empty limits and epimorphisms. Thus, by the dual of 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.
diff --git a/database/data/categories/Set_family_mostly_1.yaml b/database/data/categories/Set_family_mostly_1.yaml
index cce361162..9380537f6 100644
--- a/database/data/categories/Set_family_mostly_1.yaml
+++ b/database/data/categories/Set_family_mostly_1.yaml
@@ -1,7 +1,7 @@
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'
+objects: 'families of sets $X = (X_i)_{i \in I}$ such that $S(X) \coloneqq \{i \in I : \card(X_i) \neq 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$. 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
@@ -22,7 +22,7 @@ satisfied_properties:
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.'
+ 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, $L_i$ is a limit of singletons and hence a singleton. Thus, $S(L) \subseteq \bigcup_{j \in \J} S(D(j))$, and hence $S(L)$ is essentially small.'
- property: locally cartesian closed
proof: >-
@@ -30,12 +30,12 @@ satisfied_properties:
$$\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,
+ Thus, if $X_i$ and $Z_i$ are singletons, then $[Y \to X, Z \to X]_i$ is a singleton. 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.'
+ 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, $C_i$ is a colimit of singletons indexed by the connected category $\J$ and hence a singleton. 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$.
@@ -47,7 +47,7 @@ satisfied_properties:
proof: Based on the pointwise descriptions of regular monomorphisms and pushouts, this follows from the corresponding property of $\Set$.
- 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.
+ 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$ is a singleton, then $Y_i$ is a singleton as well. 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.
@@ -69,42 +69,42 @@ unsatisfied_properties:
- 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.
+ 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 = \{\ast\}$ 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, let $T$ be the terminal object, given by $T_i = \{\ast\}$ for all $i \in I$. Then $S(T+T) = I$, which is not essentially small. Thus, the coproduct $T+T$ 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.'
+ proof: 'Assume that $(N,z,s)$ is a natural numbers object. Let $T$ be the terminal object, given by $T_i = \{\ast\}$ for all $i \in I$. Since $z : T \to N$ is a morphism consisting of maps $z_i : \{\ast\} \to N_i$, we have $N_i \neq \varnothing$ for every $i \in I$. By Lemma 2 here, the coproduct $T + N$ exists, and we have $N \cong T + 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 \{\ast\} + 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 the dual of Lemma 2 here, the claim follows from the fact that epimorphisms in $\Set$ are not stable under cofiltered limits.
+ 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 = \{\ast\}$ for indices $j \neq i$. This embedding is faithful and preserves limits and epimorphisms. Thus, by the dual of 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.
+ 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 = \{\ast\}$ 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.
+ proof: Let $T$ be the terminal object, given by $T_i = \{\ast\}$ for all $i \in I$. The collection $\Sub(T)$ 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 T$ by $X_i = \varnothing$ for $i \in J$ and $X_i = \{\ast\}$ for $i \notin J$. Every subobject of $T$ has this form. Since for every $i \in I$ the collection $\{i\} \subseteq I$ is essentially small, we conclude that $\Sub(T)$ 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
+ We will show that Isbell's condition for concretizability fails. Let $T$ be the terminal object, given by $T_i = \{\ast\}$ for all $i \in I$. For every object $X$ there is a unique span $T \leftarrow X \rightarrow T$. A cospan $T \xrightarrow{u} Y \xleftarrow{v} T$ 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 \\
+ X_i @>>> \{\ast\} \\
@VVV @VV{v_i}V \\
- 1 @>>{u_i}> Y_i
+ \{\ast\} @>>{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$.
+ 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 : T \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.
+ We have thus fully characterized the equivalence classes of spans $T \leftarrow X \rightarrow T$. 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:
diff --git a/database/data/categories/Set_ff.yaml b/database/data/categories/Set_ff.yaml
index 392390a7d..831fe6c05 100644
--- a/database/data/categories/Set_ff.yaml
+++ b/database/data/categories/Set_ff.yaml
@@ -89,7 +89,7 @@ unsatisfied_properties:
proof: This is trivial.
- property: locally finite
- proof: If $X$ is an infinite set, there are infinitely many maps $1 \to X$. They are injective and hence finite-to-one.
+ proof: If $X$ is an infinite set, there are infinitely many maps $\{\ast\} \to X$. They are injective and hence finite-to-one.
- property: strongly connected
proof: Already $\Set$ is not strongly connected.
@@ -98,7 +98,7 @@ unsatisfied_properties:
proof: 'More generally, if $X,Y$ are two non-empty sets such that $X \times Y$ exists in $\Set_\ff$, then both $X$ and $Y$ must be finite. In fact, the forgetful functor to $\Set$ is representable, so it must preserve products. This means we can assume $X \times Y$ is the usual cartesian product with the usual projections. Since $p_1 : X \times Y \to X$ is finite-to-one and $X$ is non-empty, $Y$ is finite. By symmetry, also $X$ is finite. (Conversely, if $X$ and $Y$ are finite, or one of them is empty, then indeed $X \times Y$ exists.)'
- property: countable copowers
- proof: 'Assume that the copower $X \coloneqq \IN \otimes 1$ exists, where $1$ is the singleton set. This is a set with a map $i : \IN \to X$ (not necessarily finite-to-one) such that for every other such map $j : \IN \to Y$ there is a unique finite-to-one map $f : X \to Y$ with $f \circ i = j$. Applying this to $j : \IN \to 1$, we see that $X$ is finite. Applying the universal property to maps $j : \IN \to \{0,1\}$, we see that for every subset $E \subseteq \IN$ there is a unique finite subset $F \subseteq X$ with $i^*(F) = E$. But finiteness of $F$ is automatic, so $i^* : P(X) \to P(\IN)$ is bijective. But then $P(\IN)$ is finite, which is absurd.'
+ proof: 'Assume that the copower $X \coloneqq \IN \otimes \{\ast\}$ exists. This is a set with a map $i : \IN \to X$ (not necessarily finite-to-one) such that for every other such map $j : \IN \to Y$ there is a unique finite-to-one map $f : X \to Y$ with $f \circ i = j$. Applying this to $j : \IN \to \{\ast\}$, we see that $X$ is finite. Applying the universal property to maps $j : \IN \to \{0,1\}$, we see that for every subset $E \subseteq \IN$ there is a unique finite subset $F \subseteq X$ with $i^*(F) = E$. But finiteness of $F$ is automatic, so $i^* : P(X) \to P(\IN)$ is bijective. But then $P(\IN)$ is finite, which is absurd.'
- property: filtered
proof: 'Consider the maps $f,g : \IN \rightrightarrows \IN$ defined by $f(x)=x$ and $g(x)=2x$. They are injective, hence finite-to-one. If a map $h : \IN \to X$ coequalizes them, we have $h(x)=h(2x)$, in particular $h(1)=h(2^n)$ for all $n \in \IN$. Thus, $h$ is not finite-to-one.'
@@ -107,7 +107,7 @@ unsatisfied_properties:
proof: Consider the set $[n] \coloneqq \{0,\dotsc,n\}$ for $n \in \IN$. The forgetful functor to $\Set$ is representable (by the singleton set), hence preserves all limits. Thus, if the diagram of truncation maps $\cdots \twoheadrightarrow [2] \twoheadrightarrow [1] \twoheadrightarrow [0]$ has a limit in $\Set_\ff$, its underlying set is isomorphic to the limit taken in $\Set$, which is $\IN \cup \{\infty\}$. But there is no finite-to-one map $\IN \cup \{\infty\} \to [0]$.
- property: cogenerating collection
- proof: 'Suppose that $S$ is an essentially small collection of objects of $\Set_\ff$, and let $\kappa$ be an uncountable cardinal greater than $\card(Q)$ for each $Q \in S$. Then for each $Q \in S$, $\Hom(\kappa, Q) = \varnothing$ (or else we would have $\kappa = \card(\kappa) \le \aleph_0 \cdot \card(Q) = \max(\aleph_0, \card(Q)) < \kappa$, giving a contradiction). This makes it impossible for any morphisms from $\kappa$ to an object of $S$ to distinguish the two morphisms $0, 1 : 1 \rightrightarrows \kappa$.'
+ proof: 'Suppose that $S$ is an essentially small collection of objects of $\Set_\ff$, and let $\kappa$ be an uncountable cardinal greater than $\card(Q)$ for each $Q \in S$. Then for each $Q \in S$, $\Hom(\kappa, Q) = \varnothing$ (or else we would have $\kappa = \card(\kappa) \le \aleph_0 \cdot \card(Q) = \max(\aleph_0, \card(Q)) < \kappa$, giving a contradiction). This makes it impossible for any morphisms from $\kappa$ to an object of $S$ to distinguish the two morphisms $0, 1 : \{\ast\} \rightrightarrows \kappa$.'
special_objects:
initial object:
@@ -124,4 +124,4 @@ special_morphisms:
proof: For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the singleton), hence preserves monomorphisms.
epimorphisms:
description: surjective maps with finite fibers
- proof: 'For the non-trivial direction, if $f : X \to Y$ is an epimorphism in this category, then in particular $f^* : \Hom(Y,2) \to \Hom(X,2)$ is injective, which identifies with $f^* : E(Y) \to E(X)$, where $E(-)$ denotes the set of finite subsets. Then for all $y \in Y$ we have $f^*(\{y\}) \neq f^*(\varnothing) = \varnothing$, so that $y$ has a preimage.'
+ proof: 'For the non-trivial direction, if $f : X \to Y$ is an epimorphism in this category, then in particular $f^* : \Hom(Y,\{0,1\}) \to \Hom(X,\{0,1\})$ is injective, which identifies with $f^* : E(Y) \to E(X)$, where $E(-)$ denotes the set of finite subsets. Then for all $y \in Y$ we have $f^*(\{y\}) \neq f^*(\varnothing) = \varnothing$, so that $y$ has a preimage.'
diff --git a/database/data/categories/Setne.yaml b/database/data/categories/Setne.yaml
index 28ef0f5d8..df1f05a5f 100644
--- a/database/data/categories/Setne.yaml
+++ b/database/data/categories/Setne.yaml
@@ -78,7 +78,7 @@ unsatisfied_properties:
proof: The two maps $\{0\} \rightrightarrows \{0,1\}$ are equalized by no map $X \to \{0\}$ in this category.
- property: sequential limits
- proof: Assume that the sequence of inclusions $\cdots \to \IN_{\geq 2} \to \IN_{\geq 1} \to \IN_{\geq 0} = \IN$ has a limit $X$, consisting of maps $X \to \IN_{\geq n}$. Since $X$ is non-empty, there is a map $1 \to X$. This corresponds to a family of compatible maps $1 \to \IN_{\geq n}$, i.e. to compatible elements in $\IN_{\geq n}$. But the set $\bigcap_{n \geq 0} \IN_{\geq n}$ is empty.
+ proof: Assume that the sequence of inclusions $\cdots \to \IN_{\geq 2} \to \IN_{\geq 1} \to \IN_{\geq 0} = \IN$ has a limit $X$, consisting of maps $X \to \IN_{\geq n}$. Since $X$ is non-empty, there is a map $\{\ast\} \to X$. This corresponds to a family of compatible maps $\{\ast\} \to \IN_{\geq n}$, i.e. to compatible elements in $\IN_{\geq n}$. But the set $\bigcap_{n \geq 0} \IN_{\geq n}$ is empty.
- property: ℵ₁-cofiltered limits
proof: 'Since the forgetful functor $\Setne \to \Set$ is representable, it preserves limits. Thus it suffices to find an $\aleph_1$-cofiltered diagram of non-empty sets whose limit in $\Set$ is empty. Let $R$ be an uncountable set (such as $\IR$) and consider the poset $P$ of subsets $A \subseteq R$ whose complement $R \setminus A$ is countable; in particular, every such $A$ is non-empty. Then $P$ is $\aleph_1$-cofiltered, since a countable union of countable sets is countable. The limit of the diagram $P \to \Setne$, $A \mapsto A$, in $\Set$ is the intersection $\bigcap_{A \in P} A$ in $R$, which is empty, because for every $r \in R$ we have $r \notin R \setminus \{r\} \in P$.'
diff --git a/database/data/categories/Sh(X).yaml b/database/data/categories/Sh(X).yaml
index 7d243d172..1fada67e3 100644
--- a/database/data/categories/Sh(X).yaml
+++ b/database/data/categories/Sh(X).yaml
@@ -35,7 +35,7 @@ unsatisfied_properties:
- property: generator
proof: >-
Suppose $\Sh(X)$ had a generator. Then by this result, every subterminal object would be either initial or terminal. On the other hand, the subterminal objects of $\Sh(X)$ are of the form $y_U \coloneqq \Hom({-}, U)$ for $U$ open. (Alternative descriptions of $y_U$ include:
- $$y_U(V) = \begin{cases} 1, & V \subseteq U; \\ \varnothing & \text{otherwise} \end{cases}$$
+ $$y_U(V) = \begin{cases} \{\ast\}, & V \subseteq U; \\ \varnothing & \text{otherwise} \end{cases}$$
with the unique restriction maps; and $y_U$ represents the functor $\Gamma(U, {-})$ of sections over $U$.) Therefore, the lemma implies that every open set of $X$ is either $\varnothing$ or $X$, contradicting our assumption that $X$ does not have the indiscrete topology.
special_objects:
diff --git a/database/data/categories/Sp.yaml b/database/data/categories/Sp.yaml
index c0d298571..e0d44006d 100644
--- a/database/data/categories/Sp.yaml
+++ b/database/data/categories/Sp.yaml
@@ -22,7 +22,7 @@ satisfied_properties:
proof: The category is equivalent to $\prod_{n \geq 0} \Sigma_n{-}\FinSet$ (where $\Sigma_n$ denotes the symmetric group of degree $n$), and each $\Sigma_n{-}\FinSet$ is an elementary topos since $\FinSet$ is an elementary topos and $\Sigma_n$ is a finite group, cf. Johnstone, Part B, Corollary 2.3.18.
- property: cogenerator
- proof: 'This follows from $\Sp \simeq \prod_{n \geq 0} \Sigma_n{-}\FinSet$, this lemma, and the fact that if $G$ is a (finite) group, the power set $P(G)$ with the evident $G$-action is a weakly terminal cogenerator in $G{-}\Set$ (resp. $G{-}\FinSet$). For the proof, notice that $\varnothing,G \in P(G)$ are fixed points, yielding two $G$-maps $1 \rightrightarrows P(G)$. In particular, $P(G)$ is weakly terminal. If $X$ is a $G$-set with distinct points $x,y$, we construct a $G$-map $f : X \to P(G)$ that separates $x,y$: First, $X$ is a coproduct of orbits. If $x,y$ lie in different orbits, let $f|_{Gx}$ be constant $\varnothing$, $f|_{Gy}$ be constant $G$, and, say, $f$ be constant $\varnothing$ on all other orbits. If $x,y$ lie in the same orbit, say $y = g_0 x$, define $f|_{Gx} : Gx \to P(G)$ by $f(x) = G_x$ (stabilizer), which is well-defined, and choose $f$ to be $\varnothing$ on all other orbits. Then $f(y) = g_0 G_x \neq G_x = f(x)$.'
+ proof: 'This follows from $\Sp \simeq \prod_{n \geq 0} \Sigma_n{-}\FinSet$, this lemma, and the fact that if $G$ is a (finite) group, the power set $P(G)$ with the evident $G$-action is a weakly terminal cogenerator in $G{-}\Set$ (resp. $G{-}\FinSet$). For the proof, notice that $\varnothing,G \in P(G)$ are fixed points, yielding two $G$-maps $\{\ast\} \rightrightarrows P(G)$. In particular, $P(G)$ is weakly terminal. If $X$ is a $G$-set with distinct points $x,y$, we construct a $G$-map $f : X \to P(G)$ that separates $x,y$: First, $X$ is a coproduct of orbits. If $x,y$ lie in different orbits, let $f|_{Gx}$ be constant $\varnothing$, $f|_{Gy}$ be constant $G$, and, say, $f$ be constant $\varnothing$ on all other orbits. If $x,y$ lie in the same orbit, say $y = g_0 x$, define $f|_{Gx} : Gx \to P(G)$ by $f(x) = G_x$ (stabilizer), which is well-defined, and choose $f$ to be $\varnothing$ on all other orbits. Then $f(y) = g_0 G_x \neq G_x = f(x)$.'
- property: ℵ₁-accessible
proof: We know that $\FinSet$ has $\aleph_1$-filtered colimits and that every object is $\aleph_1$-presentable; see here. It follows that for every $n \in \IN$ also $\Sigma_n{-}\FinSet$ has $\aleph_1$-filtered colimits and that every object is $\aleph_1$-presentable. From this it follows formally that $\Sp \simeq \prod_{n \geq 0} \Sigma_n{-}\FinSet$ also has these properties. In particular, $\Sp$ is $\aleph_1$-accessible.
@@ -35,7 +35,7 @@ unsatisfied_properties:
proof: This is trivial.
- property: locally finite
- proof: If $1$ denotes the terminal species, there are infinitely many morphisms $1 \to 1 \sqcup 1$ since they correspond to functions $\IN \to \{1,2\}$.
+ proof: If $T$ denotes the terminal species, there are infinitely many morphisms $T \to T \sqcup T$ since they correspond to functions $\IN \to \{1,2\}$.
- property: locally small
proof: Since $\FinSet$ is not small, this follows exactly like Lemma 2 here; but this result is not really relevant; all that matters is that $\Sp$ is locally essentially small.
@@ -53,13 +53,13 @@ unsatisfied_properties:
Alternatively, the claim follows from this result.
- property: natural numbers object
- proof: By Lemma 2 here, if $(N,z,s)$ is a natural numbers object, then $N \cong 1 \sqcup N$. But there is no combinatorial species $N$ with this property, since evaluating this isomorphism at, say, $\varnothing$, would yield a finite set $N$ with this property.
+ proof: By Lemma 2 here, if $(N,z,s)$ is a natural numbers object, then $N \cong T \sqcup N$, where $T$ denotes the terminal species. But there is no combinatorial species $N$ with this property, since evaluating this isomorphism at, say, $\varnothing$, would yield a finite set $N$ with this property.
special_objects:
initial object:
description: species $X$ with $X_n = \varnothing$
terminal object:
- description: species $X$ with $X_n = 1$
+ description: species $X$ with $X_n = \{\ast\}$
coproducts:
description: '[finite case] pointwise finite disjoint union'
products:
diff --git a/database/data/categories/Top.yaml b/database/data/categories/Top.yaml
index c3ffed922..c8678cb62 100644
--- a/database/data/categories/Top.yaml
+++ b/database/data/categories/Top.yaml
@@ -92,7 +92,7 @@ unsatisfied_properties:
label: Top_not_co-malcev
- property: effective cocongruences
- proof: 'Consider the indiscrete topological space $I$ on two points. This represents the functor which takes a topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $1 \rightrightarrows I$, where the maps are the two possible functions. However, this cannot be effective: if we have $h : Z\to 1$ which equalizes the two maps, then $Z$ must be empty. But that means the cokernel pair of $h$ is the discrete space on two points.'
+ proof: 'Consider the indiscrete topological space $I$ on two points. This represents the functor which takes a topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $\{\ast\} \rightrightarrows I$, where the maps are the two possible functions. However, this cannot be effective: if we have $h : Z \to \{\ast\}$ which equalizes the two maps, then $Z$ must be empty. But that means the cokernel pair of $h$ is the discrete space on two points.'
label: Top_no_effective_cocongruences
- property: extremal generating collection
@@ -121,7 +121,7 @@ special_morphisms:
proof: For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the terminal object), hence preserves monomorphisms.
epimorphisms:
description: surjective continuous maps
- proof: The proof works exactly as for the category of sets, where we endow $2$ with the indiscrete topology.
+ proof: The proof works exactly as for the category of sets, where we endow $\{0,1\}$ with the indiscrete topology.
regular monomorphisms:
description: embeddings
proof: 'Equalizers are embeddings by their construction. Conversely, if $f : X \to Y$ is an embedding, then $f$ is the equalizer of the two characteristic maps $\chi_Y, \chi_{f(X)} : Y \rightrightarrows \{0,1\}$, where $\{0,1\}$ carries the indiscrete topology.'
diff --git a/database/data/categories/Top_pointed.yaml b/database/data/categories/Top_pointed.yaml
index f5cfe1122..424a0a316 100644
--- a/database/data/categories/Top_pointed.yaml
+++ b/database/data/categories/Top_pointed.yaml
@@ -101,7 +101,7 @@ unsatisfied_properties:
- Set_*_not_conormal
- property: coaccessible
- proof: 'We can adjust the proof for $\Top$ as follows: Assume $\Top_*$ is coaccessible. Let $S_0=\{x,*\}$ be the pointed topological space such that $\{*\}$ is the only non-trivial open set, and let $S_1=\{x,*\}$ be the pointed space such that $\{x\}$ is the only non-trivial open set. Let $p_i : S_i \to \{x,*\}$ be the identity function to the two-element indiscrete pointed space. Then, a pointed topological space is discrete if and only if it is projective to the morphisms $p_0$ and $p_1$. This implies that the full subcategory spanned by all discrete pointed spaces, which is equivalent to $\Set_*$, is coaccessible by Adámek–Rosický, Prop. 4.7. However, since $\Set_*$ is not coaccessible, this is a contradiction.'
+ proof: 'We can adjust the proof for $\Top$ as follows: Assume $\Top_*$ is coaccessible. Let $S_0=\{x,\ast\}$ be the pointed topological space such that $\{\ast\}$ is the only non-trivial open set, and let $S_1=\{x,\ast\}$ be the pointed space such that $\{x\}$ is the only non-trivial open set. Let $p_i : S_i \to \{x,\ast\}$ be the identity function to the two-element indiscrete pointed space. Then, a pointed topological space is discrete if and only if it is projective to the morphisms $p_0$ and $p_1$. This implies that the full subcategory spanned by all discrete pointed spaces, which is equivalent to $\Set_*$, is coaccessible by Adámek–Rosický, Prop. 4.7. However, since $\Set_*$ is not coaccessible, this is a contradiction.'
references:
- Top_not_coaccessible
@@ -112,7 +112,7 @@ unsatisfied_properties:
proof: Suppose that $\Top_*$ had effective congruences. Then by this result, $\Top$ would also have effective congruences, which we know is not the case.
- property: effective cocongruences
- proof: 'This counterexample is adapted from the counterexample for $\Top$. Consider the pointed topological space $I \coloneqq \{ *, a, b \}$ with topology $\{ \varnothing, \{ * \}, \{ a, b \}, \{ *, a, b \} \}$. This represents the functor which sends a pointed topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $\{ *, a \} \rightrightarrows I$ on the discrete space $\{ *, a \}$, where the maps are $*\mapsto *, a\mapsto a$ and $*\mapsto *, a\mapsto b$, respectively. However, this cannot be effective: if we have $h : Z \to \{ *, a \}$ which equalizes the cocongruence, then $h$ must be the constant function with value $*$. But that means the cokernel pair of $h$ is the discrete space on $\{ *, a, b \}$.'
+ proof: 'This counterexample is adapted from the counterexample for $\Top$. Consider the pointed topological space $I \coloneqq \{ \ast, a, b \}$ with topology $\{ \varnothing, \{ \ast \}, \{ a, b \}, \{ \ast, a, b \} \}$. This represents the functor which sends a pointed topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $\{ \ast, a \} \rightrightarrows I$ on the discrete space $\{ \ast, a \}$, where the maps are $\ast \mapsto \ast, a \mapsto a$ and $\ast \mapsto \ast, a \mapsto b$, respectively. However, this cannot be effective: if we have $h : Z \to \{ \ast, a \}$ which equalizes the cocongruence, then $h$ must be the constant function with value $\ast$. But that means the cokernel pair of $h$ is the discrete space on $\{ \ast, a, b \}$.'
references:
- Top_no_effective_cocongruences
diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml
index 8eb4cee3b..fc884d013 100644
--- a/database/data/categories/Unif.yaml
+++ b/database/data/categories/Unif.yaml
@@ -121,16 +121,16 @@ unsatisfied_properties:
proof: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to \Unif$ which equips a set $X$ with the indiscrete uniform structure having $X \times X$ as its only entourage. This functor is right adjoint to the forgetful functor and therefore preserves cofiltered limits.
- property: effective cocongruences
- proof: 'The proof is very similar to $\Top$. Consider the indiscrete uniform space $I$ on two points whose only entourage is $I \times I$. This represents the functor which maps a uniform space $X$ to the set of pairs of points $(x,y) \in X$ that are indistinguishable, i.e. every entourage of $X$ contains $(x,y)$. This is an equivalence relation on $X$. Therefore, we get a cocongruence $1 \rightrightarrows I$, where the maps are the two possible functions. However, this cannot be effective: If a uniform map $h : Z \to 1$ equalizes the two maps, then $Z$ must be empty. But that means the cokernel pair of $h$ is the discrete uniform space on two points.'
+ proof: 'The proof is very similar to $\Top$. Consider the indiscrete uniform space $I$ on two points whose only entourage is $I \times I$. This represents the functor which maps a uniform space $X$ to the set of pairs of points $(x,y) \in X$ that are indistinguishable, i.e. every entourage of $X$ contains $(x,y)$. This is an equivalence relation on $X$. Therefore, we get a cocongruence $\{\ast\} \rightrightarrows I$, where the maps are the two possible functions. However, this cannot be effective: If a uniform map $h : Z \to \{\ast\}$ equalizes the two maps, then $Z$ must be empty. But that means the cokernel pair of $h$ is the discrete uniform space on two points.'
references:
- Top_no_effective_cocongruences
- property: parametrized natural numbers object
proof: >-
- We equip $[0,1]$ with the usual metric, which induces a uniform structure in the usual way: for $\varepsilon > 0$, we have the basic entourage $U_{\varepsilon} \coloneqq \{(r,s) \in [0,1]^2 : |r-s| < \varepsilon\}$. We equip the set $\IN$ with the discrete uniform structure (i.e., every reflexive relation is an entourage). This uniform space is isomorphic to the coproduct of one-point spaces $\coprod_{n \in \IN} 1$.
+ We equip $[0,1]$ with the usual metric, which induces a uniform structure in the usual way: for $\varepsilon > 0$, we have the basic entourage $U_{\varepsilon} \coloneqq \{(r,s) \in [0,1]^2 : |r-s| < \varepsilon\}$. We equip the set $\IN$ with the discrete uniform structure (i.e., every reflexive relation is an entourage). This uniform space is isomorphic to the coproduct of one-point spaces $\coprod_{n \in \IN} \{\ast\}$.
If there were a parametrized natural numbers object, then by Lemma 4 here, the canonical map
- $$\textstyle\coprod_{n \in \IN} [0,1] \to [0,1] \times \coprod_{n \in \IN} 1 \cong [0,1] \times \IN$$
+ $$\textstyle\coprod_{n \in \IN} [0,1] \to [0,1] \times \coprod_{n \in \IN} \{\ast\} \cong [0,1] \times \IN$$
would be an isomorphism.
Choose any sequence of positive numbers $\varepsilon_n > 0$ converging to $0$. Then $\coprod_{n \in \IN} U_{\varepsilon_n}$ is an entourage of $\coprod_{n \in \IN} [0,1]$. Its image in $[0,1] \times \IN$ consists of all $((r,n),(s,m))$ such that $n=m$ and $|r-s| < \varepsilon_n$. Assume, for a contradiction, that this set is an entourage of the product. Then it contains $(p_1 \times p_1)^*(U_\delta) \cap (p_2 \times p_2)^*(\Delta_{\IN})$ for some $\delta > 0$. In other words, $|r-s| < \delta$ implies $|r-s| < \varepsilon_n$ for all $n \in \IN$ and $r,s \in [0,1]$. Taking $s=0$ and $r=\delta/2$, we see that the sequence $(\varepsilon_n)$ is bounded below by $\delta/2$, contradicting the assumption that it converges to $0$.
diff --git a/database/data/categories/Z.yaml b/database/data/categories/Z.yaml
index a170d7d80..763106270 100644
--- a/database/data/categories/Z.yaml
+++ b/database/data/categories/Z.yaml
@@ -54,7 +54,7 @@ unsatisfied_properties:
proof: See MO/390611 for example.
- property: cartesian closed
- proof: 'There are functors $F,G : \CRing \rightrightarrows \Set$ such that $\Hom(F,G)$ is not essentially small; see MO/390611 for example. Now if the exponential $[F,G] : \CRing \to \Set$ exists, we get $[F,G](\IZ) \cong \Hom(\Hom(\IZ,-),[F,G])$ by Yoneda, which simplifies to $\Hom(1,[F,G]) \cong \Hom(1 \times F,G) \cong \Hom(F,G)$, a contradiction.'
+ proof: 'There are functors $F,G : \CRing \rightrightarrows \Set$ such that $\Hom(F,G)$ is not essentially small; see MO/390611 for example. Now if the exponential $[F,G] : \CRing \to \Set$ exists, we get $[F,G](\IZ) \cong \Hom(\Hom(\IZ,-),[F,G])$ by Yoneda. Since $\Hom(\IZ,-)$ is the terminal object $T$, this simplifies to $\Hom(T,[F,G]) \cong \Hom(T \times F,G) \cong \Hom(F,G)$, a contradiction.'
- property: cofiltered-limit-stable epimorphisms
proof: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to [\CRing, \Set]$ that maps a set to its constant functor.
diff --git a/database/data/categories/cocompletion-discrete-pair-join.yaml b/database/data/categories/cocompletion-discrete-pair-join.yaml
index 2759656ed..8331d8ce4 100644
--- a/database/data/categories/cocompletion-discrete-pair-join.yaml
+++ b/database/data/categories/cocompletion-discrete-pair-join.yaml
@@ -46,7 +46,7 @@ satisfied_properties:
label: cocompletion-discrete-pair-join_terminal_presheaf_small
proof: >-
It suffices to check that the terminal presheaf is small. This follows immediately from the description of small presheaves, since in fact, for every set $X$, the diagram
- $$1 ~\overset{f^*}{\underset{g^*}{\rightrightarrows}}~ 1 \xrightarrow{u_X^*} 1$$
+ $$\{\ast\} ~\overset{f^*}{\underset{g^*}{\rightrightarrows}}~ \{\ast\} \xrightarrow{u_X^*} \{\ast\}$$
is a coequalizer diagram. Alternatively, one can easily check that the terminal presheaf is a coequalizer of $f_*,g_* : \Hom(-,A) \rightrightarrows \Hom(-,B)$, which directly implies that it is small.
- property: epi-regular
@@ -83,7 +83,7 @@ unsatisfied_properties:
- property: well-powered
references:
- cocompletion-discrete-pair-join_terminal_presheaf_small
- proof: We already know that the terminal presheaf $1$ is small. For every set $X$, the unique morphism $\Hom(-,X) \to 1$ is a monomorphism since $X$ is subterminal in $\C$ (in fact, any morphism with codomain $X$ is the identity). For different sets $X,X'$ we have $\Hom(-,X) \not\cong \Hom(-,X')$ since there is not even a morphism $X \to X'$ in $\C$. This shows that $\Sub(1)$ is not essentially small.
+ proof: We already know that the terminal presheaf $T$ is small. For every set $X$, the unique morphism $\Hom(-,X) \to T$ is a monomorphism since $X$ is subterminal in $\C$ (in fact, any morphism with codomain $X$ is the identity). For different sets $X,X'$ we have $\Hom(-,X) \not\cong \Hom(-,X')$ since there is not even a morphism $X \to X'$ in $\C$. This shows that $\Sub(T)$ is not essentially small.
- property: well-copowered
proof: >-
@@ -157,7 +157,7 @@ unsatisfied_properties:
# - property: cofiltered-limit-stable epimorphisms
# references:
# - cocompletion-discrete-pair-join_terminal_presheaf_small
- # proof: We already know that the terminal presheaf $1$ is small. Now consider for $n \in \IN$ the copower $\IN_{\geq n} \otimes 1$ and for $n < m$ the morphism $\IN_{\geq m} \otimes 1 \to \IN_{\geq n} \otimes 1$ induced by the inclusion $\IN_{\geq m} \subseteq \IN_{\geq n}$. This sequence has a limit, the empty presheaf; this can easily be deduced from $\bigcap_{n \in \IN} \IN_{\geq n} = \varnothing$ in $\IN$. Therefore, the unique morphisms $\IN_{\geq n} \otimes 1 \to 1$ are epimorphisms, but their limit $0 \to 1$ is not.
+ # proof: We already know that the terminal presheaf $T$ is small. Now consider for $n \in \IN$ the copower $\IN_{\geq n} \otimes T$ and for $n < m$ the morphism $\IN_{\geq m} \otimes T \to \IN_{\geq n} \otimes T$ induced by the inclusion $\IN_{\geq m} \subseteq \IN_{\geq n}$. This sequence has a limit, the empty presheaf; this can easily be deduced from $\bigcap_{n \in \IN} \IN_{\geq n} = \varnothing$ in $\IN$. Therefore, the unique morphisms $\IN_{\geq n} \otimes T \to T$ are epimorphisms, but their limit, the morphism from the empty presheaf to $T$, is not.
- property: concretizable
proof: >-
@@ -171,9 +171,9 @@ unsatisfied_properties:
special_objects:
initial object:
- description: constant presheaf with value $0$
+ description: constant presheaf with value $\varnothing$
terminal object:
- description: constant presheaf with value $1$
+ description: constant presheaf with value $\{\ast\}$
coproducts:
description: objectwise defined disjoint union of presheaves
diff --git a/database/data/categories/forked_commutative_square.yaml b/database/data/categories/forked_commutative_square.yaml
index 4f3000855..baaf8afd0 100644
--- a/database/data/categories/forked_commutative_square.yaml
+++ b/database/data/categories/forked_commutative_square.yaml
@@ -59,15 +59,15 @@ satisfied_properties:
$$\textstyle L : \ForkSquare^{\op} \to \Set, \, X \mapsto \lim_{i \in \I} \Hom(X,F(i))$$
is representable.
- Since $A$ is initial and $\I$ is connected, we have $L(A)=1$ (the singleton set).
+ Since $A$ is initial and $\I$ is connected, we have $L(A)=\{\ast\}$.
- Case 1: $F$ hits $A$. Then $L(X)= \varnothing$ for every $X \neq A$, since it maps to $\Hom(X,A) = \varnothing$. Moreover, we have $L(A)=1$. Therefore, $L \cong \Hom(-,A)$.
+ Case 1: $F$ hits $A$. Then $L(X)= \varnothing$ for every $X \neq A$, since it maps to $\Hom(X,A) = \varnothing$. Moreover, we have $L(A)=\{\ast\}$. Therefore, $L \cong \Hom(-,A)$.
Case 2: $F$ hits $B$, but does not hit $A$. We claim that $F$ then does not hit $C$. In fact, if $F(i)=B$ and $F(j)=C$, since $\I$ is cosifted, there is a span
$$i \leftarrow k \rightarrow j,$$
which induces a span
$$B \leftarrow F(k) \rightarrow C.$$
- But then $F(k)=A$ is forced, contradicting our assumption that $F$ does not hit $A$. Therefore, $F$ takes values in $\{B,D,E\}$. Since $B$ has a unique morphism to each of these objects and $\I$ is connected, we see that $L(B)=1$. Moreover, we have $L(C)=\varnothing$ since it maps to $\Hom(C,B)=\varnothing$, and for the same reason we have $L(D)=\varnothing$ and $L(E)=\varnothing$. From these values, it is clear that $L \cong \Hom(-,B)$. (There is a bijection for each object, and naturality is automatic since we are only dealing with sets with at most one element.)
+ But then $F(k)=A$ is forced, contradicting our assumption that $F$ does not hit $A$. Therefore, $F$ takes values in $\{B,D,E\}$. Since $B$ has a unique morphism to each of these objects and $\I$ is connected, we see that $L(B)=\{\ast\}$. Moreover, we have $L(C)=\varnothing$ since it maps to $\Hom(C,B)=\varnothing$, and for the same reason we have $L(D)=\varnothing$ and $L(E)=\varnothing$. From these values, it is clear that $L \cong \Hom(-,B)$. (There is a bijection for each object, and naturality is automatic since we are only dealing with sets with at most one element.)
Case 3: $F$ hits $C$, but does not hit $A$. This is symmetric to Case 2 and leads to $L \cong \Hom(-,C)$. In fact, there is an automorphism of $\ForkSquare$ that swaps $B$ and $C$.
@@ -75,7 +75,7 @@ satisfied_properties:
Case 5: $F$ takes values in $\{D,E\}$ and hits $D$. In this case, we will show that $L \cong \Hom(-,D)$. Choose $i_0 \in \I$ with
$$F(i_0)=D.$$
- Since there is no morphism $E \to D = F(i_0)$, we have $L(E) = \varnothing$. We already know $L(A)=1$. Since $B$ has a unique morphism to each value of $F$ and $\I$ is connected, we see that $L(B)=1$. For the same reason, we have $L(C)=1$. Therefore, it remains to show that $L(D)=1$.
+ Since there is no morphism $E \to D = F(i_0)$, we have $L(E) = \varnothing$. We already know $L(A)=\{\ast\}$. Since $B$ has a unique morphism to each value of $F$ and $\I$ is connected, we see that $L(B)=\{\ast\}$. For the same reason, we have $L(C)=\{\ast\}$. Therefore, it remains to show that $L(D)=\{\ast\}$.
We first show that $L(D)$ has at most one element. Assume that $x,y \in L(D)$. For every $i \in \I$ we have morphisms $x_i,y_i : D \rightrightarrows F(i)$. Since $D$ has only one endomorphism, namely the identity, we must have $x_{i_0} = \id_D = y_{i_0}$. Since $\I$ is connected, it therefore remains to show that
$$x_i = y_i \iff x_j = y_j$$
diff --git a/database/data/categories/omega-Set.yaml b/database/data/categories/omega-Set.yaml
index 8caf6addc..407877fe9 100644
--- a/database/data/categories/omega-Set.yaml
+++ b/database/data/categories/omega-Set.yaml
@@ -41,7 +41,7 @@ satisfied_properties:
proof: If $(X, R_X) \twoheadrightarrow (Y, R_Y)$ is an epimorphism, then by the description below, this implies the underlying function $X \to Y$ is surjective. Therefore, if $E$ is the kernel pair of this underlying function, then we can find an equivalent quotient object $(X / E, R_{X / E})$ by transporting $R_X$ to $X / E$. The collection of possible equivalence relations $E$ is then small, and for each $E$, the collection of possible $R_{X / E}$ is also small.
- property: terminal object
- proof: 'The $\omega$-set $\nabla 1 = (1, \IN \times 1)$ is terminal, since $\nabla$ is a right adjoint and therefore preserves terminal objects.'
+ proof: 'The $\omega$-set $\nabla \{\ast\} = (\{\ast\}, \IN \times \{\ast\})$ is terminal, since $\nabla$ is a right adjoint and therefore preserves terminal objects.'
check_redundancy: false
- property: binary products
@@ -124,7 +124,7 @@ satisfied_properties:
- property: regular subobject classifier
proof: >-
- We claim that $\Omega \coloneqq \nabla 2 = (2, \IN \times 2)$ is a regular subobject classifier, with $\top : 1 \to \Omega$ being the morphism whose underlying set function is $0 \mapsto 1$. To see this, note that from the construction of equalizers above, any regular subobject of $(X, R_X)$ is equivalent to $(X', R_X \cap (\IN \times X'))$ for some $X' \subseteq X$. It is then straightforward to check that the characteristic function $\chi_{X'} : X \to 2$ induces a morphism $(X, R_X) \to \Omega$, and that $(X', R_X \cap (\IN \times X'))$ is also the pullback of $\chi_{X'}$ and $\top$. For the uniqueness of $\chi_{X'}$, observe that for each morphism $\chi : X \to \Omega$, the pullback of $\chi$ and $\top$ has underlying set $\chi^*(\{ 1 \})$ and the morphism to $(X, R_X)$ is the inclusion map. Thus, each morphism $\chi : (X, R_X) \to \Omega$ induces a distinct subobject of $X$ as the pullback of $\chi$ and $\top$.
+ We claim that $\Omega \coloneqq \nabla \{0,1\} = (\{0,1\}, \IN \times \{0,1\})$ is a regular subobject classifier, with $\top : \nabla \{\ast\} \to \Omega$ being the morphism whose underlying set function is $\ast \mapsto 1$. To see this, note that from the construction of equalizers above, any regular subobject of $(X, R_X)$ is equivalent to $(X', R_X \cap (\IN \times X'))$ for some $X' \subseteq X$. It is then straightforward to check that the characteristic function $\chi_{X'} : X \to \{0,1\}$ induces a morphism $(X, R_X) \to \Omega$, and that $(X', R_X \cap (\IN \times X'))$ is also the pullback of $\chi_{X'}$ and $\top$. For the uniqueness of $\chi_{X'}$, observe that for each morphism $\chi : X \to \Omega$, the pullback of $\chi$ and $\top$ has underlying set $\chi^*(\{ 1 \})$ and the morphism to $(X, R_X)$ is the inclusion map. Thus, each morphism $\chi : (X, R_X) \to \Omega$ induces a distinct subobject of $X$ as the pullback of $\chi$ and $\top$.
- property: disjoint finite coproducts
proof: >-
@@ -137,7 +137,7 @@ satisfied_properties:
which is empty since the images of $\iota_1$ and $\iota_2$ are disjoint. Since the realization relation of an $\omega$-set is a subset of $\IN$ times its underlying set, the realization relation of the pullback is empty as well. Hence the pullback is the initial object $(\varnothing, \varnothing)$ constructed above.
- property: generator
- proof: The terminal object $(1, \IN \times 1)$ represents the forgetful functor $\omegaSet \to \Set$ which is clearly faithful. (For the non-trivial direction of the isomorphism between $\Hom_{\omegaSet}((1, \IN \times 1), (X, R_X))$ and $X$, suppose we have $x \in X$. Then there exists $n \in \IN$ such that $n$ realizes $x$; therefore, the total recursive function given by the constant function with image $n$ forms a realizer tracker compatible with the corresponding function $1 \to X$.)
+ proof: The terminal object $(\{\ast\}, \IN \times \{\ast\})$ represents the forgetful functor $\omegaSet \to \Set$ which is clearly faithful. (For the non-trivial direction of the isomorphism between $\Hom_{\omegaSet}((\{\ast\}, \IN \times \{\ast\}), (X, R_X))$ and $X$, suppose we have $x \in X$. Then there exists $n \in \IN$ such that $n$ realizes $x$; therefore, the total recursive function given by the constant function with image $n$ forms a realizer tracker compatible with the corresponding function $\{\ast\} \to X$.)
- property: extremal generating collection
proof: >-
@@ -155,15 +155,15 @@ satisfied_properties:
- property: extremal cogenerator
proof: >-
- We first claim that $\nabla 2$ and $(P(\IN) \setminus \{ \varnothing \}, {\in}_{\IN})$ form an extremal cogenerating collection. To see this, we first consider morphisms to the first member $\nabla 2$ of the family. Note that
- $$\Hom_{\omegaSet}({-}, \nabla 2) \cong \Hom_{\Set}(U{-}, 2),$$
- where $U : \omegaSet \to \Set$ is the forgetful functor. Therefore, $\Hom_{\omegaSet}({-}, \nabla 2)$ is isomorphic to the composition of $U$ and the power set functor $P : \Set^{\op} \to \Set$, both of which are faithful. This shows that $\nabla 2$ is a cogenerator, so the collection is also a cogenerating collection.
+ We first claim that $\nabla \{0,1\}$ and $(P(\IN) \setminus \{ \varnothing \}, {\in}_{\IN})$ form an extremal cogenerating collection. To see this, we first consider morphisms to the first member $\nabla \{0,1\}$ of the family. Note that
+ $$\Hom_{\omegaSet}({-}, \nabla \{0,1\}) \cong \Hom_{\Set}(U{-}, \{0,1\}),$$
+ where $U : \omegaSet \to \Set$ is the forgetful functor. Therefore, $\Hom_{\omegaSet}({-}, \nabla \{0,1\})$ is isomorphic to the composition of $U$ and the power set functor $P : \Set^{\op} \to \Set$, both of which are faithful. This shows that $\nabla \{0,1\}$ is a cogenerator, so the collection is also a cogenerating collection.
To show the collection is an extremal cogenerating collection, suppose we have a morphism $f : (X, R_X) \to (Y, R_Y)$ such that ${-} \circ f$ induces bijections of morphism sets to both members of the collection. From the first assumption that
- $${-} \circ f : \Hom((Y, R_Y), \nabla 2) \to \Hom((X, R_X), \nabla 2)$$
+ $${-} \circ f : \Hom((Y, R_Y), \nabla \{0,1\}) \to \Hom((X, R_X), \nabla \{0,1\})$$
is a bijection, we see that
- $${-} \circ f : \Hom_{\Set}(Y, 2) \to \Hom_{\Set}(X, 2)$$
- is a bijection. Since $2$ is an extremal cogenerator of $\Set$, we conclude that the underlying function of $f$ is a bijection.
+ $${-} \circ f : \Hom_{\Set}(Y, \{0,1\}) \to \Hom_{\Set}(X, \{0,1\})$$
+ is a bijection. Since $\{0,1\}$ is an extremal cogenerator of $\Set$, we conclude that the underlying function of $f$ is a bijection.
Now, consider the morphism
$$g : (X, R_X) \to (P(\IN) \setminus \{ \varnothing \}, {\in}_{\IN})$$
@@ -171,14 +171,14 @@ satisfied_properties:
$$h : (Y, R_Y) \to (P(\IN) \setminus \{ \varnothing \}, {\in}_{\IN})$$
such that $g = h \circ f$. Choose a compatible realizer tracker $\code{h} : \IN \dashrightarrow \IN$. Then for any $x\in X$, if $n$ realizes $f(x)$, then $\code{h}(n)$ exists and $\code{h}(n)$ realizes $h(f(x)) = g(x)$. Thus, by definition of $g$, $\code{h}(n)$ is in the set of realizers of $x$, i.e. $\code{h}(n)$ realizes $x$. From the characterization of isomorphisms below, this implies that $f$ is an isomorphism.
- Finally, since $\nabla 2$ and $(P(\IN) \setminus \{ \varnothing \}, {\in}_{\IN})$ both have non-empty underlying sets, they form a strongly connected family (see the proof above that $\omegaSet$ is semi-strongly connected). Therefore, by this result, the product of these two objects is an extremal cogenerator.
+ Finally, since $\nabla \{0,1\}$ and $(P(\IN) \setminus \{ \varnothing \}, {\in}_{\IN})$ both have non-empty underlying sets, they form a strongly connected family (see the proof above that $\omegaSet$ is semi-strongly connected). Therefore, by this result, the product of these two objects is an extremal cogenerator.
references:
- omega_Set_ssc
- Set_extremal_cogenerator
- property: parametrized natural numbers object
proof: >-
- We claim that $N \coloneqq (\IN, \Delta_{\IN})$, where $\Delta_{\IN}$ is the diagonal, is a parametrized natural numbers object. (In other words, the realization relation is that $m$ realizes $n$ if and only if $m = n$.) First, the zero function $z : 1 \to \IN$ and the successor function $s : \IN \to \IN$ clearly induce morphisms of $\omega$-sets $z : 1 \to N$ and $s : N \to N$. Now, suppose we have $f : (A, R_A) \to (X, R_X)$ and $g : (X, R_X) \to (X, R_X)$. Choose compatible realizer trackers $\code{f}, \code{g} : \IN \dashrightarrow \IN$. Also, let $\Phi : A \times \IN \to X$ be the function $(a, n) \mapsto g^n(f(a))$. Then since the collection of partial recursive functions is closed under primitive recursion, we can also construct a partial recursive function $\code{\Phi}$ such that
+ We claim that $N \coloneqq (\IN, \Delta_{\IN})$, where $\Delta_{\IN}$ is the diagonal, is a parametrized natural numbers object. (In other words, the realization relation is that $m$ realizes $n$ if and only if $m = n$.) First, the zero function $z : \{\ast\} \to \IN$ and the successor function $s : \IN \to \IN$ clearly induce morphisms of $\omega$-sets $z : \nabla \{\ast\} \to N$ and $s : N \to N$. Now, suppose we have $f : (A, R_A) \to (X, R_X)$ and $g : (X, R_X) \to (X, R_X)$. Choose compatible realizer trackers $\code{f}, \code{g} : \IN \dashrightarrow \IN$. Also, let $\Phi : A \times \IN \to X$ be the function $(a, n) \mapsto g^n(f(a))$. Then since the collection of partial recursive functions is closed under primitive recursion, we can also construct a partial recursive function $\code{\Phi}$ such that
$$\code{\Phi}(\langle b, 0 \rangle) = \code{f}(b)$$
and
$$\code{\Phi}(\langle b, n+1 \rangle) = \code{g}(\code{\Phi}(\langle b, n \rangle)).$$
@@ -196,7 +196,7 @@ unsatisfied_properties:
- property: locally finite
proof: >-
The right adjoint $\nabla : \Set \to \omegaSet$ to the forgetful functor is fully faithful. Therefore, for example,
- $$\Hom_{\omegaSet}(\nabla 1, \nabla \IN) \cong \Hom_{\Set}(1, \IN)$$
+ $$\Hom_{\omegaSet}(\nabla \{\ast\}, \nabla \IN) \cong \Hom_{\Set}(\{\ast\}, \IN)$$
is infinite.
- property: balanced
@@ -205,7 +205,7 @@ unsatisfied_properties:
- property: co-Malcev
proof: >-
- Consider the two possible morphisms $j_1, j_2 : \nabla 1 \rightrightarrows \nabla 2$. This defines a corelation representing the functor which to $(X, R_X)$ assigns the binary relation on $X$ of two elements having a common realizer. That shows that this corelation is coreflexive, since by definition any element of an $\omega$-set has a realizer. However, it is easy to see that it is not cotransitive; for example, in the $\omega$-set
+ Consider the two possible morphisms $j_1, j_2 : \nabla \{\ast\} \rightrightarrows \nabla \{0,1\}$. This defines a corelation representing the functor which to $(X, R_X)$ assigns the binary relation on $X$ of two elements having a common realizer. That shows that this corelation is coreflexive, since by definition any element of an $\omega$-set has a realizer. However, it is easy to see that it is not cotransitive; for example, in the $\omega$-set
$$\bigl(\{0,1,2\}, \{ (0, 0), (0, 1), (1, 1), (1, 2) \}\bigr),$$
the elements $0$ and $1$ have a common realizer, as do $1$ and $2$; but $0$ and $2$ do not have a common realizer.
@@ -213,8 +213,8 @@ unsatisfied_properties:
proof: >-
Let $N \coloneqq (\IN, \Delta_{\IN})$ be the natural numbers object. Then for any $\omega$-set $(X, R_X)$, we claim $\Hom_{\omegaSet}((X, R_X), N)$ is countable. This follows from the fact that any unary partial recursive function $\varphi : \IN \dashrightarrow \IN$ can be a compatible realizer tracker for at most one function $f : X \to \IN$, since any $x\in X$ is realized by some $n\in \IN$, and then we must have that $\varphi(n)$ is defined and $f(x) = \varphi(n)$. Therefore, we get a surjective function from a subset of the unary partial recursive functions to $\Hom_{\omegaSet}((X, R_X), N)$.
- From this, we see that for every infinite set $S$, there is no $S$-indexed copower of $1$, since if $(X, R_X)$ were such a copower, we would have
- $$\textstyle\Hom_{\omegaSet}((X, R_X), N) \cong \prod_{s \in S} \Hom_{\omegaSet}(1, N) \cong \IN^S,$$
+ From this, we see that for every infinite set $S$, there is no $S$-indexed copower of $\nabla \{\ast\}$, since if $(X, R_X)$ were such a copower, we would have
+ $$\textstyle\Hom_{\omegaSet}((X, R_X), N) \cong \prod_{s \in S} \Hom_{\omegaSet}(\nabla \{\ast\}, N) \cong \IN^S,$$
which is uncountable.
check_redundancy: false
@@ -222,7 +222,7 @@ unsatisfied_properties:
proof: >-
Let $N \coloneqq (\IN, \Delta_{\IN})$ be the natural numbers object. For any $\omega$-set $(X, R_X)$ with a sequence of morphisms $f_n : (X, R_X) \to N$, we can define a function $g : X \to \IN^{\IN}$ which sends $x \in X$ to the sequence $(f_n(x))_{n\in \IN}$. We claim that $g$ has countable image. To see this, choose realizer trackers $\code{f_n} : \IN \dashrightarrow \IN$ compatible with $f_n$. Now let $x \in X$. Then there exists $m \in \IN$ such that $m$ realizes $x$. It follows that $\code{f_n}(m)$ is defined and $\code{f_n}(m) = f_n(x)$ for each $n$. Therefore, the image of $g$ is contained in the set of sequences $(\code{f_n}(m))_{n\in \IN}$ where $m \in \IN$ is such that $\code{f_n}(m)$ is defined for each $n$.
- From this, we see that there is no $\IN$-indexed power of $N$. Suppose $(X, R_X)$ were such a power, with projections $p_n : (X, R_X) \to N$, and let $g : X \to \IN^{\IN}$ be the function associated to $(p_n)_{n \in \IN}$ as above. For any sequence $(a_n) \in \IN^{\IN}$, the morphisms $a_n : 1 \to N$ induce a morphism $1 \to (X, R_X)$, that is, an element $x \in X$ with $p_n(x) = a_n$ for all $n$. Then $g(x) = (a_n)$. Thus, $g$ is surjective, which contradicts the countability of its image, since $\IN^{\IN}$ is uncountable.
+ From this, we see that there is no $\IN$-indexed power of $N$. Suppose $(X, R_X)$ were such a power, with projections $p_n : (X, R_X) \to N$, and let $g : X \to \IN^{\IN}$ be the function associated to $(p_n)_{n \in \IN}$ as above. For any sequence $(a_n) \in \IN^{\IN}$, the morphisms $a_n : \nabla \{\ast\} \to N$ induce a morphism $\nabla \{\ast\} \to (X, R_X)$, that is, an element $x \in X$ with $p_n(x) = a_n$ for all $n$. Then $g(x) = (a_n)$. Thus, $g$ is surjective, which contradicts the countability of its image, since $\IN^{\IN}$ is uncountable.
- property: ℵ₁-filtered colimits
proof: >-
@@ -290,7 +290,7 @@ special_objects:
initial object:
description: $(\varnothing, \varnothing)$
terminal object:
- description: $(1, \IN \times 1)$
+ description: $(\{\ast\}, \IN \times \{\ast\})$
coproducts:
description: '[binary case] The binary coproduct of $(X, R_X)$ and $(Y, R_Y)$ is $X \sqcup Y$ with realization relation $$R_{X\sqcup Y} \coloneqq \{ (2n, x) \mid (n, x) \in R_X \} \cup \{ (2n+1, y) \mid (n, y) \in R_Y \}.$$'
products:
@@ -302,7 +302,7 @@ special_morphisms:
proof: This is easy, since the condition on the existence of $\psi$ just says that the set-level inverse of $f$ is also a morphism in $\omegaSet$.
monomorphisms:
description: Morphisms of $\omega$-sets whose underlying set function is injective
- proof: This follows from the fact that the forgetful functor $\omegaSet \to \Set$ is clearly faithful, and it is representable by the terminal object $(1, \IN \times 1)$.
+ proof: This follows from the fact that the forgetful functor $\omegaSet \to \Set$ is clearly faithful, and it is representable by the terminal object $(\{\ast\}, \IN \times \{\ast\})$.
regular monomorphisms:
description: 'A morphism $f : (X, R_X) \to (Y, R_Y)$ is a regular monomorphism if and only if the underlying function $X \to Y$ is injective, and there exists a partial recursive function $\psi : \IN \dashrightarrow \IN$ such that whenever we have $n\in \IN$ and $x\in X$ such that $n$ realizes $f(x) \in Y$, then $\psi(n)$ exists and $\psi(n)$ realizes $x\in X$'
proof: 'Following the constructions above, we can see that for any morphism $f : (X, R_X) \to (Y, R_Y)$, the equalizer of the cokernel pair of $f$ is $(\im(f), R_Y \cap (\IN \times \im(f)))$; and the condition above is equivalent to the condition that the canonical map $X \to \im(f)$ induces an isomorphism of $\omega$-sets $(X, R_X) \to (\im(f), R_Y \cap (\IN \times \im(f)))$.'
diff --git a/database/data/categories/sSet.yaml b/database/data/categories/sSet.yaml
index 07f4019f6..e8b1cdff7 100644
--- a/database/data/categories/sSet.yaml
+++ b/database/data/categories/sSet.yaml
@@ -42,7 +42,7 @@ special_objects:
initial object:
description: simplicial set $X$ with $X_n = \varnothing$
terminal object:
- description: simplicial set $X$ with $X_n = 1$
+ description: simplicial set $X$ with $X_n = \{\ast\}$
coproducts:
description: pointwise disjoint union
products:
diff --git a/database/data/category-implications/generators.yaml b/database/data/category-implications/generators.yaml
index f99c81e31..e3d5aa1a1 100644
--- a/database/data/category-implications/generators.yaml
+++ b/database/data/category-implications/generators.yaml
@@ -62,7 +62,7 @@
- one-sorted finitary algebraic
conclusions:
- extremal generator
- proof: Pick an algebraic theory that represents the category. The free algebra $F(1)$ on one generator is an extremal generator since it represents the underlying set functor, which is faithful and conservative.
+ proof: Pick an algebraic theory that represents the category. The free algebra $F(\{\ast\})$ on one generator is an extremal generator since it represents the underlying set functor, which is faithful and conservative.
- id: locally-finite_left-cancellative_semi-strongly-connected_extremal-generating-set
assumptions:
diff --git a/database/data/functor-implications/adjoints.yaml b/database/data/functor-implications/adjoints.yaml
index ed65a6a76..19c1de577 100644
--- a/database/data/functor-implications/adjoints.yaml
+++ b/database/data/functor-implications/adjoints.yaml
@@ -48,7 +48,7 @@
- trivial
conclusions:
- coreflector
- proof: 'Let $F : \C \to 1$ be the unique functor into the trivial category, and assume that $\C$ has an initial object $X$. Then the constant functor $X : 1 \to \C$ is fully faithful and left adjoint to $F$ because $\Hom(X(*),Y) \cong * \cong \Hom(*,F(Y))$.'
+ proof: 'Let $F : \C \to \1$ be the unique functor into the trivial category, and assume that $\C$ has an initial object $X$. Then the constant functor $X : \1 \to \C$ is fully faithful and left adjoint to $F$ because $\Hom(X(*),Y) \cong * \cong \Hom(*,F(Y))$.'
- id: reflector_preserves_terminal_objects
assumptions:
diff --git a/database/data/functor-implications/limits preservation.yaml b/database/data/functor-implications/limits preservation.yaml
index 374cb021d..306ace84e 100644
--- a/database/data/functor-implications/limits preservation.yaml
+++ b/database/data/functor-implications/limits preservation.yaml
@@ -220,7 +220,7 @@
- trivial
conclusions:
- continuous
- proof: 'We need to show that for every category $\C$ the unique functor $!_{\C} : \C \to 1$ into the trivial category is continuous. This is easy to verify directly because in the trivial category every limit is, well, trivial. More generally, for every category $\C$ and every set $S$ the diagonal functor $\Delta : \C \to \C^S$ is continuous. Here we apply this to $S = \varnothing$ so that $\C^S$ is the trivial category.'
+ proof: 'We need to show that for every category $\C$ the unique functor $!_{\C} : \C \to \1$ into the trivial category is continuous. This is easy to verify directly because in the trivial category every limit is, well, trivial. More generally, for every category $\C$ and every set $S$ the diagonal functor $\Delta : \C \to \C^S$ is continuous. Here we apply this to $S = \varnothing$ so that $\C^S$ is the trivial category.'
- id: automatically_preserve_equalizers
assumptions: []
diff --git a/database/data/functor-implications/misc.yaml b/database/data/functor-implications/misc.yaml
index 86cf97da0..432ce438d 100644
--- a/database/data/functor-implications/misc.yaml
+++ b/database/data/functor-implications/misc.yaml
@@ -110,7 +110,7 @@
- trivial
conclusions:
- right-invertible
- proof: 'Let $\C$ be an inhabited category and let $F : \C \to 1$ be the unique functor to the trivial category. Choose any object $X \in \C$. Then the constant functor $X : 1 \to \C$ satisfies $F \circ X = \id_1$.'
+ proof: 'Let $\C$ be an inhabited category and let $F : \C \to \1$ be the unique functor to the trivial category. Choose any object $X \in \C$. Then the constant functor $X : \1 \to \C$ satisfies $F \circ X = \id_{\1}$.'
- id: full_functor_to_trivial_category
# TODO: add the converse once we have category_conclusions
@@ -122,7 +122,7 @@
- trivial
conclusions:
- full
- proof: 'Let $\C$ be a strongly connected category. Then the unique functor $F : \C \to 1$ to the trivial category is full: for all $X,Y \in \C$ the map $\Hom(X,Y) \to \Hom(F(X),F(Y))$ is surjective since its domain is non-empty and its codomain is a singleton set.'
+ proof: 'Let $\C$ be a strongly connected category. Then the unique functor $F : \C \to \1$ to the trivial category is full: for all $X,Y \in \C$ the map $\Hom(X,Y) \to \Hom(F(X),F(Y))$ is surjective since its domain is non-empty and its codomain is a singleton set.'
- id: functor_conservative_on_groupoids
assumptions: []
diff --git a/database/data/functors/binary_coproduct_sets.yaml b/database/data/functors/binary_coproduct_sets.yaml
index 3806b6fd4..add60fa96 100644
--- a/database/data/functors/binary_coproduct_sets.yaml
+++ b/database/data/functors/binary_coproduct_sets.yaml
@@ -20,7 +20,7 @@ related:
satisfied_properties:
- property: right-invertible
- proof: The functor $\Set \to \Set \times \Set$, $X \mapsto (X,0)$ provides a right inverse since $X + 0 \cong X$.
+ proof: The functor $\Set \to \Set \times \Set$, $X \mapsto (X,\varnothing)$ provides a right inverse since $X + \varnothing \cong X$.
- property: preserves equalizers
proof: This can be checked with a straightforward calculation.
@@ -44,4 +44,4 @@ unsatisfied_properties:
proof: The canonical map $(X_1 \times X_2) + (Y_1 \times Y_2) \to (X_1 + Y_1) \times (X_2 + Y_2)$ is injective, but misses the "mixed terms" $X_1 \times Y_2$ and $Y_1 \times X_2$ in the codomain, hence is not surjective when $X_1,Y_2$ (or $Y_1,X_2$) are non-empty.
- property: essentially injective
- proof: Both $(1,0)$ and $(0,1)$ are mapped to $1$.
+ proof: Both $(\{\ast\},\varnothing)$ and $(\varnothing,\{\ast\})$ are mapped to $\{\ast\}$.
diff --git a/database/data/functors/binary_product_sets.yaml b/database/data/functors/binary_product_sets.yaml
index dff238106..707d93a42 100644
--- a/database/data/functors/binary_product_sets.yaml
+++ b/database/data/functors/binary_product_sets.yaml
@@ -20,7 +20,7 @@ related:
satisfied_properties:
- property: right-invertible
- proof: The functor $\Set \to \Set \times \Set$, $X \mapsto (X,1)$ provides a right inverse since $X \times 1 \cong X$.
+ proof: The functor $\Set \to \Set \times \Set$, $X \mapsto (X,\{\ast\})$ provides a right inverse since $X \times \{\ast\} \cong X$.
- property: preserves initial objects
proof: This is obvious.
@@ -44,7 +44,7 @@ unsatisfied_properties:
proof: 'If $f,g : A \rightrightarrows B$ are two maps, we always have $f \times \id_{\varnothing} = g \times \id_{\varnothing} : A \times \varnothing \rightrightarrows B \times \varnothing$.'
- property: essentially injective
- proof: Both $(1,0)$ and $(0,1)$ are mapped to $0$.
+ proof: Both $(\{\ast\},\varnothing)$ and $(\varnothing,\{\ast\})$ are mapped to $\varnothing$.
- property: preserves coequalizers
proof: 'Since the diagonal functor $\Delta : \Set \to \Set \times \Set$ preserves coequalizers (in fact, all colimits), it would follow that the composition $\Set \to \Set$, $X \mapsto X^2$ preserves coequalizers. But this is the squaring functor, of which we already know that it does not preserve coequalizers.'
diff --git a/database/data/functors/continuous_functions.yaml b/database/data/functors/continuous_functions.yaml
index ddeea2b27..29790ffff 100644
--- a/database/data/functors/continuous_functions.yaml
+++ b/database/data/functors/continuous_functions.yaml
@@ -34,8 +34,8 @@ unsatisfied_properties:
- property: full
proof: >-
Every continuous function $\omega_1 \to \IR$ is eventually constant, where $\omega_1$ denotes the first uncountable ordinal equipped with the order topology. We obtain a homomorphism
- $$\varphi : C(\omega_1) \to \IR \cong C(1)$$
- mapping each continuous function $\omega_1 \to \IR$ to its eventual value. Assume that it is induced by a continuous map $1 \to \omega_1$. This corresponds to an ordinal $\alpha < \omega_1$ such that $\varphi(u) = u(\alpha)$ for all $u \in C(\omega_1)$. But the continuous function
+ $$\varphi : C(\omega_1) \to \IR \cong C(\{\ast\})$$
+ mapping each continuous function $\omega_1 \to \IR$ to its eventual value. Assume that it is induced by a continuous map $\{\ast\} \to \omega_1$. This corresponds to an ordinal $\alpha < \omega_1$ such that $\varphi(u) = u(\alpha)$ for all $u \in C(\omega_1)$. But the continuous function
$$u(\beta) \coloneqq \begin{cases} 0 & \beta \leq \alpha \\ 1 & \beta > \alpha \end{cases}$$
satisfies $\varphi(u) = u(\alpha + 1) \neq u(\alpha)$.
diff --git a/database/data/functors/countable_copower_sets.yaml b/database/data/functors/countable_copower_sets.yaml
index 1dacb2ebe..8cbbb762e 100644
--- a/database/data/functors/countable_copower_sets.yaml
+++ b/database/data/functors/countable_copower_sets.yaml
@@ -36,7 +36,7 @@ satisfied_properties:
unsatisfied_properties:
- property: preserves terminal objects
- proof: We have $\IN \times 1 \cong \IN \not\cong 1$.
+ proof: We have $\IN \times \{\ast\} \cong \IN \not\cong \{\ast\}$.
- property: preserves binary products
proof: The canonical map $\IN \times (X \times Y) \to (\IN \times X) \times (\IN \times Y)$ is given by $(n,(x,y)) \mapsto ((n,x),(n,y))$. It is clearly not surjective when $X$ and $Y$ are non-empty.
diff --git a/database/data/functors/nerve.yaml b/database/data/functors/nerve.yaml
index d4dae2026..1366f1b6e 100644
--- a/database/data/functors/nerve.yaml
+++ b/database/data/functors/nerve.yaml
@@ -31,7 +31,7 @@ satisfied_properties:
unsatisfied_properties:
- property: preserves regular epimorphisms
proof: >-
- Consider the thin categories $\C = \{0 \to 1, \, 1' \to 2\}$ and $\D = \{0 \to 1 \to 2\}$. There is a regular epimorphism $P : \C \to \D$ that identifies $1$ with $1'$. In fact, it is the coequalizer of the two functors $\{*\} \rightrightarrows \C$ whose images are $1$ and $1'$, respectively.
+ Consider the thin categories $\C = \{0 \to 1, \, 1' \to 2\}$ and $\D = \{0 \to 1 \to 2\}$. There is a regular epimorphism $P : \C \to \D$ that identifies $1$ with $1'$. In fact, it is the coequalizer of the two functors $\{\ast\} \rightrightarrows \C$ whose images are $1$ and $1'$, respectively.
Notice that the map $\Mor(P) : \Mor(\C) \to \Mor(\D)$ is not surjective, as the morphism $0 \to 2$ in $\D$ has no preimage in $\C$. In other words, the map $N_1(P) : N_1(\C) \to N_1(\D)$ is not surjective. Therefore, $N(P)$ is not an epimorphism.
- property: dominant
diff --git a/database/data/functors/power_set_contravariant.yaml b/database/data/functors/power_set_contravariant.yaml
index 84eca828c..331d22c93 100644
--- a/database/data/functors/power_set_contravariant.yaml
+++ b/database/data/functors/power_set_contravariant.yaml
@@ -19,7 +19,7 @@ related:
satisfied_properties:
- property: representable
- proof: This is because there are natural bijections $P(X) \cong \Hom(X,2)$, sending a subset to its characteristic function.
+ proof: This is because there are natural bijections $P(X) \cong \Hom(X,\{0,1\})$, sending a subset to its characteristic function.
- property: conservative
proof: >-
@@ -71,7 +71,7 @@ unsatisfied_properties:
proof: Consider the sequence of truncation maps $\cdots \twoheadrightarrow \{0,1\}^2 \twoheadrightarrow \{0,1\}^1$. Its limit in $\Set$ (i.e. colimit in $\Set^{\op}$) is $\{0,1\}^{\IN}$, which is uncountable, so that $P(\{0,1\}^{\IN})$ is also uncountable. But the colimit of the induced diagram $P(\{0,1\}^1) \hookrightarrow P(\{0,1\}^2) \hookrightarrow \cdots$ is countable since each set $P(\{0,1\}^n)$ is finite.
- property: left-invertible
- proof: 'Assume for a contradiction that there is a functor $F : \Set \to \Set^{\op}$ with (natural) isomorphisms $X \cong F(P(X))$. For any non-empty set $X$ there is a map $1 \to X$, which yields a map $F(X) \to F(1)$. Since $F(1) \cong F(P(0)) \cong 0$ is empty, it follows that also $F(X)$ is empty. Since this holds for every non-empty set, it also follows that $X \cong F(P(X)) \cong 0$, which is a contradiction.'
+ proof: 'Assume for a contradiction that there is a functor $F : \Set \to \Set^{\op}$ with (natural) isomorphisms $X \cong F(P(X))$. For any non-empty set $X$ there is a map $\{\ast\} \to X$, which yields a map $F(X) \to F(\{\ast\})$. Since $F(\{\ast\}) \cong F(P(\varnothing)) \cong \varnothing$ is empty, it follows that also $F(X)$ is empty. Since this holds for every non-empty set, it also follows that $X \cong F(P(X)) \cong \varnothing$, which is a contradiction.'
undecidable_properties:
- property: essentially injective
diff --git a/database/data/functors/power_set_covariant.yaml b/database/data/functors/power_set_covariant.yaml
index fe3da3394..021ff8a82 100644
--- a/database/data/functors/power_set_covariant.yaml
+++ b/database/data/functors/power_set_covariant.yaml
@@ -73,9 +73,9 @@ unsatisfied_properties:
proof: >-
Assume that there is a functor $F : \Set \to \Set$ with natural isomorphisms
$$\alpha_X : X \to F(P(X)).$$
- By the Yoneda lemma, there is some element $u \in F(P(1))$ (where $1$ is the singleton set as usual) such that $\alpha_X$ is given by
- $$\alpha_X(x) = F(P(x : 1 \to X))(u).$$
- The map $P(x) : P(1) \to P(X)$ is given by $\varnothing \mapsto \varnothing$ and $1 \mapsto \{x\}$. It factors through the map $e : X + 1 \to P(X)$ which maps $a \in X$ to $\{a\}$ and the unique element of $1$ to $\varnothing$. Since $\alpha_X$ is surjective, it follows that also $F(e) : F(X + 1) \to F(P(X))$ is surjective. Since $e$ is a split monomorphism, also $F(e)$ is a split monomorphism. Hence, $F(e)$ must be an isomorphism. But then $F(X+1) \cong F(P(X)) \cong X$ for all sets $X$. If $X$ is a finite non-empty set, we conclude $\card(F(X)) = \card(X) - 1$. But then
+ By the Yoneda lemma, there is some element $u \in F(P(\{\ast\}))$ such that $\alpha_X$ is given by
+ $$\alpha_X(x) = F(P(x : \{\ast\} \to X))(u).$$
+ The map $P(x) : P(\{\ast\}) \to P(X)$ is given by $\varnothing \mapsto \varnothing$ and $\{\ast\} \mapsto \{x\}$. It factors through the map $e : X \sqcup \{\ast\} \to P(X)$ which maps $a \in X$ to $\{a\}$ and $\ast$ to $\varnothing$. Since $\alpha_X$ is surjective, it follows that also $F(e) : F(X \sqcup \{\ast\}) \to F(P(X))$ is surjective. Since $e$ is a split monomorphism, also $F(e)$ is a split monomorphism. Hence, $F(e)$ must be an isomorphism. But then $F(X \sqcup \{\ast\}) \cong F(P(X)) \cong X$ for all sets $X$. If $X$ is a finite non-empty set, we conclude $\card(F(X)) = \card(X) - 1$. But then
$$\card(X) = \card(F(P(X))) = \card(P(X)) - 1 = 2^{\card(X)} - 1$$
yields a contradiction when $\card(X) > 1$.
diff --git a/database/data/functors/rational_product.yaml b/database/data/functors/rational_product.yaml
index d7e170056..f51ad3822 100644
--- a/database/data/functors/rational_product.yaml
+++ b/database/data/functors/rational_product.yaml
@@ -57,4 +57,4 @@ unsatisfied_properties:
Based on the description of regular epimorphisms as surjective quotient maps, this amounts to finding a surjective quotient map $p : X \to Y$ such that the map $p \times \IQ : X \times \IQ \to Y \times \IQ$ (which is certainly surjective) is not a quotient map. The standard example is the projection $p : \IQ \to \IQ / \IZ$ (where $\IZ$ is collapsed to a point); see Brown's Topology and Groupoids, the Example after Theorem 4.3.2 on p. 111. A weaker statement, namely that coequalizers are not preserved, is proven in MSE/2969372.
- property: essentially injective
- proof: By Sierpiński's theorem on metric spaces, there is a homeomorphism between $\IQ$ and the coproduct $\IQ \sqcup \IQ$. Alternatively, this can be deduced from Cantor's isomorphism theorem on dense linear orders. Thus, $1 \times \IQ \cong 2 \times \IQ$, but of course $1 \not\cong 2$, where $2 = 1 \sqcup 1$ is the discrete space with two points.
+ proof: By Sierpiński's theorem on metric spaces, there is a homeomorphism between $\IQ$ and the coproduct $\IQ \sqcup \IQ$. Alternatively, this can be deduced from Cantor's isomorphism theorem on dense linear orders. Thus, $\{0\} \times \IQ \cong \{0,1\} \times \IQ$, but of course $\{0\} \not\cong \{0,1\}$, where $\{0,1\}$ carries the discrete topology.
diff --git a/database/data/functors/sequences_sets.yaml b/database/data/functors/sequences_sets.yaml
index 8698498d3..9ad76feae 100644
--- a/database/data/functors/sequences_sets.yaml
+++ b/database/data/functors/sequences_sets.yaml
@@ -40,7 +40,7 @@ unsatisfied_properties:
proof: A finite set with at least $2$ elements is not contained in the essential image.
- property: essentially injective
- proof: There is an isomorphism $2^{\IN} \cong 2^{2 \cdot \IN} \cong 4^{\IN}$. There are also counterexamples for infinite sets, such as $\IN^{\IN} \cong 2^{\IN} \cong \IR \cong \IR^{\IN}$.
+ proof: We have $\{0,1\}^{\IN} \cong \{0,1\}^{\IN \sqcup \IN} \cong (\{0,1\} \times \{0,1\})^{\IN}$, but $\{0,1\} \not\cong \{0,1\} \times \{0,1\}$. There are also counterexamples for infinite sets, such as $\IN^{\IN} \cong \{0,1\}^{\IN} \cong \IR \cong \IR^{\IN}$, but $\IN \not\cong \IR$.
- property: finitary
proof: >-
diff --git a/database/data/functors/simple_group_probing.yaml b/database/data/functors/simple_group_probing.yaml
index b9af8a6c9..d3e857836 100644
--- a/database/data/functors/simple_group_probing.yaml
+++ b/database/data/functors/simple_group_probing.yaml
@@ -26,7 +26,7 @@ satisfied_properties:
unsatisfied_properties:
- property: right adjoint
# TODO: refactor this once functor implications may have category equality assumptions
- proof: 'If $F : \Grp \to \Set$ is right adjoint to $G : \Set \to \Grp$, then $F$ is representable with representing object $U \coloneqq G(1)$. Let $u \in F(U)$ be a universal element, consisting of homomorphisms $u_\kappa : L_\kappa \to U$. Choose an infinite cardinal $\kappa > \card(U)$. Then $u_\kappa$ must be trivial. The set $F(L_\kappa) = \prod_{\lambda \leq \kappa} \Hom(L_\lambda,L_\kappa)$ contains the element $x$ whose $\kappa$-component is $\id_{L_\kappa}$ and all other components are trivial. Since $u \in F(U)$ is universal, there is a unique homomorphism $f : U \to L_\kappa$ such that $F(f)(u) = x$ in $F(L_\kappa)$. The $\kappa$-component of this equality is $f \circ u_\kappa = \id_{L_\kappa}$. Thus, $u_\kappa$ is injective, contradicting our previous observation that $u_\kappa$ is trivial and the fact that $L_\kappa$ is non-trivial.'
+ proof: 'If $F : \Grp \to \Set$ is right adjoint to $G : \Set \to \Grp$, then $F$ is representable with representing object $U \coloneqq G(\{\ast\})$. Let $u \in F(U)$ be a universal element, consisting of homomorphisms $u_\kappa : L_\kappa \to U$. Choose an infinite cardinal $\kappa > \card(U)$. Then $u_\kappa$ must be trivial. The set $F(L_\kappa) = \prod_{\lambda \leq \kappa} \Hom(L_\lambda,L_\kappa)$ contains the element $x$ whose $\kappa$-component is $\id_{L_\kappa}$ and all other components are trivial. Since $u \in F(U)$ is universal, there is a unique homomorphism $f : U \to L_\kappa$ such that $F(f)(u) = x$ in $F(L_\kappa)$. The $\kappa$-component of this equality is $f \circ u_\kappa = \id_{L_\kappa}$. Thus, $u_\kappa$ is injective, contradicting our previous observation that $u_\kappa$ is trivial and the fact that $L_\kappa$ is non-trivial.'
# TODO: refactor this once functor implications may have category_conclusions
# here: if a functor preserves terminal objects, and the domain is pointed,
diff --git a/database/data/functors/squaring_sets.yaml b/database/data/functors/squaring_sets.yaml
index e2226b864..35d276272 100644
--- a/database/data/functors/squaring_sets.yaml
+++ b/database/data/functors/squaring_sets.yaml
@@ -59,7 +59,7 @@ unsatisfied_properties:
proof: >-
Assume that there is a functor $F : \Set \to \Set$ with natural isomorphisms
$$\alpha_X : X \to F(X^2).$$
- By the Yoneda lemma, there is some $u \in F(1)$ such that $\alpha_X$ is given by
- $$\alpha_X(x) = F((x,x) : 1 \to X^2)(u)$$
- for $x \in X$. Since $(x,x)$ factors through the diagonal $\Delta_X : X \to X^2$, and $\alpha_X$ is surjective, it follows that $F(\Delta_X) : F(X) \to F(X^2)$ is surjective. It is also injective since $\Delta_X$ is a split monomorphism. Hence, $F(\Delta_X)$ is an isomorphism.
+ By the Yoneda lemma, there is some $u \in F(\{\ast\}^2)$ such that $\alpha_X$ is given by
+ $$\alpha_X(x) = F(x \times x)(u)$$
+ for $x \in X$, where we regard $x$ as a map $x : \{\ast\} \to X$. Since $x \times x : \{\ast\}^2 \to X^2$ factors through the diagonal $\Delta_X : X \to X^2$, and $\alpha_X$ is surjective, it follows that $F(\Delta_X) : F(X) \to F(X^2)$ is surjective. It is also injective since $\Delta_X$ is a split monomorphism. Hence, $F(\Delta_X)$ is an isomorphism.
Thus, $X \cong F(X^2) \cong F(X)$. But then also $X \cong F(X^2) \cong X^2$, and we obtain a contradiction.
diff --git a/database/data/functors/trivial_BG.yaml b/database/data/functors/trivial_BG.yaml
index 3fe018218..d404a6921 100644
--- a/database/data/functors/trivial_BG.yaml
+++ b/database/data/functors/trivial_BG.yaml
@@ -6,7 +6,7 @@ associated:
codomain: '1'
left_adjoint: null
right_adjoint: null
-description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the delooping of a non-trivial group $G$. It is a basic example of a conservative functor which is not faithful.'
+description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to \1$ into the trivial category. Here, we specify that $\C$ is the delooping of a non-trivial group $G$. It is a basic example of a conservative functor which is not faithful.'
nlab_link: null
tags:
diff --git a/database/data/functors/trivial_Idem.yaml b/database/data/functors/trivial_Idem.yaml
index ef8537ddc..245fb5721 100644
--- a/database/data/functors/trivial_Idem.yaml
+++ b/database/data/functors/trivial_Idem.yaml
@@ -6,7 +6,7 @@ associated:
codomain: '1'
left_adjoint: null
right_adjoint: null
-description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the walking idempotent. It is a basic example of an essentially injective functor which is not conservative.'
+description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to \1$ into the trivial category. Here, we specify that $\C$ is the walking idempotent. It is a basic example of an essentially injective functor which is not conservative.'
nlab_link: null
tags:
@@ -25,8 +25,8 @@ unsatisfied_properties:
- property: left adjoint
# TODO: refactor this once functor implications support category_conclusions
- proof: A functor $1 \to \Idem$ which is right adjoint to $\Idem \to 1$ provides a terminal object in $\Idem$, which does not exist.
+ proof: A functor $\1 \to \Idem$ which is right adjoint to $\Idem \to \1$ provides a terminal object in $\Idem$, which does not exist.
- property: right adjoint
# TODO: refactor this once functor implications support category_conclusions
- proof: A functor $1 \to \Idem$ which is left adjoint to $\Idem \to 1$ provides an initial object in $\Idem$, which does not exist.
+ proof: A functor $\1 \to \Idem$ which is left adjoint to $\Idem \to \1$ provides an initial object in $\Idem$, which does not exist.
diff --git a/database/data/functors/trivial_groups.yaml b/database/data/functors/trivial_groups.yaml
index ef8ee8eb0..4b9f8e50d 100644
--- a/database/data/functors/trivial_groups.yaml
+++ b/database/data/functors/trivial_groups.yaml
@@ -6,7 +6,7 @@ associated:
codomain: '1'
left_adjoint: null
right_adjoint: null
-description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the category of groups. It is a basic example of a full functor which is not faithful.'
+description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to \1$ into the trivial category. Here, we specify that $\C$ is the category of groups. It is a basic example of a full functor which is not faithful.'
nlab_link: null
tags:
diff --git a/database/data/functors/trivial_sets.yaml b/database/data/functors/trivial_sets.yaml
index 766ff861d..e5dc1cdf8 100644
--- a/database/data/functors/trivial_sets.yaml
+++ b/database/data/functors/trivial_sets.yaml
@@ -6,7 +6,7 @@ associated:
codomain: '1'
left_adjoint: null
right_adjoint: null
-description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the category of sets.'
+description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to \1$ into the trivial category. Here, we specify that $\C$ is the category of sets.'
nlab_link: null
tags:
diff --git a/database/data/functors/walking_morphism_representation.yaml b/database/data/functors/walking_morphism_representation.yaml
index 2a6d2e583..dd065f52d 100644
--- a/database/data/functors/walking_morphism_representation.yaml
+++ b/database/data/functors/walking_morphism_representation.yaml
@@ -6,7 +6,7 @@ associated:
codomain: Set
left_adjoint: null
right_adjoint: null
-description: This is the functor $I \to \Set$ that maps the universal morphism $0 \to 1$ to the unique map $\varnothing \to \{*\}$ in $\Set$. It provides a very simple example of a functor that preserves coequalizers (and hence regular epimorphisms) but does not preserve epimorphisms.
+description: This is the functor $I \to \Set$ that maps the universal morphism $0 \to 1$ to the unique map $\varnothing \to \{\ast\}$ in $\Set$. It provides a very simple example of a functor that preserves coequalizers (and hence regular epimorphisms) but does not preserve epimorphisms.
nlab_link: null
tags:
@@ -29,7 +29,7 @@ satisfied_properties:
unsatisfied_properties:
- property: preserves epimorphisms
- proof: The universal morphism $0 \to 1$ is an epimorphism in $I$ (simply because $I$ is thin), but its image $\varnothing \to \{*\}$ in $\Set$ is not an epimorphism.
+ proof: The universal morphism $0 \to 1$ is an epimorphism in $I$ (simply because $I$ is thin), but its image $\varnothing \to \{\ast\}$ in $\Set$ is not an epimorphism.
- property: dominant
proof: This is trivial.
diff --git a/database/data/morphisms/terminal-map.yaml b/database/data/morphisms/terminal-map.yaml
index 09d6cb10d..838adc586 100644
--- a/database/data/morphisms/terminal-map.yaml
+++ b/database/data/morphisms/terminal-map.yaml
@@ -3,7 +3,7 @@ name: map into the singleton set
notation: $!$
associated:
category: Set
-description: 'For every set $X$ there is a unique map $! : X \to 1$, where $1$ is the singleton set. In this entry, we require that $X$ has at least $2$ elements.'
+description: 'For every set $X$ there is a unique map $! : X \to \{\ast\}$. In this entry, we require that $X$ has at least $2$ elements.'
nlab_link: null
keywords:
- terminal map
@@ -15,14 +15,14 @@ related: []
satisfied_properties:
- property: split epimorphism
- proof: 'Take any element $x \in X$. The corresponding map $x : 1 \to X$ is a section of $! : X \to 1$.'
+ proof: 'Take any element $x \in X$. The corresponding map $x : \{\ast\} \to X$ is a section of $! : X \to \{\ast\}$.'
- property: constant
- proof: This is clear because $1$ is terminal; see also Lemma 4 here.
+ proof: This is clear because $\{\ast\}$ is terminal; see also Lemma 4 here.
unsatisfied_properties:
- property: monomorphism
proof: Since $X$ has two different elements by assumption, which trivially have the same image, the map is not injective.
- property: coconstant
- proof: 'A direct proof is possible, but we can also argue as follows: Since the map is an epimorphism, if it were coconstant, by the dual of Lemma 5 here, $1$ would be co-subterminal, which is absurd.'
+ proof: 'A direct proof is possible, but we can also argue as follows: Since the map is an epimorphism, if it were coconstant, by the dual of Lemma 5 here, $\{\ast\}$ would be co-subterminal, which is absurd.'
diff --git a/database/data/symmetric_monoidal_categories/1_tensor.yaml b/database/data/symmetric_monoidal_categories/1_tensor.yaml
index 278f4eccf..245824b2b 100644
--- a/database/data/symmetric_monoidal_categories/1_tensor.yaml
+++ b/database/data/symmetric_monoidal_categories/1_tensor.yaml
@@ -1,9 +1,9 @@
id: 1_tensor
name: trivial symmetric monoidal category
-notation: $(1,\times,0)$
+notation: $(\1,\times,0)$
associated:
underlying_category: '1'
-description: This is the terminal symmetric monoidal category. It is the trivial category $1$ equipped with its unique strict symmetric monoidal structure. The monoidal unit is the unique object $0$.
+description: This is the terminal symmetric monoidal category. It is the trivial category $\1$ equipped with its unique strict symmetric monoidal structure. The monoidal unit is the unique object $0$.
nlab_link: null
tags:
diff --git a/database/data/symmetric_monoidal_categories/Cat_cartesian.yaml b/database/data/symmetric_monoidal_categories/Cat_cartesian.yaml
index 3a007e744..226b14b37 100644
--- a/database/data/symmetric_monoidal_categories/Cat_cartesian.yaml
+++ b/database/data/symmetric_monoidal_categories/Cat_cartesian.yaml
@@ -1,6 +1,6 @@
id: Cat_cartesian
name: cartesian symmetric monoidal category of small categories
-notation: $(\Cat,\times,1)$
+notation: $(\Cat,\times,\1)$
associated:
underlying_category: Cat
description: Every category with finite products (also called a cartesian category) can be endowed with a symmetric monoidal structure, where $1$ is the terminal object and $\otimes$ is the product $\times$. In this case, we apply this to the category $\Cat$ of small categories.
diff --git a/database/data/symmetric_monoidal_categories/Set_cartesian.yaml b/database/data/symmetric_monoidal_categories/Set_cartesian.yaml
index bcc599a32..789ec1a34 100644
--- a/database/data/symmetric_monoidal_categories/Set_cartesian.yaml
+++ b/database/data/symmetric_monoidal_categories/Set_cartesian.yaml
@@ -1,6 +1,6 @@
id: Set_cartesian
name: cartesian symmetric monoidal category of sets
-notation: $(\Set,\times,1)$
+notation: $(\Set,\times,\{\ast\})$
associated:
underlying_category: Set
description: Every category with finite products (also called a cartesian category) can be endowed with a symmetric monoidal structure, where $1$ is the terminal object and $\otimes$ is the product $\times$. In this case, we apply this to the category $\Set$.
diff --git a/database/data/symmetric_monoidal_categories/Set_cocartesian.yaml b/database/data/symmetric_monoidal_categories/Set_cocartesian.yaml
index ddfd1f32d..d6f7260d1 100644
--- a/database/data/symmetric_monoidal_categories/Set_cocartesian.yaml
+++ b/database/data/symmetric_monoidal_categories/Set_cocartesian.yaml
@@ -1,6 +1,6 @@
id: Set_cocartesian
name: cocartesian symmetric monoidal category of sets
-notation: $(\Set,\sqcup,0)$
+notation: $(\Set,\sqcup,\varnothing)$
associated:
underlying_category: Set
description: Every category with finite coproducts (also called a cocartesian category) can be endowed with a symmetric monoidal structure, where the monoidal unit is the initial object and $\otimes$ is the coproduct $\sqcup$. In this case, we apply this to the category $\Set$.
diff --git a/database/data/symmetric_monoidal_categories/Top_cartesian.yaml b/database/data/symmetric_monoidal_categories/Top_cartesian.yaml
index a40203abf..cd4667fb0 100644
--- a/database/data/symmetric_monoidal_categories/Top_cartesian.yaml
+++ b/database/data/symmetric_monoidal_categories/Top_cartesian.yaml
@@ -1,6 +1,6 @@
id: Top_cartesian
name: cartesian symmetric monoidal category of topological spaces
-notation: $(\Top,\times,1)$
+notation: $(\Top,\times,\{\ast\})$
associated:
underlying_category: Top
description: Every category with finite products (also called a cartesian category) can be endowed with a symmetric monoidal structure, where $1$ is the terminal object and $\otimes$ is the product $\times$. In this case, we apply this to the category $\Top$.
diff --git a/database/data/symmetric_monoidal_category-properties/strict.yaml b/database/data/symmetric_monoidal_category-properties/strict.yaml
index dd6084fbc..409a2d6d2 100644
--- a/database/data/symmetric_monoidal_category-properties/strict.yaml
+++ b/database/data/symmetric_monoidal_category-properties/strict.yaml
@@ -1,6 +1,6 @@
id: strict
relation: is
-description: 'A symmetric monoidal category is called strict when its associator, symmetry, left unitor, and right unitor are identities. A strict symmetric monoidal category is simply a commutative monoid object in $(\Cat^+,\times,1)$.'
+description: 'A symmetric monoidal category is called strict when its associator, symmetry, left unitor, and right unitor are identities. A strict symmetric monoidal category is simply a commutative monoid object in $(\Cat^+,\times,\1)$.'
nlab_link: https://ncatlab.org/nlab/show/strict+monoidal+category
invariant_under_equivalences: false
dual: strict