Add property: ℵ₁-filtered colimits

.cspell.json

@@ -64,6 +64,7 @@
 		"coexponentials",
 		"cofiltered",
 		"cofiltering",
+		"cofinal",
 		"cofinitary",
 		"cofull",
 		"cogenerates",
@@ -125,6 +126,7 @@
 		"extremal",
 		"fieldification",
 		"finitary",
+		"foundedness",
 		"Freyd",
 		"functor",
 		"functorial",
@@ -265,5 +267,8 @@
 		".netlify",
 		"build"
 	],
-	"ignoreRegExpList": ["\\$[^$]*\\$", "\\$\\$[^$]*\\$\\$"]
+	"ignoreRegExpList": [
+		"\\$[^$]*\\$",
+		"\\$\\$[^$]*\\$\\$"
+	]
 }

databases/catdat/data/categories/BN.yaml

@@ -40,6 +40,45 @@ satisfied_properties:
   - property: locally cartesian closed
     reason: The slice category $B\IN / *$ is isomorphic to the poset $(\IN,\geq)$ (not to $(\IN,\leq)$). This category is thin and and semi-strongly connected, <a href="/category-implication/sequential_implies_lcc">hence</a> cartesian closed.
 
+  - property: ℵ₁-filtered colimits
+    reason: >-
+      Let $D : \I \to B\IN$ be an $\aleph_1$-filtered diagram. Every two parallel morphisms $i \rightrightarrows j$ are mapped to the same morphism in $B \IN$, because they are coequalized by some morphism and $(\IN,+)$ is cancellative. Hence, $D$ factors through the preorder reflection of $\I$, and we may therefore assume that $\I$ itself is a preorder. Thus, the diagram consists of numbers $D(i,j) \in \IN$ for all $i \leq j$ satisfying
+      $$D(j,k) + D(i,j) = D(i,k)$$
+      for all $i \leq j \leq k$. In particular, $D(i,j) \leq D(i,k)$.
+
+      Let $i \in \I$. The set of natural numbers $\{D(i,k) : k \geq i\}$ is bounded above. Otherwise, for every $n \in \IN$ we could find $k_n \in \I$ with $k_n \geq i$ and $D(i,k_n) \geq n$. Since $\I$ is $\aleph_1$-filtered, the family $(k_n)_{n \in \IN}$ has an upper bound $k_\infty \in \I$. But then
+      $$D(i, k_\infty) = D(k_n,k_\infty) + D(i, k_n) \geq D(i, k_n) \geq n$$
+      for all $n \in \IN$, contradicting the fact that $D(i,k_\infty) \in \IN$.
+
+      Therefore, the maximum
+      $$u_i \coloneqq \max \{D(i,k) : k \geq i\} \in \IN$$
+      is well-defined, which we regard as a morphism in $B\IN$. For $i \leq j$ we compute
+      $$\begin{align*}
+      u_i & = \max \{D(i,k) : k \geq i\} \\
+      & = \max \{D(i,k) : k \geq j\} \\
+      & = \max \{ D(j,k) + D(i,j) : k \geq j\} \\
+      & = \max \{D(j,k) : k \geq j\}  + D(i,j)\\
+      & = u_j + D(i,j),
+      \end{align*}$$
+      showing that $(u_i)$ defines a cocone. It is universal: let $(v_i)$ be another cocone, i.e. $v_i \in \IN$ and $v_i = v_j + D(i,j)$ for all $i \leq j$. Then $v_i \geq D(i,j)$ for all $i \leq j$, hence $v_i \geq u_i$. Write $v_i = w_i + u_i$ for some uniquely determined $w_i \in \IN$. For $i \leq j$ we compute
+      $$w_j + u_j + D(i,j) = v_j + D(i,j) = v_i = w_i + u_i = w_i + u_j + D(i,j),$$
+      hence $w_j = w_i$. Therefore, the $w_i$ are constant, and the required factorization follows.
+    check_redundancy: false
+
+  - property: ℵ₁-accessible
+    reason: >-
+      We continue the proof that $\aleph_1$-filtered colimits exist. It remains to show that the unique object $*$ is $\aleph_1$-presentable, i.e. that for every diagram $D : \I \to B\IN$ as above, the canonical map
+      $$\alpha : \colim_{i \in \I} \Hom(*,D(i)) \to \Hom(*,\colim_{i \in \I} D(i))$$
+      is bijective. On objects, we necessarily have $D(i)=*$ and $\colim_{i \in \I} D(i)=*$. Hence, the codomain of $\alpha$ is simply $\IN$, while the domain consists of equivalence classes $[i,n]$ of pairs $(i,n) \in \I \times \IN$, where $(i,n) \sim (j,m)$ iff there exists some $k \geq i,j$ such that
+      $$D(i,k) + n = D(j,k) + m.$$
+      By the construction of the colimit cocone, we have
+      $$\alpha([i,n]) = u_i + n = \max \{D(i,j) : j \geq i\} + n.$$
+      (1) The map $\alpha$ is surjective: Pick some $i \in \I$. Choose $j \geq i$ such that $u_i = D(i,j)$. For all $k \geq j$ we then have
+      $$u_i \geq D(i,k) = D(j,k) + D(i,j) = D(j,k) + u_i,$$
+      hence $D(j,k)=0$. Therefore, $u_j=0$, and thus $\alpha([j,n]) = n$ for all $n \in \IN$.
+
+      (2) The map $\alpha$ is injective: Assume that $[i,n]$ and $[j,m]$ have the same image. Since $\I$ is filtered, we may assume $i=j$. The condition then becomes $u_i + n = u_i + m$, and therefore $n=m$. This completes the proof.
+
 unsatisfied_properties:
   - property: one-way
     reason: This is trivial.

