Add properties: cartesian filtered colimits + cocartesian cofiltered limits

.vscode/settings.json

@@ -124,6 +124,7 @@
 		"injection",
 		"injections",
 		"injective",
+		"injectivity",
 		"Isbell",
 		"Johnstone",
 		"Kashiwara",

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

@@ -82,6 +82,24 @@ VALUES
 	NULL,
 	TRUE
 ),
+(
+	'cartesian filtered colimits',
+	'has',
+	'In a category $\mathcal{C}$, which we assume to have filtered colimits and finite products, we say that <i>filtered colimits are cartesian</i> if for every finite set $I$ the product functor $\prod : \mathcal{C}^I \to \mathcal{C}$ preserves filtered colimits. Equivalently, for every $X \in \mathcal{C}$ the functor $X \times - : \mathcal{C} \to \mathcal{C}$ preserves filtered colimits.<br>
+	This is no standard terminology, it has been suggested in <a href="https://mathoverflow.net/questions/510240" target="_blank">MO/510240</a>. We have added it to the database since it clarifies the relationship between many related properties.',
+	NULL,
+	'cocartesian cofiltered limits',
+	TRUE
+),
+(
+	'cocartesian cofiltered limits',
+	'has',
+	'In a category $\mathcal{C}$, which we assume to have cofiltered limits and finite coproducts, we say that <i>cofiltered limits are cocartesian</i> if for every finite set $I$ the coproduct functor $\coprod : \mathcal{C}^I \to \mathcal{C}$ preserves cofiltered limits. Equivalently, for every $X \in \mathcal{C}$ the functor $X \sqcup - : \mathcal{C} \to \mathcal{C}$ preserves cofiltered limits.<br>
+	This is no standard terminology, its dual has been suggested in <a href="https://mathoverflow.net/questions/510240" target="_blank">MO/510240</a>. We have added it to the database since it clarifies the relationship between many related properties.',
+	NULL,
+	'cartesian filtered colimits',
+	TRUE
+),
 (
 	'disjoint finite coproducts',
 	'has',

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

@@ -151,6 +151,12 @@ VALUES
 ('codistributive', 'finite coproducts'),
 ('exact filtered colimits', 'filtered colimits'),
 ('exact filtered colimits', 'finitely complete'),
+('exact filtered colimits', 'cartesian filtered colimits'),
+('cartesian filtered colimits', 'filtered colimits'),
+('cartesian filtered colimits', 'finite products'),
+('cartesian filtered colimits', 'exact filtered colimits'),
+('cocartesian cofiltered limits', 'cofiltered limits'),
+('cocartesian cofiltered limits', 'finite coproducts'),
 ('generator', 'generating set'),
 ('generating set', 'generator'),
 ('Grothendieck abelian', 'abelian'),

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

@@ -82,4 +82,12 @@ VALUES
 	'regular quotient object classifier',
 	FALSE,
 	'We may copy the proof for the <a href="/category/CAlg(R)">category of commutative algebras</a> (since the proof there did not use that $P$ is commutative). Alternatively, any regular quotient object classifier in $\mathbf{Alg}(R)$ would produce one in $\mathbf{CAlg}(R)$ by <a href="/lemma/subobject_classifiers_coreflection">this lemma</a> (dualized).'
+),
+(
+	'Alg(R)',
+	'cocartesian cofiltered limits',
+	FALSE,
+	'Consider the ring $A = R[X]$ and the sequence of rings $B_n = R[Y]/(Y^{n+1})$ with projections $B_{n+1} \to B_n$, whose colimit is $R[[Y]]$. Every element in the coproduct of rings $R[X] \sqcup R[[Y]]$ has a finite "free product" length. Now consider the elements
+	<br>$w_n = (1 + XY) (1+XY^2) \cdots (1+X Y^n) \in A \sqcup B_n$.</br>
+	Because of $w_n \equiv w_{n-1} \bmod Y^n$ these form an element $w \in \lim_n (A \sqcup B_n)$. Expanding $w_n$, the longest term is $XY XY^2 \cdots X Y^n$ of "free product" length $2n$, which is unbounded.'
 );

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

