From 8e9a15aeb3199d3fb8df4f6f221ab14e7ed74a68 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 17 Aug 2026 01:15:09 +0200 Subject: [PATCH 01/10] change name of NNO to parameterized NNO --- content/nno_distributive_criterion.md | 14 ++++++------- database/data/categories/CompHaus.yaml | 4 ++-- database/data/categories/FinSet.yaml | 4 ++-- database/data/categories/Met.yaml | 4 ++-- database/data/categories/PMet.yaml | 4 ++-- database/data/categories/SemiGrp.yaml | 4 ++-- database/data/categories/Setne.yaml | 4 ++-- database/data/categories/Sp.yaml | 4 ++-- database/data/categories/Unif.yaml | 4 ++-- database/data/category-implications/NNO.yaml | 20 +++++++++---------- .../category-properties/elementary topos.yaml | 2 +- ...parameterized natural numbers object.yaml} | 6 +++--- database/scripts/expected-data/Ab.json | 2 +- database/scripts/expected-data/Set.json | 2 +- database/scripts/expected-data/Top.json | 2 +- 15 files changed, 40 insertions(+), 40 deletions(-) rename database/data/category-properties/{natural numbers object.yaml => parameterized natural numbers object.yaml} (54%) diff --git a/content/nno_distributive_criterion.md b/content/nno_distributive_criterion.md index f5e133efc..9c2f72a73 100644 --- a/content/nno_distributive_criterion.md +++ b/content/nno_distributive_criterion.md @@ -1,12 +1,12 @@ --- -title: Natural number objects indicate distributivity -description: A partial converse of the result that countably distributive categories have a NNO. +title: Parametrized natural number objects indicate distributivity +description: We prove a partial converse of the result that countably distributive categories have a parametrized natural numbers object. --- -## Natural number objects indicate distributivity +## Parametrized 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 +Let $\C$ be a category with finite products, arbitrary 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 a split monomorphism. ::: @@ -14,11 +14,11 @@ 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 +In any category with finite products and arbitrary 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.$$ -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$. +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 parametrized NNO, it is also a non-parametrized 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 +Next, we 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 tells us that there is a map $$\Phi : A \times N \to \IN \otimes A$$ diff --git a/database/data/categories/CompHaus.yaml b/database/data/categories/CompHaus.yaml index c1ecb7d60..63db0ea28 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/FinSet.yaml b/database/data/categories/FinSet.yaml index 3b723fef9..b88d3eabd 100644 --- a/database/data/categories/FinSet.yaml +++ b/database/data/categories/FinSet.yaml @@ -54,9 +54,9 @@ unsatisfied_properties: - property: countable proof: This is trivial. - - property: natural numbers object + - property: parametrized natural numbers object proof: >- - If $(N,z,s)$ is a natural numbers object, then + If $(N,z,s)$ is a parametrized 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$. diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml index 8120e40b7..9a02448cd 100644 --- a/database/data/categories/Met.yaml +++ b/database/data/categories/Met.yaml @@ -147,9 +147,9 @@ unsatisfied_properties: For $n \geq 1$ let $X_n$ denote the metric space with underlying set $\{0,1\}$ in which $0,1$ have distance $1/n$. We have bijective non-expansive maps $X_n \to X_{n+1}$, $x \mapsto x$. The colimit of this sequence in $\PMet$ is $\{0,1\}$ where $0,1$ have distance $0$, so the colimit in $\Met$ collapses to $\{0\}$. Therefore, the colimit of the monomorphisms $X_1 \to X_n$, $x \mapsto x$ is the non-injective map $X_1 \to \{0\}$. label: met_no_filtered_colimit_stable_monos - - property: natural numbers object + - property: parametrized natural numbers object proof: >- - If $(N,z,s)$ is a natural numbers object in $\Met$, then + If $(N,z,s)$ is a parametrized 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. diff --git a/database/data/categories/PMet.yaml b/database/data/categories/PMet.yaml index 772327f0f..360788466 100644 --- a/database/data/categories/PMet.yaml +++ b/database/data/categories/PMet.yaml @@ -113,9 +113,9 @@ unsatisfied_properties: - property: binary copowers 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 + - property: parametrized natural numbers object proof: >- - If $(N,z,s)$ is a natural numbers object in $\PMet$, then + If $(N,z,s)$ is a parametrized 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. diff --git a/database/data/categories/SemiGrp.yaml b/database/data/categories/SemiGrp.yaml index 0723d65b1..8a43e3692 100644 --- a/database/data/categories/SemiGrp.yaml +++ b/database/data/categories/SemiGrp.yaml @@ -76,9 +76,9 @@ 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 this result, 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 $$x_{n_1} * \cdots * x_{n_s}$$ diff --git a/database/data/categories/Setne.yaml b/database/data/categories/Setne.yaml index 612b6a9b8..38e3275e9 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 1ddd9e404..e1b04e4d2 100644 --- a/database/data/categories/Sp.yaml +++ b/database/data/categories/Sp.yaml @@ -54,9 +54,9 @@ unsatisfied_properties: Alternatively, the claim follows from this result. - - property: natural numbers object + - property: parametrized natural numbers object proof: >- - If $(N,z,s)$ is a natural numbers object, then + If $(N,z,s)$ is a parametrized 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. diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml index 014f3a886..42f1fab8c 100644 --- a/database/data/categories/Unif.yaml +++ b/database/data/categories/Unif.yaml @@ -121,11 +121,11 @@ 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 this result 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. diff --git a/database/data/category-implications/NNO.yaml b/database/data/category-implications/NNO.yaml index 8e7a5fb6e..1de609708 100644 --- a/database/data/category-implications/NNO.yaml +++ b/database/data/category-implications/NNO.yaml @@ -1,8 +1,8 @@ -# results on natural numbers objects +# results on (parametrized) natural numbers objects - id: nno_assumption assumptions: - - natural numbers object + - parametrized natural numbers object conclusions: - finite products proof: This holds by definition. @@ -11,29 +11,29 @@ assumptions: - countably distributive 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$.' + - 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$. 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 parametrized natural numbers object in $\Set$.) Concretely, $\phi_n = g^n \circ f$.' - id: nno_pointed_case assumptions: - - natural numbers object + - parametrized natural numbers object - pointed 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$.' + 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. 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$.' - id: nno_terminal assumptions: - - natural numbers object + - parametrized natural numbers object - strict terminal object conclusions: - 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.)' + proof: 'By assumption, $z : 1 \to N$ is an isomorphism. Therefore, the terminal object $1$ is a parametrized natural numbers object 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.)' - id: nno_thin assumptions: - finite products - thin conclusions: - - natural numbers object - proof: The triple $(1, \id_1, \id_1)$ is clearly a NNO. + - parametrized natural numbers object + proof: The triple $(1, \id_1, \id_1)$ is clearly a parametrized natural numbers object. diff --git a/database/data/category-properties/elementary topos.yaml b/database/data/category-properties/elementary topos.yaml index acc9bc2ab..f471a7049 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/parameterized natural numbers object.yaml similarity index 54% rename from database/data/category-properties/natural numbers object.yaml rename to database/data/category-properties/parameterized natural numbers object.yaml index fe1fef4f0..9289d4ed9 100644 --- a/database/data/category-properties/natural numbers object.yaml +++ b/database/data/category-properties/parameterized natural numbers object.yaml @@ -1,11 +1,11 @@ -id: natural numbers object +id: parametrized natural numbers object relation: has a description: >- - A natural numbers object (NNO) in a category with finite products is a triple + 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 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 provide a parametrized natural numbers object 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). nlab_link: https://ncatlab.org/nlab/show/natural+numbers+object dual: null invariant_under_equivalences: true diff --git a/database/scripts/expected-data/Ab.json b/database/scripts/expected-data/Ab.json index 5805a4e49..39c59ef83 100644 --- a/database/scripts/expected-data/Ab.json +++ b/database/scripts/expected-data/Ab.json @@ -164,7 +164,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 2f30015f1..dda9992d3 100644 --- a/database/scripts/expected-data/Set.json +++ b/database/scripts/expected-data/Set.json @@ -99,7 +99,7 @@ "multi-initial object": true, "cartesian filtered colimits": true, "cocartesian cofiltered limits": true, - "natural numbers object": true, + "parametrized natural numbers object": true, "countably distributive": true, "filtered-colimit-stable monomorphisms": true, "quotients of congruences": true, diff --git a/database/scripts/expected-data/Top.json b/database/scripts/expected-data/Top.json index 0c5683308..547c0e59f 100644 --- a/database/scripts/expected-data/Top.json +++ b/database/scripts/expected-data/Top.json @@ -73,7 +73,7 @@ "multi-initial object": true, "cocartesian cofiltered limits": true, "countably distributive": true, - "natural numbers object": true, + "parametrized natural numbers object": true, "filtered-colimit-stable monomorphisms": true, "quotients of congruences": true, "coquotients of cocongruences": true, From c6a02524228e085566176812a8589e3dc157882f Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 17 Aug 2026 11:54:56 +0200 Subject: [PATCH 02/10] add non-parametrized NNOs --- database/data/category-implications/NNO.yaml | 96 ++++++++++++++++--- .../natural numbers object.yaml | 20 ++++ .../parameterized natural numbers object.yaml | 3 +- .../symmetric_monoidal_categories/N+.yaml | 2 +- database/scripts/expected-data/Ab.json | 1 + database/scripts/expected-data/Set.json | 1 + database/scripts/expected-data/Top.json | 1 + 7 files changed, 109 insertions(+), 15 deletions(-) create mode 100644 database/data/category-properties/natural numbers object.yaml diff --git a/database/data/category-implications/NNO.yaml b/database/data/category-implications/NNO.yaml index 1de609708..ad2b993b4 100644 --- a/database/data/category-implications/NNO.yaml +++ b/database/data/category-implications/NNO.yaml @@ -1,20 +1,98 @@ # results on (parametrized) natural numbers objects -- id: nno_assumption +- 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: + - terminal object + proof: This holds by definition. + +- id: parametrized_nno_implies_nno + assumptions: + - parametrized natural numbers object + conclusions: + - natural numbers object + proof: Every parametrized natural numbers object is also a natural numbers object; we just need to apply the universal property to $A=1$. + +- id: parametrized_nno_cartesian_closed + assumptions: + - natural numbers object + - cartesian closed + conclusions: + - 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. Then we get morphisms $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) = f$ and $\Psi(s(n)) = g_*(\Psi(n))$. This corresponds to a morphism $\Phi : A \times N \to X$ satisfying $\Phi(z,a) = f(a)$ and $\Phi(a,s(n)) = g(\Phi(a,n))$.' + - 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$. We 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$, for every $n \in \IN$ we define the morphism $\phi_n : 1 \to X$ recursively by $\phi_0 \coloneqq a$ and $\phi_{n+1} \coloneqq g \circ \phi_n$. (Here we are basically using that $(\IN,0,n \mapsto n+1)$ is a natural numbers object in $\Set$.) + The universal property of the copower implies that there exist a unique morphism $\Phi : N \to X$ with $\Phi \circ i_n = \phi_n$. In particular, we have $\Phi \circ z = \phi_0 = a$. Moreover, $\Phi \circ s = g \circ \Phi$ holds because 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, if $\Phi' : N \to X$ is a morphism with $\Phi' \circ z = a$ and $\Phi' \circ s = g \circ \Phi'$, then + $$\Phi' \circ i_n = \Phi \circ i_n$$ + follows by induction for every $n \in \IN$: It is true 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$ holds for every $n \in \IN$, we conclude $\Phi' = \Phi$. + +- id: strict_terminal_implies_nno + assumptions: + - strict terminal object + conclusions: + - natural numbers object + proof: 'Let $1$ be a strict terminal object. Then $(1,\id_1,\id_1)$ is a natural numbers object: If $a : 1 \to X$, $g : X \to X$ are given, then $a$ must be an isomorphism, so that $X$ is terminal. In particular, $g = \id_X$. Then $\Phi \coloneqq a$ is the unique morphism $\Phi : 1 \to X$ satisfying $\Phi \circ \id_1 = a$ and $\Phi \circ \id_1 = g \circ \Phi$.' + +- id: pointed_has_nno + assumptions: + - pointed + conclusions: + - natural numbers object + proof: If $0$ is a zero object, then it is easy to check that $(0, \id_0, \id_0)$ is a natural numbers object. + +- id: one_way_implies_nno + assumptions: + - terminal object + - one-way + conclusions: + - natural numbers object + proof: 'Let $1$ be a terminal object in a one-way category. Then $(1,\id_1,\id_1)$ is a natural numbers object: If $a : 1 \to X$, $g : X \to X$ are given, then $g = \id_X$ is forced. Then $\Phi \coloneqq a$ is the unique morphism $\Phi : 1 \to X$ satisfying $\Phi \circ \id_1 = a$ and $\Phi \circ \id_1 = g \circ \Phi$.' + +- id: one_way_implies_parametrized_nno + assumptions: + - finite products + - one-way + conclusions: + - parametrized natural numbers object + proof: 'If $1$ denotes the terminal object, then the triple $(1, \id_1, \id_1)$ is a parametrized natural numbers object: If $f : A \to X$ and $g : X \to X$ are given, then $g = \id_X$ is forced, and $\Phi \coloneqq f : A \to X$ is the unique morphism satisfying the requirements.' + +- 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$. 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 parametrized natural numbers object in $\Set$.) Concretely, $\phi_n = g^n \circ f$.' + 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_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$, $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, 0, n \mapsto n+1)$ is a natural numbers object in $\Set$.) Concretely, $\phi_n = g^n \circ f$.' -- id: nno_pointed_case +- id: parametrized_nno_pointed_case assumptions: - parametrized natural numbers object - pointed @@ -22,18 +100,10 @@ - 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. 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$.' -- id: nno_terminal +- id: parametrized_nno_strict_terminal assumptions: - parametrized natural numbers object - strict terminal object conclusions: - one-way - proof: 'By assumption, $z : 1 \to N$ is an isomorphism. Therefore, the terminal object $1$ is a parametrized natural numbers object 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.)' - -- id: nno_thin - assumptions: - - finite products - - thin - conclusions: - - parametrized natural numbers object - proof: The triple $(1, \id_1, \id_1)$ is clearly a parametrized natural numbers object. + proof: 'Let $(N,z,s)$ be a parametrized natural numbers object. By assumption, $z : 1 \to N$ is an isomorphism. Therefore, the terminal object $1$ is a parametrized natural numbers object 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.)' diff --git a/database/data/category-properties/natural numbers object.yaml b/database/data/category-properties/natural numbers object.yaml new file mode 100644 index 000000000..b774aa9c7 --- /dev/null +++ b/database/data/category-properties/natural numbers object.yaml @@ -0,0 +1,20 @@ +id: natural numbers object +relation: has a +description: >- + 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 $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 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 + - terminal object + +tags: + - topos theory + - object behavior diff --git a/database/data/category-properties/parameterized natural numbers object.yaml b/database/data/category-properties/parameterized natural numbers object.yaml index 9289d4ed9..012c593e8 100644 --- a/database/data/category-properties/parameterized natural numbers object.yaml +++ b/database/data/category-properties/parameterized natural numbers object.yaml @@ -5,12 +5,13 @@ description: >- $$(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 provide a parametrized natural numbers object 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 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 diff --git a/database/data/symmetric_monoidal_categories/N+.yaml b/database/data/symmetric_monoidal_categories/N+.yaml index dcc695d57..931a4eac6 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 39c59ef83..c8cc22fab 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, diff --git a/database/scripts/expected-data/Set.json b/database/scripts/expected-data/Set.json index dda9992d3..40fa66d4c 100644 --- a/database/scripts/expected-data/Set.json +++ b/database/scripts/expected-data/Set.json @@ -100,6 +100,7 @@ "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, "quotients of congruences": true, diff --git a/database/scripts/expected-data/Top.json b/database/scripts/expected-data/Top.json index 547c0e59f..359a0c3d0 100644 --- a/database/scripts/expected-data/Top.json +++ b/database/scripts/expected-data/Top.json @@ -74,6 +74,7 @@ "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, "coquotients of cocongruences": true, From 6d8de28c0d96d7a1ec586314fed2bd40f4d4b0db Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 17 Aug 2026 12:07:05 +0200 Subject: [PATCH 03/10] prove the coproduct lemma on NNOs --- content/natural_number_objects.md | 48 ++++++++++++++++++++++++++++ database/data/categories/FinSet.yaml | 7 ++-- database/data/categories/Met.yaml | 10 ++---- database/data/categories/PMet.yaml | 10 ++---- database/data/categories/Sp.yaml | 7 ++-- 5 files changed, 56 insertions(+), 26 deletions(-) create mode 100644 content/natural_number_objects.md diff --git a/content/natural_number_objects.md b/content/natural_number_objects.md new file mode 100644 index 000000000..803b49659 --- /dev/null +++ b/content/natural_number_objects.md @@ -0,0 +1,48 @@ +--- +title: Natural number objects +description: We prove some results on natural number objects. +--- + +## Natural number objects + +The definition of a [natural number object](/category-property/natural_numbers_object) a priori only allows for recursively defined morphisms for which the next value $\Phi(s(n))$ depends only on the previous value $\Phi(n)$. But in many cases, we would like to also use $n$ to recursively 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 are using element notation to simplify the exposition. For example, the equation $\Phi(s(n)) = g(n,\Phi(n))$ says that the diagram + +$$ +\begin{CD} +N @>{s}>> N \\ +@V{(\id_N,\Phi)}VV @VV{\Phi}V \\ +N \times X @>>{g}> X +\end{CD} +$$ + +commutes. + +_Proof._ We 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))$. Using the universal property of $(N,z,s)$, there exist a unique morphism $\Psi : N \to N \times X$ such that + +- $\Psi(z) = b$ +- $\Psi(s(n)) = h(\Psi(n))$ + +holds. We may write $\Psi(n) = (\Psi_0(n),\Psi_1(n))$ with two morphisms $\Psi_0 : N \to N$ and $\Psi_1 : N \to X$. The two equations above 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 := \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 a bit more concise because we have extracted Lemma 1 before. + +::: 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$ diff --git a/database/data/categories/FinSet.yaml b/database/data/categories/FinSet.yaml index b88d3eabd..05ac03765 100644 --- a/database/data/categories/FinSet.yaml +++ b/database/data/categories/FinSet.yaml @@ -54,11 +54,8 @@ unsatisfied_properties: - property: countable proof: This is trivial. - - property: parametrized natural numbers object - proof: >- - If $(N,z,s)$ is a parametrized 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$. + - 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. special_objects: initial object: diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml index 9a02448cd..702cd32aa 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)$. @@ -147,11 +144,8 @@ unsatisfied_properties: For $n \geq 1$ let $X_n$ denote the metric space with underlying set $\{0,1\}$ in which $0,1$ have distance $1/n$. We have bijective non-expansive maps $X_n \to X_{n+1}$, $x \mapsto x$. The colimit of this sequence in $\PMet$ is $\{0,1\}$ where $0,1$ have distance $0$, so the colimit in $\Met$ collapses to $\{0\}$. Therefore, the colimit of the monomorphisms $X_1 \to X_n$, $x \mapsto x$ is the non-injective map $X_1 \to \{0\}$. label: met_no_filtered_colimit_stable_monos - - property: parametrized natural numbers object - proof: >- - If $(N,z,s)$ is a parametrized 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. + - 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. - 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 360788466..973d1ea80 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.' @@ -113,11 +110,8 @@ unsatisfied_properties: - property: binary copowers 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: parametrized natural numbers object - proof: >- - If $(N,z,s)$ is a parametrized 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. + - 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. - 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/Sp.yaml b/database/data/categories/Sp.yaml index e1b04e4d2..b4912b57a 100644 --- a/database/data/categories/Sp.yaml +++ b/database/data/categories/Sp.yaml @@ -54,11 +54,8 @@ unsatisfied_properties: Alternatively, the claim follows from this result. - - property: parametrized natural numbers object - proof: >- - If $(N,z,s)$ is a parametrized 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. + - 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. special_objects: initial object: From 0712e0b8b6381395eb9655901eeb873b6aca438c Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 17 Aug 2026 12:16:47 +0200 Subject: [PATCH 04/10] move existing result on parametrized NNOs to new content page --- content/natural_number_objects.md | 28 ++++++++++++++++++++++++ content/nno_distributive_criterion.md | 31 --------------------------- database/data/categories/SemiGrp.yaml | 2 +- database/data/categories/Unif.yaml | 2 +- 4 files changed, 30 insertions(+), 33 deletions(-) delete mode 100644 content/nno_distributive_criterion.md diff --git a/content/natural_number_objects.md b/content/natural_number_objects.md index 803b49659..b186ba6d9 100644 --- a/content/natural_number_objects.md +++ b/content/natural_number_objects.md @@ -46,3 +46,31 @@ 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 prove a partial converse of the [result](/category-implication/parametrized_nno_criterion) that countably distributive categories have a parametrized natural numbers object. + +::: Lemma 3 +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 a split monomorphism. +::: + +_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 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 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 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/content/nno_distributive_criterion.md b/content/nno_distributive_criterion.md deleted file mode 100644 index 9c2f72a73..000000000 --- a/content/nno_distributive_criterion.md +++ /dev/null @@ -1,31 +0,0 @@ ---- -title: Parametrized natural number objects indicate distributivity -description: We prove a partial converse of the result that countably distributive categories have a parametrized natural numbers object. ---- - -## Parametrized natural number objects indicate distributivity - -::: Lemma -Let $\C$ be a category with finite products, arbitrary 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 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-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.$$ -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 parametrized NNO, it is also a non-parametrized 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 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 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/SemiGrp.yaml b/database/data/categories/SemiGrp.yaml index 8a43e3692..6d60f957d 100644 --- a/database/data/categories/SemiGrp.yaml +++ b/database/data/categories/SemiGrp.yaml @@ -78,7 +78,7 @@ unsatisfied_properties: - property: parametrized natural numbers object proof: >- - Assume that a parametrized 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 3 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 $$x_{n_1} * \cdots * x_{n_s}$$ diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml index 42f1fab8c..f14308bd7 100644 --- a/database/data/categories/Unif.yaml +++ b/database/data/categories/Unif.yaml @@ -125,7 +125,7 @@ unsatisfied_properties: 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 parametrized natural numbers object, then by this result the canonical map + If there were a parametrized natural numbers object, then by Lemma 3 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. From ecfa1121dbaaf03fbfaae54ea75036bef5cbaadf Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 17 Aug 2026 14:31:27 +0200 Subject: [PATCH 05/10] add lemma that decides when 1 is NNO --- ...al_number_objects.md => natural_numbers_objects.md} | 8 +++++++- database/data/categories/FinSet.yaml | 2 +- database/data/categories/Met.yaml | 2 +- database/data/categories/PMet.yaml | 2 +- database/data/categories/SemiGrp.yaml | 2 +- database/data/categories/Sp.yaml | 2 +- database/data/categories/Unif.yaml | 2 +- database/data/category-implications/NNO.yaml | 10 +++++----- 8 files changed, 18 insertions(+), 12 deletions(-) rename content/{natural_number_objects.md => natural_numbers_objects.md} (81%) diff --git a/content/natural_number_objects.md b/content/natural_numbers_objects.md similarity index 81% rename from content/natural_number_objects.md rename to content/natural_numbers_objects.md index b186ba6d9..6ebfd762a 100644 --- a/content/natural_number_objects.md +++ b/content/natural_numbers_objects.md @@ -47,9 +47,15 @@ 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$ +::: 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._ This first statement is immediate from the definition of a natural numbers of 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$. But these equations simplify to $\Phi = f$ and $f = g \circ f$. Since this must hold for all $f : A \to X$, we must have $g = \id_X$ (by the Yoneda Lemma or a direct argument). $\square$ + Next, we prove a partial converse of the [result](/category-implication/parametrized_nno_criterion) that countably distributive categories have a parametrized natural numbers object. -::: Lemma 3 +::: 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 a split monomorphism. diff --git a/database/data/categories/FinSet.yaml b/database/data/categories/FinSet.yaml index 05ac03765..1ffea278c 100644 --- a/database/data/categories/FinSet.yaml +++ b/database/data/categories/FinSet.yaml @@ -55,7 +55,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 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 702cd32aa..3415d557d 100644 --- a/database/data/categories/Met.yaml +++ b/database/data/categories/Met.yaml @@ -145,7 +145,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 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 973d1ea80..4635ae69c 100644 --- a/database/data/categories/PMet.yaml +++ b/database/data/categories/PMet.yaml @@ -111,7 +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: 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 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 6d60f957d..b144ca40d 100644 --- a/database/data/categories/SemiGrp.yaml +++ b/database/data/categories/SemiGrp.yaml @@ -78,7 +78,7 @@ unsatisfied_properties: - property: parametrized natural numbers object proof: >- - Assume that a parametrized natural numbers object exists. Then by Lemma 3 here, 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 $$x_{n_1} * \cdots * x_{n_s}$$ diff --git a/database/data/categories/Sp.yaml b/database/data/categories/Sp.yaml index b4912b57a..b43eeec43 100644 --- a/database/data/categories/Sp.yaml +++ b/database/data/categories/Sp.yaml @@ -55,7 +55,7 @@ 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 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 f14308bd7..10b6a0349 100644 --- a/database/data/categories/Unif.yaml +++ b/database/data/categories/Unif.yaml @@ -125,7 +125,7 @@ unsatisfied_properties: 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 parametrized natural numbers object, then by Lemma 3 here, 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. diff --git a/database/data/category-implications/NNO.yaml b/database/data/category-implications/NNO.yaml index ad2b993b4..ce603b968 100644 --- a/database/data/category-implications/NNO.yaml +++ b/database/data/category-implications/NNO.yaml @@ -60,14 +60,14 @@ - strict terminal object conclusions: - natural numbers object - proof: 'Let $1$ be a strict terminal object. Then $(1,\id_1,\id_1)$ is a natural numbers object: If $a : 1 \to X$, $g : X \to X$ are given, then $a$ must be an isomorphism, so that $X$ is terminal. In particular, $g = \id_X$. Then $\Phi \coloneqq a$ is the unique morphism $\Phi : 1 \to X$ satisfying $\Phi \circ \id_1 = a$ and $\Phi \circ \id_1 = g \circ \Phi$.' + 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, so that $X$ is terminal, forcing $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 it is easy to check that $(0, \id_0, \id_0)$ is a natural numbers object. + proof: If $0$ is a zero object, then it is easy to check that $(0, \id_0, \id_0)$ is a natural numbers object; one can also derive this from Lemma 3 here. - id: one_way_implies_nno assumptions: @@ -75,7 +75,7 @@ - one-way conclusions: - natural numbers object - proof: 'Let $1$ be a terminal object in a one-way category. Then $(1,\id_1,\id_1)$ is a natural numbers object: If $a : 1 \to X$, $g : X \to X$ are given, then $g = \id_X$ is forced. Then $\Phi \coloneqq a$ is the unique morphism $\Phi : 1 \to X$ satisfying $\Phi \circ \id_1 = a$ and $\Phi \circ \id_1 = g \circ \Phi$.' + proof: This follows from Lemma 3 here. - id: one_way_implies_parametrized_nno assumptions: @@ -83,7 +83,7 @@ - one-way conclusions: - parametrized natural numbers object - proof: 'If $1$ denotes the terminal object, then the triple $(1, \id_1, \id_1)$ is a parametrized natural numbers object: If $f : A \to X$ and $g : X \to X$ are given, then $g = \id_X$ is forced, and $\Phi \coloneqq f : A \to X$ is the unique morphism satisfying the requirements.' + proof: This follows from Lemma 3 here. - id: parametrized_nno_criterion assumptions: @@ -106,4 +106,4 @@ - 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. Therefore, the terminal object $1$ is a parametrized natural numbers object 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.)' + 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. Now the claim follows from Lemma 3 here.' From b68398cf62c7735342e789bdc98c2c8a4cdfa49e Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 17 Aug 2026 15:11:18 +0200 Subject: [PATCH 06/10] FinOrd, Delta, and the walking coreflexive pair have no NNO --- database/data/categories/Delta.yaml | 7 +++++-- database/data/categories/FinOrd.yaml | 3 +++ database/data/categories/walking_coreflexive_pair.yaml | 9 ++++++--- 3 files changed, 14 insertions(+), 5 deletions(-) diff --git a/database/data/categories/Delta.yaml b/database/data/categories/Delta.yaml index 2ccb85b7e..e72803e5c 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 @@ -100,6 +100,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 edd577865..fdaa537c4 100644 --- a/database/data/categories/FinOrd.yaml +++ b/database/data/categories/FinOrd.yaml @@ -88,6 +88,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/walking_coreflexive_pair.yaml b/database/data/categories/walking_coreflexive_pair.yaml index 2d3352482..e28a9a5a4 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 @@ -76,13 +76,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: From 0a88f80489b17f0e92f57e2bbb4b6cff218b0f33 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 17 Aug 2026 15:31:12 +0200 Subject: [PATCH 07/10] improve spelling for content on NNOs --- content/natural_numbers_objects.md | 54 ++++++++++---------- database/data/category-implications/NNO.yaml | 27 +++++----- 2 files changed, 40 insertions(+), 41 deletions(-) diff --git a/content/natural_numbers_objects.md b/content/natural_numbers_objects.md index 6ebfd762a..20e80dddc 100644 --- a/content/natural_numbers_objects.md +++ b/content/natural_numbers_objects.md @@ -1,17 +1,17 @@ --- -title: Natural number objects -description: We prove some results on natural number objects. +title: Natural numbers objects +description: We prove some results on natural numbers objects. --- -## Natural number objects +## Natural numbers objects -The definition of a [natural number object](/category-property/natural_numbers_object) a priori only allows for recursively defined morphisms for which the next value $\Phi(s(n))$ depends only on the previous value $\Phi(n)$. But in many cases, we would like to also use $n$ to recursively define $\Phi(s(n))$. This can be done in categories with finite products: +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 are using element notation to simplify the exposition. For example, the equation $\Phi(s(n)) = g(n,\Phi(n))$ says that the diagram +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} @@ -21,23 +21,21 @@ N \times X @>>{g}> X \end{CD} $$ -commutes. - -_Proof._ We 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))$. Using the universal property of $(N,z,s)$, there exist a unique morphism $\Psi : N \to N \times X$ such that +_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))$ -holds. We may write $\Psi(n) = (\Psi_0(n),\Psi_1(n))$ with two morphisms $\Psi_0 : N \to N$ and $\Psi_1 : N \to X$. The two equations above become: +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))$ +- $\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 := \Psi_1$ is the unique morphism $\Phi : N \to X$ satisfying $\Phi(z)=a$ and $\Phi(s(n)) = g(n,\Phi(n))$. $\square$ +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 a bit more concise because we have extracted Lemma 1 before. +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 @@ -47,13 +45,15 @@ 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._ This first statement is immediate from the definition of a natural numbers of 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$. But these equations simplify to $\Phi = f$ and $f = g \circ f$. Since this must hold for all $f : A \to X$, we must have $g = \id_X$ (by the Yoneda Lemma or a direct argument). $\square$ +_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 of the [result](/category-implication/parametrized_nno_criterion) that countably distributive categories have a parametrized natural numbers object. +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 @@ -61,22 +61,22 @@ $$\alpha : \IN \otimes A \to A \times (\IN \otimes 1)$$ is a split monomorphism. ::: -_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).$$ +_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 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$. +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, we apply the parametrized universal property of the NNO to the diagram +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 tells us that there is a map +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$$ -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}$. +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}$. $\square$ diff --git a/database/data/category-implications/NNO.yaml b/database/data/category-implications/NNO.yaml index ce603b968..b2fe9fd0b 100644 --- a/database/data/category-implications/NNO.yaml +++ b/database/data/category-implications/NNO.yaml @@ -19,7 +19,7 @@ - parametrized natural numbers object conclusions: - natural numbers object - proof: Every parametrized natural numbers object is also a natural numbers object; we just need to apply the universal property to $A=1$. + proof: Every parametrized natural numbers object is also a natural numbers object; it suffices to apply the universal property with $A=1$. - id: parametrized_nno_cartesian_closed assumptions: @@ -27,7 +27,7 @@ - cartesian closed conclusions: - 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. Then we get morphisms $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) = f$ and $\Psi(s(n)) = g_*(\Psi(n))$. This corresponds to a morphism $\Phi : A \times N \to X$ satisfying $\Phi(z,a) = f(a)$ and $\Phi(a,s(n)) = g(\Phi(a,n))$.' + 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_criterion assumptions: @@ -38,36 +38,35 @@ 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$. We define $z \coloneqq i_0 : 1 \to N$ and $s : N \to N$ by + 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$, for every $n \in \IN$ we define the morphism $\phi_n : 1 \to X$ recursively by $\phi_0 \coloneqq a$ and $\phi_{n+1} \coloneqq g \circ \phi_n$. (Here we are basically using that $(\IN,0,n \mapsto n+1)$ is a natural numbers object in $\Set$.) - The universal property of the copower implies that there exist a unique morphism $\Phi : N \to X$ with $\Phi \circ i_n = \phi_n$. In particular, we have $\Phi \circ z = \phi_0 = a$. Moreover, $\Phi \circ s = g \circ \Phi$ holds because for every $n \in \IN$ we have + 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, if $\Phi' : N \to X$ is a morphism with $\Phi' \circ z = a$ and $\Phi' \circ s = g \circ \Phi'$, then + 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 for every $n \in \IN$: It is true for $n = 0$ since both sides are $a : 1 \to X$. If it holds for $n$, then + 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} + & = \Phi \circ i_{n+1}. \end{align*}$$ - Since $\Phi' \circ i_n = \Phi \circ i_n$ holds for every $n \in \IN$, we conclude $\Phi' = \Phi$. + 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, so that $X$ is terminal, forcing $g = \id_X$. Therefore, $(1,\id_1,\id_1)$ is a natural numbers object by Lemma 3 here.' + 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 it is easy to check that $(0, \id_0, \id_0)$ is a natural numbers object; one can also derive this from Lemma 3 here. + 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: @@ -90,7 +89,7 @@ - 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$. We 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$, $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, 0, n \mapsto n+1)$ is a natural numbers object in $\Set$.) Concretely, $\phi_n = g^n \circ f$.' + 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: @@ -98,7 +97,7 @@ - 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. 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$.' + 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: @@ -106,4 +105,4 @@ - 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. Now the claim follows from Lemma 3 here.' + 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.' From baa37c565e04ad03c1fd0ebe0d2a2352e542ac99 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 17 Aug 2026 18:35:56 +0200 Subject: [PATCH 08/10] fix proof that SemiGrp has no parametrized NNO --- database/data/categories/SemiGrp.yaml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/database/data/categories/SemiGrp.yaml b/database/data/categories/SemiGrp.yaml index b144ca40d..82b1279dc 100644 --- a/database/data/categories/SemiGrp.yaml +++ b/database/data/categories/SemiGrp.yaml @@ -84,9 +84,9 @@ unsatisfied_properties: $$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: >- From d34834e869c5e8bb8fac1caed24a7c85dd6cd67c Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 17 Aug 2026 22:53:47 +0200 Subject: [PATCH 09/10] remove new redundancies; rename file --- database/data/categories/Delta.yaml | 3 --- database/data/categories/FinOrd.yaml | 6 ------ database/data/categories/walking_coreflexive_pair.yaml | 3 --- ...object.yaml => parametrized natural numbers object.yaml} | 0 4 files changed, 12 deletions(-) rename database/data/category-properties/{parameterized natural numbers object.yaml => parametrized natural numbers object.yaml} (100%) diff --git a/database/data/categories/Delta.yaml b/database/data/categories/Delta.yaml index e72803e5c..e53d50eaa 100644 --- a/database/data/categories/Delta.yaml +++ b/database/data/categories/Delta.yaml @@ -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.' diff --git a/database/data/categories/FinOrd.yaml b/database/data/categories/FinOrd.yaml index fdaa537c4..209ad6d7b 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 diff --git a/database/data/categories/walking_coreflexive_pair.yaml b/database/data/categories/walking_coreflexive_pair.yaml index e28a9a5a4..a0dc89c15 100644 --- a/database/data/categories/walking_coreflexive_pair.yaml +++ b/database/data/categories/walking_coreflexive_pair.yaml @@ -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.' diff --git a/database/data/category-properties/parameterized natural numbers object.yaml b/database/data/category-properties/parametrized natural numbers object.yaml similarity index 100% rename from database/data/category-properties/parameterized natural numbers object.yaml rename to database/data/category-properties/parametrized natural numbers object.yaml From 81b36bef96c735ea4438766258065de529bc6a93 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 18 Aug 2026 00:20:50 +0200 Subject: [PATCH 10/10] strengthen the connection between distributivity and parametrized NNOs --- content/natural_numbers_objects.md | 25 +++++++++++++++++++++++-- database/data/categories/SemiGrp.yaml | 2 +- database/data/categories/Unif.yaml | 2 +- 3 files changed, 25 insertions(+), 4 deletions(-) diff --git a/content/natural_numbers_objects.md b/content/natural_numbers_objects.md index 20e80dddc..b3bd73d6b 100644 --- a/content/natural_numbers_objects.md +++ b/content/natural_numbers_objects.md @@ -58,7 +58,7 @@ Next, we prove a partial converse to the [result](/category-implication/parametr ::: 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 a split monomorphism. +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 @@ -79,4 +79,25 @@ $$\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}$. -$\square$ + +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/database/data/categories/SemiGrp.yaml b/database/data/categories/SemiGrp.yaml index 82b1279dc..d9899349c 100644 --- a/database/data/categories/SemiGrp.yaml +++ b/database/data/categories/SemiGrp.yaml @@ -80,7 +80,7 @@ unsatisfied_properties: proof: >- 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).$$ diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml index 10b6a0349..5e3c9d61c 100644 --- a/database/data/categories/Unif.yaml +++ b/database/data/categories/Unif.yaml @@ -127,7 +127,7 @@ unsatisfied_properties: 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$.