From 778fddb7fd013bb4e6bbec3499b188a1fb8c36e8 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 15 Apr 2026 10:12:47 +0200 Subject: [PATCH 1/9] add property: cartesian filtered colimits --- .../003_limits-colimits-behavior.sql | 9 +++++++++ .../003_properties/100_related-properties.sql | 4 ++++ ...002_limits-colimits-behavior-implications.sql | 16 +++++++++++++++- .../006_trivial-categories-implications.sql | 7 +++++++ .../008_topos-theory-implications.sql | 7 +++++++ 5 files changed, 42 insertions(+), 1 deletion(-) diff --git a/database/data/003_properties/003_limits-colimits-behavior.sql b/database/data/003_properties/003_limits-colimits-behavior.sql index 1780db7d..270e5fd7 100644 --- a/database/data/003_properties/003_limits-colimits-behavior.sql +++ b/database/data/003_properties/003_limits-colimits-behavior.sql @@ -82,6 +82,15 @@ 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 filtered colimits are cartesian 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.
+ This is no standard terminology, it has been suggested in MO/510240. We have added it to the database since it clarifies the relationship between many related properties.', + NULL, + NULL, + TRUE +), ( 'disjoint finite coproducts', 'has', diff --git a/database/data/003_properties/100_related-properties.sql b/database/data/003_properties/100_related-properties.sql index 724d263d..31ed1fa1 100644 --- a/database/data/003_properties/100_related-properties.sql +++ b/database/data/003_properties/100_related-properties.sql @@ -151,6 +151,10 @@ 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'), ('generator', 'generating set'), ('generating set', 'generator'), ('Grothendieck abelian', 'abelian'), 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 7e6a2414..b795f69d 100644 --- a/database/data/005_implications/002_limits-colimits-behavior-implications.sql +++ b/database/data/005_implications/002_limits-colimits-behavior-implications.sql @@ -62,6 +62,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"]', @@ -162,7 +176,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 diff --git a/database/data/005_implications/006_trivial-categories-implications.sql b/database/data/005_implications/006_trivial-categories-implications.sql index fe81e4d6..fea25223 100644 --- a/database/data/005_implications/006_trivial-categories-implications.sql +++ b/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 ); \ No newline at end of file diff --git a/database/data/005_implications/008_topos-theory-implications.sql b/database/data/005_implications/008_topos-theory-implications.sql index 418e8223..7ef2880c 100644 --- a/database/data/005_implications/008_topos-theory-implications.sql +++ b/database/data/005_implications/008_topos-theory-implications.sql @@ -27,6 +27,13 @@ VALUES 'See the nLab.', 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"]', From ac0d68750157bb5ffd7f6ef6d1ba7ccfc6dde5ed Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 15 Apr 2026 10:33:21 +0200 Subject: [PATCH 2/9] decide cartesian filtered colimits for Haus, Meas, Top, Top* --- database/data/004_property-assignments/Haus.sql | 2 +- database/data/004_property-assignments/Meas.sql | 8 +------- database/data/004_property-assignments/Top.sql | 10 ++-------- database/data/004_property-assignments/Top_pointed.sql | 4 ++-- scripts/expected-data/Ab.json | 1 + scripts/expected-data/Set.json | 1 + scripts/expected-data/Top.json | 1 + 7 files changed, 9 insertions(+), 18 deletions(-) diff --git a/database/data/004_property-assignments/Haus.sql b/database/data/004_property-assignments/Haus.sql index 4197977a..6005cdf3 100644 --- a/database/data/004_property-assignments/Haus.sql +++ b/database/data/004_property-assignments/Haus.sql @@ -67,7 +67,7 @@ VALUES ), ( 'Haus', - 'cartesian closed', + 'cartesian filtered colimits', FALSE, 'It is shown in MSE/1255678 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}$.' ), diff --git a/database/data/004_property-assignments/Meas.sql b/database/data/004_property-assignments/Meas.sql index e6e3ea7f..a1ef314e 100644 --- a/database/data/004_property-assignments/Meas.sql +++ b/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 MSE/5027218, hence cannot be left adjoints.' -), -( - 'Meas', - 'exact filtered colimits', + 'cartesian filtered colimits', FALSE, 'See MSE/5027218.' ), diff --git a/database/data/004_property-assignments/Top.sql b/database/data/004_property-assignments/Top.sql index 7814a7c4..a9e940b9 100644 --- a/database/data/004_property-assignments/Top.sql +++ b/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 MSE/2969372 for a proof.' + 'The functor $\mathbb{Q} \times - : \mathbf{Top} \to \mathbf{Top}$ does not preserve colimits, see MSE/2969372.' ), ( '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 MSE/1255678.' -), ( 'Top', 'skeletal', diff --git a/database/data/004_property-assignments/Top_pointed.sql b/database/data/004_property-assignments/Top_pointed.sql index 9709b606..ad2eb384 100644 --- a/database/data/004_property-assignments/Top_pointed.sql +++ b/database/data/004_property-assignments/Top_pointed.sql @@ -103,9 +103,9 @@ VALUES ), ( 'Top*', - 'exact filtered colimits', + 'cartesian filtered colimits', FALSE, - 'See MSE/1255678 (the counterexample also works for pointed spaces).' + 'The functor $\mathbb{Q} \times - : \mathbf{Top}_* \to \mathbf{Top}_*$ does not preserve colimits, see MSE/2969372. The counterexample also works for pointed spaces.' ), ( 'Top*', diff --git a/scripts/expected-data/Ab.json b/scripts/expected-data/Ab.json index b387f2e5..0784afdc 100644 --- a/scripts/expected-data/Ab.json +++ b/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, diff --git a/scripts/expected-data/Set.json b/scripts/expected-data/Set.json index e714c158..dbc2e2e4 100644 --- a/scripts/expected-data/Set.json +++ b/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, diff --git a/scripts/expected-data/Top.json b/scripts/expected-data/Top.json index 0458704a..81992bcc 100644 --- a/scripts/expected-data/Top.json +++ b/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, From a2e23b113f7b8109a50d154b4f94d691c576f309 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 15 Apr 2026 10:33:30 +0200 Subject: [PATCH 3/9] reword paper reference --- .vscode/settings.json | 1 + database/data/004_property-assignments/Met.sql | 2 +- database/data/004_property-assignments/Met_oo.sql | 2 +- 3 files changed, 3 insertions(+), 2 deletions(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index aa6cb7a7..8bf28de5 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -124,6 +124,7 @@ "injection", "injections", "injective", + "injectivity", "Isbell", "Johnstone", "Kashiwara", diff --git a/database/data/004_property-assignments/Met.sql b/database/data/004_property-assignments/Met.sql index 16d5d589..38cc3ec4 100644 --- a/database/data/004_property-assignments/Met.sql +++ b/database/data/004_property-assignments/Met.sql @@ -117,7 +117,7 @@ VALUES 'Met', 'exact filtered colimits', FALSE, - 'Remark 2.7 in this paper' + 'See Remark 2.7 in Approximate injectivity and smallness in metric-enriched categories by Adamek-Rosicky.' ), ( 'Met', diff --git a/database/data/004_property-assignments/Met_oo.sql b/database/data/004_property-assignments/Met_oo.sql index b538eb78..1ec4889c 100644 --- a/database/data/004_property-assignments/Met_oo.sql +++ b/database/data/004_property-assignments/Met_oo.sql @@ -57,7 +57,7 @@ VALUES 'Met_oo', 'exact filtered colimits', FALSE, - '2.7 in this paper' + 'See Remark 2.7 in Approximate injectivity and smallness in metric-enriched categories by Adamek-Rosicky.' ), ( 'Met_oo', From f555479cbe9db1c30b09763d7ba5156d73d7f142 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 15 Apr 2026 14:02:27 +0200 Subject: [PATCH 4/9] biproducts ensure cartesian filtered colimits --- .../002_limits-colimits-behavior-implications.sql | 7 +++++++ 1 file changed, 7 insertions(+) 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 b795f69d..639976a1 100644 --- a/database/data/005_implications/002_limits-colimits-behavior-implications.sql +++ b/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 all colimits that exist in $\mathcal{C}$.', + FALSE +), ( 'pointed_characterization', '["pointed"]', From 38fc07c66f5bee9c14f71937bb5d8cdb946ea94c Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 15 Apr 2026 22:48:23 +0200 Subject: [PATCH 5/9] show that Met and Met_oo do have cartesian filtered colimits --- database/data/004_property-assignments/Met.sql | 6 ++++++ database/data/004_property-assignments/Met_oo.sql | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/database/data/004_property-assignments/Met.sql b/database/data/004_property-assignments/Met.sql index 38cc3ec4..dbe4fc64 100644 --- a/database/data/004_property-assignments/Met.sql +++ b/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', diff --git a/database/data/004_property-assignments/Met_oo.sql b/database/data/004_property-assignments/Met_oo.sql index 1ec4889c..bb97a1ed 100644 --- a/database/data/004_property-assignments/Met_oo.sql +++ b/database/data/004_property-assignments/Met_oo.sql @@ -23,6 +23,12 @@ VALUES TRUE, 'Example 4.5 in this preprint' ), +( + 'Met_oo', + 'cartesian filtered colimits', + TRUE, + 'We can use the same proof as for the category of metric spaces 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', From 462148633b4ac3db3f54448c6795706e5c759311 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 15 Apr 2026 19:18:04 +0200 Subject: [PATCH 6/9] add property: cocartesian cofiltered limits --- .../data/003_properties/003_limits-colimits-behavior.sql | 9 +++++++++ database/data/003_properties/100_related-properties.sql | 2 ++ 2 files changed, 11 insertions(+) diff --git a/database/data/003_properties/003_limits-colimits-behavior.sql b/database/data/003_properties/003_limits-colimits-behavior.sql index 270e5fd7..48aee05f 100644 --- a/database/data/003_properties/003_limits-colimits-behavior.sql +++ b/database/data/003_properties/003_limits-colimits-behavior.sql @@ -88,7 +88,16 @@ VALUES 'In a category $\mathcal{C}$, which we assume to have filtered colimits and finite products, we say that filtered colimits are cartesian 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.
This is no standard terminology, it has been suggested in MO/510240. 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 cofiltered limits are cocartesian 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.
+ This is no standard terminology, its dual has been suggested in MO/510240. We have added it to the database since it clarifies the relationship between many related properties.', NULL, + 'cartesian filtered colimits', TRUE ), ( diff --git a/database/data/003_properties/100_related-properties.sql b/database/data/003_properties/100_related-properties.sql index 31ed1fa1..a9d28f8e 100644 --- a/database/data/003_properties/100_related-properties.sql +++ b/database/data/003_properties/100_related-properties.sql @@ -155,6 +155,8 @@ VALUES ('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'), From 25d7fd4aaae21bba82e793a65a4f73fb0a4fa9e0 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 15 Apr 2026 19:18:32 +0200 Subject: [PATCH 7/9] add result connecting extensive with cocartesian cofiltered limits this settles in particular the category of sets (and many more) --- .../002_limits-colimits-behavior-implications.sql | 7 +++++++ 1 file changed, 7 insertions(+) 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 639976a1..b7f00e0f 100644 --- a/database/data/005_implications/002_limits-colimits-behavior-implications.sql +++ b/database/data/005_implications/002_limits-colimits-behavior-implications.sql @@ -160,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"]', From ac838d18cdf166b42b192f406ac4b72220ce0247 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 15 Apr 2026 22:02:32 +0200 Subject: [PATCH 8/9] show that Mon and Grp do not have cocartesian cofiltered limits --- database/data/004_property-assignments/Grp.sql | 10 ++++++++++ database/data/004_property-assignments/Mon.sql | 6 ++++++ 2 files changed, 16 insertions(+) diff --git a/database/data/004_property-assignments/Grp.sql b/database/data/004_property-assignments/Grp.sql index ec6dacb9..5d71a2e6 100644 --- a/database/data/004_property-assignments/Grp.sql +++ b/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 +
$\alpha : G \sqcup \lim_i H_i \to \lim_i (G \sqcup H_i)$
+ is injective, but often fails to be surjective because the components of an element in the image have bounded free product length (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 +
$p_n := x_1 \, y \, x_2 \, y \, \cdots \, x_{n-1} \, y \, x_n \, y^{-(n-1)} \in G \sqcup H_n$.
+ 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.' ); \ No newline at end of file diff --git a/database/data/004_property-assignments/Mon.sql b/database/data/004_property-assignments/Mon.sql index 31382130..5e694937 100644 --- a/database/data/004_property-assignments/Mon.sql +++ b/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 category of commutative monoids. Alternatively, we may use this lemma (dualized).' +), +( + 'Mon', + 'cocartesian cofiltered limits', + FALSE, + 'We know that the category of groups 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.' ); From 5d18203f1ee306f808945dd3a5724ea9034cb567 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 15 Apr 2026 23:32:21 +0200 Subject: [PATCH 9/9] show that Ring and Alg(R) do not have cocartesian cofiltered limits --- database/data/004_property-assignments/Alg(R).sql | 8 ++++++++ database/data/004_property-assignments/Ring.sql | 8 ++++++++ 2 files changed, 16 insertions(+) diff --git a/database/data/004_property-assignments/Alg(R).sql b/database/data/004_property-assignments/Alg(R).sql index 761ddafb..d4f3d5fa 100644 --- a/database/data/004_property-assignments/Alg(R).sql +++ b/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 category of commutative algebras (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 this lemma (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 +
$w_n = (1 + XY) (1+XY^2) \cdots (1+X Y^n) \in A \sqcup B_n$.
+ 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.' ); \ No newline at end of file diff --git a/database/data/004_property-assignments/Ring.sql b/database/data/004_property-assignments/Ring.sql index b1a7e4c2..872ea0cb 100644 --- a/database/data/004_property-assignments/Ring.sql +++ b/database/data/004_property-assignments/Ring.sql @@ -82,4 +82,12 @@ VALUES 'regular quotient object classifier', FALSE, 'We may copy the proof for the category of commutative rings (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 this lemma (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 +
$w_n = (1 + XY) (1+XY^2) \cdots (1+X Y^n) \in A \sqcup B_n$.
+ 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.' ); \ No newline at end of file