@@ -82,4 +82,14 @@ VALUES
 	'regular quotient object classifier',
 	FALSE,
 	'Assume that $\mathbf{Grp}$ has a (regular) quotient object classifier, i.e. a group $P$ such that every surjective homomorphism $G \to H$ is the cokernel of a unique homomorphism $\varphi : P \to G$. Equivalently, every normal subgroup $N \subseteq G$ is $\langle \langle \varphi(P) \rangle \rangle$ for a unique homomorphism $\varphi : P \to G$, where $\langle \langle - \rangle \rangle$ denotes the normal closure. If $c_g : G \to G$ denotes the conjugation with $g \in G$, then the images of $\varphi$ and $c_g \circ \varphi$ have the same normal closures, so the homomorphisms must be equal. In other words, $\varphi$ factors through the center $Z(G)$. But then every normal subgroup of $G$, in particular $G$ itself, would be contained in $Z(G)$, which is wrong for every non-abelian group $G$.'
+),
+(
+	'Grp',
+	'cocartesian cofiltered limits',
+	FALSE,
+	'For cofiltered diagrams of groups $(H_i)$ and a group $G$ the canonical homomorphism
+	<br>$\alpha : G \sqcup \lim_i H_i \to \lim_i (G \sqcup H_i)$<br>
+	is injective, but often fails to be surjective because the components of an element in the image have bounded <i>free product length</i> (the number of factors appearing in the reduced form). Specifically, consider the free groups $G = \langle y \rangle$ and $H_n = \langle x_1,\dotsc,x_n \rangle$ for $n \in \mathbb{N}$ with the truncation maps $H_{n+1} \to H_n$, $x_{n+1} \mapsto 1$. Define
+	<br>$p_n := x_1 \, y \, x_2 \, y \, \cdots \, x_{n-1} \, y \, x_n \, y^{-(n-1)} \in G \sqcup H_n$.<br>
+	If we substitute $x_{n+1}=1$ in $p_{n+1}$, we get $p_n$. Thus, we have $p = (p_n) \in \lim_n (G \sqcup H_n)$. This element does not lie in the image of $\alpha$ since the free product length of $p_n$ (which is well-defined) is $2n$, which is unbounded.'
 );

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

@@ -67,7 +67,7 @@ VALUES
 ),
 (
 	'Haus',
-	'cartesian closed',
+	'cartesian filtered colimits',
 	FALSE,
 	'It is shown in <a href="https://math.stackexchange.com/questions/1255678">MSE/1255678</a> that $\mathbb{Q} \times - : \mathbf{Top} \to \mathbf{Top}$ does not preserve sequential colimits (so that it cannot be a left adjoint). The same example also works in $\mathbf{Haus}$: Surely $\mathbb{Q}$ is Hausdorff, $X_n$ is Hausdorff, as is their colimit $X$, and the colimit (taken in $\mathbf{Top}$) of the $X_n \times \mathbb{Q}$ admits a bijective continuous map to a Hausdorff space, therefore is also Hausdorff, meaning it is also the colimit taken in $\mathbf{Haus}$.'
 ),

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

@@ -67,13 +67,7 @@ VALUES
 ),
 (
 	'Meas',
-	'cartesian closed',
-	FALSE,
-	'The functors $X \times -$ do not preserve filtered colimits by <a href="https://math.stackexchange.com/questions/5027218" target="_blank">MSE/5027218</a>, hence cannot be left adjoints.'
-),
-(
-	'Meas',
-	'exact filtered colimits',
+	'cartesian filtered colimits',
 	FALSE,
 	'See <a href="https://math.stackexchange.com/questions/5027218" target="_blank">MSE/5027218</a>.'
 ),

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