databases/catdat/data/categories/BOn.yaml

@@ -41,6 +41,47 @@ satisfied_properties:
   - property: locally cartesian closed
     reason: The slice category $B\On / *$ is isomorphic to the poset $(\On,\geq)$ (not to $(\On,\leq)$). This category is thin and and semi-strongly connected, <a href="/category-implication/sequential_implies_lcc">hence</a> cartesian closed.
 
+  - property: ℵ₁-filtered colimits
+    reason: >-
+      The proof is similar to <a href="/category/BN">$B\IN$</a>. Let $\I$ be an $\aleph_1$-filtered small category and $D : \I \to B\On$ a diagram. A cocone $\lambda = (\lambda_i)_{i \in \I}$ for $D$ is a family of ordinals satisfying $\lambda_i = \lambda_j + D(f)$ for every morphism $f: i \to j$ in $\I$.
+
+
+      We first observe that $D$ factors uniquely through the preorder reflection of $\I$. Indeed, any two parallel morphisms in $\I$ are coequalized by some morphism, and $B\On$ is left cancellative. Thus, we may assume that $\I$ is a preorder. Each inequality $i \leq j$ in $\I$ is mapped to an ordinal number $\alpha_{i,j} \coloneqq D(i \to j)$, and these numbers satisfy
+      $$\alpha_{i,k} = \alpha_{j,k} + \alpha_{i,j}$$
+      for all $i \leq j \leq k$. In particular, $\alpha_{i,j} \leq \alpha_{i,k}$.
+
+
+      For fixed $i \in \I$, the collection $\{\alpha_{i,j} : j \geq i\}$ is a set of ordinals because $\I$ is small, hence bounded above in $\On$. We claim that it has a maximum element. Otherwise, we can find a countable chain $i = j_0 \leq j_1 \leq j_2 \leq \dotsc$ in $\I$ such that $\alpha_{i,j_n} < \alpha_{i,j_{n+1}}$ for all $n \in \IN$. Since $\I$ is $\aleph_1$-filtered, there is an upper bound $j_\infty \in \I$ of $(j_n)_{n \in \IN}$. For each $n \in \IN$, the equation
+      $$\alpha_{i,j_{n+1}} = \alpha_{j_n,j_{n+1}} + \alpha_{i,j_n}$$
+      implies that $\alpha_{j_n,j_{n+1}} > 0$. Hence,
+      $$\alpha_{j_n,j_\infty} = \alpha_{j_{n+1},j_\infty} + \alpha_{j_n,j_{n+1}} > \alpha_{j_{n+1},j_\infty},$$
+      so $(\alpha_{j_n,j_\infty})_{n \in \IN}$ is a strictly decreasing infinite sequence of ordinals, contradicting the well-foundedness of $\On$. Thus, the maximum
+      $$u_i \coloneqq \max \{ \alpha_{i,j} : j \geq i \}$$
+      is a well-defined ordinal number, which we regard as a morphism in $B\On$. The family $(u_i)_{i \in \I}$ forms a cocone for $D$, since for all $i \leq j$ we have
+      $$\begin{align*}
+      u_i & = \max \{ \alpha_{i,k} : k \geq i \} \\
+      & = \max \{ \alpha_{i,k} : k \geq j \} \\
+      & = \max \{ \alpha_{j,k} + \alpha_{i,j} : k \geq j \} \\
+      & = \max \{ \alpha_{j,k} : k \geq j \} + \alpha_{i,j} \\
+      & = u_j + \alpha_{i,j}.
+      \end{align*}$$
+      To establish the universal property, let $(\lambda_i)_{i \in \I}$ be any cocone for $D$, so that $\lambda_i = \lambda_j + \alpha_{i,j}$ for all $i \leq j$. The cocone relation $u_i = u_j + \alpha_{i,j}$ implies that $u_i \geq u_j$ whenever $i \leq j$. By the well-foundedness of $\On$, there exists $i_0 \in \I$ such that $u_j = u_{i_0}$ for all $j \geq i_0$. For such $j$, the relation
+      $$u_{i_0} = u_j + \alpha_{i_0,j} = u_{i_0} + \alpha_{i_0,j}$$
+      forces $\alpha_{i_0,j} = 0$. Consequently,
+      $$u_{i_0} = \max \{ \alpha_{i_0,j} : j \geq i_0 \} = 0.$$
+      Define the mediating morphism to be the ordinal $\kappa \coloneqq \lambda_{i_0}$. We must show that $\lambda_i = \kappa + u_i$ for all $i \in \I$. Choose $j \in \I$ with $j \geq i$ and $j \geq i_0$. Since $j \geq i_0$, we have $u_j = 0$ and $\alpha_{i_0,j} = 0$. The cocone condition for $\lambda$ gives
+      $$\kappa = \lambda_{i_0} = \lambda_j + \alpha_{i_0,j} = \lambda_j.$$
+      Applying the cocone conditions for $u$ and $\lambda$ to $i \leq j$, we obtain
+      $$u_i = u_j + \alpha_{i,j} = 0 + \alpha_{i,j} = \alpha_{i,j}$$
+      and
+      $$\lambda_i = \lambda_j + \alpha_{i,j} = \kappa + \alpha_{i,j} = \kappa + u_i.$$
+      This proves the existence of the mediating morphism.
+
+
+      For uniqueness, suppose $\kappa'$ is any ordinal satisfying $\lambda_i = \kappa' + u_i$ for all $i \in \I$. Evaluating at $i_0$ yields
+      $$\lambda_{i_0} = \kappa' + u_{i_0} = \kappa' + 0 = \kappa',$$
+      hence $\kappa' = \kappa$. Therefore, the cocone $(u_i)_{i \in \I}$ is the colimit of $D$ in $B\On$.
+
 unsatisfied_properties:
   - property: initial object
     reason: This is trivial.

