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/001_categories/100_related-categories.sql b/database/data/001_categories/100_related-categories.sql index 19d5395e..b5370f9f 100644 --- a/database/data/001_categories/100_related-categories.sql +++ b/database/data/001_categories/100_related-categories.sql @@ -11,6 +11,7 @@ VALUES ('Alg(R)', 'CAlg(R)'), ('Alg(R)', 'R-Mod'), ('Alg(R)', 'Ring'), +('Ban','Met'), ('B', 'FI'), ('B', 'FS'), ('BG', 'BG_f'), @@ -58,6 +59,7 @@ VALUES ('Meas', 'Top'), ('Met', 'Met_c'), ('Met', 'Met_oo'), +('Met', 'Ban'), ('Met_c', 'Met'), ('Met_c', 'Met_oo'), ('Met_c', 'Top'), diff --git a/database/data/003_properties/003_limits-colimits-behavior.sql b/database/data/003_properties/003_limits-colimits-behavior.sql index 1780db7d..48aee05f 100644 --- a/database/data/003_properties/003_limits-colimits-behavior.sql +++ b/database/data/003_properties/003_limits-colimits-behavior.sql @@ -82,6 +82,24 @@ VALUES NULL, TRUE ), +( + 'cartesian filtered colimits', + 'has', + 'In a category $\mathcal{C}$, which we assume to have filtered colimits and finite products, we say that 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 +), ( '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..a9d28f8e 100644 --- a/database/data/003_properties/100_related-properties.sql +++ b/database/data/003_properties/100_related-properties.sql @@ -151,6 +151,12 @@ VALUES ('codistributive', 'finite coproducts'), ('exact filtered colimits', 'filtered colimits'), ('exact filtered colimits', 'finitely complete'), +('exact filtered colimits', 'cartesian filtered colimits'), +('cartesian filtered colimits', 'filtered colimits'), +('cartesian filtered colimits', 'finite products'), +('cartesian filtered colimits', 'exact filtered colimits'), +('cocartesian cofiltered limits', 'cofiltered limits'), +('cocartesian cofiltered limits', 'finite coproducts'), ('generator', 'generating set'), ('generating set', 'generator'), ('Grothendieck abelian', 'abelian'), diff --git a/database/data/004_property-assignments/Alg(R).sql b/database/data/004_property-assignments/Alg(R).sql index 761ddafb..6b665d36 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 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 diff --git a/database/data/004_property-assignments/Ban.sql b/database/data/004_property-assignments/Ban.sql index f7f6f9fd..3ae433bc 100644 --- a/database/data/004_property-assignments/Ban.sql +++ b/database/data/004_property-assignments/Ban.sql @@ -23,6 +23,18 @@ VALUES TRUE, 'Example 1.48 in Adamek-Rosicky.' ), +( + 'Ban', + 'cartesian filtered colimits', + TRUE, + 'If $X$ is a Banach space and $(Y_i)$ is a filtered diagram of Banach spaces, the canonical map $\mathrm{colim}_i (X \times Y_i) \to X \times \mathrm{colim}_i Y_i$ is the completion of the canonical map in the category of normed vector spaces with non-expansive linear maps. Now the claim follows directly from the category of metric spaces with non-expansive maps.' +), +( + 'Ban', + 'cocartesian cofiltered limits', + 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', 'cogenerator', 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/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/Met.sql b/database/data/004_property-assignments/Met.sql index 16d5d589..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', @@ -117,7 +123,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..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', @@ -57,7 +63,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', 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.' ); diff --git a/database/data/004_property-assignments/Ring.sql b/database/data/004_property-assignments/Ring.sql index b1a7e4c2..e17d1ee5 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 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.' ); \ 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 d5b70e54..08a6240c 100644 --- a/database/data/004_property-assignments/Rng.sql +++ b/database/data/004_property-assignments/Rng.sql @@ -70,4 +70,12 @@ VALUES 'regular quotient object classifier', FALSE, 'Assume that $\mathbf{Rng}$ has a regular quotient object classifier $P$. Consider the functor $N : \mathbf{Ab} \to \mathbf{Rng}$ that equips an abelian group with zero multiplication. It is fully faithful and has a left adjoint mapping a rng $R$ to the abelian group $R/R^2$. If $R$ is a rng with zero multiplication and $R \to S$ is a surjective homomorphism, then $S$ has zero multiplication. Therefore, the assumptions of this lemma (dualized) apply and we conclude that $P/P^2$ is a regular quotient object classifier of $\mathbf{Ab}$. But we already know that this category has no such object (in fact, the only additive categories with such an object are trivial by MSE/4086192).' +), +( + 'Rng', + '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 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 diff --git a/database/data/004_property-assignments/Set_pointed.sql b/database/data/004_property-assignments/Set_pointed.sql index efe845f3..a0719751 100644 --- a/database/data/004_property-assignments/Set_pointed.sql +++ b/database/data/004_property-assignments/Set_pointed.sql @@ -53,6 +53,14 @@ VALUES TRUE, 'Malcev categories are closed under slice categories by Prop. 2.2.14 in Malcev, protomodular, homological and semi-abelian categories. It follows that co-Malcev categories are closed under coslice categories, and $\mathbf{Set}_*$ is a coslice category of $\mathbf{Set}$, which is co-Malcev since every elementary topos is co-Malcev.' ), +( + 'Set*', + 'cocartesian cofiltered limits', + TRUE, + 'Let $X$ be a pointed set and $(Y_i)$ be a filtered diagram of pointed sets. Base points will be denoted by $0$. The canonical map $X \vee \lim_i Y_i \to \lim_i (X \vee Y_i)$ is injective since the wedge sum naturally embeds into the product and the natural map $X \vee \prod_i Y_i \to \prod_i (X \times Y_i)$ is injective. Now let $z = (z_i) \in \lim_i (X \vee Y_i)$. +
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*', 'skeletal', 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..fc5e500f 100644 --- a/database/data/004_property-assignments/Top_pointed.sql +++ b/database/data/004_property-assignments/Top_pointed.sql @@ -77,6 +77,13 @@ 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*', + 'cocartesian cofiltered limits', + TRUE, + '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*', 'coregular', @@ -103,9 +110,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/database/data/005_implications/002_limits-colimits-behavior-implications.sql b/database/data/005_implications/002_limits-colimits-behavior-implications.sql index 7e6a2414..b7f00e0f 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"]', @@ -62,6 +69,20 @@ VALUES 'This holds by definition.', FALSE ), +( + 'cartesian_filtered_colimits_condition', + '["cartesian filtered colimits"]', + '["filtered colimits", "finite products"]', + 'This holds by definition.', + FALSE +), +( + 'exact_includes_cartesian_filtered_colimits', + '["exact filtered colimits"]', + '["cartesian filtered colimits"]', + 'If filtered colimits commute with finite limits, they commute with finite products in particular.', + FALSE +), ( 'infinitary_distributive_consequence', '["infinitary distributive"]', @@ -139,6 +160,13 @@ VALUES 'This is obvious.', FALSE ), +( + 'extensive_cocartesian_cofiltered_limits', + '["extensive", "cofiltered limits", "terminal object"]', + '["cocartesian cofiltered limits"]', + 'Let $\mathcal{C}$ be an extensive category with cofiltered limits and a terminal object. Then the coproduct functor $\mathcal{C} \times \mathcal{C} \cong \mathcal{C}/1 \times \mathcal{C}/1 \to \mathcal{C}/(1+1)$ is an equivalence. The forgetful functor $\mathcal{C}/A \to \mathcal{C}$ creates connected limits, and hence preserves cofiltered limits. For every $X \in \mathcal{C}$ the functor $(X,-) : \mathcal{C} \to \mathcal{C} \times \mathcal{C}$ also preserves cofiltered limits. The composition of these functors is $X \sqcup - : \mathcal{C} \to \mathcal{C}$ and therefore also preserves cofiltered limits.', + FALSE +), ( 'distributive_consequence', '["distributive"]', @@ -162,7 +190,7 @@ VALUES ), ( 'infinite_distributive_filtered_criterion', - '["distributive", "exact filtered colimits", "coproducts"]', + '["distributive", "cartesian filtered colimits", "coproducts"]', '["infinitary distributive"]', 'Each functor $A \times -$ preserves finite coproducts and filtered colimits, hence all coproducts.', FALSE 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"]', diff --git a/scripts/expected-data/Ab.json b/scripts/expected-data/Ab.json index b387f2e5..350904ca 100644 --- a/scripts/expected-data/Ab.json +++ b/scripts/expected-data/Ab.json @@ -86,6 +86,8 @@ "cokernels": true, "normal": true, "conormal": true, + "cartesian filtered colimits": true, + "cocartesian cofiltered limits": true, "cartesian closed": false, "locally cartesian closed": false, diff --git a/scripts/expected-data/Set.json b/scripts/expected-data/Set.json index e714c158..c11a16dd 100644 --- a/scripts/expected-data/Set.json +++ b/scripts/expected-data/Set.json @@ -81,6 +81,8 @@ "cofiltered": true, "sifted": true, "cosifted": true, + "cartesian filtered colimits": true, + "cocartesian cofiltered limits": true, "Grothendieck abelian": false, "Malcev": false, diff --git a/scripts/expected-data/Top.json b/scripts/expected-data/Top.json index 0458704a..94b5cc11 100644 --- a/scripts/expected-data/Top.json +++ b/scripts/expected-data/Top.json @@ -65,6 +65,7 @@ "cofiltered": true, "sifted": true, "cosifted": true, + "cocartesian cofiltered limits": true, "abelian": false, "additive": false, @@ -124,5 +125,6 @@ "kernels": false, "cokernels": false, "normal": false, - "conormal": false + "conormal": false, + "cartesian filtered colimits": false }