Add property: ℵ₁-filtered colimits (WIP)

databases/catdat/data/categories/Delta.yaml

@@ -54,6 +54,9 @@ satisfied_properties:
   - property: epi-regular
     reason: The proof for <a href="/category/FinOrd">$\FinOrd$</a> also works for $\FinSet \setminus \{\varnothing\}$.
 
+  - property: ℵ₁-filtered colimits
+    reason: This can be deduced from the property for <a href="/category/FinOrd">$\FinOrd$</a>.
+
   - property: cosifted
     reason: >-
       Let $X,Y \in \Delta$. We may pick $x \in X$, $y \in Y$. Then there is a "point span" $X \xleftarrow{x} [0] \xrightarrow{y} Y$. Every span $X \xleftarrow{f} Z \xrightarrow{g} Y$ is connected to such a point span: Pick $z \in Z$. This defines a morphism of spans: 

databases/catdat/data/categories/FinOrd.yaml

@@ -55,6 +55,9 @@ satisfied_properties:
   - property: core-thin
     reason: 'Let $f : \{1 < \cdots < n \} \to \{1 < \cdots < n \}$ be an automorphism. Then $f(i)$ is the smallest element not contained in $\{f(j) : j < i\}$. From this one can deduce $f(i)=i$ by induction.'
 
+  - property: ℵ₁-filtered colimits
+    reason: The proof is similar to <a href="/category/FinSet">$\FinSet$</a>.
+
 unsatisfied_properties:
   - property: small
     reason: Even the collection of all singleton orders is not small.

databases/catdat/data/categories/FinSet.yaml

@@ -42,7 +42,7 @@ satisfied_properties:
     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.
+    reason: The inclusion $\FinSet \hookrightarrow \Set$ is closed under ℵ₁-filtered colimits, that is, any ℵ₁-filtered colimit of finite sets is again finite (<a href="https://mathoverflow.net/questions/400763" target="_blank">MO/400763</a>). 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

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="/lemma/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/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="/lemma/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: ℵ₁-filtered colimits
+    reason: This is because <a href="/category/FinSet">$\FinSet$</a> has this property.
+
 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

databases/catdat/data/category-implications/accessible.yaml

@@ -132,6 +132,7 @@
     - ℵ₁-accessible
   conclusions:
     - accessible
+    - ℵ₁-filtered colimits
   reason: This is trivial.
   is_equivalence: false
 
@@ -148,7 +149,7 @@
     - accessible
   conclusions:
     - Cauchy complete
-  reason: This is because the walking idempotent is $\kappa$-filtered for any regular cardinal $\kappa$.
+  reason: This is because the walking idempotent is $\kappa$-filtered for any regular cardinal $\kappa$. See also <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a>, Prop. 2.2.1.
   is_equivalence: false
 
 - id: small_accessible_characterization
@@ -160,13 +161,35 @@
   reason: See <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a>, Thm. 2.2.2.
   is_equivalence: false
 
-- id: countably_accessible_thin
+- id: countably_accessible_criterion
+  # TODO: based on this, remove some of the assignments
   assumptions:
     - essentially countable
-    - thin
+    - locally finite
+    - Cauchy complete # TODO: clarify where this is used. it must be used (Idem...)
   conclusions:
     - ℵ₁-accessible