databases/catdat/data/categories/FinAb.yaml

@@ -31,9 +31,6 @@ satisfied_properties:
   - property: self-dual
     reason: 'This is a simple special case of Pontryagin duality: The functor $\Hom(-,\IQ/\IZ)$ provides the equivalence.'
 
-  - property: ℵ₁-accessible
-    reason: The proof works exactly as for <a href="/category/FinSet">$\FinSet$</a>.
-
 unsatisfied_properties:
   - property: small
     reason: Even the collection of trivial groups is not small.

databases/catdat/data/categories/FinGrp.yaml

@@ -46,9 +46,6 @@ satisfied_properties:
   - property: regular
     reason: The category is Malcev and hence finitely complete, and it has all coequalizers. The regular epimorphisms coincide with the surjective group homomorphisms (see below), hence are clearly stable under pullbacks.
 
-  - property: ℵ₁-accessible
-    reason: The proof works exactly as for <a href="/category/FinSet">$\FinSet$</a>.
-
 unsatisfied_properties:
   - property: small
     reason: Even the collection of trivial groups is not small.

databases/catdat/data/categories/FinSet.yaml

@@ -41,9 +41,6 @@ satisfied_properties:
   - property: elementary topos
     reason: This follows easily from the fact that sets form an elementary topos.
 