@@ -47,6 +47,12 @@ VALUES
 	TRUE,
 	'Given a directed diagram $(X_i)$ of metric spaces, take the directed colimit $X$ of the underlying sets with the following metric: If $x,y \in X$, let $d(x,y)$ be infimum of all $d(x_i,y_i)$, where $x_i,y_i \in X_i$ are some preimages of $x,y$ in some $X_i$. This is only a pseudo-metric, so finally take the associated metric space (Kolmogorov quotient). The definition ensures that each $X_i \to X$ is non-expansive, and the universal property is easy to check.' 
 ),
+(
+	'Met',
+	'cartesian filtered colimits',
+	TRUE,
+	'The canonical map $\mathrm{colim}_i  (X \times Y_i) \to X \times \mathrm{colim}_i Y_i$ is an isomorphism for directed diagrams $(Y_i)$: It is surjective by the concrete description of directed colimits. It is isometric because of the elementary observation $\inf_i \max(r, s_i) = \max(r, \inf_i s_i)$ for $r, s_i \in \mathbb{R}$, where $i \leq j \implies s_i \geq s_j$.'
+),
 (
 	'Met',
 	'strict initial object',
@@ -117,7 +123,7 @@ VALUES
 	'Met',
 	'exact filtered colimits',
 	FALSE,
-	'Remark 2.7 in <a href="https://arxiv.org/abs/2006.01399" target="_blank">this paper</a>'
+	'See Remark 2.7 in <a href="https://arxiv.org/abs/2006.01399" target="_blank">Approximate injectivity and smallness in metric-enriched categories</a> by Adamek-Rosicky.'
 ),
 (
 	'Met',

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

@@ -23,6 +23,12 @@ VALUES
 	TRUE,
 	'Example 4.5 in <a href="https://arxiv.org/abs/1504.02660" target="_blank">this preprint</a>'
 ),
+(
+	'Met_oo',
+	'cartesian filtered colimits',
+	TRUE,
+	'We can use the same proof as for the <a href="/category/Met">category of metric spaces</a> since the equation $\inf_i \max(r, s_i) = \max(r, \inf_i s_i)$ also holds for for $r, s_i \in \mathbb{R} \cup \{\infty\}$.'
+),
 (
 	'Met_oo',
 	'infinitary extensive',
@@ -57,7 +63,7 @@ VALUES
 	'Met_oo',
 	'exact filtered colimits',
 	FALSE,
-	'2.7 in <a href="https://arxiv.org/abs/2006.01399" target="_blank">this paper</a>'
+	'See Remark 2.7 in <a href="https://arxiv.org/abs/2006.01399" target="_blank">Approximate injectivity and smallness in metric-enriched categories</a> by Adamek-Rosicky.'
 ),
 (
 	'Met_oo',

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

@@ -76,5 +76,11 @@ VALUES
 	'regular quotient object classifier',
 	FALSE,
 	'We can just copy the proof for the <a href="/category/CMon">category of commutative monoids</a>. Alternatively, we may use <a href="/lemma/subobject_classifiers_coreflection">this lemma</a> (dualized).'
+),
+(
+	'Mon',
+	'cocartesian cofiltered limits',
+	FALSE,
+	'We know that the <a href="/category/Grp">category of groups</a> fails to satisfy this property. The same counterexample works here since the inclusion $\mathbf{Grp} \hookrightarrow \mathbf{Mon}$ preserves limits and colimits (it has a left and a right adjoint) and is conservative. A similar counterexample is given by the free monoids $N_n = \langle x_1,\dotsc,x_n \rangle$ and the Boolean monoid $M = \langle e : e^2=e \rangle$ with the maps $N_{n+1} \to N_n$, $x_{n+1} \mapsto 1$. Then the element $(x_1 e \cdots x_n e) \in \lim_n (M \sqcup N_n)$ does not come from $M \sqcup \lim_n N_n$ because its components have unbounded free product length.'
 );
 

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

@@ -82,4 +82,12 @@ VALUES
 	'regular quotient object classifier',
 	FALSE,
 	'We may copy the proof for the <a href="/category/CRing">category of commutative rings</a> (since the proof there did not use that $P$ is commutative). Alternatively, any regular quotient object classifier in $\mathbf{Ring}$ would produce one in $\mathbf{CRing}$ by <a href="/lemma/subobject_classifiers_coreflection">this lemma</a> (dualized).'