-  reason: In general, every $\kappa$-filtered diagram in a poset whose elements are less than $\kappa$ admits the greatest element. Therefore, all the elements are $\kappa$-presentable, and the poset is $\kappa$-accessible.
+  reason: >-
+    Under the given assumptions, we will prove that every $\aleph_1$-filtered diagram $D : \I \to \C$ indexed by a $\aleph_1$-filtered poset is eventually constant, i.e. there is some $i \in \I$ such that for every morphism $j \geq i$ the morphism $D(i) \to D(j)$ is an isomorphism. This will prove right away that $\aleph_1$-filtered colimits exist and that every object is $\aleph_1$-presentable. The proof will be similar to Thm. 2.2.2 in <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a> (which only gives $\aleph_2$-accessibility) and to <a href="https://mathoverflow.net/questions/509853" target="_blank">MO/509853</a> (which concerns $\aleph_0$-accessibility under stronger assumptions).
+
+    It suffices to prove this for the special case $\C = \FinSet$: For every $X \in \C$ we have a diagram of finite sets $\Hom(X,D(-)) : \I \to \FinSet$ (a priori these are only finite collections, but we may assume that they are finite sets by replacing $\C$ with an equivalent category). Assume that we have found $i_X \in \I$ such that the map of finite sets $\Hom(X,D(i_X)) \to \Hom(X,D(j))$ is an isomorphism for all $j \geq i_X$. Equivalently, $\Hom(X,D(j)) \to \Hom(X,D(j'))$ is an isomorphism for all $i_X \leq j \leq j'$. Since $\C$ is w.l.o.g. countable, we find $i_\infty \in \I$ such that $i_\infty \geq i_X$ for all $X \in \C$. Then for all $i_\infty \leq j \leq j'$ and every $X \in \C$ the map $\Hom(X,D(j)) \to \Hom(X,D(j'))$ is an isomorphism. By the Yoneda Lemma, this means that $D(j) \to D(j')$ is an isomorphism. This finishes the proof of the reduction.
+
+    So now let $D : \I \to \FinSet$ be a diagram indexed by a $\aleph_1$-filtered poset. The transition maps will be denoted by $u_{ij} : D(i) \to D(j)$ for $i \leq j$. Let $L \in \Set$ be the colimit of $D$ considered as a diagram of sets. Thus, we have maps $u_i : D(i) \to L$ satisfying $u_j \circ u_{ij} = u_i$. These maps are jointly surjective, and we have $u_i(x)=u_i(x)$ if and only if $u_{ij}(x) = u_{ij}(y)$ for some $j \geq i$.
+
+    We first show that $L$ is finite. If not, choose distinct elements $a_1,a_2,\dotsc$ in $L$. Each $a_n$ has a preimage $b_{i_n} \in D(i_n)$ for some $i_n \in \I$. Choose some $j \in \I$ with $i_n \leq j$ for all $n$. Then all $a_1,a_2,\dotsc$ have a preimage in $D(j)$. But this is a finite set by assumption; so we have a contradiction.
+
+    Next, we claim that there is some $i_0 \in \I$ such that $u_{i_0} : D(i_0) \to L$ is surjective. Each of the finitely many elements in $L$ has a preimage in some $D(i)$. Since $\I$ is filtered, there is some index which works for all elements.
+
+    Then for every $j \geq i_0$, also the map $u_j : D(j) \to L$ is surjective. However, it does not have to be injective.
+
+    Assume we have found $i_\infty \geq i_0$ such that $u_j$ is injective (and hence bijective) for all $j \geq i_\infty$. Then for all $i_\infty \leq j \leq j'$ the equation $u_{j'} \circ u_{jj'} = u_j$ shows that $u_{jj'}$ is an isomorphism, and we are done.
+
+    So assume the contrary: for all $i \geq i_0$ there is $j \geq i$ such that $u_j$ is not injective. By the description of the elements in $L$, this means that there is some $k \geq j$ such that $u_{jk}$ is not injective.
+
+    For $j \geq i_0$, consider the set $R_j$ of all pairs $a,b \in D(j)$ with $u_j(a)=u_j(b)$ in $L$. For each of these, there is some $k_j \geq j$ with $u_{jk}(a) = u_{jk}(b)$. Since $R_j$ is finite and $\I$ is filtered, we may choose $k_j$ independently from the pair. Thus, $u_{jk}$ induces an injective map $D(j) / R_j \hookrightarrow D(k_j)$.
+
+  # TODO: complete this proof
+
   is_equivalence: false
 
 - id: locally_presentable_another_definition

databases/catdat/data/category-implications/filtered + sifted.yaml