-  - property: ℵ₁-accessible
-    reason: The inclusion $\FinSet \hookrightarrow \Set$ is closed under ℵ₁-filtered colimits, that is, any ℵ₁-filtered colimit of finite sets is again finite. Since every finite set is ℵ₁-presentable in $\Set$, it is still ℵ₁-presentable in $\FinSet$. Therefore, $\FinSet$ is ℵ₁-accessible, where every object is ℵ₁-presentable.
-
 unsatisfied_properties:
   - property: small
     reason: Even the collection of all singletons is not a set.

databases/catdat/data/categories/FreeAb.yaml

@@ -54,6 +54,9 @@ unsatisfied_properties:
   - property: sequential colimits
     reason: See <a href="https://mathoverflow.net/questions/509715" target="_blank">MO/509715</a>.
 
+  - property: ℵ₁-filtered colimits
+    reason: It is shown in <a href="https://mathoverflow.net/questions/511426" target="_blank">MO/511426</a> that the $\aleph_1$-filtered diagram of countable subgroups of $\IZ^{\IN}$ does not have a colimit in $\FreeAb$.
+
 category_property_comments:
   - property: accessible
     comment: The question if this category is accessible is undecidable in ZFC. See <a href="https://math.stackexchange.com/questions/720885" target="_blank">MSE/720885</a>.

databases/catdat/data/categories/Grp_c.yaml

@@ -85,7 +85,7 @@ unsatisfied_properties:
   - property: cogenerator
     reason: 'Assume that a cogenerator $Q$ exists in $\Grp_\c$. There are only countably many finitely generated subgroups of $Q$. But there are continuum many finitely generated simple groups; this follows from Corollary 1.5 in <a href="https://arxiv.org/abs/1807.06478" target="_blank">Finitely generated infinite simple groups of homeomorphisms of the real line</a> by J. Hyde and Y. Lodha. Hence, there is a finitely generated (and hence countable) simple group $H$ which does not embed into $Q$. Since $H$ is simple, any homomorphism $H \to Q$ must be trivial then. But then $\id_H, 1 : H \rightrightarrows H$ are not separated by a homomorphism $H \to Q$.'
 
-  - property: ℵ₁-accessible
+  - property: ℵ₁-filtered colimits
     reason: 'We can almost copy the proof from <a href="/category/Set_c">$\Set_\c$</a> to show that $\Grp_\c$ does not have $\aleph_1$-filtered colimits: Fix an uncountable set $X$, let $P_\c(X)$ be the poset of countable subsets of $X$, which is $\aleph_1$-filtered, and consider the functor $P_\c(X) \to \Grp_\c$ taking a subset $Y \subseteq X$ to the free group $F(Y)$. The colimit of this diagram in $\Grp$ is given by $F(X)$ itself, so if $G$ were a colimit in $\Grp_\c$, then $\Hom(G, C_2) \cong \Hom(F(X),C_2) \cong \{0,1\}^X$. But the former has cardinality at most $2^{\aleph_0}$ and the latter has cardinality $2^{\card(X)}$, so we have obtained a contradiction if we pick $X$ large enough (e.g. $\card(X)=2^{\aleph_0}$).'
 
 special_objects:

databases/catdat/data/categories/Man.yaml

@@ -71,7 +71,7 @@ unsatisfied_properties:
   - property: sequential colimits
     reason: If $\Man$ had sequential colimits, then by <a href="/content/special_sequential_colimits">this lemma</a> there would be a manifold $M$ that admits a split epimorphism $M \to \IR^n$ for every $n$. But then $M$ will have an infinite-dimensional tangent space, which is a contradiction.
 
