Add Natural Numbers Object

database/data/003_properties/003_limits-colimits-behavior.sql

@@ -58,6 +58,22 @@ VALUES
 	'infinitary codistributive',
 	TRUE
 ),
+(
+	'countably distributive',
+	'is',
+	'A category is <i>countably distributive</i> if it has finite products, countable coproducts, and for every object $A$ the functor $A \times -$ preserves countable coproducts. Concretely, for every countable family of objects $(B_i)$ the canonical morphism $\coprod_i (A \times B_i) \to A \times \coprod_i B_i$ must be an isomorphism.',
+	NULL,
+	'countably codistributive',
+	TRUE
+),
+(
+	'countably codistributive',
+	'is',
+	'A category is <i>countably codistributive</i> if it has finite coproducts, countable products, and for every object $A$ the functor $A \sqcup -$ preserves countable products. Concretely, for every countable family of objects $(B_i)$ the canonical morphism $A \sqcup \prod_i B_i \to \prod_i (A \sqcup B_i)$ must be an isomorphism.',
+	NUll,
+	'countably distributive',
+	TRUE
+),
 (
 	'codistributive',
 	'is',

database/data/003_properties/009_topos-theory.sql

@@ -98,4 +98,15 @@ VALUES
 	'https://ncatlab.org/nlab/show/Grothendieck+topos',
 	NULL,
 	TRUE
+),
+(
+	'natural numbers object',
+	'has a',
+	'A <i>natural numbers object</i> (NNO) in a category with finite products is a triple
+	<p>$(N,\, z : 1 \to N,\, s : N \to N)$</p>
+	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.
+	<br>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. <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, Part A, Remark 2.5.3).',
+	'https://ncatlab.org/nlab/show/natural+numbers+object',
+	NULL,
+	TRUE
 );

database/data/003_properties/100_related-properties.sql

@@ -59,7 +59,10 @@ VALUES
 ('elementary topos', 'cartesian closed'),
 ('elementary topos', 'finitely complete'),
 ('elementary topos', 'subobject classifier'),
+('elementary topos', 'natural numbers object'),
 ('Grothendieck topos', 'elementary topos'),
+('natural numbers object', 'elementary topos'),
+('natural numbers object', 'finite products'),
 ('initial object', 'finite coproducts'),
 ('initial object', 'multi-initial object'),
 ('terminal object', 'finite products'),
@@ -155,18 +158,30 @@ VALUES
 ('quotient object classifier', 'regular quotient object classifier'),
 ('regular quotient object classifier', 'quotient object classifier'),
 ('regular quotient object classifier', 'finitely cocomplete'),
-('infinitary distributive', 'distributive'),
-('infinitary distributive', 'finite products'),
-('infinitary distributive', 'coproducts'),
 ('distributive', 'infinitary distributive'),
+('distributive', 'countably distributive'),
 ('distributive', 'finite products'),
 ('distributive', 'finite coproducts'),
-('infinitary codistributive', 'codistributive'),
-('infinitary codistributive', 'finite coproducts'),
-('infinitary codistributive', 'products'),
+('countably distributive', 'distributive'),
+('countably distributive', 'infinitary distributive'),
+('countably distributive', 'finite products'),
+('countably distributive', 'countable coproducts'),
+('infinitary distributive', 'distributive'),
+('infinitary distributive', 'countably distributive'),
+('infinitary distributive', 'finite products'),
+('infinitary distributive', 'coproducts'),
 ('codistributive', 'infinitary codistributive'),
+('codistributive', 'countably codistributive'),
 ('codistributive', 'finite products'),
 ('codistributive', 'finite coproducts'),
+('countably codistributive', 'codistributive'),
+('countably codistributive', 'infinitary codistributive'),
+('countably codistributive', 'finite coproducts'),
+('countably codistributive', 'countable products'),
+('infinitary codistributive', 'codistributive'),
+('infinitary codistributive', 'countably codistributive'),
+('infinitary codistributive', 'finite coproducts'),
+('infinitary codistributive', 'products'),
 ('exact filtered colimits', 'filtered colimits'),
 ('exact filtered colimits', 'finitely complete'),
 ('exact filtered colimits', 'cartesian filtered colimits'),

database/data/004_property-assignments/CAlg(R).sql