+),
+(
+	'Ring',
+	'cocartesian cofiltered limits',
+	FALSE,
+	'Consider the ring $A = \mathbb{Z}[X]$ and the sequence of rings $B_n = \mathbb{Z}[Y]/(Y^{n+1})$ with projections $B_{n+1} \to B_n$, whose colimit is $\mathbb{Z}[[Y]]$. Every element in the coproduct of rings $\mathbb{Z}[X] \sqcup \mathbb{Z}[[Y]]$ has a finite "free product" length. Now consider the elements
+	<br>$w_n = (1 + XY) (1+XY^2) \cdots (1+X Y^n) \in A \sqcup B_n$.</br>
+	Because of $w_n \equiv w_{n-1} \bmod Y^n$ these form an element $w \in \lim_n (A \sqcup B_n)$. Expanding $w_n$, the longest term is $XY XY^2 \cdots X Y^n$ of "free product" length $2n$, which is unbounded.'
 );

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

@@ -73,9 +73,9 @@ VALUES
 ),
 (
 	'Top',
-	'cartesian closed',
+	'cartesian filtered colimits',
 	FALSE,
-	'The functor $\mathbb{Q} \times - : \mathbf{Top} \to \mathbf{Top}$ does not preserve colimits, hence has no right adjoint. See <a href="https://math.stackexchange.com/questions/2969372" target="_blank">MSE/2969372</a> for a proof.'
+	'The functor $\mathbb{Q} \times - : \mathbf{Top} \to \mathbf{Top}$ does not preserve colimits, see <a href="https://math.stackexchange.com/questions/2969372" target="_blank">MSE/2969372</a>.'
 ),
 (
 	'Top',
@@ -95,12 +95,6 @@ VALUES
 	FALSE,
 	'If $X$ is a set, consider the discrete space $X_d$ on $X$ and the indiscrete space $X_i$ on $X$. The identity map $X \to X$ lifts to a continuous map $X_d \to X_i$, which is bijective and therefore both a mono- and an epimorphism, but it is not an isomorphism unless $X$ has at most one element.'
 ),
-(
-	'Top',
-	'exact filtered colimits',
-	FALSE,
-	'See <a href="https://math.stackexchange.com/questions/1255678" target="_blank">MSE/1255678</a>.'
-),
 (
 	'Top',
 	'skeletal',

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

@@ -103,9 +103,9 @@ VALUES
 ),
 (
 	'Top*',
-	'exact filtered colimits',
+	'cartesian filtered colimits',
 	FALSE,
-	'See <a href="https://math.stackexchange.com/questions/1255678" target="_blank">MSE/1255678</a> (the counterexample also works for pointed spaces).'
+	'The functor $\mathbb{Q} \times - : \mathbf{Top}_* \to \mathbf{Top}_*$ does not preserve colimits, see <a href="https://math.stackexchange.com/questions/2969372" target="_blank">MSE/2969372</a>. The counterexample also works for pointed spaces.'
 ),
 (
 	'Top*',

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

@@ -20,6 +20,13 @@ VALUES
 	'For all objects $X,Y$ the morphism $X \sqcup Y \to X \times Y$ is an isomorphism, hence a strong epimorphism.',
 	FALSE
 ),
+(
+	'biproducts_cartesian_filtered_colimits',
+	'["biproducts", "filtered colimits"]',
+	'["cartesian filtered colimits"]',
+	'If $I$ is a finite set, the product functor $\mathcal{C}^I \to \mathcal{C}$ is isomorphic to the coproduct functor $\mathcal{C}^I \to \mathcal{C}$, hence preserves <i>all</i> colimits that exist in $\mathcal{C}$.',
+	FALSE
+),
 (
 	'pointed_characterization',
 	'["pointed"]',
@@ -62,6 +69,20 @@ VALUES
 	'This holds by definition.',
 	FALSE
 ),