-  - property: ℵ₁-accessible
+  - property: ℵ₁-filtered colimits
     reason: 'We already know that <a href="/category/Set_c">$\Set_\c$</a> does not have $\aleph_1$-filtered colimits. The functor $\pi_0: \Man \to \Set_\c$ is well-defined (because manifolds are second-countable), and it admits a fully faithful right adjoint (regarding a countable set as a discrete manifold). Therefore, $\Man$ does not have $\aleph_1$-filtered colimits.'
 
   - property: quotients of congruences

databases/catdat/data/categories/Met_c.yaml

@@ -48,7 +48,7 @@ satisfied_properties:
     reason: This follows from the existence of coproducts and finite products, and from the fact that <a href="/category/Top">$\Top$</a> is infinitary extensive.
 
   - property: effective cocongruences
-    reason: 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Met_\c$. Then the image in $\Haus$ is a coreflexive corelation (since epimorphisms in both categories are continuous maps with dense image). By <a href="https://mathoverflow.net/a/509582/2841" target="_blank">MO/509548</a>, that implies that image is of the form $X +_S X$ for a closed subset $S$ of $X$. Since $S$ is metrizable, and the functor $\Met_\c \to \Haus$ is fully faithful <a href="https://ncatlab.org/nlab/show/reflected+limit#FullSubcategoryInclusionReflectCoLimits" target="_blank">and therefore reflects colimits</a>, we conclude that $E$ is effective in $\Met_\c$.'
+    reason: 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Met_c$. Then the image in $\Haus$ is a coreflexive corelation (since epimorphisms in both categories are continuous maps with dense image). By <a href="https://mathoverflow.net/a/509582/2841" target="_blank">MO/509548</a>, that implies that image is of the form $X +_S X$ for a closed subset $S$ of $X$. Since $S$ is metrizable, and the functor $\Met_c \to \Haus$ is fully faithful <a href="https://ncatlab.org/nlab/show/reflected+limit#FullSubcategoryInclusionReflectCoLimits" target="_blank">and therefore reflects colimits</a>, we conclude that $E$ is effective in $\Met_c$.'
 
 unsatisfied_properties:
   - property: skeletal
@@ -67,7 +67,10 @@ unsatisfied_properties:
     reason: 'We recycle the proof from <a href="/category/Haus">$\Haus$</a>: Assume that there is a regular subobject classifier $\Omega$. By the classification of regular monomorphisms, we would have an isomorphism between $\Hom(X,\Omega)$ and the set of closed subsets of $X$ for any metric 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 $\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]$).'
 
   - property: sequential colimits
-    reason: See <a href="https://mathoverflow.net/questions/510316" target="_blank">MO/510316</a>.
+    reason: See <a href="https://mathoverflow.net/questions/510316" target="_blank">MO/510316</a> for a proof that the diagram $\IN \to \Met_c$, $n \mapsto \IR^n$ does not have a colimit.
+
+  - property: ℵ₁-filtered colimits
+    reason: See <a href="https://mathoverflow.net/questions/511433" target="_blank">MO/511433</a> for a proof that the diagram $\omega_1 \to \Met_c$, $\alpha \mapsto \IR^\alpha$ does not have a colimit.
 
   - property: quotients of congruences
     reason: If $\Met_c$ had quotients of congruences, then by <a href="/content/monic-sequential-colimits-via-congruence-quotients">this lemma</a> it would have sequential colimits of sequences of monomorphisms. This contradicts <a href="https://mathoverflow.net/questions/510316" target="_blank">MO/510316</a>.

databases/catdat/data/categories/Set_c.yaml

@@ -69,8 +69,8 @@ unsatisfied_properties:
   - property: countable powers
     reason: Since the forgetful functor $\Set_\c \to \Set$ is representable, it preserves (countable) products. Therefore, if the power $\{0,1\}^{\IN}$ exists in $\Set_\c$, it must be the ordinary cartesian product, which however is uncountable.
 