@@ -55,7 +55,7 @@ VALUES
 ),
 (
 	'CAlg(R)',
-	'infinitary codistributive',
+	'countably codistributive',
 	FALSE,
 	'The canonical homomorphism $A \otimes_R R^{\mathbb{N}} \to A^{\mathbb{N}}$ is given by $a \otimes (r_n)_n \mapsto (r_n a)_n$ and does not have to be surjective: Since $R \neq 0$, there is a commutative $R$-algebra $K$ which is a field. Now take $A := K[X]$ and consider the sequence $(X^n)_{n} \in A^{\mathbb{N}}$.'
 ),

database/data/004_property-assignments/CRing.sql

@@ -55,7 +55,7 @@ VALUES
 ),
 (
 	'CRing',
-	'infinitary codistributive',
+	'countably codistributive',
 	FALSE,
 	'The canonical homomorphism $\mathbb{Q} \otimes \mathbb{Z}^{\mathbb{N}} \to (\mathbb{Q} \otimes \mathbb{Z})^{\mathbb{N}} = \mathbb{Q}^{\mathbb{N}}$ is not an isomorphism: its image consists of those sequences of rational numbers whose denominators can be bounded.'
 ),

database/data/004_property-assignments/Delta.sql

@@ -127,5 +127,5 @@ VALUES
     'Delta',
     'pushouts',
     FALSE,
-    'Assume that the two inclusions $\{0 < 1\} \leftarrow \{0\} \rightarrow \{0 < 2\}$ have a pushout in $\mathbf{FinOrd} \setminus \{\emptyset\}$. 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.'
+    'Assume that the two inclusions $\{0 < 1\} \leftarrow \{0\} \rightarrow \{0 < 2\}$ have a pushout in $\mathbf{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.'
 );

database/data/004_property-assignments/FinSet.sql

@@ -82,4 +82,12 @@ VALUES
 	'countable',
 	FALSE,
 	'This is trivial.'
+),
+(
+	'FinSet',
+	'natural numbers object',
+	FALSE,
+	'If $(N,z,s)$ is a natural numbers object, then
+	<p>$1 \xrightarrow{z} N \xleftarrow{s} N$</p>
+	is a coproduct cocone by <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, Part A, Lemma 2.5.5. But there is no finite set $N$ with $N \cong 1 + N$.'
 );

database/data/004_property-assignments/Man.sql

@@ -48,10 +48,11 @@ VALUES
 	'[Sketch] Since $\mathbf{Top}$ is infinitary extensive, a continuous map $f : M \to \coprod_i N_i$ corresponds to a decomposition $M = \coprod_i M_i$ (as topological spaces) with continuous maps $f_i : M_i \to N_i$. Endow the open subset $M_i \subseteq M$ with the smooth structure inherited from $M$. Now remark that $f$ is smooth iff each $f_i$ is smooth.'
 ),
 (
+	-- TODO: maybe add "countably extensive" to make this more conceptual
 	'Man',
-	'countable coproducts',
+	'countably distributive',
 	TRUE,
-	'Take the usual disjoint union, which is clearly locally Euclidean and Hausdorff, and it is second countable since we are using only countable many spaces. (Without that condition, all coproducts would exist.)'
+	'To construct countable coproducts, take the usual disjoint union of spaces, which is clearly locally Euclidean and Hausdorff, and it is second countable since we are using only countable many spaces. (Without that condition, all coproducts would exist.) Now we need to check that the canonical smooth map $\coprod_i X \times Y_i \to X \times \coprod_i Y_i$ is a diffeomorphism (for countable families). It is a homeomorphism since $\mathbf{Top}$ is infinitary distributive. The inverse $X \times \coprod_i Y_i \to \coprod_i X \times Y_i$ is smooth since the domain is covered by the open subsets $X \times Y_i$ on which the map is clearly smooth.'
 ),
 (
 	'Man',

database/data/004_property-assignments/Met.sql

@@ -136,4 +136,12 @@ VALUES
 	'Malcev',
 	FALSE,
 	'Consider the metric subspace $\{(a,b) \in \mathbb{R}^2 : a \leq b\}$ of $\mathbb{R}^2$.'
-);
+),
+(
+	'Met',
+	'natural numbers object',
+	FALSE,
+	'If $(N,z,s)$ is a natural numbers object in $\mathbf{Met}$, then
+	<p>$1 \xrightarrow{z} N \xleftarrow{s} N$</p>
+	is a coproduct cocone by <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, 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 <a href="https://math.stackexchange.com/questions/1778408" target="_blank">MSE/1778408</a>.'
+);

