$(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. +$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/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/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.' +); 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 778e6960..8c2450f5 100644 --- a/database/data/005_implications/008_topos-theory-implications.sql +++ b/database/data/005_implications/008_topos-theory-implications.sql @@ -187,4 +187,39 @@ 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', + '["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 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 diff --git a/scripts/expected-data/Ab.json b/scripts/expected-data/Ab.json index 65d6a56a..97ebd8eb 100644 --- a/scripts/expected-data/Ab.json +++ b/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 } diff --git a/scripts/expected-data/Set.json b/scripts/expected-data/Set.json index 5d5e6f4c..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, @@ -141,5 +143,6 @@ "locally copresentable": false, "coaccessible": false, "countable": false, - "essentially countable": false + "essentially countable": false, + "countably codistributive": false } diff --git a/scripts/expected-data/Top.json b/scripts/expected-data/Top.json index 6229543a..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, @@ -141,5 +143,6 @@ "coaccessible": false, "countable": false, "essentially countable": false, - "cartesian filtered colimits": false + "cartesian filtered colimits": false, + "countably codistributive": false }