add new properties: countably distributive, countably codistributive

Author: ScriptRaccoon

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/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'),

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/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/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

@@ -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
 ),
 (

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
 }

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
 }