database/data/004_property-assignments/Setne.sql

@@ -102,6 +102,12 @@ VALUES
 	TRUE,
 	'Let $D$ be a diagram in $\mathbf{Set}_{\neq \varnothing}$, and let $L$ be a limit of $D$ in $\mathbf{Set}$. If $L$ is non-empty, it gives a limit in $\mathbf{Set}_{\neq \varnothing}$ as well. If $L$ is the empty set, there is no cone over $D$ in $\mathbf{Set}_{\neq \varnothing}$; hence the empty set of cones gives a multi-limit of $D$ in $\mathbf{Set}_{\neq \varnothing}$.'
 ),
+(
+	'Setne',
+	'natural numbers object',
+	TRUE,
+	'Any natural numbers object in $\mathbf{Set}$, such as $(\mathbb{N},0,n \mapsto n+1)$, is clearly also one in $\mathbf{Set}_{\neq \varnothing}$.'
+),
 (
 	'Setne',
 	'sequential limits',

database/data/004_property-assignments/Sp.sql

@@ -70,4 +70,12 @@ VALUES
 	'essentially countable',
 	FALSE,
 	'Any function $f\colon\mathbb{N} \to \mathbb{N}$ can be regarded as a combinatorial species with trivial actions, and distinct functions yield non-isomorphic species.'
-);
+),
+(
+	'Sp',
+	'natural numbers object',
+	FALSE,
+	'If $(N,z,s)$ is a natural numbers object, then
+	<p>$1 \xrightarrow{z} N \xleftarrow{s} N$</p>
+	is a coproduct cocone by <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, 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.'
+);

database/data/004_property-assignments/Z_div.sql

@@ -61,13 +61,13 @@ VALUES
 ),
 (
 	'Z_div',
-	'infinitary distributive',
+	'countably distributive',
 	FALSE,
 	'We have $2 \times \coprod_n 3^n = \gcd(2,\mathrm{lcm}_n(3^n)) = \gcd(2,0) = 2$, but $\coprod_n (2 \times 3^n) = \mathrm{lcm}_n \gcd(2,3^n) = \mathrm{lcm}_n 1  = 1$.'
 ),
 (
 	'Z_div',
-	'infinitary codistributive',
+	'countably codistributive',
 	FALSE,
 	'If $p$ runs through all odd primes, we have $2 \sqcup \prod_p p = \mathrm{lcm}(2,\mathrm{gcd}_p p) = \mathrm{lcm}(2,0) = 0$, but $\prod_p (2 \sqcup p) = \gcd_p (\mathrm{lcm}(2,p)) = \gcd_p (2 \cdot p) = 2$.'
 );

database/data/005_implications/002_limits-colimits-behavior-implications.sql

@@ -84,26 +84,40 @@ VALUES
 	FALSE
 ),
 (
-	'infinitary_distributive_consequence',
+	'infinitary_distributive_assumption',
 	'["infinitary distributive"]',
 	'["finite products", "coproducts"]',
 	'This holds by definition.',
 	FALSE
 ),
 (
-	'infinitary_distributive_condition',
-	'["infinitary distributive"]',
-	'["distributive"]',
-	'This is trivial.',
+	'countably_distributive_assumption',
+	'["countably distributive"]',
+	'["finite products", "countable coproducts"]',
+	'This holds by definition.',
 	FALSE
 ),
 (
-	'distributive_condition',
+	'distributive_assumption',
 	'["distributive"]',
 	'["finite products", "finite coproducts"]',
 	'This holds by definition.',
 	FALSE
 ),
+(
+	'infinitary_distributive_trivial',
+	'["infinitary distributive"]',
+	'["countably distributive"]',
+	'This is trivial.',
+	FALSE
+),
+(
+	'countably_distributive_trivial',
+	'["countably distributive"]',
+	'["distributive"]',
+	'This is trivial.',
+	FALSE
+),
 (
 	'distributive_duality',
 	'["thin", "distributive"]',
@@ -181,6 +195,13 @@ VALUES
 	'Each functor $A \times -$ is left adjoint and hence preserves finite coproducts (in fact, all colimits).',
 	FALSE
 ),