-  - property: ℵ₁-accessible
-    reason: 'In fact, $\Set_\c$ does not have $\aleph_1$-filtered colimits: Fix an uncountable set $X$, let $P_\c(X)$ be the poset of countable subsets of $X$, which is $\aleph_1$-filtered, and consider the functor $P_\c(X) \to \Set_\c$ taking a subset $Y \subseteq X$ to $Y$. The colimit of this diagram in $\Set$ is given by $X$ itself, so if $X_c$ were a colimit in $\Set_\c$, then $\Hom(X_c, \{0,1\}) \cong \Hom(X, \{0,1\})$. But the former has cardinality at most $2^{\aleph_0}$ and the latter has cardinality $2^{\card(X)}$, so we have obtained a contradiction if we pick $X$ large enough (e.g. $\card(X)=2^{\aleph_0}$).'
+  - property: ℵ₁-filtered colimits
+    reason: 'Fix an uncountable set $X$, let $P_\c(X)$ be the poset of countable subsets of $X$, which is $\aleph_1$-filtered, and consider the functor $P_\c(X) \to \Set_\c$ taking a subset $Y \subseteq X$ to $Y$. The colimit of this diagram in $\Set$ is given by $X$ itself, so if $X_c$ were a colimit in $\Set_\c$, then $\Hom(X_c, \{0,1\}) \cong \Hom(X, \{0,1\})$. But the former has cardinality at most $2^{\aleph_0}$ and the latter has cardinality $2^{\card(X)}$, so we have obtained a contradiction if we pick $X$ large enough (e.g. $\card(X)=2^{\aleph_0}$).'
 
 special_objects:
   initial object:

databases/catdat/data/categories/Sp.yaml

@@ -23,6 +23,9 @@ satisfied_properties:
   - property: cogenerator
     reason: 'This follows from $\Sp \simeq \prod_{n \geq 0} \Sigma_n{-}\FinSet$, <a href="/content/cogenerators_in_product_categories">this lemma</a>, and the fact that if $G$ is a (finite) group, the power set $P(G)$ with the evident $G$-action is a weakly terminal cogenerator in $G{-}\Set$ (resp. $G{-}\FinSet$). For the proof, notice that $\varnothing,G \in P(G)$ are fixed points, yielding two $G$-maps $1 \rightrightarrows P(G)$. In particular, $P(G)$ is weakly terminal. If $X$ is a $G$-set with distinct points $x,y$, we construct a $G$-map $f : X \to P(G)$ that separates $x,y$: First, $X$ is a coproduct of orbits. If $x,y$ lie in different orbits, let $f|_{Gx}$ be constant $\varnothing$, $f|_{Gy}$ be constant $G$, and, say, $f$ be constant $\varnothing$ on all other orbits. If $x,y$ lie in the same orbit, say $y = g_0 x$, define $f|_{Gx} : Gx \to P(G)$ by $f(x) = G_x$ (stabilizer), which is well-defined, and choose $f$ to be $\varnothing$ on all other orbits. Then $f(y) = g_0 G_x \neq G_x = f(x)$.'
 
+  - property: ℵ₁-accessible
+    reason: We know that <a href="/category/FinSet">$\FinSet$</a> has $\aleph_1$-filtered colimits and that every object is $\aleph_1$-presentable. It follows that for every $n \in \IN$ also $\Sigma_n{-}\FinSet$ has $\aleph_1$-filtered colimits and that every object is $\aleph_1$-presentable. From this it follows formally that $\Sp \simeq \prod_{n \geq 0} \Sigma_n{-}\FinSet$ also has these properties. In particular, $\Sp$ is $\aleph_1$-accessible.
+
 unsatisfied_properties:
   - property: skeletal
     reason: This is trivial.

databases/catdat/data/categories/walking_idempotent.yaml

@@ -39,8 +39,8 @@ satisfied_properties:
   - property: preadditive
     reason: The monoid $\{1,e\}$ with $e^2=e$ is the underlying multiplicative monoid of the ring $\IZ/2$, where $e=0$. Thus, the (unique) preadditive structure is given by $1 + e = e + 1 = 1$, $e + e = e$ and $1 + 1 = e$.
 
-  - property: filtered
-    reason: The pair $\id,e$ is coequalized by $e$ (non-universally).
+  - property: ℵ₁-filtered
+    reason: 'In fact, the walking idempotent is $\kappa$-filtered for every regular infinite cardinal $\kappa$: Every diagram $D : \I \to \Idem$ has the cocone $(e : D(i) \to 0)_{i \in \I}$.'
 
 unsatisfied_properties:
   - property: terminal object