From 0b71907431f75a23a6713fbdc510b49785edbbc6 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 17 Apr 2026 17:53:02 +0200 Subject: [PATCH 1/6] add nno definition and some implications --- .../data/003_properties/009_topos-theory.sql | 11 ++++++++++ .../003_properties/100_related-properties.sql | 3 +++ .../008_topos-theory-implications.sql | 21 +++++++++++++++++++ scripts/expected-data/Ab.json | 3 ++- scripts/expected-data/Set.json | 3 ++- scripts/expected-data/Top.json | 3 ++- 6 files changed, 41 insertions(+), 3 deletions(-) diff --git a/database/data/003_properties/009_topos-theory.sql b/database/data/003_properties/009_topos-theory.sql index 3b202080..9fa4ca54 100644 --- a/database/data/003_properties/009_topos-theory.sql +++ b/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 natural numbers object (NNO) 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).', + 'https://ncatlab.org/nlab/show/natural+numbers+object', + NULL, + TRUE ); \ No newline at end of file diff --git a/database/data/003_properties/100_related-properties.sql b/database/data/003_properties/100_related-properties.sql index cb9923e1..dc412c2d 100644 --- a/database/data/003_properties/100_related-properties.sql +++ b/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'), diff --git a/database/data/005_implications/008_topos-theory-implications.sql b/database/data/005_implications/008_topos-theory-implications.sql index 778e6960..09f512c8 100644 --- a/database/data/005_implications/008_topos-theory-implications.sql +++ b/database/data/005_implications/008_topos-theory-implications.sql @@ -187,4 +187,25 @@ VALUES '["co-Malcev"]', 'This is Example 2.2.18 in Malcev, protomodular, homological and semi-abelian categories. 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', + '["infinitary 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 infinitary 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_additive_case', + '["natural numbers object", "additive"]', + '["trivial"]', + 'Let $(N,z,s)$ be a natural numbers object in an additive category. The morphism $z : 0 \to N$ must be the zero morphism. 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$ for all $f$.', + FALSE ); \ No newline at end of file diff --git a/scripts/expected-data/Ab.json b/scripts/expected-data/Ab.json index 65d6a56a..d8fa9ead 100644 --- a/scripts/expected-data/Ab.json +++ b/scripts/expected-data/Ab.json @@ -141,5 +141,6 @@ "locally copresentable": false, "coaccessible": false, "countable": false, - "essentially countable": false + "essentially countable": false, + "natural numbers object": false } diff --git a/scripts/expected-data/Set.json b/scripts/expected-data/Set.json index 5d5e6f4c..a2e112b9 100644 --- a/scripts/expected-data/Set.json +++ b/scripts/expected-data/Set.json @@ -141,5 +141,6 @@ "locally copresentable": false, "coaccessible": false, "countable": false, - "essentially countable": false + "essentially countable": false, + "natural numbers object": true } diff --git a/scripts/expected-data/Top.json b/scripts/expected-data/Top.json index 6229543a..bd75793a 100644 --- a/scripts/expected-data/Top.json +++ b/scripts/expected-data/Top.json @@ -141,5 +141,6 @@ "coaccessible": false, "countable": false, "essentially countable": false, - "cartesian filtered colimits": false + "cartesian filtered colimits": false, + "natural numbers object": true } From 69afccda73de4bcceeb0576889d4eaf62b85c629 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 17 Apr 2026 18:06:06 +0200 Subject: [PATCH 2/6] generalize result to pointed categories --- .../data/005_implications/008_topos-theory-implications.sql | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/database/data/005_implications/008_topos-theory-implications.sql b/database/data/005_implications/008_topos-theory-implications.sql index 09f512c8..0b8e8e5c 100644 --- a/database/data/005_implications/008_topos-theory-implications.sql +++ b/database/data/005_implications/008_topos-theory-implications.sql @@ -203,9 +203,9 @@ VALUES FALSE ), ( - 'nno_additive_case', - '["natural numbers object", "additive"]', + 'nno_pointed_case', + '["natural numbers object", "pointed"]', '["trivial"]', - 'Let $(N,z,s)$ be a natural numbers object in an additive category. The morphism $z : 0 \to N$ must be the zero morphism. 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$ for all $f$.', + '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 ); \ No newline at end of file From 862a223053be21a57a1131c0f24f3b8ad3254afc Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 17 Apr 2026 22:37:22 +0200 Subject: [PATCH 3/6] nno for strict terminal objects --- .../005_implications/008_topos-theory-implications.sql | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/database/data/005_implications/008_topos-theory-implications.sql b/database/data/005_implications/008_topos-theory-implications.sql index 0b8e8e5c..7a9cf3b3 100644 --- a/database/data/005_implications/008_topos-theory-implications.sql +++ b/database/data/005_implications/008_topos-theory-implications.sql @@ -208,4 +208,11 @@ VALUES '["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 further deduce that the category is thin.)', + FALSE ); \ No newline at end of file From 4b9d07b9b7b1918cf2a9b4ddedba7f60482fae76 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 17 Apr 2026 23:20:35 +0200 Subject: [PATCH 4/6] add new properties: countably distributive, countably codistributive --- .../003_limits-colimits-behavior.sql | 16 ++++++++ .../003_properties/100_related-properties.sql | 24 ++++++++--- .../data/004_property-assignments/CAlg(R).sql | 2 +- .../data/004_property-assignments/CRing.sql | 2 +- .../data/004_property-assignments/Man.sql | 5 ++- .../data/004_property-assignments/Z_div.sql | 4 +- ..._limits-colimits-behavior-implications.sql | 40 ++++++++++++++++--- .../008_topos-theory-implications.sql | 4 +- scripts/expected-data/Ab.json | 4 +- scripts/expected-data/Set.json | 4 +- scripts/expected-data/Top.json | 4 +- 11 files changed, 86 insertions(+), 23 deletions(-) diff --git a/database/data/003_properties/003_limits-colimits-behavior.sql b/database/data/003_properties/003_limits-colimits-behavior.sql index 59d6b5b5..208234c7 100644 --- a/database/data/003_properties/003_limits-colimits-behavior.sql +++ b/database/data/003_properties/003_limits-colimits-behavior.sql @@ -58,6 +58,22 @@ VALUES 'infinitary codistributive', TRUE ), +( + 'countably distributive', + 'is', + 'A category is countably distributive 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 countably codistributive 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', diff --git a/database/data/003_properties/100_related-properties.sql b/database/data/003_properties/100_related-properties.sql index dc412c2d..dfd1b997 100644 --- a/database/data/003_properties/100_related-properties.sql +++ b/database/data/003_properties/100_related-properties.sql @@ -158,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'), diff --git a/database/data/004_property-assignments/CAlg(R).sql b/database/data/004_property-assignments/CAlg(R).sql index 8c334e39..2b723450 100644 --- a/database/data/004_property-assignments/CAlg(R).sql +++ b/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}}$.' ), diff --git a/database/data/004_property-assignments/CRing.sql b/database/data/004_property-assignments/CRing.sql index 606a5ad9..8511ccee 100644 --- a/database/data/004_property-assignments/CRing.sql +++ b/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.' ), diff --git a/database/data/004_property-assignments/Man.sql b/database/data/004_property-assignments/Man.sql index 304c9f6c..f907f627 100644 --- a/database/data/004_property-assignments/Man.sql +++ b/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', diff --git a/database/data/004_property-assignments/Z_div.sql b/database/data/004_property-assignments/Z_div.sql index 4f38b97f..29548b56 100644 --- a/database/data/004_property-assignments/Z_div.sql +++ b/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$.' ); diff --git a/database/data/005_implications/002_limits-colimits-behavior-implications.sql b/database/data/005_implications/002_limits-colimits-behavior-implications.sql index ac23032e..26cc5805 100644 --- a/database/data/005_implications/002_limits-colimits-behavior-implications.sql +++ b/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"]', diff --git a/database/data/005_implications/008_topos-theory-implications.sql b/database/data/005_implications/008_topos-theory-implications.sql index 7a9cf3b3..796802ff 100644 --- a/database/data/005_implications/008_topos-theory-implications.sql +++ b/database/data/005_implications/008_topos-theory-implications.sql @@ -197,9 +197,9 @@ VALUES ), ( 'nno_criterion', - '["infinitary distributive"]', + '["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 infinitary 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$.', + '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 ), ( diff --git a/scripts/expected-data/Ab.json b/scripts/expected-data/Ab.json index d8fa9ead..97ebd8eb 100644 --- a/scripts/expected-data/Ab.json +++ b/scripts/expected-data/Ab.json @@ -142,5 +142,7 @@ "coaccessible": false, "countable": false, "essentially countable": false, - "natural numbers object": false + "natural numbers object": false, + "countably distributive": false, + "countably codistributive": false } diff --git a/scripts/expected-data/Set.json b/scripts/expected-data/Set.json index a2e112b9..00206fe0 100644 --- a/scripts/expected-data/Set.json +++ b/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, @@ -142,5 +144,5 @@ "coaccessible": false, "countable": false, "essentially countable": false, - "natural numbers object": true + "countably codistributive": false } diff --git a/scripts/expected-data/Top.json b/scripts/expected-data/Top.json index bd75793a..0e6ea903 100644 --- a/scripts/expected-data/Top.json +++ b/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, @@ -142,5 +144,5 @@ "countable": false, "essentially countable": false, "cartesian filtered colimits": false, - "natural numbers object": true + "countably codistributive": false } From 253f3932540ec13bc5cd3f30805e519227afa478 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 17 Apr 2026 23:37:33 +0200 Subject: [PATCH 5/6] thin categories have NNO --- .../005_implications/008_topos-theory-implications.sql | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/database/data/005_implications/008_topos-theory-implications.sql b/database/data/005_implications/008_topos-theory-implications.sql index 796802ff..8c2450f5 100644 --- a/database/data/005_implications/008_topos-theory-implications.sql +++ b/database/data/005_implications/008_topos-theory-implications.sql @@ -215,4 +215,11 @@ VALUES '["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 further deduce 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 ); \ No newline at end of file From 4ebfd58ce613fb15293da677ab619f3005c3233b Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 18 Apr 2026 00:19:52 +0200 Subject: [PATCH 6/6] decide NNO for various categories --- database/data/004_property-assignments/Delta.sql | 2 +- database/data/004_property-assignments/FinSet.sql | 8 ++++++++ database/data/004_property-assignments/Met.sql | 10 +++++++++- database/data/004_property-assignments/Setne.sql | 6 ++++++ database/data/004_property-assignments/Sp.sql | 10 +++++++++- 5 files changed, 33 insertions(+), 3 deletions(-) diff --git a/database/data/004_property-assignments/Delta.sql b/database/data/004_property-assignments/Delta.sql index ec5cb288..c279d115 100644 --- a/database/data/004_property-assignments/Delta.sql +++ b/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.' ); \ No newline at end of file diff --git a/database/data/004_property-assignments/FinSet.sql b/database/data/004_property-assignments/FinSet.sql index c389e46b..3b91f482 100644 --- a/database/data/004_property-assignments/FinSet.sql +++ b/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 +

$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/004_property-assignments/Met.sql b/database/data/004_property-assignments/Met.sql index dbe4fc64..9536df23 100644 --- a/database/data/004_property-assignments/Met.sql +++ b/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 +

$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.' +); \ No newline at end of file diff --git a/database/data/004_property-assignments/Setne.sql b/database/data/004_property-assignments/Setne.sql index fc969618..0f34870f 100644 --- a/database/data/004_property-assignments/Setne.sql +++ b/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', diff --git a/database/data/004_property-assignments/Sp.sql b/database/data/004_property-assignments/Sp.sql index b75420d1..aa297aae 100644 --- a/database/data/004_property-assignments/Sp.sql +++ b/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.' -); \ No newline at end of file +), +( + 'Sp', + 'natural numbers object', + FALSE, + 'If $(N,z,s)$ is a natural numbers object, then +

$1 \xrightarrow{z} N \xleftarrow{s} N$

+ is a coproduct cocone by Johnstone, Part A, Lemma 2.5.5. But there is no combinatorial species $N$ with $N \cong 1 + N$, since evaluating this at, say, $\varnothing$, would yield a finite set $N$ with this property.' +);