+(
+	'countably_distributive_criterion',
+	'["cartesian closed", "countable coproducts"]',
+	'["countably distributive"]',
+	'Each functor $A \times -$ is left adjoint and hence preserves countable coproducts (in fact, all colimits).',
+	FALSE
+),
 (
 	'infinitary_distributive_criterion',
 	'["cartesian closed", "coproducts"]',
@@ -195,6 +216,13 @@ VALUES
 	'Each functor $A \times -$ preserves finite coproducts and filtered colimits, hence all coproducts.',
 	FALSE
 ),
+(
+	'countably_distributive_filtered_criterion',
+	'["distributive", "cartesian filtered colimits", "countable coproducts"]',
+	'["countably distributive"]',
+	'Each functor $A \times -$ preserves finite coproducts and filtered colimits, hence all countable coproducts.',
+	FALSE
+),
 (
 	'extensive_consequences',
 	'["extensive"]',

database/data/005_implications/008_topos-theory-implications.sql

@@ -187,4 +187,39 @@ VALUES
 	'["co-Malcev"]',
 	'This is Example 2.2.18 in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>. An alternative proof is given later in A.5.17.',
 	FALSE
+),
+(
+	'nno_assumption',
+	'["natural numbers object"]',
+	'["finite products"]',
+	'This holds by definition.',
+	FALSE
+),
+(
+	'nno_criterion',
+	'["countably distributive"]',
+	'["natural numbers object"]',
+	'Consider the copower $N := \coprod_{n \in \mathbb{N}} 1$ with inclusions $i_n : 1 \to N$ for $n \in \mathbb{N}$. We define $z := 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 \mathbb{N}} 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 \mathbb{N}$. 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 $\mathbb{N}$ is a natural numbers object in $\mathbf{Set}$.) Concretely, $\phi_n = g^n \circ f$.',
+	FALSE
+),
+(
+	'nno_pointed_case',	
+	'["natural numbers object", "pointed"]',
+	'["trivial"]',
+	'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$.',
+	FALSE
+),
+(
+	'nno_terminal',
+	'["natural numbers object", "strict terminal object"]',
+	'["one-way"]',
+	'By assumption, $z : 1 \to N$ is an isomorphism. Therefore, the terminal object $1$ is a NNO with $z = \mathrm{id}_1$ and $s = \mathrm{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 = \mathrm{id}_X$ (take $f = \mathrm{id}_X$), which proves the claim. (From here one can <a href="/category-implication/one-way_products_thin">further deduce</a> that the category is thin.)',
+	FALSE
+),
+(
+	'nno_thin',
+	'["finite products", "thin"]',
+	'["natural numbers object"]',
+	'The triple $(1, \mathrm{id}_1, \mathrm{id}_1)$ is clearly a NNO.',
+	FALSE
 );

scripts/expected-data/Ab.json

@@ -141,5 +141,8 @@
 	"locally copresentable": false,
 	"coaccessible": false,
 	"countable": false,
-	"essentially countable": false
+	"essentially countable": false,
+	"natural numbers object": false,
+	"countably distributive": false,
+	"countably codistributive": false
 }

scripts/expected-data/Set.json

@@ -94,6 +94,8 @@
 	"multi-initial object": true,
 	"cartesian filtered colimits": true,
 	"cocartesian cofiltered limits": true,
+	"natural numbers object": true,
+	"countably distributive": true,
 
 	"Grothendieck abelian": false,
 	"Malcev": false,
@@ -141,5 +143,6 @@
 	"locally copresentable": false,
 	"coaccessible": false,
 	"countable": false,
-	"essentially countable": false
+	"essentially countable": false,
+	"countably codistributive": false
 }

scripts/expected-data/Top.json

@@ -69,6 +69,8 @@
 	"multi-terminal object": true,
 	"multi-initial object": true,
 	"cocartesian cofiltered limits": true,
+	"countably distributive": true,
+	"natural numbers object": true,
 
 	"abelian": false,
 	"additive": false,
@@ -141,5 +143,6 @@
 	"coaccessible": false,
 	"countable": false,
 	"essentially countable": false,
-	"cartesian filtered colimits": false
+	"cartesian filtered colimits": false,
+	"countably codistributive": false
 }