@@ -39,27 +39,64 @@
     where $f=g$; hence when the category is also sifted, all cospans must be of this form, and so any two parallel morphisms are equal.
   is_equivalence: false
 
-- id: terminal_object_yields_filtered
+- id: filtered_criterion
   assumptions:
-    - terminal object
+    - finitely cocomplete
+  conclusions:
+    - filtered
+  reason: Every finite diagram even admits a <i>universal</i> cocone.
+  is_equivalence: false
+
+- id: filtered_via_coequalizers
+  assumptions:
+    - coequalizers
+    - semi-strongly connected
   conclusions:
     - filtered
   reason: This is obvious.
   is_equivalence: false
 
-- id: filtered_criterion
+- id: aleph1-filtered-consequence
   assumptions:
-    - finitely cocomplete
+    - ℵ₁-filtered
   conclusions:
     - filtered
-  reason: Every finite diagram even admits a <i>universal</i> cocone.
+  reason: This is trivial.
   is_equivalence: false
 
-- id: filtered_via_equalizers
+- id: aleph1-filtered_criterion
   assumptions:
     - coequalizers
-    - semi-strongly connected
+    - countable coproducts
   conclusions:
-    - filtered
+    - ℵ₁-filtered
+  reason: Every countable diagram even admits a <i>universal</i> cocone.
+  is_equivalence: false
+
+- id: terminal_object_yields_kappa_filtered
+  assumptions:
+    - terminal object
+  conclusions:
+    - ℵ₁-filtered
   reason: This is obvious.
   is_equivalence: false
+
+- id: filtered-finite-thin
+  assumptions:
+    - thin
+    - filtered
+    - essentially finite
+  conclusions:
+    - terminal object
+  reason: Let $\C$ be a thin, filtered, and w.l.o.g. finite category. The identity diagram $\C \to \C$ admits a cocone. That is, there is an object $T$ with a morphism $A \to T$ for all $A \in \C$. Then $T$ is terminal.
+  is_equivalence: false
+
+- id: aleph1-filtered-countable-thin
+  assumptions:
+    - thin
+    - ℵ₁-filtered
+    - essentially countable
+  conclusions:
+    - terminal object
+  reason: Let $\C$ be a thin, $\aleph_1$-filtered, and w.l.o.g. countable category. The identity diagram $\C \to \C$ admits a cocone. That is, there is an object $T$ with a morphism $A \to T$ for all $A \in \C$. Then $T$ is terminal.
+  is_equivalence: false

databases/catdat/data/category-implications/filtered colimits.yaml

@@ -61,6 +61,22 @@
   reason: We may assume that the category $\C$ is finite and Cauchy complete. The answer at <a href="https://mathoverflow.net/questions/509853" target="_blank">MO/509853</a> shows that every filtered colimit in $\C$ exists, in fact it is a retract of one of the objects in the diagram. Now apply this to the morphism category of $\C$. It follows that for every filtered diagram of morphisms $X_i \to Y_i$ their colimit $X_\infty \to Y_\infty$ exists, which is a retract of one of the $X_i \to Y_i$. Therefore, if every $X_i \to Y_i$ is a monomorphism, also $X_\infty \to Y_\infty$ is a monomorphism.
   is_equivalence: false
 
+- id: aleph1-filtered-colimits-include-filtered-colimits
+  assumptions:
+    - filtered colimits
+  conclusions:
+    - ℵ₁-filtered colimits
+  reason: Every $\aleph_1$-filtered category is also $\aleph_0$-filtered, i.e. filtered. Therefore, every $\aleph_1$-filtered diagram is also a filtered diagram, hence has a colimit by assumption.
+  is_equivalence: false
+
+- id: kappa-filtered-colimits_require_Cauchy_complete
+  assumptions:
+    - ℵ₁-filtered colimits
+  conclusions:
+    - Cauchy complete
+  reason: More generally, if $\kappa$ is any infinite regular cardinal, a category with $\kappa$-filtered colimits must be Cauchy cocomplete. This is because the <a href="/category/walking_idempotent">walking idempotent</a> is $\kappa$-filtered. See also <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a>, Prop. 2.2.1.
+  is_equivalence: false
+
 - id: sifted_categories_are_connected
   assumptions:
     - connected colimits