+(
+	'cartesian_filtered_colimits_condition',
+	'["cartesian filtered colimits"]',
+	'["filtered colimits", "finite products"]',
+	'This holds by definition.',
+	FALSE
+),
+(
+	'exact_includes_cartesian_filtered_colimits',
+	'["exact filtered colimits"]',
+	'["cartesian filtered colimits"]',
+	'If filtered colimits commute with finite limits, they commute with finite products in particular.',
+	FALSE
+),
 (
 	'infinitary_distributive_consequence',
 	'["infinitary distributive"]',
@@ -139,6 +160,13 @@ VALUES
 	'This is obvious.',
 	FALSE
 ),
+(
+	'extensive_cocartesian_cofiltered_limits',
+	'["extensive", "cofiltered limits", "terminal object"]',
+	'["cocartesian cofiltered limits"]',
+	'Let $\mathcal{C}$ be an extensive category with cofiltered limits and a terminal object. Then the coproduct functor $\mathcal{C} \times \mathcal{C} \cong \mathcal{C}/1 \times \mathcal{C}/1 \to \mathcal{C}/(1+1)$ is an equivalence. The forgetful functor $\mathcal{C}/A \to \mathcal{C}$ creates connected limits, and hence preserves cofiltered limits. For every $X \in \mathcal{C}$ the functor $(X,-) : \mathcal{C} \to \mathcal{C} \times \mathcal{C}$ also preserves cofiltered limits. The composition of these functors is $X \sqcup - : \mathcal{C} \to \mathcal{C}$ and therefore also preserves cofiltered limits.',
+	FALSE
+),
 (
 	'distributive_consequence',
 	'["distributive"]',
@@ -162,7 +190,7 @@ VALUES
 ),
 (
 	'infinite_distributive_filtered_criterion',
-	'["distributive", "exact filtered colimits", "coproducts"]',
+	'["distributive", "cartesian filtered colimits", "coproducts"]',
 	'["infinitary distributive"]',
 	'Each functor $A \times -$ preserves finite coproducts and filtered colimits, hence all coproducts.',
 	FALSE

database/data/005_implications/006_trivial-categories-implications.sql

@@ -117,4 +117,11 @@ VALUES
 	'["binary powers"]',
 	'This is because $X \times X = X$.',
 	FALSE
+),
+(
+	'thin_exact_filtered_colimits',
+	'["thin", "cartesian filtered colimits"]',
+	'["exact filtered colimits"]',
+	'In a thin category, every (finite) limit can be reduced to a (finite) product.',
+	FALSE
 );

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

@@ -27,6 +27,13 @@ VALUES
 	'See the <a href="https://ncatlab.org/nlab/show/strict+initial+object" target="_blank">nLab</a>.',
 	FALSE
 ),
+(
+	'ccc_cartesian_filtered_colimits',
+	'["cartesian closed", "filtered colimits"]',
+	'["cartesian filtered colimits"]',
+	'Each functor $X \times -$ is a left adjoint and therefore preserves (filtered) colimits.',
+	FALSE
+),
 (
 	'ccc_no_strict_terminal',
 	'["cartesian closed", "strict terminal object"]',

scripts/expected-data/Ab.json

@@ -23,6 +23,7 @@
 	"epi-regular": true,
 	"equalizers": true,
 	"exact filtered colimits": true,
+	"cartesian filtered colimits": true,
 	"filtered colimits": true,
 	"cofiltered limits": true,
 	"directed limits": true,

scripts/expected-data/Set.json

@@ -25,6 +25,7 @@
 	"epi-regular": true,
 	"equalizers": true,
 	"exact filtered colimits": true,
+	"cartesian filtered colimits": true,
 	"filtered colimits": true,
 	"cofiltered limits": true,
 	"directed limits": true,

scripts/expected-data/Top.json

@@ -78,6 +78,7 @@
 	"essentially finite": false,
 	"essentially small": false,
 	"exact filtered colimits": false,
+	"cartesian filtered colimits": false,
 	"finitary algebraic": false,
 	"finite": false,
 	"Grothendieck abelian": false,