diff --git a/content/natural_numbers_objects.md b/content/natural_numbers_objects.md new file mode 100644 index 00000000..b3bd73d6 --- /dev/null +++ b/content/natural_numbers_objects.md @@ -0,0 +1,103 @@ +--- +title: Natural numbers objects +description: We prove some results on natural numbers objects. +--- + +## Natural numbers objects + +The definition of a [natural numbers object](/category-property/natural_numbers_object) a priori only allows for recursively defined morphisms in which the next value $\Phi(s(n))$ depends only on the previous value $\Phi(n)$. In many cases, however, we would also like to use $n$ itself to define $\Phi(s(n))$. This can be done in categories with finite products: + +::: Lemma 1 +Let $(N,z,s)$ be a natural numbers object in a category with finite products. Then for every $a : 1 \to X$ and every $g : N \times X \to X$ there exists a unique morphism $\Phi : N \to X$ such that $\Phi(z) = a$ and $\Phi(s(n)) = g(n, \Phi(n))$. +::: + +Here, we use element notation to simplify the exposition. For example, the equation $\Phi(s(n)) = g(n,\Phi(n))$ means that the following diagram commutes: + +$$ +\begin{CD} +N @>{s}>> N \\ +@V{(\id_N,\Phi)}VV @VV{\Phi}V \\ +N \times X @>>{g}> X +\end{CD} +$$ + +_Proof._ Define the morphism $b : 1 \to N \times X$ by $b \coloneqq (z,a)$ and the morphism $h : N \times X \to N \times X$ by $h(n,x) \coloneqq (n,g(n,x))$. By the universal property of $(N,z,s)$, there is a unique morphism $\Psi : N \to N \times X$ such that: + +- $\Psi(z) = b$ +- $\Psi(s(n)) = h(\Psi(n))$ + +Write $\Psi(n) = (\Psi_0(n),\Psi_1(n))$, where $\Psi_0 : N \to N$ and $\Psi_1 : N \to X$. The two equations above then become: + +- $\Psi_0(z) = z$ +- $\Psi_0(s(n)) = \Psi_0(n)$ +- $\Psi_1(z) = a$ +- $\Psi_1(s(n)) = g(\Psi_0(n),\Psi_1(n))$ + +The uniqueness in the universal property of $(N,z,s)$ implies $\Psi_0 = \id_N$. Therefore, $\Phi \coloneqq \Psi_1$ is the unique morphism $\Phi : N \to X$ satisfying $\Phi(z)=a$ and $\Phi(s(n)) = g(n,\Phi(n))$. $\square$ + +The next result appears in [Johnstone](https://ncatlab.org/nlab/show/Sketches+of+an+Elephant), Part A, Lemma 2.5.5. Our proof is slightly more concise because we have extracted Lemma 1. + +::: Lemma 2 +Let $(N,z,s)$ be a natural numbers object in a category with finite products. Then +$$1 \xrightarrow{z} N \xleftarrow{s} N$$ +is a coproduct cocone. Thus, $N \cong 1 \sqcup N$. +::: + +_Proof._ Let $a : 1 \to X$ and $b : N \to X$ be morphisms. We need to show that there is a unique morphism $c : N \to X$ satisfying $c(z) = a$ and $c(s(n)) = b(n)$. This follows by applying Lemma 1 to the morphism $g : N \times X \to X$ defined by $g(n,x) \coloneqq b(n)$. $\square$ + +Next, we will check when the terminal object $1$ itself is a natural numbers object. In that case, $z : 1 \to 1$ and $s : 1 \to 1$ are necessarily equal to $\id_1$. + +::: Lemma 3 +Let $1$ be a terminal object in a category. Then $(1,\id_1,\id_1)$ is a natural numbers object if and only if for every endomorphism $g : X \to X$ and every morphism $a : 1 \to X$ we have $g \circ a = a$. If the category has finite products, $(1,\id_1,\id_1)$ is a parametrized natural numbers object if and only if $g = \id_X$ for every endomorphism $g : X \to X$, i.e. the category is [one-way](/category-property/one-way). +::: + +_Proof._ The first statement is immediate from the definition of a natural numbers object. For the second, $(1,\id_1,\id_1)$ is a parametrized natural numbers object if and only if, for all morphisms $f : A \to X$ and all endomorphisms $g : X \to X$, there is a unique morphism $\Phi : A \to X$ such that $\Phi \circ \id_A = f$ and $\Phi \circ \id_A = g \circ \Phi$. These equations simplify to $\Phi = f$ and $f = g \circ f$. Since this must hold for every $f : A \to X$, we must have $g = \id_X$ (by the Yoneda Lemma or by a direct argument). $\square$ + +Next, we prove a partial converse to the [result](/category-implication/parametrized_nno_criterion) that countably distributive categories have a parametrized natural numbers object. + +::: Lemma 4 +Let $\C$ be a category with finite products, countable copowers denoted $\otimes$, and a parametrized natural numbers object $1 \xrightarrow{z} N \xrightarrow{s} N$. Then there is an isomorphism $N \cong \IN \otimes 1$, and for every object $A$ the natural morphism +$$\alpha : \IN \otimes A \to A \times (\IN \otimes 1)$$ +is an isomorphism. +::: + +_Proof._ We will use element notation extensively. In particular, for every element $a \in A$ and $n \in \IN$, there is an element $n \otimes a \in \IN \otimes A$, formally defined by the $n$th coproduct inclusion. The morphism $\alpha$ is defined by +$$\alpha(n \otimes a) = (a,n \otimes 1).$$ + +In any category with a terminal object and countable copowers, we can construct the non-parametrized NNO $\IN \otimes 1$ with the element $0 \otimes 1 \in \IN \otimes 1$ and the map +$$s : \IN \otimes 1 \to \IN \otimes 1, \quad s(n \otimes 1) \coloneqq (n+1) \otimes 1.$$ +See [here](/category-implication/nno_criterion) for a detailed proof. Since, by assumption, $1 \xrightarrow{z} N \xrightarrow{s} N$ is a parametrized NNO, it is also a non-parametrized NNO and is therefore isomorphic to the one just constructed. We may assume without loss of generality that they are equal and hence work with $N = \IN \otimes 1$. + +Next, apply the parametrized universal property of the NNO to the diagram +$$A \xrightarrow{f} \IN \otimes A \xrightarrow{g} \IN \otimes A$$ +defined by $f(a) \coloneqq 0 \otimes a$ and $g(n \otimes a) \coloneqq (n+1) \otimes a$. It gives a morphism +$$\Phi : A \times N \to \IN \otimes A$$ +satisfying +$$\Phi(a,0 \otimes 1) = 0 \otimes a, \quad \Phi(a,s(m)) = g(\Phi(a,m)).$$ +For $m \coloneqq n \otimes 1 \in N$, where $n \in \IN$, the second equation becomes +$$\Phi(a,(n+1) \otimes 1) = g(\Phi(a,n \otimes 1)).$$ +By induction on $n \in \IN$, it follows that +$$\Phi(a,n \otimes 1) = n \otimes a,$$ +which is exactly the statement that $\Phi \circ \alpha = \id_{\IN \otimes A}$. + +It remains to prove $\alpha \circ \Phi = \id_{A \times N}$. We first observe that +$$\alpha \circ g = (\id_A \times s) \circ \alpha$$ +as morphisms $\IN \otimes A \to A \times (\IN \otimes 1)$. Indeed, for every $n \otimes a \in \IN \otimes A$, +$$\alpha(g(n \otimes a)) = \alpha((n+1) \otimes a) = (a, (n+1) \otimes 1),$$ +while +$$(\id_A \times s)(\alpha(n \otimes a)) = (\id_A \times s)(a, n \otimes 1) = (a, (n+1) \otimes 1).$$ +The universal property applied to the diagram +$$A \xrightarrow{(\id_A,z)} A \times N \xrightarrow{\id_A \times s} A \times N$$ +shows that there is a _unique_ morphism $\Psi : A \times N \to A \times N$ satisfying +$$\Psi \circ (\id_A,z) = (\id_A,z)$$ +and +$$\Psi \circ (\id_A \times s) = (\id_A \times s) \circ \Psi,$$ +namely $\id_{A \times N}$. Thus, it suffices to verify that $\alpha \circ \Phi : A \times N \to A \times N$ satisfies these two equations. We have +$$\alpha(\Phi(a,z)) = \alpha(0 \otimes a) = (a, 0 \otimes 1) = (a,z),$$ +and hence $\alpha \circ \Phi \circ (\id_A,z) = (\id_A,z)$. Moreover, +$$\alpha \circ \Phi \circ (\id_A \times s) = \alpha \circ g \circ \Phi = (\id_A \times s) \circ \alpha \circ \Phi.$$ +This finishes the proof. $\square$ + +_Remark._ Actually, the mentioned [result](/category-implication/parametrized_nno_criterion) and Lemma 4 can be combined into an equivalent characterization as follows: In a category with finite products and countable copowers, the NNO (which exists, see [here](/category-implication/nno_criterion)) is a parametrized NNO if and only if for all objects $A$ the canonical morphism +$$\textstyle \coprod_{n \in \IN} A = \coprod_{n \in \IN} (A \times 1) \to A \times \coprod_{n \in \IN} 1$$ +is an isomorphism. This is the precise connection to countable distributivity. diff --git a/content/nno_distributive_criterion.md b/content/nno_distributive_criterion.md deleted file mode 100644 index f5e133ef..00000000 --- a/content/nno_distributive_criterion.md +++ /dev/null @@ -1,31 +0,0 @@ ---- -title: Natural number objects indicate distributivity -description: A partial converse of the result that countably distributive categories have a NNO. ---- - -## Natural number objects indicate distributivity - -::: Lemma -Let $\C$ be a category with finite products, arbitrary copowers (denoted $\otimes$), and a natural numbers object $1 \xrightarrow{z} N \xrightarrow{s} N$. Then there is an isomorphism $N \cong \IN \otimes 1$, and for every object $A$ the natural morphism -$$\alpha : \IN \otimes A \to A \times (\IN \otimes 1)$$ -is a split monomorphism. -::: - -_Proof._ -We will use generalized elements extensively. In particular, for every element $a \in A$ and $n \in \IN$ there is an element $n \otimes a \in \IN \otimes A$, formally defined by the $n$th coproduct inclusion. The morphism $\alpha$ is defined by -$$\alpha(n \otimes a) = (a , n \otimes 1).$$ -In any category with finite products and arbitrary copowers, we can construct the non-parameterized NNO $\IN \otimes 1$ with the element $0 \otimes 1 \in \IN \otimes 1$ and the map -$$s : \IN \otimes 1 \to \IN \otimes 1, \quad s(n \otimes 1) \coloneqq (n+1) \otimes 1.$$ -Its universal property states that it is initial in the category of pairs $1 \xrightarrow{x_0} X \xrightarrow{r} X$. Hence, it is unique up to isomorphism. Since by assumption $1 \xrightarrow{z} N \xrightarrow{s} N$ is a full, parameterized NNO, it is also a non-parameterized NNO and therefore isomorphic to the one described. We will assume w.l.o.g. that it is equal to it and continue to work with $N = \IN \otimes 1$. - -Next, we apply the (parameterized) universal property of the NNO to the diagram -$$A \xrightarrow{f} \IN \otimes A \xrightarrow{g} \IN \otimes A$$ -defined by $f(a) \coloneqq 0 \otimes a$ and $g(n \otimes a) \coloneqq (n+1) \otimes a$. It tells us that there is a map -$$\Phi : A \times N \to \IN \otimes A$$ -with -$$\Phi(a,0 \otimes 1) = 0 \otimes a, \quad \Phi(a, s(m)) = g(\Phi(a,m)).$$ -For $m \coloneqq n \otimes 1 \in N$ (where $n \in \IN$) the second equation reads -$$\Phi(a, (n+1) \otimes 1) = g(\Phi(a, n \otimes 1)).$$ -By classical induction on $n \in \IN$ it follows that -$$\Phi(a, n \otimes 1) = n \otimes a,$$ -which exactly means $\Phi \circ \alpha = \id_{\IN \otimes A}$. $\square$ diff --git a/database/data/categories/CompHaus.yaml b/database/data/categories/CompHaus.yaml index c1ecb7d6..63db0ea2 100644 --- a/database/data/categories/CompHaus.yaml +++ b/database/data/categories/CompHaus.yaml @@ -73,9 +73,9 @@ unsatisfied_properties: references: - haus_no_regular_subobject_classifier - - property: natural numbers object + - property: parametrized natural numbers object proof: >- - Let $I \coloneqq [0, 1]$. If a 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 : 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 $$\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/Delta.yaml b/database/data/categories/Delta.yaml index 2ccb85b7..e53d50ea 100644 --- a/database/data/categories/Delta.yaml +++ b/database/data/categories/Delta.yaml @@ -57,12 +57,12 @@ satisfied_properties: proof: The category $\FinOrd \setminus \{\varnothing\}$ is core-thin because already $\FinOrd$ is core-thin. - property: mono-regular - proof: The proof for $\FinOrd$ also works for $\FinSet \setminus \{\varnothing\}$. + proof: The proof for $\FinOrd$ also works for $\FinOrd \setminus \{\varnothing\}$. references: - finord_mono-regular - property: epi-regular - proof: The proof for $\FinOrd$ also works for $\FinSet \setminus \{\varnothing\}$. + proof: The proof for $\FinOrd$ also works for $\FinOrd \setminus \{\varnothing\}$. references: - finord_epi-regular @@ -81,9 +81,6 @@ satisfied_properties: - finset_aleph1-cofiltered-limits unsatisfied_properties: - - property: strict terminal object - proof: This is trivial. - - property: cofiltered proof: 'The two maps $d^0,d^1 : [0] \rightrightarrows [1]$ are not equalized by any morphism.' @@ -100,6 +97,9 @@ unsatisfied_properties: references: - finord_no_sequential_limits + - property: natural numbers object + proof: Any natural numbers object in $\FinOrd \setminus \{\varnothing\}$ would also be a natural numbers object in $\FinOrd$, which we know does not exist. + - property: pushouts proof: Assume that the two inclusions $\{0 < 1\} \leftarrow \{0\} \rightarrow \{0 < 2\}$ have a pushout in $\FinOrd \setminus \{\varnothing\}$. This would be a universal non-empty finite ordered set $X$ with three elements $0,1,2$ satisfying $0 \leq 1$ and $0 \leq 2$. Assume w.l.o.g. $1 \leq 2$ (the case $2 \leq 1$ is similar). The universal property yields an order-preserving map $X \to \{a < b < c\}$ with $0 \mapsto a$, $1 \mapsto c$, $2 \mapsto b$. But then $c \leq b$, which is a contradiction. diff --git a/database/data/categories/FinOrd.yaml b/database/data/categories/FinOrd.yaml index edd57786..209ad6d7 100644 --- a/database/data/categories/FinOrd.yaml +++ b/database/data/categories/FinOrd.yaml @@ -71,15 +71,9 @@ unsatisfied_properties: - property: skeletal proof: This is trivial. - - property: one-way - proof: There are three different order-preserving maps $\{0 < 1\} \to \{0 < 1\}$. - - property: countable proof: This is trivial. - - property: strict terminal object - proof: This is trivial. - - property: sequential limits proof: Consider the (non-empty) ordered set $[n] \coloneqq \{0 < \cdots < n\}$ for $n \in \IN$. The forgetful functor to $\Set$ is representable, hence preserves all limits. Thus, if the diagram of truncation maps $\cdots \twoheadrightarrow [2] \twoheadrightarrow [1] \twoheadrightarrow [0]$ has a limit in $\FinOrd$, its underlying set is isomorphic to the limit taken in $\Set$, which is $\IN \cup \{\infty\}$. But this is not a finite set. label: finord_no_sequential_limits @@ -88,6 +82,9 @@ unsatisfied_properties: proof: 'Consider the (non-empty) ordered set $[n] \coloneqq \{0 < \cdots < n\}$ for $n \in \IN$. Assume the sequence of inclusion maps $[0] \hookrightarrow [1] \hookrightarrow [2] \hookrightarrow \cdots$ has a colimit $(f_n : [n] \to X)$ in $\FinOrd$. Let $n_0 \geq 0$ be fixed. I claim that $f_{n_0}$ is injective, which will then yield a contradiction by taking $n_0 \geq \card(X)$. For $n \geq 0$ define $g_n : [n] \to [n_0]$ as follows. For $n \leq n_0$ it is the inclusion, and for $n \geq n_0$ it is the surjection which keeps all elements of $[n_0]$ and maps all other elements to $n_0$. Observe that $g_n$ preserves the order and $g_{n+1} |_{[n]} = g_n$. Hence, there is a unique order-preserving map $g : X \to [n_0]$ with $g \circ f_n = g_n$ for all $n$. For $n = n_0$ this shows $g \circ f_{n_0} = \id_{[n_0]}$, and $f_{n_0}$ is injective.' label: finord_no_sequential_colimits + - property: natural numbers object + proof: 'Assume that there is a natural numbers object $(N,z,s)$, where $z \in N$ and $s : N \to N$. Let $d \coloneqq \card(N)$. Consider the finite ordered set $X \coloneqq \{1 < \dotsc < d+1\}$ and the order-preserving map $g : X \to X$ defined by $g(k) \coloneqq k + 1$ for $k \leq d$ and $g(d+1) \coloneqq d+1$. By the universal property of $(N,z,s)$, there is a unique order-preserving map $\Phi : N \to X$ such that $\Phi(z) = 1$ and $\Phi(s(n)) = g(\Phi(n))$ for all $n \in N$. We then have $\Phi(s(z)) = 2$, $\Phi(s^2(z)) = 3$, and so on. Formally, an induction shows that $\Phi(s^n(z)) = n+1$ for every $0 \leq n \leq d$. Thus, $\Phi$ is surjective, contradicting $\card(N) < \card(X)$.' + special_objects: initial object: description: empty ordered set diff --git a/database/data/categories/FinSet.yaml b/database/data/categories/FinSet.yaml index 3b723fef..1ffea278 100644 --- a/database/data/categories/FinSet.yaml +++ b/database/data/categories/FinSet.yaml @@ -55,10 +55,7 @@ unsatisfied_properties: proof: This is trivial. - property: natural numbers object - proof: >- - If $(N,z,s)$ is a natural numbers object, then - $$1 \xrightarrow{z} N \xleftarrow{s} N$$ - is a coproduct cocone by Johnstone, Part A, Lemma 2.5.5. But there is no finite set $N$ with $N \cong 1 + N$. + 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. special_objects: initial object: diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml index 8120e40b..3415d557 100644 --- a/database/data/categories/Met.yaml +++ b/database/data/categories/Met.yaml @@ -123,9 +123,6 @@ unsatisfied_properties: - property: locally finite proof: This is obvious. - - property: strict terminal object - proof: This is trivial. - - property: balanced proof: The inclusion $\IQ \hookrightarrow \IR$ is a counterexample; it is an epimorphism since $\IQ$ is dense in $\IR$. Alternatively, consider the identity map $(X,2d) \to (X,d)$ for any non-trivial metric space $(X,d)$. @@ -148,10 +145,7 @@ unsatisfied_properties: label: met_no_filtered_colimit_stable_monos - property: natural numbers object - proof: >- - If $(N,z,s)$ is a natural numbers object in $\Met$, then - $$1 \xrightarrow{z} N \xleftarrow{s} N$$ - is a coproduct cocone by Johnstone, Part A, Lemma 2.5.5. 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 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. - 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.' diff --git a/database/data/categories/PMet.yaml b/database/data/categories/PMet.yaml index 772327f0..4635ae69 100644 --- a/database/data/categories/PMet.yaml +++ b/database/data/categories/PMet.yaml @@ -95,9 +95,6 @@ unsatisfied_properties: - property: locally finite proof: This is obvious. - - property: strict terminal object - proof: This is trivial. - - property: balanced proof: 'Let $d : \IR \times \IR \to \IR_{\geq 0}$ be the usual Euclidean metric on $\IR$ and $0 : \IR \times \IR \to \IR_{\geq 0}$ be the zero pseudo-metric. Then the identity map $(\IR,d) \to (\IR,0)$ provides a counterexample.' @@ -114,10 +111,7 @@ 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: >- - If $(N,z,s)$ is a natural numbers object in $\PMet$, then - $$1 \xrightarrow{z} N \xleftarrow{s} N$$ - is a coproduct cocone by Johnstone, Part A, Lemma 2.5.5. 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 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. - 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.' diff --git a/database/data/categories/SemiGrp.yaml b/database/data/categories/SemiGrp.yaml index 0723d65b..d9899349 100644 --- a/database/data/categories/SemiGrp.yaml +++ b/database/data/categories/SemiGrp.yaml @@ -76,17 +76,17 @@ unsatisfied_properties: references: - mon_no_effective_cocongruences - - property: natural numbers object + - property: parametrized natural numbers object proof: >- - Assume that a natural numbers object exists. Then by this result, for every semigroup $A$ the natural homomorphism + Assume that a parametrized natural numbers object exists. Then by Lemma 4 here, for every semigroup $A$ the natural homomorphism $$\textstyle\alpha : \coprod_{n \geq 0} A \to A \times \coprod_{n \geq 0} 1$$ - is a split monomorphism. But this is not true: For each $n \geq 0$ let $A_n$ denote a copy of $A$. The elements of the coproduct in $\alpha$'s domain have a unique representation as + is an isomorphism. But this is not true: For each $n \geq 0$ let $A_n$ denote a copy of $A$. The elements of the coproduct in $\alpha$'s domain have a unique representation as $$x_{n_1} * \cdots * x_{n_s}$$ with $x_i \in A_i$ and $n_i \neq n_{i+1}$, and we have $$\alpha(x_{n_1} * \cdots * x_{n_s}) = (x_{n_1} \cdots x_{n_s}, n_1 * \cdots * n_s).$$ - In particular, if $A$ has two non-equal commuting elements $x,y$ (for example, if $A$ is any non-trivial monoid), we have - $$\alpha(y_0 x_0) = \alpha(x_0 y_0),$$ - showing that $\alpha$ is not injective. + In particular, if $A$ has distinct commuting elements $x,y$ (for example, if $A$ is any non-trivial monoid), we have + $$\alpha(x_0 y_1) = \alpha(y_0 x_1),$$ + where $x_i$ (resp. $y_i$) denotes the image of $x$ (resp. $y$) in the copy $A_i$. This shows that $\alpha$ is not injective. - property: coregular proof: >- diff --git a/database/data/categories/Setne.yaml b/database/data/categories/Setne.yaml index 612b6a9b..38e3275e 100644 --- a/database/data/categories/Setne.yaml +++ b/database/data/categories/Setne.yaml @@ -51,8 +51,8 @@ satisfied_properties: - property: generalized variety proof: Since the inclusion $\Setne \hookrightarrow \Set$ is closed under non-empty colimits, it is also closed under sifted colimits. Therefore, non-empty finite sets are still strongly finitely presentable in $\Setne$, and every non-empty set is written as a sifted colimit of them. - - property: natural numbers object - proof: Any natural numbers object in $\Set$, such as $(\IN,0,n \mapsto n+1)$, is clearly also one in $\Setne$. + - property: parametrized natural numbers object + proof: Any parametrized natural numbers object in $\Set$, such as $(\IN,0,n \mapsto n+1)$, is clearly also one in $\Setne$. - property: multi-complete proof: Let $D$ be a diagram in $\Setne$, and let $L$ be a limit of $D$ in $\Set$. If $L$ is non-empty, it gives a limit in $\Setne$ as well. If $L$ is the empty set, there is no cone over $D$ in $\Setne$; hence the empty set of cones gives a multi-limit of $D$ in $\Setne$. diff --git a/database/data/categories/Sp.yaml b/database/data/categories/Sp.yaml index 1ddd9e40..b43eeec4 100644 --- a/database/data/categories/Sp.yaml +++ b/database/data/categories/Sp.yaml @@ -55,10 +55,7 @@ unsatisfied_properties: Alternatively, the claim follows from this result. - property: natural numbers object - proof: >- - If $(N,z,s)$ is a natural numbers object, then - $$1 \xrightarrow{z} N \xleftarrow{s} N$$ - is a coproduct cocone by Johnstone, Part A, Lemma 2.5.5. But there is no combinatorial species $N$ with $N \cong 1 + N$, since evaluating this 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 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. special_objects: initial object: diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml index 014f3a88..5e3c9d61 100644 --- a/database/data/categories/Unif.yaml +++ b/database/data/categories/Unif.yaml @@ -121,13 +121,13 @@ unsatisfied_properties: references: - top_no_effective_cocongruences - - property: natural numbers object + - 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$. - If there were a natural numbers object, then by this result the canonical map + 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$$ - would be a split monomorphism. It is certainly surjective and hence an epimorphism. Thus, it would be an isomorphism. + 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/walking_coreflexive_pair.yaml b/database/data/categories/walking_coreflexive_pair.yaml index 2d335248..a0dc89c1 100644 --- a/database/data/categories/walking_coreflexive_pair.yaml +++ b/database/data/categories/walking_coreflexive_pair.yaml @@ -2,11 +2,11 @@ id: walking_coreflexive_pair name: walking coreflexive pair notation: $\Delta^{\leq 1}$ objects: two objects $[0]$ and $[1]$ -morphisms: 'the identities, two morphisms $i,j : [0] \rightrightarrows [1]$, a morphism $p : [1] \to [0]$ with $p i = p j = \id_{[0]}$, and the two idempotent morphisms $ip, jp : [1] \to [1]$.' +morphisms: 'the identities, two morphisms $i,j : [0] \rightrightarrows [1]$, a morphism $p : [1] \to [0]$ with $p i = p j = \id_{[0]}$, and the two idempotent morphisms $ip, jp : [1] \rightrightarrows [1]$.' description: >- This category is equal to the truncated simplex category $\Delta^{\leq 1}$, i.e. the full subcategory of $\Delta$ spanned by $[0] = \{0\}$ and $[1] = \{0 < 1\}$; this also explains our notation of the category and its objects. $$[0] \begin{array}{c} \xhookrightarrow{~~i~~} \\ \xtwoheadleftarrow{~~p~~} \\ \xhookrightarrow{~~j~~} \end{array} [1]$$ - The morphisms $i,j$ are the two inclusions, $p$ is their unique retraction, and $ip,jp : [1] \to [1]$ are the two constant maps. The name of this category comes from the fact that a functor $\Delta^{\leq 1} \to \C$ is the same as a coreflexive pair in $\C$. Its dual is therefore the walking reflexive pair. + The morphisms $i,j$ are the two inclusions, $p$ is their unique retraction, and $ip,jp : [1] \rightrightarrows [1]$ are the two constant maps. The name of this category comes from the fact that a functor $\Delta^{\leq 1} \to \C$ is the same as a coreflexive pair in $\C$. Its dual is therefore the walking reflexive pair. nlab_link: null tags: - category theory @@ -64,9 +64,6 @@ satisfied_properties: proof: This actually holds for every truncated simplex category $\Delta^{\leq n}$. See MO/510760 for a proof that sifted colimits exist. See MO/510827 for a proof that every object is strongly finitely presentable. unsatisfied_properties: - - property: strict terminal object - proof: 'The morphism $i : [0] \to [1]$ from the terminal object $[0]$ is a witness.' - - property: cofiltered proof: 'The morphisms $i,j : [0] \rightrightarrows [1]$ are not equalized by any morphism.' @@ -76,13 +73,16 @@ unsatisfied_properties: - property: pushouts proof: Assume that $[1] \xleftarrow{i} [0] \xrightarrow{i} [1]$ has a pushout in $\Delta^{\leq 1}$, where $i(0)=0$. This amounts to a universal totally ordered set of cardinality $\leq 2$ with elements $a,b,c$ satisfying $a \leq b$, $a \leq c$. Since a finite totally ordered set has trivial automorphism group, the automorphism defined by $a \mapsto a$, $b \mapsto c$, $c \mapsto b$ must be the identity, i.e., we have $b = c$. However, in $[1]$ the equations $0 \leq 0$, $0 \leq 1$ then show that the universal property fails. + - property: natural numbers object + proof: 'We work with the representation of this category as the full subcategory of $\FinOrd$ consisting of $\{0\}$ and $\{0 < 1\}$. First, the terminal object $\{0\}$ cannot be the underlying object of a natural numbers object: otherwise, by Lemma 3 here and the fact that $\{0\}$ is a generator, every endomorphism in the category would be the identity, which is not the case. It remains to show that $(\{0 < 1\}, z, s)$ is not a natural numbers object for any choice of $z \in \{0,1\}$ and $s : \{0 < 1\} \to \{0 < 1\}$. Using the isomorphism of the category that swaps the two morphisms $\{0\} \rightrightarrows \{0 < 1\}$, we may assume that $z = 0$. Every subobject of $\{0 < 1\}$ that contains $0$ and is closed under $s$ is also a natural numbers object and hence must be equal to $\{0 < 1\}$. It follows that $\{0,1\} = \{0,s(0),s^2(0),\dotsc\}$ as sets. In particular, $s(0) \neq 0$, so $s(0) = 1$. (We do not need to determine $s(1)$.) Now apply the universal property to the element $1 \in \{0 < 1\}$ and the zero map $\{0 < 1\} \to \{0 < 1\}$, $n \mapsto 0$. We obtain an order-preserving map $p : \{0 < 1\} \to \{0 < 1\}$ satisfying $p(0) = 1$ and $p(s(n)) = 0$. Thus, $p(1) = p(s(0)) = 0$, so $p(0) > p(1)$, contradicting the fact that $p$ is order-preserving.' + - property: multi-complete # TODO: remove this manual proof once locally multi-presentable is dualized, cf. #139 proof: 'This follows directly from existing results: If its dual, the walking reflexive pair, was multi-cocomplete, then since it is also accessible, it would be locally multi-presentable. But then it would have connected limits, in particular pullbacks.' special_objects: terminal object: - description: $[1]$ + description: $[0]$ special_morphisms: monomorphisms: diff --git a/database/data/category-implications/NNO.yaml b/database/data/category-implications/NNO.yaml index 8e7a5fb6..b2fe9fd0 100644 --- a/database/data/category-implications/NNO.yaml +++ b/database/data/category-implications/NNO.yaml @@ -1,39 +1,108 @@ -# results on natural numbers objects +# results on (parametrized) natural numbers objects + +- id: parametrized_nno_assumption + assumptions: + - parametrized natural numbers object + conclusions: + - finite products + proof: This holds by definition. - id: nno_assumption assumptions: - natural numbers object conclusions: - - finite products + - terminal object proof: This holds by definition. -- id: nno_criterion +- id: parametrized_nno_implies_nno assumptions: - - countably distributive + - parametrized natural numbers object conclusions: - natural numbers object - proof: 'Consider the copower $N \coloneqq \coprod_{n \in \IN} 1$ with inclusions $i_n : 1 \to N$ for $n \in \IN$. We define $z \coloneqq i_1 : 1 \to N$ and $s : N \to N$ by $s \circ i_n = i_{n+1}$. Since the category is countably distributive, we have $A \times N \cong \coprod_{n \in \IN} A$ for every object $A$. Given morphisms $f : A \to X$, $g : X \to X$, a morphism $\Phi : A \times N \to X$ therefore corresponds to a family of morphisms $\phi_n : A \to X$ for $n \in \IN$. The condition $\Phi(a,z)=f(a)$ becomes $\phi_0 = f$. The condition $\Phi(a,s(n)) = g(\Phi(a,n))$ becomes $\phi_{n+1} = g \circ \phi_n$. This recursively defines the morphisms $\phi_n$. (We are basically using that $\IN$ is a natural numbers object in $\Set$.) Concretely, $\phi_n = g^n \circ f$.' + proof: Every parametrized natural numbers object is also a natural numbers object; it suffices to apply the universal property with $A=1$. -- id: nno_pointed_case +- id: parametrized_nno_cartesian_closed assumptions: - natural numbers object - - pointed + - cartesian closed conclusions: - - trivial - proof: 'Let $(N,z,s)$ be a natural numbers object in a category with a zero object, denoted $0$. The morphism $z : 0 \to N$ must be zero. The universal property applied to $A=1$ implies that $s : N \to N$ is an initial object in the category of endomorphisms. This exists, it is given by the identity $0 \to 0$. Therefore, $N = 0$. The general universal property now becomes: For all $f : A \to X$, $g : X \to X$ there is a unique $\Phi : A \to X$ such that $\Phi(a) = f(a)$ and $\Phi(a)=g(\Phi(a))$. Apply this to $g = 0$ to conclude $f = 0$.' + - parametrized natural numbers object + proof: 'Let $(N,z,s)$ be a natural numbers object in a cartesian closed category. Let $f : A \to X$ and $g : X \to X$ be morphisms. These induce morphisms $\hat{f} : 1 \to [A,X]$ and $g_* : [A,X] \to [A,X]$. By the universal property of $(N,z,s)$, there is a unique morphism $\Psi : N \to [A,X]$ satisfying $\Psi(z) = \hat{f}$ and $\Psi(s(n)) = g_*(\Psi(n))$. By the exponential adjunction, this corresponds to a morphism $\Phi : A \times N \to X$ satisfying $\Phi(a,z) = f(a)$ and $\Phi(a,s(n)) = g(\Phi(a,n))$.' -- id: nno_terminal +- id: nno_criterion assumptions: + - terminal object + - countable copowers + conclusions: - natural numbers object + proof: >- + Let $1$ be a terminal object and consider the copower + $$\textstyle N \coloneqq \coprod_{n \in \IN} 1$$ + with inclusions $i_n : 1 \to N$ for $n \in \IN$. Define $z \coloneqq i_0 : 1 \to N$ and $s : N \to N$ by + $$s \circ i_n \coloneqq i_{n+1},$$ + using the universal property of the copower. Given a morphism $a : 1 \to X$ and a morphism $g : X \to X$, recursively define morphisms $\phi_n : 1 \to X$ by $\phi_0 \coloneqq a$ and $\phi_{n+1} \coloneqq g \circ \phi_n$. (Here we are essentially using the fact that $(\IN,0,n \mapsto n+1)$ is a natural numbers object in $\Set$.) The universal property of the copower gives a unique morphism $\Phi : N \to X$ satisfying $\Phi \circ i_n = \phi_n$. In particular, $\Phi \circ z = \phi_0 = a$. Moreover, $\Phi \circ s = g \circ \Phi$, since for every $n \in \IN$ we have + $$\Phi \circ s \circ i_n = \Phi \circ i_{n+1} = \phi_{n+1} = g \circ \phi_n = g \circ \Phi \circ i_n.$$ + Conversely, suppose that $\Phi' : N \to X$ satisfies $\Phi' \circ z = a$ and $\Phi' \circ s = g \circ \Phi'$. Then + $$\Phi' \circ i_n = \Phi \circ i_n$$ + follows by induction on $n \in \IN$. It holds for $n=0$ since both sides are $a : 1 \to X$. If it holds for $n$, then + $$\begin{align*} + \Phi' \circ i_{n+1} & = \Phi' \circ s \circ i_n \\ + & = g \circ \Phi' \circ i_n \\ + & = g \circ \Phi \circ i_n \\ + & = \Phi \circ s \circ i_n \\ + & = \Phi \circ i_{n+1}. + \end{align*}$$ + Since $\Phi' \circ i_n = \Phi \circ i_n$ for every $n \in \IN$, we conclude that $\Phi' = \Phi$. + +- id: strict_terminal_implies_nno + assumptions: - strict terminal object conclusions: + - natural numbers object + proof: 'Let $1$ be a strict terminal object. For every endomorphism $g : X \to X$ and every morphism $a : 1 \to X$, we have $g \circ a = a$, because $a$ is an isomorphism and hence $X$ is terminal, which forces $g = \id_X$. Therefore, $(1,\id_1,\id_1)$ is a natural numbers object by Lemma 3 here.' + +- id: pointed_has_nno + assumptions: + - pointed + conclusions: + - natural numbers object + proof: 'If $0$ is a zero object, then $(0,\id_0,\id_0)$ is readily seen to be a natural numbers object; alternatively, this follows from Lemma 3 here.' + +- id: one_way_implies_nno + assumptions: + - terminal object - one-way - proof: 'By assumption, $z : 1 \to N$ is an isomorphism. Therefore, the terminal object $1$ is a NNO with $z = \id_1$ and $s = \id_1$. This precisely means that for all $f : A \to X$ and $g : X \to X$ there is a unique $\Phi : A \to X$ with $\Phi = f$ and $\Phi = g \circ \Phi$. In other words, we have $f = g \circ f$, and therefore $g = \id_X$ (take $f = \id_X$), which proves the claim. (From here one can further deduce that the category is thin.)' + conclusions: + - natural numbers object + proof: This follows from Lemma 3 here. -- id: nno_thin +- id: one_way_implies_parametrized_nno assumptions: - finite products - - thin + - one-way conclusions: - - natural numbers object - proof: The triple $(1, \id_1, \id_1)$ is clearly a NNO. + - parametrized natural numbers object + proof: This follows from Lemma 3 here. + +- id: parametrized_nno_criterion + assumptions: + - countably distributive + conclusions: + - parametrized natural numbers object + proof: 'Consider the copower $N \coloneqq \coprod_{n \in \IN} 1$ with inclusions $i_n : 1 \to N$ for $n \in \IN$. Define $z \coloneqq i_0 : 1 \to N$ and $s : N \to N$ by $s \circ i_n \coloneqq i_{n+1}$. Since the category is countably distributive, we have $A \times N \cong \coprod_{n \in \IN} A$ for every object $A$. Given morphisms $f : A \to X$ and $g : X \to X$, a morphism $\Phi : A \times N \to X$ therefore corresponds to a family of morphisms $\phi_n : A \to X$ for $n \in \IN$. The condition $\Phi(a,z)=f(a)$ becomes $\phi_0 = f$, while the condition $\Phi(a,s(n)) = g(\Phi(a,n))$ becomes $\phi_{n+1} = g \circ \phi_n$. Thus, the morphisms $\phi_n$ are recursively determined; concretely, $\phi_n = g^n \circ f$.' + +- id: parametrized_nno_pointed_case + assumptions: + - parametrized natural numbers object + - pointed + conclusions: + - trivial + proof: 'Let $(N,z,s)$ be a parametrized natural numbers object in a category with a zero object, denoted $0$. The morphism $z : 0 \to N$ must be zero. Applying the universal property with $A=1$ shows that $s : N \to N$ is an initial object in the category of endomorphisms. This initial object exists and is given by the identity $0 \to 0$. Therefore, $N = 0$. Now, Lemma 3 here implies that $\id_X = 0$ for every object $X$, so that $X = 0$.' + +- id: parametrized_nno_strict_terminal + assumptions: + - parametrized natural numbers object + - strict terminal object + conclusions: + - one-way + proof: 'Let $(N,z,s)$ be a parametrized natural numbers object. By assumption, $z : 1 \to N$ is an isomorphism. Hence, $(1,\id_1,\id_1)$ is a parametrized natural numbers object. The claim now follows from Lemma 3 here.' diff --git a/database/data/category-properties/elementary topos.yaml b/database/data/category-properties/elementary topos.yaml index acc9bc2a..f471a704 100644 --- a/database/data/category-properties/elementary topos.yaml +++ b/database/data/category-properties/elementary topos.yaml @@ -9,7 +9,7 @@ related: - Grothendieck topos - cartesian closed - finitely complete - - natural numbers object + - parametrized natural numbers object - subobject classifier - pretopos - quasitopos diff --git a/database/data/category-properties/natural numbers object.yaml b/database/data/category-properties/natural numbers object.yaml index fe1fef4f..b774aa9c 100644 --- a/database/data/category-properties/natural numbers object.yaml +++ b/database/data/category-properties/natural numbers object.yaml @@ -1,18 +1,19 @@ id: natural numbers object relation: has a description: >- - A natural numbers object (NNO) in a category with finite products is a triple + A natural numbers object in a category with a terminal object $1$ is a triple $$(N,\, z : 1 \to N,\, s : N \to N)$$ - satisfying the following universal property: for all $f : A \to X$, $g : X \to X$ there is a unique $\Phi : A \times N \to X$ such that $\Phi(a,z)=f(a)$ and $\Phi(a,s(n)) = g(\Phi(a,n))$ in element notation. + satisfying the following universal property: for all $a : 1 \to X$, $g : X \to X$ there is a unique $\Phi : N \to X$ such that $\Phi \circ z = a$ and $\Phi \circ s = g \circ \Phi$. In element notation, this can also be written as $\Phi(z)=a$ and $\Phi(s(n)) = g(\Phi(n))$. - This concept is an abstraction of the set of natural numbers, which indeed provide a NNO for the category of sets. We have used the parametrized definition here which is more natural (sic!) for categories that are not cartesian closed (cf. Johnstone, Part A, Remark 2.5.3). + This concept is an abstraction of the set of natural numbers, which indeed provides a natural numbers object for the category of sets. There is also a parametrized version, which is more useful in categories that are not cartesian closed. Also, the results below show that "too many" categories have a natural numbers object. nlab_link: https://ncatlab.org/nlab/show/natural+numbers+object dual: null invariant_under_equivalences: true related: + - parametrized natural numbers object - elementary topos - - finite products + - terminal object tags: - topos theory diff --git a/database/data/category-properties/parametrized natural numbers object.yaml b/database/data/category-properties/parametrized natural numbers object.yaml new file mode 100644 index 00000000..012c593e --- /dev/null +++ b/database/data/category-properties/parametrized natural numbers object.yaml @@ -0,0 +1,20 @@ +id: parametrized natural numbers object +relation: has a +description: >- + A parametrized natural numbers object in a category with finite products is a triple + $$(N,\, z : 1 \to N,\, s : N \to N)$$ + satisfying the following universal property: for all $f : A \to X$, $g : X \to X$ there is a unique $\Phi : A \times N \to X$ such that $\Phi(a,z)=f(a)$ and $\Phi(a,s(n)) = g(\Phi(a,n))$ in element notation. + + This concept is an abstraction of the set of natural numbers, which indeed provides a parametrized natural numbers object for the category of sets. If we specialize the universal property to $A=1$, we get the notion of a natural numbers object. The parametrized version is more natural (sic!) for categories that are not cartesian closed (cf. Johnstone, Part A, Remark 2.5.3). +nlab_link: https://ncatlab.org/nlab/show/natural+numbers+object +dual: null +invariant_under_equivalences: true + +related: + - natural numbers object + - elementary topos + - finite products + +tags: + - topos theory + - object behavior diff --git a/database/data/symmetric_monoidal_categories/N+.yaml b/database/data/symmetric_monoidal_categories/N+.yaml index dcc695d5..931a4eac 100644 --- a/database/data/symmetric_monoidal_categories/N+.yaml +++ b/database/data/symmetric_monoidal_categories/N+.yaml @@ -2,7 +2,7 @@ id: N+ name: symmetric monoidal poset of natural numbers notation: $(\IN,\leq,+,0)$ underlying_category: N -description: We view the poset $(\IN,\leq)$ as a thin category and equip it with the strict symmetric monoidal structure defined by $a \otimes b := a + b$ and the monoidal unit $0$. +description: We view the poset $(\IN,\leq)$ as a thin category and equip it with the strict symmetric monoidal structure defined by $a \otimes b \coloneqq a + b$ and the monoidal unit $0$. nlab_link: https://ncatlab.org/nlab/show/monoidal+preorder tags: diff --git a/database/scripts/expected-data/Ab.json b/database/scripts/expected-data/Ab.json index 5805a4e4..c8cc22fa 100644 --- a/database/scripts/expected-data/Ab.json +++ b/database/scripts/expected-data/Ab.json @@ -120,6 +120,7 @@ "extremal generating set": true, "extremal cogenerator": true, "extremal cogenerating set": true, + "natural numbers object": true, "cartesian closed": false, "locally cartesian closed": false, @@ -164,7 +165,7 @@ "coaccessible": false, "countable": false, "essentially countable": false, - "natural numbers object": false, + "parametrized natural numbers object": false, "countably distributive": false, "countably codistributive": false, "CSP": false, diff --git a/database/scripts/expected-data/Set.json b/database/scripts/expected-data/Set.json index 2f30015f..40fa66d4 100644 --- a/database/scripts/expected-data/Set.json +++ b/database/scripts/expected-data/Set.json @@ -99,6 +99,7 @@ "multi-initial object": true, "cartesian filtered colimits": true, "cocartesian cofiltered limits": true, + "parametrized natural numbers object": true, "natural numbers object": true, "countably distributive": true, "filtered-colimit-stable monomorphisms": true, diff --git a/database/scripts/expected-data/Top.json b/database/scripts/expected-data/Top.json index 0c568330..359a0c3d 100644 --- a/database/scripts/expected-data/Top.json +++ b/database/scripts/expected-data/Top.json @@ -73,6 +73,7 @@ "multi-initial object": true, "cocartesian cofiltered limits": true, "countably distributive": true, + "parametrized natural numbers object": true, "natural numbers object": true, "filtered-colimit-stable monomorphisms": true, "quotients of congruences": true,