databases/catdat/data/category-properties/aleph1-accessible.yaml

@@ -1,10 +1,11 @@
 id: ℵ₁-accessible
 relation: is
-description: This is the special case of the notion of $\kappa$-accessible categories, where $\kappa = \aleph_1$ is the first uncountable cardinal.
+description: This is the special case of the notion of a $\kappa$-accessible category, where $\kappa = \aleph_1$ is the first uncountable cardinal. Concretely, a category is $\aleph_1$-accessible when it has $\aleph_1$-filtered colimits and there is a small set $G$ of $\aleph_1$-presentable objects such that every object is a $\aleph_1$-filtered colimit of objects in $G$.
 nlab_link: https://ncatlab.org/nlab/show/accessible+category
 invariant_under_equivalences: true
 
 related_properties:
   - accessible
   - finitely accessible
   - locally ℵ₁-presentable
+  - ℵ₁-filtered colimits

databases/catdat/data/category-properties/aleph1-filtered colimits.yaml

@@ -0,0 +1,12 @@
+id: ℵ₁-filtered colimits
+relation: has
+description: A category has <i>$\aleph_1$-filtered colimits</i> if it has colimits of diagrams indexed by small $\aleph_1$-filtered categories. This is the special case of having small $\kappa$-filtered colimits for $\kappa=\aleph_1$, the first uncountable cardinal.
+nlab_link: https://ncatlab.org/nlab/show/filtered+colimit
+dual_property: null
+invariant_under_equivalences: true
+
+related_properties:
+  - cocomplete
+  - filtered colimits
+  - ℵ₁-accessible
+  - ℵ₁-filtered

databases/catdat/data/category-properties/aleph1-filtered.yaml

@@ -0,0 +1,11 @@
+id: ℵ₁-filtered
+relation: is
+description: A category is <i>$\aleph_1$-filtered</i> if every countable diagram admits a cocone. This is the special case of the notion of a $\kappa$-filtered category for $\kappa = \aleph_1$, the first uncountable cardinal. An equivalent characterization is given as Theorem 2.2 at the <a href="https://ncatlab.org/nlab/show/filtered+category">nLab</a>.
+nlab_link: https://ncatlab.org/nlab/show/filtered+category
+dual_property: null
+invariant_under_equivalences: true
+
+related_properties:
+  - filtered
+  - ℵ₁-filtered colimits
+  - cocomplete

databases/catdat/data/category-properties/filtered colimits.yaml

@@ -10,3 +10,4 @@ related_properties:
   - directed colimits
   - filtered
   - sifted colimits
+  - ℵ₁-filtered colimits

databases/catdat/data/category-properties/filtered.yaml

@@ -1,10 +1,12 @@
 id: filtered
 relation: is
-description: A category is <i>filtered</i> if every finite diagram admits a cocone. Equivalently, it is inhabited, for every two objects $x,y$ there is a cospan $x \rightarrow s \leftarrow y$ (not necessarily universal), and every parallel pair $x \rightrightarrows y$ is coequalized by some morphism $y \to c$ (not necessarily universal).
+description: A category is <i>filtered</i> if every finite diagram admits a cocone. Equivalently, it is inhabited, for every two objects $x,y$ there is a cospan $x \rightarrow s \leftarrow y$ (not necessarily universal), and every parallel pair $x \rightrightarrows y$ is coequalized by some morphism $y \to c$ (not necessarily universal). This is the special case of the notion of a $\kappa$-filtered category for $\kappa = \aleph_0$.
 nlab_link: https://ncatlab.org/nlab/show/filtered+category
 dual_property: cofiltered
 invariant_under_equivalences: true
 
 related_properties:
+  - ℵ₁-filtered
   - filtered colimits
-  - finitely cocomplete
+  - cocomplete
+  - sifted