From e7517e69fbb38eb3d760a3f9e7d3e080b9a41b2e Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 20 Apr 2026 10:23:32 +0200 Subject: [PATCH 1/8] add properties: exact cofiltered limits, CIP, CSP, stable monos, stable epis --- .../data/003_properties/001_relations.sql | 3 +- .../003_limits-colimits-behavior.sql | 42 ++++++++++++++++++- .../003_properties/005_morphism-behavior.sql | 16 +++++++ .../003_properties/100_related-properties.sql | 21 +++++++++- 4 files changed, 78 insertions(+), 4 deletions(-) diff --git a/database/data/003_properties/001_relations.sql b/database/data/003_properties/001_relations.sql index 49192545..3378639f 100644 --- a/database/data/003_properties/001_relations.sql +++ b/database/data/003_properties/001_relations.sql @@ -4,4 +4,5 @@ INSERT INTO relations (relation, negation) VALUES ('is an', 'is not an'), ('has', 'does not have'), ('has a', 'does not have a'), -('has an', 'does not have an'); \ No newline at end of file +('has an', 'does not have an'), +('satisfies', 'does not satisfy'); \ No newline at end of file diff --git a/database/data/003_properties/003_limits-colimits-behavior.sql b/database/data/003_properties/003_limits-colimits-behavior.sql index 208234c7..129126e0 100644 --- a/database/data/003_properties/003_limits-colimits-behavior.sql +++ b/database/data/003_properties/003_limits-colimits-behavior.sql @@ -93,9 +93,27 @@ VALUES ( 'exact filtered colimits', 'has', - 'In a category $\mathcal{C}$, which we assume to have filtered colimits and finite limits, we say that filtered colimits are exact if for every finite category $\mathcal{I}$ the functor $\lim : [\mathcal{I}, \mathcal{C}] \to \mathcal{C}$ preserves filtered colimits. Equivalently, for every diagram $X : \mathcal{I} \times \mathcal{J} \to \mathcal{C}$, where $\mathcal{I}$ is finite and $\mathcal{J}$ is filtered, the canonical morphism $\mathrm{colim}_{j} \lim_{i} X(i,j) \to \lim_{i} \mathrm{colim}_j X(i,j)$ is an isomorphism.', + 'In a category $\mathcal{C}$, which we assume to have filtered colimits and finite limits, we say that filtered colimits are exact if the following equivalent conditions are satisfied: +
    +
  1. For every finite category $\mathcal{I}$ the functor $\lim : [\mathcal{I}, \mathcal{C}] \to \mathcal{C}$ preserves filtered colimits.
    2. +
  2. For every small filtered category $\mathcal{J}$ the functor $\mathrm{colim} : [\mathcal{J},\mathcal{C}] \to \mathcal{C}$ preserves finite limits.
    3. +
  3. For every diagram $X : \mathcal{I} \times \mathcal{J} \to \mathcal{C}$, where $\mathcal{I}$ is finite and $\mathcal{J}$ is small filtered, the canonical morphism $\mathrm{colim}_j \lim_i X(i,j) \to \lim_i \mathrm{colim}_j X(i,j)$ is an isomorphism.
    4. +
', 'https://ncatlab.org/nlab/show/commutativity+of+limits+and+colimits', - NULL, + 'exact cofiltered limits', + TRUE +), +( + 'exact cofiltered limits', + 'has', + 'In a category $\mathcal{C}$, which we assume to have cofiltered limits and finite colimits, we say that cofiltered limits are exact if the following equivalent conditions are satisfied: +
    +
  1. For every finite category $\mathcal{I}$ the functor $\mathrm{colim} : [\mathcal{I}, \mathcal{C}] \to \mathcal{C}$ preserves cofiltered limits.
    2. +
  2. For every small cofiltered category $\mathcal{J}$ the functor $\lim : [\mathcal{J},\mathcal{C}] \to \mathcal{C}$ preserves finite colimits.
    3. +
  3. For every diagram $X : \mathcal{I} \times \mathcal{J} \to \mathcal{C}$, where $\mathcal{I}$ is finite and $\mathcal{J}$ is small cofiltered, the canonical morphism $\mathrm{colim}_i \lim_j X(i,j) \to \lim_j \mathrm{colim}_i X(i,j)$ is an isomorphism.
    4. +
', + 'https://ncatlab.org/nlab/show/commutativity+of+limits+and+colimits', + 'exact filtered colimits', TRUE ), ( @@ -211,4 +229,24 @@ VALUES NULL, 'unital', TRUE +), +( + 'CIP', + 'satisfies', + 'A category satisfies CIP ("coproducts inject into products") if it has zero morphisms, products, coproducts, and for every family of objects $(X_i)_{i \in I}$ the canonical morphism +

$\alpha : \coprod_i X_i \to \prod_{i \in I} X_i$

+ defined by $p_j \circ \alpha \circ \iota_i = \delta_{i,j}$ is a monomorphism. This is no standard terminology. This property has been added to clarify relationships between other properties, in particular those concerning the commutation between limits and colimits.', + NULL, + 'CSP', + TRUE +), +( + 'CSP', + 'satisfies', + 'A category satisfies CSP ("coproducts surject onto products") if it has zero morphisms, products, coproducts, and for every family of objects $(X_i)_{i \in I}$ the canonical morphism +

$\alpha : \coprod_i X_i \to \prod_{i \in I} X_i$

+ defined by $p_j \circ \alpha \circ \iota_i = \delta_{i,j}$ is an epimorphism. This is no standard terminology. This property has been added to clarify relationships between other properties, in particular those concerning the commutation between limits and colimits.', + NULL, + 'CIP', + TRUE ); \ No newline at end of file diff --git a/database/data/003_properties/005_morphism-behavior.sql b/database/data/003_properties/005_morphism-behavior.sql index 86b416e1..e520dd01 100644 --- a/database/data/003_properties/005_morphism-behavior.sql +++ b/database/data/003_properties/005_morphism-behavior.sql @@ -105,4 +105,20 @@ VALUES 'https://ncatlab.org/nlab/show/one-way+category', 'one-way', TRUE +), +( + 'filtered-colimit-stable monomorphisms', + 'has', + 'A category has filtered-colimit-stable monomorphisms if it has filtered colimits and for every filtered diagram of monomorphisms $(X_i \to Y_i)$ also their colimit $\mathrm{colim}_i X_i \to \mathrm{colim}_i Y_i$ is a monomorphism.', + NULL, + 'cofiltered-limit-stable epimorphisms', + TRUE +), +( + 'cofiltered-limit-stable epimorphisms', + 'has', + 'A category has cofiltered-limit-stable epimorphisms if it has cofiltered limits and for every cofiltered diagram of epimorphisms $(X_i \to Y_i)$ also their limit $\lim_i X_i \to \lim_i Y_i$ is an epimorphism.', + NULL, + 'filtered-colimit-stable monomorphisms', + 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 dfd1b997..29a1bf3f 100644 --- a/database/data/003_properties/100_related-properties.sql +++ b/database/data/003_properties/100_related-properties.sql @@ -185,11 +185,20 @@ VALUES ('exact filtered colimits', 'filtered colimits'), ('exact filtered colimits', 'finitely complete'), ('exact filtered colimits', 'cartesian filtered colimits'), +('exact cofiltered limits', 'cofiltered limits'), +('exact cofiltered limits', 'finitely cocomplete'), +('exact cofiltered limits', 'cocartesian cofiltered limits'), +('exact cofiltered limits', 'cofiltered-limit-stable epimorphisms'), ('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'), +('cocartesian cofiltered limits', 'exact cofiltered limits'), +('filtered-colimit-stable monomorphisms', 'exact filtered colimits'), +('filtered-colimit-stable monomorphisms', 'filtered colimits'), +('cofiltered-limit-stable epimorphisms', 'exact cofiltered limits'), +('cofiltered-limit-stable epimorphisms', 'cofiltered limits'), ('generator', 'generating set'), ('generating set', 'generator'), ('Grothendieck abelian', 'abelian'), @@ -353,4 +362,14 @@ VALUES ('multi-algebraic', 'multi-cocomplete'), ('generalized variety', 'multi-algebraic'), ('generalized variety', 'locally strongly finitely presentable'), -('generalized variety', 'sifted colimits'); +('generalized variety', 'sifted colimits'), +('CIP', 'coproducts'), +('CIP', 'products'), +('CIP', 'zero morphisms'), +('CIP', 'counital'), +('CIP', 'filtered-colimit-stable monomorphisms'), +('CSP', 'coproducts'), +('CSP', 'products'), +('CSP', 'zero morphisms'), +('CSP', 'unital'), +('CSP', 'cofiltered-limit-stable epimorphisms'); From 088047a9a3e4a4557c8a9015ecae690ce861fe0b Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 20 Apr 2026 10:25:02 +0200 Subject: [PATCH 2/8] add results on filtered-colimit-stable monos and CIP --- ..._limits-colimits-behavior-implications.sql | 23 +++++++++++++++++++ .../004_morphism-behavior-implications.sql | 14 +++++++++++ .../007_locally-presentable-implications.sql | 7 ++++++ database/data/010_lemmas/000_lemmas.sql | 9 ++++++++ 4 files changed, 53 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 26cc5805..fd80f268 100644 --- a/database/data/005_implications/002_limits-colimits-behavior-implications.sql +++ b/database/data/005_implications/002_limits-colimits-behavior-implications.sql @@ -69,6 +69,15 @@ VALUES 'This holds by definition.', FALSE ), +( + 'exact_filtered_colimits_monos', + '["exact filtered colimits"]', + '["filtered-colimit-stable monomorphisms"]', + 'This is because $X \to Y$ is a monomorphism iff the diagram +

$\begin{array}{ccc} X & \rightarrow & X \\ \downarrow && \downarrow \\ X & \rightarrow & Y \end{array}$

+ is a pullback, and if a functor preserves finite limits, it preserves pullbacks in particular.', + FALSE +), ( 'cartesian_filtered_colimits_condition', '["cartesian filtered colimits"]', @@ -268,4 +277,18 @@ VALUES '["countable powers"]', 'We can recycle this proof.', FALSE +), +( + 'CIP_assumption', + '["CIP"]', + '["zero morphisms", "products", "coproducts"]', + 'This is true by definition.', + FALSE +), +( + 'CIP_criterion', + '["biproducts", "products", "filtered colimits", "filtered-colimit-stable monomorphisms"]', + '["CIP"]', + 'Let $(X_i)_{i \in I}$ be a family of objects. For every finite subset $E \subseteq I$ the canonical morphism $\coprod_{i \in E} X_i = \prod_{i \in E} X_i \to \prod_{i \in I} X_i$ is a (split) monomorphism. Hence, their colimit is also a monomorphism, which is the canonical morphism $\coprod_{i \in I} X_i \to \prod_{i \in I} X_i$.', + FALSE ); \ No newline at end of file diff --git a/database/data/005_implications/004_morphism-behavior-implications.sql b/database/data/005_implications/004_morphism-behavior-implications.sql index 951bc3e4..0deaa2b9 100644 --- a/database/data/005_implications/004_morphism-behavior-implications.sql +++ b/database/data/005_implications/004_morphism-behavior-implications.sql @@ -152,4 +152,18 @@ VALUES '["reflexive coequalizers"]', 'Every reflexive pair is equal: If $f s = g s = \mathrm{id}$, then since $s f = \mathrm{id}$ (one-way), we must have $f = s^{-1}$, and likewise $g = s^{-1}$.', FALSE +), +( + 'filtered_monos_assumption', + '["filtered-colimit-stable monomorphisms"]', + '["filtered colimits"]', + 'This holds by definition.', + FALSE +), +( + 'filtered_monos_trivial', + '["left cancellative", "filtered colimits"]', + '["filtered-colimit-stable monomorphisms"]', + 'This is trivial.', + FALSE ); \ No newline at end of file diff --git a/database/data/005_implications/007_locally-presentable-implications.sql b/database/data/005_implications/007_locally-presentable-implications.sql index d57c5142..3d52bab4 100644 --- a/database/data/005_implications/007_locally-presentable-implications.sql +++ b/database/data/005_implications/007_locally-presentable-implications.sql @@ -222,4 +222,11 @@ VALUES '["generalized variety", "multi-cocomplete"]', 'This follows from one of equivalent formulations of multi-algebraic categories.', TRUE +), +( + 'locally-finitely-multi-presentable_stable-monos', + '["locally finitely multi-presentable"]', + '["filtered-colimit-stable monomorphisms"]', + 'Every locally finitely multi-presentable category is a multi-reflective full subcategory of a presheaf category closed under filtered colimits (Adamek-Rosicky, 4.30). Since multi-reflective full subcategories are in general closed under connected limits (Adamek-Rosicky, Thm. 4.26), in particular, we can calculate not only filtered colimits but also kernel pairs as well as in a presheaf category.', + FALSE ); \ No newline at end of file diff --git a/database/data/010_lemmas/000_lemmas.sql b/database/data/010_lemmas/000_lemmas.sql index 54a52451..bb5cd410 100644 --- a/database/data/010_lemmas/000_lemmas.sql +++ b/database/data/010_lemmas/000_lemmas.sql @@ -105,4 +105,13 @@ INSERT INTO lemmas (

$\cong F(\lim_i \mathrm{colim}_j G(X(i,j)))$

$\cong \lim_i F(\mathrm{colim}_j G(X(i,j)))$

$\cong \lim_i \mathrm{colim}_j X(i,j)$

' +), +( + 'filtered-monos', + 'Detection of filtered-colimit-stable monomorphisms', + 'Let $\mathcal{C}$ be a category with filtered colimits. Assume that $U : \mathcal{C} \to \mathcal{D}$ is faithful functor which preserves monomorphisms and filtered colimits. If monomorphisms in $\mathcal{D}$ are stable under filtered colimits, then the same is true for $\mathcal{C}$. +

+ For the record, here is the dual statement: Let $\mathcal{C}$ be a category with cofiltered limits. Assume that $U : \mathcal{C} \to \mathcal{D}$ is faithful functor which preserves epimorphisms and cofiltered limits. If epimorphisms in $\mathcal{D}$ are stable under cofiltered limits, then the same is true for $\mathcal{C}$. + ', + 'Since $U$ is faithful, it reflects monomorphisms. From here the proof is straight forward.' ); \ No newline at end of file From 851677b53dad3cf2fec6a301c5d61c26b69c97b1 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 20 Apr 2026 10:31:51 +0200 Subject: [PATCH 3/8] disprove CSP for most categories --- database/data/001_categories/200_comments.sql | 2 +- database/data/004_property-assignments/Ab.sql | 6 ++++++ database/data/004_property-assignments/Ban.sql | 6 ++++++ database/data/004_property-assignments/CMon.sql | 8 +++++++- database/data/004_property-assignments/Grp.sql | 6 ++++++ database/data/004_property-assignments/Mon.sql | 6 ++++++ database/data/004_property-assignments/R-Mod.sql | 8 +++++++- database/data/004_property-assignments/R-Mod_div.sql | 6 +++--- database/data/004_property-assignments/Rng.sql | 8 +++++++- database/data/004_property-assignments/Set_pointed.sql | 6 ++++++ database/data/004_property-assignments/Top_pointed.sql | 6 ++++++ database/data/004_property-assignments/Vect.sql | 6 +++--- database/data/006_special-objects/004_coproducts.sql | 2 +- database/data/007_special-morphisms/004_epimorphisms.sql | 6 ++++++ 14 files changed, 71 insertions(+), 11 deletions(-) diff --git a/database/data/001_categories/200_comments.sql b/database/data/001_categories/200_comments.sql index f29387a4..338adda3 100644 --- a/database/data/001_categories/200_comments.sql +++ b/database/data/001_categories/200_comments.sql @@ -38,7 +38,7 @@ VALUES ), ( 'Sh(X,Ab)', - 'It is likely that neither of the currently remaining unknown properties (finitary algebraic, locally ℵ₁-presentable, etc.) are satisfied for a generic space $X$, but we need to make this precise by adding additional requirements to $X$. Maybe we need to create separate entries for specific spaces $X$.' + 'It is likely that neither of the currently remaining unknown properties (finitary algebraic, locally ℵ₁-presentable, CSP, etc.) are satisfied for a generic space $X$, but we need to make this precise by adding additional requirements to $X$. Maybe we need to create separate entries for specific spaces $X$.' ), ( 'M-Set', diff --git a/database/data/004_property-assignments/Ab.sql b/database/data/004_property-assignments/Ab.sql index 5785e039..f6d9dd6f 100644 --- a/database/data/004_property-assignments/Ab.sql +++ b/database/data/004_property-assignments/Ab.sql @@ -34,4 +34,10 @@ VALUES 'skeletal', FALSE, 'This is trivial.' +), +( + 'Ab', + 'CSP', + FALSE, + 'The canonical homomorphism $\bigoplus_{n \geq 0} \mathbb{Z} \to \prod_{n \geq 0} \mathbb{Z}$ is not surjective, hence no epimorphism.' ); diff --git a/database/data/004_property-assignments/Ban.sql b/database/data/004_property-assignments/Ban.sql index 3ae433bc..f2e1489b 100644 --- a/database/data/004_property-assignments/Ban.sql +++ b/database/data/004_property-assignments/Ban.sql @@ -76,4 +76,10 @@ VALUES 'regular subobject classifier', FALSE, 'If $\Omega$ is a regular subobject classifier, then by the classification of regular monomorphisms, $\mathrm{Hom}(X,\Omega)$ is isomorphic to the set of closed subspaces of $X$ for any Banach space $X$. For $X = \mathbb{C}$ this implies that there are exactly two vectors in $\Omega$ with norm $\leq 1$, which is absurd. (For $\Omega = 0$ there is just one, and for $\Omega \neq 0$ there are infinitely many.)' +), +( + 'Ban', + 'CSP', + FALSE, + 'By using the concrete description of products and coproducts, for the constant family $X_n = \mathbb{C}$ the canonical morphism $\coprod_n X_n \to \prod_n X_n$ becomes the canonical inclusion map $\ell^1 \hookrightarrow \ell^\infty$. This is not an epimorphism (i.e., has no dense image) since the closure of the image is precisely $c_0$. So for example, $(1,1,\dotsc)$ is not contained in the closure of the image.' ); \ No newline at end of file diff --git a/database/data/004_property-assignments/CMon.sql b/database/data/004_property-assignments/CMon.sql index 9ab207a8..08de5453 100644 --- a/database/data/004_property-assignments/CMon.sql +++ b/database/data/004_property-assignments/CMon.sql @@ -82,4 +82,10 @@ VALUES 'regular quotient object classifier', FALSE, 'If $P \in \mathbf{CMon}$ is a regular quotient object classifier, this means that every surjective homomorphism of commutative monoids $A \to B$ is the cokernel of a unique homomorphism $P \to A$. But there are many surjective homomorphisms which are no cokernels at all: Consider the Boolean monoid $(\{0,1\},\vee)$ with $1 \vee 1 = 1$ and the surjective homomorphism $f : (\mathbb{N},+) \to (\{0,1\},\vee)$ defined by $f(0)=0$ and $f(n)=1$ for $n \geq 1$. It has trivial kernel, but is no isomorphism, so it cannot be a cokernel.' -); +), +( + 'CMon', + 'CSP', + FALSE, + 'First of all, epimorphisms in $\mathbf{CMon}$ are preserved and reflected by the forgetful functor to $\mathbf{Mon}$ (see below). Furthermore, if $M \to N$ is an epimorphism in $\mathbf{Mon}$ and $M$ is infinite, then $\mathrm{card}(N) \leq \mathrm{card}(M)$ (see MO/510431). This implies that in $\mathbf{CMon}$ the canonical homomorphism $\bigoplus_{n \geq 0} \mathbb{N} \to \prod_{n \geq 0} \mathbb{N}$ is not an epimorphism because its domain is countable and its codomain is uncountable.' +); \ No newline at end of file diff --git a/database/data/004_property-assignments/Grp.sql b/database/data/004_property-assignments/Grp.sql index 5d71a2e6..20cb859b 100644 --- a/database/data/004_property-assignments/Grp.sql +++ b/database/data/004_property-assignments/Grp.sql @@ -92,4 +92,10 @@ VALUES 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.' +), +( + 'Grp', + 'CSP', + FALSE, + 'The canonical homomorphism $\coprod_{n \geq 0} \mathbb{Z} \to \prod_{n \geq 0} \mathbb{Z}$ is not surjective because its domain is countable and its codomain is uncountable. Hence it is no epimorphism.' ); \ 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 5e694937..101af4d1 100644 --- a/database/data/004_property-assignments/Mon.sql +++ b/database/data/004_property-assignments/Mon.sql @@ -82,5 +82,11 @@ VALUES '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.' +), +( + 'Mon', + 'CSP', + FALSE, + 'If $M \to N$ is an epimorphism in $\mathbf{Mon}$ and $M$ is infinite, then $\mathrm{card}(N) \leq \mathrm{card}(M)$ (see MO/510431). This implies that in $\mathbf{Mon}$ the canonical homomorphism $\coprod_{n \geq 0} \mathbb{N} \to \prod_{n \geq 0} \mathbb{N}$ is not an epimorphism because its domain is countable and its codomain is uncountable.' ); diff --git a/database/data/004_property-assignments/R-Mod.sql b/database/data/004_property-assignments/R-Mod.sql index fccdcad8..71ad95aa 100644 --- a/database/data/004_property-assignments/R-Mod.sql +++ b/database/data/004_property-assignments/R-Mod.sql @@ -34,4 +34,10 @@ VALUES 'skeletal', FALSE, 'This is trivial.' -); +), +( + 'R-Mod', + 'CSP', + FALSE, + 'The canonical homomorphism $\bigoplus_{n \geq 0} R \to \prod_{n \geq 0} R$ is not surjective, hence no epimorphism.' +); \ No newline at end of file diff --git a/database/data/004_property-assignments/R-Mod_div.sql b/database/data/004_property-assignments/R-Mod_div.sql index a2db769a..9a2e8b53 100644 --- a/database/data/004_property-assignments/R-Mod_div.sql +++ b/database/data/004_property-assignments/R-Mod_div.sql @@ -31,7 +31,7 @@ VALUES ), ( 'R-Mod_div', - 'trivial', + 'CSP', FALSE, - 'This is trivial.' -); + 'The canonical homomorphism $\bigoplus_{n \geq 0} R \to \prod_{n \geq 0} R$ is not surjective, hence no epimorphism.' +); \ No newline at end of file diff --git a/database/data/004_property-assignments/Rng.sql b/database/data/004_property-assignments/Rng.sql index 08a6240c..f00417bf 100644 --- a/database/data/004_property-assignments/Rng.sql +++ b/database/data/004_property-assignments/Rng.sql @@ -78,4 +78,10 @@ VALUES '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 limit is $\mathbb{Z}[[Y]]$ (both in $\mathbf{Ring}$ and $\mathbf{Rng}$). Every element in the coproduct of rngs $\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) - 1 \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 +), +( + 'Rng', + 'CSP', + FALSE, + 'Assume that $\coprod_n \mathbb{Z} \to \prod_n \mathbb{Z}$ is an epimorphism in $\mathbf{Rng}$. Then $((\coprod_n \mathbb{Z})^+)^{\mathrm{ab}} \to \prod_n \mathbb{Z}$ would be an epimorphism in $\mathbf{CRing}$, where $(-)^+$ denotes the unitalization and $(-)^{\mathrm{ab}}$ the abelianization. But if $R \to S$ is an epimorphism of commutative rings, then $\mathrm{card}(S) \leq \mathrm{card}(R)$ by SP/04W0. Since $((\coprod_n \mathbb{Z})^+)^{\mathrm{ab}}$ is countable and $\prod_n \mathbb{Z}$ is not, we get a contradiction.' +); diff --git a/database/data/004_property-assignments/Set_pointed.sql b/database/data/004_property-assignments/Set_pointed.sql index a0719751..7b0317c5 100644 --- a/database/data/004_property-assignments/Set_pointed.sql +++ b/database/data/004_property-assignments/Set_pointed.sql @@ -73,6 +73,12 @@ VALUES FALSE, 'The joint image of $X \to X \times Y \leftarrow Y$ is just $\{(x,0) : x \in X\} \cup \{(0,y) : y \in Y\}$ (where $0$ denotes the base point), which is clearly a proper subset of $X \times Y$ when both $X,Y$ are non-trivial.' ), +( + 'Set*', + 'CSP', -- TODO: remove duplication with unital proof + FALSE, + 'The image of $X \vee Y$ in $X \times Y$ is just $\{(x,0) : x \in X\} \cup \{(0,y) : y \in Y\}$ (where $0$ denotes the base point), which is clearly a proper subset when both $X,Y$ are non-trivial.' +), ( 'Set*', 'conormal', diff --git a/database/data/004_property-assignments/Top_pointed.sql b/database/data/004_property-assignments/Top_pointed.sql index fa4e679d..65efa277 100644 --- a/database/data/004_property-assignments/Top_pointed.sql +++ b/database/data/004_property-assignments/Top_pointed.sql @@ -143,6 +143,12 @@ VALUES 'coaccessible', FALSE, 'We can adjust the proof for $\mathbf{Top}$ as follows: Assume $\mathbf{Top}_*$ is coaccessible. Let $S_0=\{x,*\}$ be the pointed topological space such that $\{*\}$ is the only non-trivial open set, and let $S_1=\{x,*\}$ be the pointed space such that $\{x\}$ is the only non-trivial open set. Let $p_i\colon S_i \to \{x,*\}$ be the identity function to the two-element indiscrete pointed space. Then, a pointed topological space is discrete if and only if it is projective to the morphisms $p_0$ and $p_1$. This implies that the full subcategory spanned by all discrete pointed spaces, which is equivalent to $\mathbf{Set}_*$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\mathbf{Set}_*$ is not coaccessible, this is a contradiction.' +), +( + 'Top*', + 'CSP', -- TODO: remove duplication with unital proof + FALSE, + 'The image of $X \vee Y$ in $X \times Y$ is just $\{(x,0) : x \in X\} \cup \{(0,y) : y \in Y\}$ (where $0$ denotes the base point), which is clearly a proper subset when both $X,Y$ are non-trivial.' ); diff --git a/database/data/004_property-assignments/Vect.sql b/database/data/004_property-assignments/Vect.sql index e8bab05f..021cac36 100644 --- a/database/data/004_property-assignments/Vect.sql +++ b/database/data/004_property-assignments/Vect.sql @@ -25,13 +25,13 @@ VALUES ), ( 'Vect', - 'trivial', + 'skeletal', FALSE, 'This is trivial.' ), ( 'Vect', - 'skeletal', + 'CSP', FALSE, - 'This is trivial.' + 'The canonical homomorphism $\bigoplus_{n \geq 0} K \to \prod_{n \geq 0} K$ is not surjective, hence no epimorphism.' ); diff --git a/database/data/006_special-objects/004_coproducts.sql b/database/data/006_special-objects/004_coproducts.sql index 4406da7e..fb0acfb0 100644 --- a/database/data/006_special-objects/004_coproducts.sql +++ b/database/data/006_special-objects/004_coproducts.sql @@ -11,7 +11,7 @@ VALUES ('1', '$0 \sqcup 0 = 0$'), ('Ab', 'direct sums'), ('Alg(R)', 'see MSE/625874'), -('Ban', 'cocompletion of the direct sum with the $1$-norm'), +('Ban', 'The coproduct of a family of Banach spaces $(B_i)$ is the subspace $\bigl\{x \in \prod_i B_i : \sum_i |x_i| < \infty\bigr\}$ equipped with the $1$-norm $|x| := \sum_i |x_i|$.'), ('CAlg(R)', 'tensor products over $R$'), ('Cat', 'disjoint unions'), ('CMon', 'direct sums'), diff --git a/database/data/007_special-morphisms/004_epimorphisms.sql b/database/data/007_special-morphisms/004_epimorphisms.sql index 54e162c7..bd3b9213 100644 --- a/database/data/007_special-morphisms/004_epimorphisms.sql +++ b/database/data/007_special-morphisms/004_epimorphisms.sql @@ -70,6 +70,12 @@ VALUES 'A functor $F : \mathcal{C} \to \mathcal{D}$ is an epimorphism iff $F$ is surjective on objects and for every morphism $s$ in $\mathcal{D}$ there is a zigzag over $U := F(\mathcal{C})$, meaning morphisms $u_1,\dotsc,u_{m+1} \in U$, $v_1,\dotsc,v_m \in U$, $x_1,\dotsc,x_m \in \mathcal{D}$ and $y_1,\dotsc,y_m \in \mathcal{D}$ such that $s = x_1 u_1$, $u_1 = v_1 y_1$, $x_{i-1} v_{i-1} = x_i u_i$, $u_i y_{i-1} = v_i y_i$, $x_m v_m = u_{m+1}$ and $u_{m+1} y_m = s$.', 'This is an extension of the corresponding theorem for monoids and proven in Epimorphisms and Dominions, III by John R. Isbell.' ), +( + 'CMon', + 'A morphism in $\mathbf{CMon}$ is an epimorphism iff it is an epimorphism in $\mathbf{Mon}$, which in turn can be characterized by Isbell''s zigzag theorem.', + 'If $f : M \to N$ is a homomorphism of commutative monoids which is an epimorphism in $\mathbf{Mon}$, then it is trivially also an epimorphism in $\mathbf{CMon}$. The converse requires a proof, which can be found at MSE/5133488. + ' +), ( 'CAlg(R)', 'a homomorphism of algebras which is an epimorphism of commutative rings', From c5dbe90daececa09ee1a6047aa315e8486c163bd Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 20 Apr 2026 10:35:07 +0200 Subject: [PATCH 4/8] decide CIP for various categories --- database/data/004_property-assignments/Ban.sql | 6 ++++++ database/data/004_property-assignments/Grp.sql | 6 ++++++ database/data/004_property-assignments/Mon.sql | 6 ++++++ database/data/004_property-assignments/Rel.sql | 6 ++++++ database/data/004_property-assignments/Rng.sql | 6 ++++++ database/data/004_property-assignments/Set_pointed.sql | 6 ++++++ database/data/004_property-assignments/Top_pointed.sql | 6 ++++++ 7 files changed, 42 insertions(+) diff --git a/database/data/004_property-assignments/Ban.sql b/database/data/004_property-assignments/Ban.sql index f2e1489b..01c25b05 100644 --- a/database/data/004_property-assignments/Ban.sql +++ b/database/data/004_property-assignments/Ban.sql @@ -35,6 +35,12 @@ VALUES TRUE, 'If $X$ is a Banach space and $(Y_i)$ is a cofiltered diagram of Banach spaces, the canonical map $X \oplus \lim_i Y_i \to \lim_i (X \oplus Y_i)$ is an isomorphism: Since the forgetful functor $\mathbf{Ban} \to \mathbf{Vect}$ preserves finite coproducts and all limits, and $\mathbf{Vect}$ has the claimed property (see here), the canonical map is bijective. It remains to show that it is isometric. For $(x,y) \in X \oplus \lim_i Y_i$ the norm in the domain is $|x| + \sup_i |y_i|$, and the norm in the codomain is $\sup_i (|x| + |y_i|)$, and these clearly agree.' ), +( + 'Ban', + 'CIP', + TRUE, + 'This is immediate from the concrete description of coproducts and products.' +), ( 'Ban', 'cogenerator', diff --git a/database/data/004_property-assignments/Grp.sql b/database/data/004_property-assignments/Grp.sql index 20cb859b..66d4ae36 100644 --- a/database/data/004_property-assignments/Grp.sql +++ b/database/data/004_property-assignments/Grp.sql @@ -77,6 +77,12 @@ VALUES FALSE, 'The canonical morphism $F_2 = \mathbb{Z} \sqcup \mathbb{Z} \to \mathbb{Z} \times \mathbb{Z}$ is not a monomorphism since $F_2$ is not abelian.' ), +( + 'Grp', + 'CIP', -- TODO: remove code duplication with "counital" proof + FALSE, + 'The canonical morphism $F_2 = \mathbb{Z} \sqcup \mathbb{Z} \to \mathbb{Z} \times \mathbb{Z}$ is not a monomorphism since $F_2$ is not abelian.' +), ( 'Grp', 'regular quotient object classifier', diff --git a/database/data/004_property-assignments/Mon.sql b/database/data/004_property-assignments/Mon.sql index 101af4d1..1c48bf6e 100644 --- a/database/data/004_property-assignments/Mon.sql +++ b/database/data/004_property-assignments/Mon.sql @@ -59,6 +59,12 @@ VALUES FALSE, 'The canonical morphism $\mathbb{N} \sqcup \mathbb{N} \to \mathbb{N} \times \mathbb{N}$ is not a monomorphism since $\mathbb{N} \sqcup \mathbb{N}$ is not commutative.' ), +( + 'Mon', + 'CIP', -- TODO: remove code duplication with "counital" proof + FALSE, + 'The canonical morphism $\mathbb{N} \sqcup \mathbb{N} \to \mathbb{N} \times \mathbb{N}$ is not a monomorphism since $\mathbb{N} \sqcup \mathbb{N}$ is not commutative.' +), ( 'Mon', 'coregular', diff --git a/database/data/004_property-assignments/Rel.sql b/database/data/004_property-assignments/Rel.sql index adef9a73..6478ce6d 100644 --- a/database/data/004_property-assignments/Rel.sql +++ b/database/data/004_property-assignments/Rel.sql @@ -53,6 +53,12 @@ VALUES TRUE, 'This is a consequence of the description of coproducts and products, both are disjoint unions (even for infinite families).' ), +( + 'Rel', + 'CIP', + TRUE, + 'The canonical morphism from the coproduct to the product is the identity.' +), ( 'Rel', 'kernels', diff --git a/database/data/004_property-assignments/Rng.sql b/database/data/004_property-assignments/Rng.sql index f00417bf..1d8b47d1 100644 --- a/database/data/004_property-assignments/Rng.sql +++ b/database/data/004_property-assignments/Rng.sql @@ -53,6 +53,12 @@ VALUES FALSE, 'If $\mathbb{Z}\langle X_1,\dotsc,X_n \rangle_0$ denotes the free rng on $n$ generators (non-commutative polynomials without constant term), then the canonical homomorphism $\mathbb{Z}\langle X,Y \rangle_0 = \mathbb{Z}\langle X \rangle_0 \sqcup \mathbb{Z}\langle Y \rangle_0 \to \mathbb{Z}\langle X \rangle_0 \times \mathbb{Z}\langle Y \rangle_0$ is not a monomorphism since $\mathbb{Z}\langle X,Y \rangle_0$ is not commutative.' ), +( + 'Rng', + 'CIP', -- TODO: remove code duplication with "counital" proof + FALSE, + 'If $\mathbb{Z}\langle X_1,\dotsc,X_n \rangle_0$ denotes the free rng on $n$ generators (non-commutative polynomials without constant term), then the canonical homomorphism $\mathbb{Z}\langle X,Y \rangle_0 = \mathbb{Z}\langle X \rangle_0 \sqcup \mathbb{Z}\langle Y \rangle_0 \to \mathbb{Z}\langle X \rangle_0 \times \mathbb{Z}\langle Y \rangle_0$ is not a monomorphism since $\mathbb{Z}\langle X,Y \rangle_0$ is not commutative.' +), ( 'Rng', 'regular subobject classifier', diff --git a/database/data/004_property-assignments/Set_pointed.sql b/database/data/004_property-assignments/Set_pointed.sql index 7b0317c5..43a3aa49 100644 --- a/database/data/004_property-assignments/Set_pointed.sql +++ b/database/data/004_property-assignments/Set_pointed.sql @@ -61,6 +61,12 @@ VALUES
Case 1: There is some index $i$ with $z_i \in X \setminus \{0\}$. We claim $z_j \in X$ for any index $j$ and $z_j = z_i$ in $X$, so that $z$ has a preimage in $X$. To see this, choose an index $k \geq i,j$. Since $X \vee Y_i \to X \vee Y_k$ maps $z_i \mapsto z_k$ and is the identity on $X$, we see that $z_k \in X$ and $z_k = z_i$ in $X$. Since $X \vee Y_j \to X \vee Y_k$ maps $z_j \mapsto z_k$, we see that $z_j \notin Y_j$, since otherwise $z_k \in Y_k \cap X = \{0\}$. Hence, $z_j \in X \setminus \{0\}$, and then $z_j = z_k = z_i$.
Case 2: We have $z_i \in Y_i$ for all $i$. Then clearly $(z_i) \in \lim_i Y_i$ is a preimage.' ), +( + 'Set*', + 'CIP', + TRUE, + 'The coproduct (wedge sum) of a family of pointed sets $(X_i)_{i \in I}$ can be realized as the subset of $\prod_{i \in I} X_i$ consisting of those tuples $x$ such that $x_i = 0$ for all but (at most) one index.' +), ( 'Set*', 'skeletal', diff --git a/database/data/004_property-assignments/Top_pointed.sql b/database/data/004_property-assignments/Top_pointed.sql index 65efa277..80e18cd9 100644 --- a/database/data/004_property-assignments/Top_pointed.sql +++ b/database/data/004_property-assignments/Top_pointed.sql @@ -77,6 +77,12 @@ VALUES TRUE, 'Since embeddings are regular monomorphisms in this category (see below) and hence strong monomorphisms, it suffices to prove that the canonical morphism $X \vee Y \hookrightarrow X \times Y$ is an embedding. For a proof, see MSE/4055988.' ), +( + 'Top*', + 'CIP', + TRUE, + 'This follows since $\mathbf{Set}_*$ has this property and the forgetful functor preserves products and coproducts.' +), ( 'Top*', 'cocartesian cofiltered limits', From 800a9f84aab5103d16748a8d138fa0366437e087 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 20 Apr 2026 10:37:57 +0200 Subject: [PATCH 5/8] decide filtered-colimit-stable monos for various categories --- database/data/004_property-assignments/Ban.sql | 6 +++--- database/data/004_property-assignments/FS.sql | 6 ++++++ database/data/004_property-assignments/Haus.sql | 6 ++++++ database/data/004_property-assignments/Meas.sql | 6 ++++++ database/data/004_property-assignments/Met.sql | 4 ++-- database/data/004_property-assignments/Met_oo.sql | 4 ++-- database/data/004_property-assignments/Setne.sql | 6 ++++++ database/data/004_property-assignments/Top.sql | 6 ++++++ database/data/004_property-assignments/Top_pointed.sql | 6 ++++++ 9 files changed, 43 insertions(+), 7 deletions(-) diff --git a/database/data/004_property-assignments/Ban.sql b/database/data/004_property-assignments/Ban.sql index 01c25b05..e81288df 100644 --- a/database/data/004_property-assignments/Ban.sql +++ b/database/data/004_property-assignments/Ban.sql @@ -51,13 +51,13 @@ VALUES 'Ban', 'balanced', FALSE, - 'The canonical morphism $\mathbb{C} \oplus \mathbb{C} \to \mathbb{C} \times \mathbb{C}$ is a counterexample; here the direct sum (coproduct) carries the $1$-norm and the direct product the $\sup$-norm.' + 'The linear map $\mathbb{C} \to \mathbb{C}$, $x \mapsto x/2$ is a counterexample. It is bijective, hence a mono- and epimorphism, but not isometric and therefore no isomorphism.' ), ( 'Ban', - 'exact filtered colimits', + 'filtered-colimit-stable monomorphisms', FALSE, - 'We will exhibit a directed colimit of monomorphisms which is not a monomorphism. For $n \geq 1$ let $V_n$ be the Banach space with underlying vector space $\mathbb{C}$ and the norm $|x|_n := \frac{1}{n} |x|$. For $n \leq m$ the identity map provides a morphism $V_n \to V_m$, which is clearly a monomorphism (also an epimorphism by the way, but an isomorphism iff $n=m$). Let $V$ be the colimit of all $V_n$ in the category of semi-normed vector spaces. It is constructed as the colimit in the category of vector spaces with the semi-norm $|x| := \inf \{|x|_m : n \leq m \}$ for $x \in V_n$. So clearly, the semi-norm is zero. Hence, the colimit in the category of normed vector spaces is $0$. The colimit in the category of Banach spaces is its completion, also $0$. Thus, the monomorphisms $V_1 \to V_n$ become $V_1 \to 0$ in the colimit.' + 'The proof is similar to $\mathbf{Met}$. For $n \geq 1$ let $V_n$ be the Banach space with underlying vector space $\mathbb{C}$ and the norm $|x|_n := \frac{1}{n} |x|$. For $n \leq m$ the identity map provides a morphism $V_n \to V_m$, which is clearly a monomorphism (also an epimorphism by the way, but an isomorphism iff $n=m$). Let $V$ be the colimit of all $V_n$ in the category of semi-normed vector spaces. It is constructed as the colimit in the category of vector spaces with the semi-norm $|x| := \inf \{|x|_m : n \leq m \}$ for $x \in V_n$. So clearly, the semi-norm is zero. Hence, the colimit in the category of normed vector spaces is $0$. The colimit in the category of Banach spaces is its completion, also $0$. Thus, the monomorphisms $V_1 \to V_n$ become $V_1 \to 0$ in the colimit.' ), ( 'Ban', diff --git a/database/data/004_property-assignments/FS.sql b/database/data/004_property-assignments/FS.sql index b8b8d8b2..4d56a486 100644 --- a/database/data/004_property-assignments/FS.sql +++ b/database/data/004_property-assignments/FS.sql @@ -53,6 +53,12 @@ VALUES TRUE, 'If $f : X \to Y$ is a surjective map of finite sets, it is the coequalizer of the two projections $p_1, p_2 : X \times_Y X \rightrightarrows X$ in $\mathbf{FinSet}$, but also in $\mathbf{FS}$. Notice that $p_1,p_2$ are surjective. Even though $X \times_Y X$ is not a pullback in $\mathbf{FS}$, we can use this finite set here.' ), +( + 'FS', + 'filtered-colimit-stable monomorphisms', + TRUE, + 'This is because every monomorphism is an isomorphism in this category (see below), and isomorphisms are always stable under any type of colimit.' +), ( 'FS', 'multi-terminal object', diff --git a/database/data/004_property-assignments/Haus.sql b/database/data/004_property-assignments/Haus.sql index 6005cdf3..b231082b 100644 --- a/database/data/004_property-assignments/Haus.sql +++ b/database/data/004_property-assignments/Haus.sql @@ -71,6 +71,12 @@ VALUES 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}$.' ), +( + 'Haus', + 'filtered-colimit-stable monomorphisms', + FALSE, + 'The proof is similar to $\mathbf{Met}$. For $n \geq 1$ let $X_n$ be the pushout of $[-1/n,+1/n] \hookrightarrow \mathbb{R}$ with itself. That is, $X_n$ is the union of two lines $\mathbb{R} \times \{1\}$ and $\mathbb{R} \times \{2\}$ where we identify $(x,1) \equiv (x,2)$ when $|x| \leq 1/n$. Then $X_n$ is Hausdorff, and there is a canonical surjective continuous map $X_n \to X_{n+1}$. The colimit in $\mathbf{Top}$ is the union of two lines where we identify $(x,1) \equiv (x,2)$ when $|x| \leq 1/n$ for some $n$, i.e. when $x \neq 0$. This is the line with the double origin, which is not Hausdorff. Its Hausdorff reflection is the line $\mathbb{R}$ where all points of both lines are identified, and it provides the colimit in $\mathbf{Haus}$. Now, the injective continuous maps $\{1,2\} \to X_n$, $i \mapsto (0,i)$ (where $\{1,2\}$ is discrete) become the constant map $0 : \{1,2\} \to \mathbb{R}$ in the colimit, which is no monomorphism.' +), ( 'Haus', 'balanced', diff --git a/database/data/004_property-assignments/Meas.sql b/database/data/004_property-assignments/Meas.sql index a1ef314e..106152a4 100644 --- a/database/data/004_property-assignments/Meas.sql +++ b/database/data/004_property-assignments/Meas.sql @@ -53,6 +53,12 @@ VALUES TRUE, 'Take the two-element set $2$ endowed with the trivial $\sigma$-algebra (where only $\varnothing$ and $2$ are measurable), and use that $2$ is a cogenerator for $\mathbf{Set}$.' ), +( + 'Meas', + 'filtered-colimit-stable monomorphisms', + TRUE, + 'This follows from this lemma applied to the forgetful functor to $\mathbf{Set}$.' +), ( 'Meas', 'semi-strongly connected', diff --git a/database/data/004_property-assignments/Met.sql b/database/data/004_property-assignments/Met.sql index fcf2ab76..de319d56 100644 --- a/database/data/004_property-assignments/Met.sql +++ b/database/data/004_property-assignments/Met.sql @@ -121,9 +121,9 @@ VALUES ), ( 'Met', - 'exact filtered colimits', + 'filtered-colimit-stable monomorphisms', FALSE, - 'See Remark 2.7 in Approximate injectivity and smallness in metric-enriched categories by Adamek-Rosicky.' + 'The following example is taken from Remark 2.7 in Approximate injectivity and smallness in metric-enriched categories by Adamek-Rosicky: For $n \geq 1$ let $X_n$ denote the metric space with underlying set $\{0,1\}$ in which $0,1$ have distance $1/n$. We have bijective non-expansive maps $X_n \to X_{n+1}$, $x \mapsto x$. The colimit of this sequence in $\mathbf{PMet}$ is $\{0,1\}$ where $0,1$ have distance $0$, so the colimit in $\mathbf{Met}$ collapses to $\{0\}$. Therefore, the colimit of the monomorphisms $X_0 \to X_n$, $x \mapsto x$ is the non-injective map $X_0 \to \{0\}$.' ), ( 'Met', diff --git a/database/data/004_property-assignments/Met_oo.sql b/database/data/004_property-assignments/Met_oo.sql index 79cd4b3d..2ad63fb9 100644 --- a/database/data/004_property-assignments/Met_oo.sql +++ b/database/data/004_property-assignments/Met_oo.sql @@ -61,9 +61,9 @@ VALUES ), ( 'Met_oo', - 'exact filtered colimits', + 'filtered-colimit-stable monomorphisms', FALSE, - 'See Remark 2.7 in Approximate injectivity and smallness in metric-enriched categories by Adamek-Rosicky.' + 'We can copy the proof from the category of metric spaces.' ), ( 'Met_oo', diff --git a/database/data/004_property-assignments/Setne.sql b/database/data/004_property-assignments/Setne.sql index 0f34870f..cb449bff 100644 --- a/database/data/004_property-assignments/Setne.sql +++ b/database/data/004_property-assignments/Setne.sql @@ -108,6 +108,12 @@ VALUES 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', + 'filtered-colimit-stable monomorphisms', + TRUE, + 'This follows from this lemma applied to the forgetful functor to $\mathbf{Set}$.' +), ( 'Setne', 'sequential limits', diff --git a/database/data/004_property-assignments/Top.sql b/database/data/004_property-assignments/Top.sql index 7b8cbdf8..dea6e8f5 100644 --- a/database/data/004_property-assignments/Top.sql +++ b/database/data/004_property-assignments/Top.sql @@ -71,6 +71,12 @@ VALUES TRUE, 'The category has all limits and colimits, and the regular monomorphisms are the subspace inclusions. Thus, it suffices to prove that subspace inclusions are stable under pushouts. For a proof see e.g. Lemma 3.6 at the nLab.' ), +( + 'Top', + 'filtered-colimit-stable monomorphisms', + TRUE, + 'This follows from this lemma applied to the forgetful functor to $\mathbf{Set}$.' +), ( 'Top', 'cartesian filtered colimits', diff --git a/database/data/004_property-assignments/Top_pointed.sql b/database/data/004_property-assignments/Top_pointed.sql index 80e18cd9..569a7a5b 100644 --- a/database/data/004_property-assignments/Top_pointed.sql +++ b/database/data/004_property-assignments/Top_pointed.sql @@ -90,6 +90,12 @@ VALUES 'We continue the proof for $\mathbf{Set}_*$ by showing that the natural bijective map
$\alpha : X \vee \lim_i Y_i \to \lim_i (X \vee Y_i)$
is open. It suffices to consider open sets of two types: (1) If $U \subseteq X$ is open, the $\alpha$-image of $U \vee \lim_i Y_i$ is $p_{i_0}^{-1}(U \vee Y_{i_0})$ for any chosen index $i_0$, hence open. (2) If $i$ is an index and $V_i \subseteq Y_i$ is open, then the $\alpha$-image of $X \vee (p_i^{-1}(V_i) \cap \lim_i Y_i)$ is $p_i^{-1}(X \vee V_i)$, hence open.' ), +( + 'Top*', + 'filtered-colimit-stable monomorphisms', + TRUE, + 'This follows from this lemma applied to the forgetful functor to $\mathbf{Set}$.' +), ( 'Top*', 'coregular', From 1bffab6ac392955676ab7b407ee4ff4c58046b32 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 20 Apr 2026 10:39:40 +0200 Subject: [PATCH 6/8] decide cofiltered-limit-stable epis for various categories --- database/data/004_property-assignments/Alg(R).sql | 8 +++++++- database/data/004_property-assignments/BOn.sql | 6 ++++++ database/data/004_property-assignments/Ban.sql | 6 ++++++ database/data/004_property-assignments/CAlg(R).sql | 8 +++++++- database/data/004_property-assignments/CRing.sql | 6 ++++++ database/data/004_property-assignments/Cat.sql | 8 +++++++- database/data/004_property-assignments/FI.sql | 6 ++++++ database/data/004_property-assignments/Fld.sql | 8 ++++++++ database/data/004_property-assignments/Grp.sql | 6 ++++++ database/data/004_property-assignments/Haus.sql | 6 ++++++ database/data/004_property-assignments/M-Set.sql | 6 ++++++ database/data/004_property-assignments/Meas.sql | 6 ++++++ database/data/004_property-assignments/Met_oo.sql | 6 ++++++ database/data/004_property-assignments/Mon.sql | 6 ++++++ database/data/004_property-assignments/Pos.sql | 6 ++++++ database/data/004_property-assignments/Prost.sql | 6 ++++++ database/data/004_property-assignments/Ring.sql | 6 ++++++ database/data/004_property-assignments/Rng.sql | 6 ++++++ database/data/004_property-assignments/Set.sql | 6 ++++++ database/data/004_property-assignments/Set_pointed.sql | 6 ++++++ database/data/004_property-assignments/SetxSet.sql | 6 ++++++ database/data/004_property-assignments/Sh(X).sql | 8 +++++++- database/data/004_property-assignments/Top.sql | 6 ++++++ database/data/004_property-assignments/Top_pointed.sql | 6 ++++++ database/data/004_property-assignments/Z.sql | 6 ++++++ database/data/004_property-assignments/sSet.sql | 8 +++++++- database/data/004_property-assignments/walking_fork.sql | 6 ++++++ 27 files changed, 169 insertions(+), 5 deletions(-) diff --git a/database/data/004_property-assignments/Alg(R).sql b/database/data/004_property-assignments/Alg(R).sql index 6b665d36..7219cf2e 100644 --- a/database/data/004_property-assignments/Alg(R).sql +++ b/database/data/004_property-assignments/Alg(R).sql @@ -90,4 +90,10 @@ VALUES '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 limit 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 +), +( + 'Alg(R)', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'We already know that $\mathbf{CAlg}(R)$ does not have this property. Now apply the contrapositive of the dual of this lemma to the forgetful functor $\mathbf{CAlg}(R) \to \mathbf{Alg}(R)$. It preserves epimorphisms by MSE/5133488.' +); diff --git a/database/data/004_property-assignments/BOn.sql b/database/data/004_property-assignments/BOn.sql index 7f87f956..b9ac414f 100644 --- a/database/data/004_property-assignments/BOn.sql +++ b/database/data/004_property-assignments/BOn.sql @@ -124,4 +124,10 @@ VALUES 'one-way', FALSE, 'This is trivial.' +), +( + 'BOn', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'The epimorphisms are the finite ordinals (see below), but the limit of the sequential diagram $\cdots \xrightarrow{1} * \xrightarrow{1} *$ is the ordinal $\omega$ by MSE/5129138.' ); \ No newline at end of file diff --git a/database/data/004_property-assignments/Ban.sql b/database/data/004_property-assignments/Ban.sql index e81288df..38864102 100644 --- a/database/data/004_property-assignments/Ban.sql +++ b/database/data/004_property-assignments/Ban.sql @@ -88,4 +88,10 @@ VALUES 'CSP', FALSE, 'By using the concrete description of products and coproducts, for the constant family $X_n = \mathbb{C}$ the canonical morphism $\coprod_n X_n \to \prod_n X_n$ becomes the canonical inclusion map $\ell^1 \hookrightarrow \ell^\infty$. This is not an epimorphism (i.e., has no dense image) since the closure of the image is precisely $c_0$. So for example, $(1,1,\dotsc)$ is not contained in the closure of the image.' +), +( + 'Ban', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'We show that epimorphisms are not stable under sequential limits. Let $X_n = Y_n = \mathbb{C}$ for all $n \geq 0$. The transition morphism $Y_{n+1} \to Y_n$ is the identity, and the transition morphism $X_{n+1} \to X_n$ is $x \mapsto x/2$. The morphisms $X_n \to Y_n$, $x \mapsto x/2^n$ are compatible with the transitions, and they are surjective, hence epimorphisms. Now we check $\lim_n X_n = 0$: An element $(x_n) \in \lim_n X_n$ is a family of complex numbers satisfying $x_n = x_{n+1}/2$ and $\sup_n |x_n| < \infty$. But then $x_n = 2^n x_0$ and this can only be bounded when $x_0=0$. Hence, $0 = \lim_n X_n \to \lim_n Y_n = \mathbb{C}$ is no epimorphism.' ); \ No newline at end of file diff --git a/database/data/004_property-assignments/CAlg(R).sql b/database/data/004_property-assignments/CAlg(R).sql index 2b723450..2841638f 100644 --- a/database/data/004_property-assignments/CAlg(R).sql +++ b/database/data/004_property-assignments/CAlg(R).sql @@ -82,4 +82,10 @@ VALUES 'regular quotient object classifier', FALSE, 'The strategy is similar to the one for $\mathbf{CRing}$: Assume that $P \to R$ is a regular quotient object classifier. If $J$ denotes the kernel of $P \to R$, every ideal $I \subseteq A$ of any commutative $R$-algebra has the form $I = \langle \varphi(J) \rangle$ for a unique homomorphism $\varphi : P \to A$. If $\sigma : A \to A$ is an automorphism with $\sigma(I)=I$, then uniqueness gives us $\sigma \circ \varphi = \varphi$, which means that $\varphi(J)$ lies in $A^{\sigma}$, the fixed algebra of $\sigma$. But then $I$ is generated by elements in $A^{\sigma} \cap I$. If $K$ is a residue field of $R$, this fails for $A = K[X,Y]$, $I = \langle X,Y \rangle$, $\sigma(X)=Y$, $\sigma(Y)=X$. The fixed algebra is the subalgebra of symmetric polynomials, which is $K[X+Y,XY]$. So $\langle X,Y \rangle$ is generated by symmetric polynomials without constant term, which implies $\langle X,Y \rangle \subseteq \langle X+Y,XY \rangle$ in $K[X,Y]$. But reducing an equation like $X = a(X,Y) \cdot (X+Y) + b(X,Y) \cdot (XY)$ modulo $\langle X^2,Y^2,XY \rangle$ yields a contradiction.' -); +), +( + 'CAlg(R)', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'Let $K$ be a field over $R$. Consider the sequence of projections $\cdots \to K[X]/\langle X^2 \rangle \to K[X]/\langle X \rangle$ and the constant sequence $\cdots \to K[X] \to K[X]$. The surjective homomorphisms $K[X] \to K[X]/\langle X^n \rangle$ induce the inclusion $K[X] \hookrightarrow K[[X]]$ in the limit, where $K[[X]]$ is the algebra of formal power series. It is clearly not surjective, but this is not sufficient, we need to argue that it is not an epimorphism in $\mathbf{CAlg}(R)$, or equivalently, in $\mathbf{CRing}$. For a proof, see MSE/2391187.' +); \ No newline at end of file diff --git a/database/data/004_property-assignments/CRing.sql b/database/data/004_property-assignments/CRing.sql index 8511ccee..c7957c66 100644 --- a/database/data/004_property-assignments/CRing.sql +++ b/database/data/004_property-assignments/CRing.sql @@ -82,4 +82,10 @@ VALUES 'regular quotient object classifier', FALSE, 'Assume that $P \to \mathbb{Z}$ is a regular quotient object classifier. If $J$ denotes its kernel, this means that every ideal $I \subseteq A$ of any commutative ring has the form $I = \langle \varphi(J) \rangle$ for a unique homomorphism $\varphi : P \to A$. If $\sigma : A \to A$ is an automorphism with $\sigma(I)=I$, then uniqueness gives us $\sigma \circ \varphi = \varphi$, which means that $\varphi(J)$ lies in $A^{\sigma}$, the fixed ring of $\sigma$. But then $I$ is generated by elements in the fixed ring. This fails for $A = \mathbb{Z}[X]$, $I = \langle X \rangle$, $\sigma(X)=-X$. The fixed ring is $\mathbb{Z}[X^2]$, and if $I$ was generated by elements $f \in \mathbb{Z}[X^2] \cap I$, they would be multiples of $X^2$, but $X$ is not a multiple of $X^2$.' +), +( + 'CRing', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'For a prime $p$ consider the sequence of projections $\cdots \to \mathbb{Z}/p^2 \to \mathbb{Z}/p$ and the constant sequence $\cdots \to \mathbb{Z} \to \mathbb{Z}$. The surjective homomorphisms $\mathbb{Z} \to \mathbb{Z}/p^n$ induce the homomorphism $\mathbb{Z} \to \mathbb{Z}_p$ in the limit, where $\mathbb{Z}_p$ is the ring of $p$-adic integers. It is not surjective since $\mathbb{Z}_p$ is uncountable, but this is not sufficient (at least, for this category): We need to use SP/04W0 to conclude that it is no epimorphism in $\mathbf{CRing}$.' ); diff --git a/database/data/004_property-assignments/Cat.sql b/database/data/004_property-assignments/Cat.sql index b68cd9cb..ac79e20f 100644 --- a/database/data/004_property-assignments/Cat.sql +++ b/database/data/004_property-assignments/Cat.sql @@ -82,4 +82,10 @@ VALUES 'coregular', FALSE, 'We already know that the category of monoids is not coregular, in fact there is a regular monomorphism $M \to N$ of monoids and a morphism $M \to K$ such that $K \to K \sqcup_M N$ is not a monomorphism. The delooping functor $B : \mathbf{Mon} \to \mathbf{Cat}$ has a left adjoint (MSE/574745), hence it preserves regular monomorphisms. It also preserves pushouts (MSE/5130854), and it reflects monomorphisms since it is faithful. Therefore, $B(M) \to B(N)$ provides the desired counterexample of a non-stable regular monomorphism of categories.' -); +), +( + 'Cat', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'We already know that $\mathbf{Set}$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\mathbf{Set} \to \mathbf{Cat}$ that maps a set to its discrete category.' +); \ No newline at end of file diff --git a/database/data/004_property-assignments/FI.sql b/database/data/004_property-assignments/FI.sql index f79eae38..42a539ea 100644 --- a/database/data/004_property-assignments/FI.sql +++ b/database/data/004_property-assignments/FI.sql @@ -71,6 +71,12 @@ VALUES TRUE, 'IF $X$ is a finite set, the slice category $\mathbf{FI} / X$ is equivalent to the poset of subsets of $X$. This is cartesian closed because $A \cap B \subseteq C$ holds if and only if $B \subseteq (X \setminus A) \cup C$, where $A,B,C \subseteq X$.' ), +( + 'FI', + 'cofiltered-limit-stable epimorphisms', + TRUE, + 'This is because every epimorphism is an isomorphism in this category (see below), and isomorphisms are always stable under any type of limit.' +), ( 'FI', 'small', diff --git a/database/data/004_property-assignments/Fld.sql b/database/data/004_property-assignments/Fld.sql index 4337fce6..64dfe834 100644 --- a/database/data/004_property-assignments/Fld.sql +++ b/database/data/004_property-assignments/Fld.sql @@ -94,4 +94,12 @@ VALUES 'multi-terminal object', FALSE, 'Every field has a non-trivial extension, for instance, the rational function field over itself in one variable. Hence, a multi-terminal object never exists.' +), +( + 'Fld', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'Inside of $\mathbb{F}_p(X)$ consider the descending sequence of subfields +

$\mathbb{F}_p(X) \supseteq \mathbb{F}_p(X^p) \supseteq \mathbb{F}_p(X^{p^2}) \supseteq \cdots,$

+ whose intersection is $\mathbb{F}_p$. Each $\mathbb{F}_p(X^{p^n}) \hookrightarrow \mathbb{F}_p(X)$ is purely inseparable, hence an epimorphism, but in the limit we get $\mathbb{F}_p \hookrightarrow \mathbb{F}_p(X)$, which is not even algebraic.' ); diff --git a/database/data/004_property-assignments/Grp.sql b/database/data/004_property-assignments/Grp.sql index 66d4ae36..94bfd848 100644 --- a/database/data/004_property-assignments/Grp.sql +++ b/database/data/004_property-assignments/Grp.sql @@ -104,4 +104,10 @@ VALUES 'CSP', FALSE, 'The canonical homomorphism $\coprod_{n \geq 0} \mathbb{Z} \to \prod_{n \geq 0} \mathbb{Z}$ is not surjective because its domain is countable and its codomain is uncountable. Hence it is no epimorphism.' +), +( + 'Grp', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'We already know that $\mathbf{Ab}$ does not have this property. Now apply the contrapositive of the dual of this lemma to the forgetful functor $\mathbf{Ab} \to \mathbf{Grp}$ which indeed preserves epimorphisms.' ); \ No newline at end of file diff --git a/database/data/004_property-assignments/Haus.sql b/database/data/004_property-assignments/Haus.sql index b231082b..94ca69b9 100644 --- a/database/data/004_property-assignments/Haus.sql +++ b/database/data/004_property-assignments/Haus.sql @@ -100,4 +100,10 @@ VALUES 'regular subobject classifier', FALSE, 'Assume that there is a regular subobject classifier $\Omega$. By the classification of regular monomorphisms, we would have an isomorphism between $\mathrm{Hom}(X,\Omega)$ and the set of closed subsets of $X$ for any Hausdorff space $X$. If we take $X = 1$ we see that $\Omega$ has two points. Since $\Omega$ is Hausdorff, $\Omega \cong 1 + 1$ must be discrete. But then $\mathrm{Hom}(X,\Omega)$ is isomorphic to the set of all clopen subsets of $X$, of which there are usually far fewer than closed subsets (consider $X = [0,1]$).' +), +( + 'Haus', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'Our counterexample for $\mathbf{Set}$ (using infinite intersections) also works in $\mathbf{Haus}$ by using discrete topologies. We could also apply a variant of (the dual of) this lemma to the discrete topology functor $\mathbf{Set} \to \mathbf{Haus}$, which does not preserve all cofiltered limits, but does preserve intersections.' ); diff --git a/database/data/004_property-assignments/M-Set.sql b/database/data/004_property-assignments/M-Set.sql index 685f8ca3..812c3567 100644 --- a/database/data/004_property-assignments/M-Set.sql +++ b/database/data/004_property-assignments/M-Set.sql @@ -34,4 +34,10 @@ VALUES 'Malcev', FALSE, 'Endow the set $\mathbb{N}$ with the trivial $M$-action, and consider the subset $\{(a,b) : a \leq b \}$ of $\mathbb{N}^2$.' +), +( + 'M-Set', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'We know that $\mathbf{Set}$ does not have this property. Now use the contrapositive of the dual of this lemma applied to the functor $\mathbf{Set} \to M{-}\mathbf{Set}$ that equips a set with the trivial $M$-action.' ); diff --git a/database/data/004_property-assignments/Meas.sql b/database/data/004_property-assignments/Meas.sql index 106152a4..37c9e8f9 100644 --- a/database/data/004_property-assignments/Meas.sql +++ b/database/data/004_property-assignments/Meas.sql @@ -94,4 +94,10 @@ VALUES 'Malcev', FALSE, 'Use that $\mathbf{Set}$ is not Malcev and endow sets with the trivial $\sigma$-algebra.' +), +( + 'Meas', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'We already know that $\mathbf{Set}$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\mathbf{Set} \to \mathbf{Meas}$ which equips a set with the trivial $\sigma$-algebra.' ); diff --git a/database/data/004_property-assignments/Met_oo.sql b/database/data/004_property-assignments/Met_oo.sql index 2ad63fb9..6b21f618 100644 --- a/database/data/004_property-assignments/Met_oo.sql +++ b/database/data/004_property-assignments/Met_oo.sql @@ -82,4 +82,10 @@ VALUES 'co-Malcev', FALSE, 'See MO/509552: Consider the forgetful functor $U : \mathbf{Met}_{\infty} \to \mathbf{Set}$ and the relation $R \subseteq U^2$ defined by $R(X) := \{(a,b) \in U(X)^2 : d(x,y) \leq 1 \}$. Both are representable: $U$ by the singleton metric space and $R$ by the metric space $\{ 0,1 \}$ where $d(0,1) := 1$. It is clear that $R$ is reflexive, but not transitive.' +), +( + 'Met_oo', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'We already know that $\mathbf{Set}$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\mathbf{Set} \to \mathbf{Met}_{\infty}$ that equips a set with the discrete topology.' ); diff --git a/database/data/004_property-assignments/Mon.sql b/database/data/004_property-assignments/Mon.sql index 1c48bf6e..037698ab 100644 --- a/database/data/004_property-assignments/Mon.sql +++ b/database/data/004_property-assignments/Mon.sql @@ -83,6 +83,12 @@ VALUES FALSE, 'We can just copy the proof for the category of commutative monoids. Alternatively, we may use this lemma (dualized).' ), +( + 'Mon', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'We already know that $\mathbf{Grp}$ does not have this property. Now apply the contrapositive of the dual of this lemma to the forgetful functor $\mathbf{Grp} \to \mathbf{Mon}$. It preserves epimorphisms since it has a right adjoint, the unit group functor.' +), ( 'Mon', 'cocartesian cofiltered limits', diff --git a/database/data/004_property-assignments/Pos.sql b/database/data/004_property-assignments/Pos.sql index 63a407ea..566b2ab8 100644 --- a/database/data/004_property-assignments/Pos.sql +++ b/database/data/004_property-assignments/Pos.sql @@ -88,4 +88,10 @@ VALUES 'regular subobject classifier', FALSE, 'Assume that there is a regular subobject classifier $\Omega$, so that (by the classification of regular monomorphisms) $\mathrm{Hom}(P,\Omega)$ is isomorphic to the set of subsets of $P$. By taking $P = \{0\}$ we see that $\Omega$ has $2$ elements, so that either $\Omega \cong \{0,1\}$ (discrete) or $\Omega \cong \{0 < 1\}$. By taking $P = \{0 < 1\}$ we see that $\Omega$ has four pairs $(x,y)$ with $x \leq y$. But $\{0,1\}$ has only two and $\{0 < 1\}$ has only three such pairs.' +), +( + 'Pos', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'Pick any poset $X$ which has a decreasing sequence of non-empty sets $X = X_0 \supseteq X_1 \supseteq \cdots$ with empty intersection, such as $X_n = \mathbb{N}_{\geq n}$ with the natural ordering. The unique map $X_n \to 1$ is surjective, but their limit $\varnothing \to 1$ is not surjective.' ); diff --git a/database/data/004_property-assignments/Prost.sql b/database/data/004_property-assignments/Prost.sql index 3b0a67b5..4a2d9a52 100644 --- a/database/data/004_property-assignments/Prost.sql +++ b/database/data/004_property-assignments/Prost.sql @@ -94,4 +94,10 @@ VALUES 'co-Malcev', FALSE, 'See MO/509552: Consider the forgetful functor $U : \mathbf{Prost} \to \mathbf{Set}$ and the relation $R \subseteq U^2$ defined by $R(A) := \{(a,b) \in U(A)^2 : a \leq b\}$. Both are representable: $U$ by the singleton preordered set and $R$ by $\{0 \leq 1 \}$. It is clear that $R$ is reflexive, but not symmetric.' +), +( + 'Prost', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'We know that $\mathbf{Set}$ does not have this property. Now use the contrapositive of the dual of this lemma applied to the functor $\mathbf{Set} \to \mathbf{Prost}$ that equips a set with the chaotic preorder.' ); diff --git a/database/data/004_property-assignments/Ring.sql b/database/data/004_property-assignments/Ring.sql index e17d1ee5..a33f9ec5 100644 --- a/database/data/004_property-assignments/Ring.sql +++ b/database/data/004_property-assignments/Ring.sql @@ -90,4 +90,10 @@ VALUES '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 limit 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.' +), +( + 'Ring', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'We know that $\mathbf{CRing}$ does not have this property. Now use the contrapositive of the dual of this lemma applied to the forgetful functor $\mathbf{CRing} \to \mathbf{Ring}$. It preserves epimorphisms by MSE/5133488.' ); \ No newline at end of file diff --git a/database/data/004_property-assignments/Rng.sql b/database/data/004_property-assignments/Rng.sql index 1d8b47d1..6b7f9b27 100644 --- a/database/data/004_property-assignments/Rng.sql +++ b/database/data/004_property-assignments/Rng.sql @@ -90,4 +90,10 @@ VALUES 'CSP', FALSE, 'Assume that $\coprod_n \mathbb{Z} \to \prod_n \mathbb{Z}$ is an epimorphism in $\mathbf{Rng}$. Then $((\coprod_n \mathbb{Z})^+)^{\mathrm{ab}} \to \prod_n \mathbb{Z}$ would be an epimorphism in $\mathbf{CRing}$, where $(-)^+$ denotes the unitalization and $(-)^{\mathrm{ab}}$ the abelianization. But if $R \to S$ is an epimorphism of commutative rings, then $\mathrm{card}(S) \leq \mathrm{card}(R)$ by SP/04W0. Since $((\coprod_n \mathbb{Z})^+)^{\mathrm{ab}}$ is countable and $\prod_n \mathbb{Z}$ is not, we get a contradiction.' +), +( + 'Rng', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'We know that $\mathbf{Ring}$ does not have this property. Now use the contrapositive of the dual of this lemma applied to the forgetful functor $\mathbf{Ring} \to \mathbf{Rng}$. We only need to verify that it preserves epimorphisms: Let $f : R \to S$ be an epimorphism in $\mathbf{Ring}$ and let $g,h : S \rightrightarrows T$ be two homomorphisms of rngs with $gf = hf$. The element $e = g(1) = h(1) \in T$ is idempotent, and $g,h$ become homomorphisms of rings $S \rightrightarrows eTe$. Hence, $g=h$.' ); diff --git a/database/data/004_property-assignments/Set.sql b/database/data/004_property-assignments/Set.sql index 8e266208..b587ee04 100644 --- a/database/data/004_property-assignments/Set.sql +++ b/database/data/004_property-assignments/Set.sql @@ -40,4 +40,10 @@ VALUES 'Malcev', FALSE, 'There are lots of non-symmetric reflexive relations, for example $\leq$ on $\mathbb{N}$.' +), +( + 'Set', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'Pick any decreasing sequence of non-empty sets $X_0 \supseteq X_1 \supseteq \cdots$ with empty intersection, such as $X_n = \mathbb{N}_{\geq n}$. The unique map $X_n \to 1$ is surjective, but their limit $\varnothing \to 1$ is not surjective.' ); diff --git a/database/data/004_property-assignments/Set_pointed.sql b/database/data/004_property-assignments/Set_pointed.sql index 43a3aa49..15bec3c1 100644 --- a/database/data/004_property-assignments/Set_pointed.sql +++ b/database/data/004_property-assignments/Set_pointed.sql @@ -90,4 +90,10 @@ VALUES 'conormal', FALSE, 'Every cokernel is "injective away from the base point". Formally, if $p : A \to B$ is a cokernel in $\mathbf{Set}_*$, it has the property that $p(x)=p(y) \neq 0$ implies $x=y$ (where $0$ denotes the base point). Clearly this is not satisfied for every surjective pointed map, consider $(\mathbb{N},0) \to (\{0,1\},0)$ defined by $0 \mapsto 0$ and $x \mapsto 1$ for $x > 0$.' +), +( + 'Set*', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'We already know that $\mathbf{Set}$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\mathbf{Set} \to \mathbf{Set}_*$ that freely adds a base point.' ); diff --git a/database/data/004_property-assignments/SetxSet.sql b/database/data/004_property-assignments/SetxSet.sql index d5c9beac..78eb6657 100644 --- a/database/data/004_property-assignments/SetxSet.sql +++ b/database/data/004_property-assignments/SetxSet.sql @@ -46,4 +46,10 @@ VALUES 'generator', FALSE, 'Assume that $(A,B)$ is a generator. Of course, $A$ and $B$ cannot be both empty. Assume w.l.o.g. that $A$ is non-empty. Then there is no morphism $(A,B) \to (0,1)$, but there are two different morphisms $(0,1) \rightrightarrows (0,2)$.' +), +( + 'SetxSet', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'We already know that $\mathbf{Set}$ does not have this property. Now apply the contrapositive of the dual of this lemma to the diagonal functor $\mathbf{Set} \to \mathbf{Set} \times \mathbf{Set}$.' ); diff --git a/database/data/004_property-assignments/Sh(X).sql b/database/data/004_property-assignments/Sh(X).sql index 0fde35bb..77c03248 100644 --- a/database/data/004_property-assignments/Sh(X).sql +++ b/database/data/004_property-assignments/Sh(X).sql @@ -28,4 +28,10 @@ VALUES 'skeletal', FALSE, 'Consider constant sheaves for isomorphic but non-equal sets.' -); +), +( + 'Sh(X)', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'Our counterexample for $\mathbf{Set}$ (using infinite intersections) also works in $\mathbf{Sh}(X)$ by using constant sheaves. We could also apply a variant of (the dual of) this lemma to the constant sheaf functor $\mathbf{Set} \to \mathbf{Sh}(X)$, which does not preserve all cofiltered limits, but does preserve intersections.' +); \ No newline at end of file diff --git a/database/data/004_property-assignments/Top.sql b/database/data/004_property-assignments/Top.sql index dea6e8f5..dcd4464d 100644 --- a/database/data/004_property-assignments/Top.sql +++ b/database/data/004_property-assignments/Top.sql @@ -124,4 +124,10 @@ VALUES 'coaccessible', FALSE, 'Assume $\mathbf{Top}$ is coaccessible. Let $p\colon S \to I$ be the identity map from the Sierpinski space to the two-element indiscrete space. Then, a topological space is discrete if and only if it is projective to the morphism $p$. This implies that the full subcategory spanned by all discrete spaces, which is equivalent to $\mathbf{Set}$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\mathbf{Set}$ is not coaccessible, this is a contradiction.' +), +( + 'Top', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'We already know that $\mathbf{Set}$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\mathbf{Set} \to \mathbf{Top}$ which equips a set with the indiscrete topology.' ); diff --git a/database/data/004_property-assignments/Top_pointed.sql b/database/data/004_property-assignments/Top_pointed.sql index 569a7a5b..644cfa6b 100644 --- a/database/data/004_property-assignments/Top_pointed.sql +++ b/database/data/004_property-assignments/Top_pointed.sql @@ -161,6 +161,12 @@ VALUES 'CSP', -- TODO: remove duplication with unital proof FALSE, 'The image of $X \vee Y$ in $X \times Y$ is just $\{(x,0) : x \in X\} \cup \{(0,y) : y \in Y\}$ (where $0$ denotes the base point), which is clearly a proper subset when both $X,Y$ are non-trivial.' +), +( + 'Top*', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'We already know that $\mathbf{Set}_*$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\mathbf{Set}_* \to \mathbf{Top}_*$ that equips a pointed set with the indiscrete topology.' ); diff --git a/database/data/004_property-assignments/Z.sql b/database/data/004_property-assignments/Z.sql index cd9a98b4..dedd72fb 100644 --- a/database/data/004_property-assignments/Z.sql +++ b/database/data/004_property-assignments/Z.sql @@ -94,4 +94,10 @@ VALUES 'well-powered', FALSE, 'Consider the functor $F$ from MO/390611 for example. The collection of subobjects of $F$ is not isomorphic to a set: for each infinite cardinal $\kappa$, simply cut off the construction of $F$ at $\kappa$. This yields a different subobject for each $\kappa$.' +), +( + 'Z', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'We already know that $\mathbf{Set}$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\mathbf{Set} \to [\mathbf{CRing}, \mathbf{Set}]$ that maps a set to its constant functor.' ); \ No newline at end of file diff --git a/database/data/004_property-assignments/sSet.sql b/database/data/004_property-assignments/sSet.sql index 4dabcd11..d0826b0d 100644 --- a/database/data/004_property-assignments/sSet.sql +++ b/database/data/004_property-assignments/sSet.sql @@ -52,4 +52,10 @@ VALUES 'finitary algebraic', FALSE, 'A one-sorted finitary algebraic category has an object $F$ (the free algebra on one generator) such that $F$ is finitely presentable and every object $X$ admits an epimorphism $\coprod_{s \in S} F \to X$ for some index set $S$. Assume that such a simplicial set $F$ exists. By using the sequence of $n$-skeletons of $F$, we see that there is some $n$ such that every $n$-simplex in $F$ is degenerate. Now take $X = \Delta^n$, which has a non-degenerate $n$-simplex. Then there cannot be an epimorphism $\coprod_{s \in S} F \to X$.' -); +), +( + 'sSet', + 'cofiltered-limit-stable epimorphisms', + FALSE, + 'We show that epimorphisms are not stable under sequential limits, intersections to be precise. Let $X_n \in \mathbf{sSet}$ be the nerve of the poset $\mathbb{N}_{\geq n}$. This means that a $k$-simplex in $X_n$ is a chain of natural numbers $n \leq x_0 \leq \cdots \leq x_k$. Then $X_{n+1} \subseteq X_n$ and $\lim_n X_n = \bigcap_n X_n = 0$ (the initial simplicial set). Each $X_n \to 1$ is an epimorphism, but $\lim_n X_n \to 1$ is not.' +); \ No newline at end of file diff --git a/database/data/004_property-assignments/walking_fork.sql b/database/data/004_property-assignments/walking_fork.sql index 9cb538b1..89ccd76e 100644 --- a/database/data/004_property-assignments/walking_fork.sql +++ b/database/data/004_property-assignments/walking_fork.sql @@ -71,6 +71,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'walking_fork', + 'cofiltered-limit-stable epimorphisms', + TRUE, + 'Let $(X_p)$ and $(Y_p)$ be diagrams in the walking fork indexed by a cofiltered poset $P$. Let $(X_p \to Y_p)_{p \in P}$ be compatible epimorphisms, we need to show that $\lim_p X_p \to \lim_p Y_p$ is an epimorphism as well. Assume it is not. The only non-epimorphism is $i : 0 \to 1$. Hence, $\lim_p X_p = 0$ and $\lim_p Y_p = 1$. So for every $p$ there is a morphism $1 \to Y_p$, meaning $Y_p \in \{1,2\}$. If $Y_p = 2$ for all $p$, the transition morphisms between them must be identities, so that $\lim_p Y_p = 2$, a contradiction. Choose $p$ with $Y_p = 1$. Then for all $q \leq p$ the morphism $Y_q \to Y_p$ shows that $Y_q = 1$ as well. Since $X_q \to Y_q = 1$ is an epimorphism by assumption, it cannot be $i : 0 \to 1$, and we see that $X_q = 1$. Then the transitions between the $X_q$ are identities, and we get the contradiction $\lim_p X_p = \lim_q X_q = 1$.' +), ( 'walking_fork', 'terminal object', From 920abfaa64ee8c4ae0a1c55a49dd29fae968ddf0 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 20 Apr 2026 10:40:22 +0200 Subject: [PATCH 7/8] adjust test files --- scripts/expected-data/Ab.json | 7 ++++++- scripts/expected-data/Set.json | 7 ++++++- scripts/expected-data/Top.json | 7 ++++++- 3 files changed, 18 insertions(+), 3 deletions(-) diff --git a/scripts/expected-data/Ab.json b/scripts/expected-data/Ab.json index 97ebd8eb..d43b9fb3 100644 --- a/scripts/expected-data/Ab.json +++ b/scripts/expected-data/Ab.json @@ -100,6 +100,8 @@ "multi-initial object": true, "cartesian filtered colimits": true, "cocartesian cofiltered limits": true, + "CIP": true, + "filtered-colimit-stable monomorphisms": true, "cartesian closed": false, "locally cartesian closed": false, @@ -144,5 +146,8 @@ "essentially countable": false, "natural numbers object": false, "countably distributive": false, - "countably codistributive": false + "countably codistributive": false, + "CSP": false, + "cofiltered-limit-stable epimorphisms": false, + "exact cofiltered limits": false } diff --git a/scripts/expected-data/Set.json b/scripts/expected-data/Set.json index 00206fe0..6270d127 100644 --- a/scripts/expected-data/Set.json +++ b/scripts/expected-data/Set.json @@ -96,6 +96,7 @@ "cocartesian cofiltered limits": true, "natural numbers object": true, "countably distributive": true, + "filtered-colimit-stable monomorphisms": true, "Grothendieck abelian": false, "Malcev": false, @@ -144,5 +145,9 @@ "coaccessible": false, "countable": false, "essentially countable": false, - "countably codistributive": false + "countably codistributive": false, + "CIP": false, + "CSP": false, + "cofiltered-limit-stable epimorphisms": false, + "exact cofiltered limits": false } diff --git a/scripts/expected-data/Top.json b/scripts/expected-data/Top.json index 0e6ea903..24260193 100644 --- a/scripts/expected-data/Top.json +++ b/scripts/expected-data/Top.json @@ -71,6 +71,7 @@ "cocartesian cofiltered limits": true, "countably distributive": true, "natural numbers object": true, + "filtered-colimit-stable monomorphisms": true, "abelian": false, "additive": false, @@ -144,5 +145,9 @@ "countable": false, "essentially countable": false, "cartesian filtered colimits": false, - "countably codistributive": false + "countably codistributive": false, + "CIP": false, + "CSP": false, + "cofiltered-limit-stable epimorphisms": false, + "exact cofiltered limits": false } From 2969d2874d9364fbdffc3c8fa3b2e84fddb93b9b Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 20 Apr 2026 12:26:08 +0200 Subject: [PATCH 8/8] expand dictionary --- .vscode/settings.json | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.vscode/settings.json b/.vscode/settings.json index a7fa599a..352178c0 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -25,6 +25,7 @@ "abelianization", "abelianize", "Adamek", + "adic", "algébriques", "anneaux", "Artin", @@ -199,12 +200,14 @@ "summands", "suprema", "supremum", + "surject", "surjection", "surjections", "surjective", "tensoring", "Turso", "unital", + "unitalization", "vercel", "Vite", "Wedderburn",