From 0a072c25cdd937faf00c93ab0679c62bd9e958c8 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 14 May 2026 17:16:59 +0200 Subject: [PATCH 1/3] =?UTF-8?q?add=20property:=20=E2=84=B5=E2=82=81-filter?= =?UTF-8?q?ed=20colimits?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- databases/catdat/data/categories/Delta.yaml | 3 +++ databases/catdat/data/categories/FinOrd.yaml | 3 +++ databases/catdat/data/categories/FinSet.yaml | 2 +- databases/catdat/data/categories/Grp_c.yaml | 2 +- databases/catdat/data/categories/Man.yaml | 2 +- databases/catdat/data/categories/Set_c.yaml | 4 ++-- databases/catdat/data/categories/Sp.yaml | 3 +++ .../data/category-implications/accessible.yaml | 3 ++- .../category-implications/filtered colimits.yaml | 16 ++++++++++++++++ .../category-properties/aleph1-accessible.yaml | 3 ++- .../aleph1-filtered colimits.yaml | 11 +++++++++++ .../category-properties/filtered colimits.yaml | 1 + databases/catdat/scripts/expected-data/Ab.json | 1 + databases/catdat/scripts/expected-data/Set.json | 1 + databases/catdat/scripts/expected-data/Top.json | 1 + 15 files changed, 49 insertions(+), 7 deletions(-) create mode 100644 databases/catdat/data/category-properties/aleph1-filtered colimits.yaml diff --git a/databases/catdat/data/categories/Delta.yaml b/databases/catdat/data/categories/Delta.yaml index de07bf0d..5bac7ad0 100644 --- a/databases/catdat/data/categories/Delta.yaml +++ b/databases/catdat/data/categories/Delta.yaml @@ -54,6 +54,9 @@ satisfied_properties: - property: epi-regular reason: The proof for $\FinOrd$ also works for $\FinSet \setminus \{\varnothing\}$. + - property: ℵ₁-filtered colimits + reason: This can be deduced from the property for $\FinOrd$. + - 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: diff --git a/databases/catdat/data/categories/FinOrd.yaml b/databases/catdat/data/categories/FinOrd.yaml index bbb37262..04933f41 100644 --- a/databases/catdat/data/categories/FinOrd.yaml +++ b/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 $\FinSet$. + unsatisfied_properties: - property: small reason: Even the collection of all singleton orders is not small. diff --git a/databases/catdat/data/categories/FinSet.yaml b/databases/catdat/data/categories/FinSet.yaml index 820d795a..224d7a29 100644 --- a/databases/catdat/data/categories/FinSet.yaml +++ b/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 (MO/400763). 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 diff --git a/databases/catdat/data/categories/Grp_c.yaml b/databases/catdat/data/categories/Grp_c.yaml index 7c8fac0a..ce9a5114 100644 --- a/databases/catdat/data/categories/Grp_c.yaml +++ b/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 Finitely generated infinite simple groups of homeomorphisms of the real line 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 $\Set_\c$ 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: diff --git a/databases/catdat/data/categories/Man.yaml b/databases/catdat/data/categories/Man.yaml index 37f73027..afca53ec 100644 --- a/databases/catdat/data/categories/Man.yaml +++ b/databases/catdat/data/categories/Man.yaml @@ -71,7 +71,7 @@ unsatisfied_properties: - property: sequential colimits reason: If $\Man$ had sequential colimits, then by this lemma 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 $\Set_\c$ 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 diff --git a/databases/catdat/data/categories/Set_c.yaml b/databases/catdat/data/categories/Set_c.yaml index e949660d..fc228389 100644 --- a/databases/catdat/data/categories/Set_c.yaml +++ b/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: diff --git a/databases/catdat/data/categories/Sp.yaml b/databases/catdat/data/categories/Sp.yaml index 62c23aef..0ecf1b45 100644 --- a/databases/catdat/data/categories/Sp.yaml +++ b/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$, this lemma, 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 $\FinSet$ has this property. + unsatisfied_properties: - property: skeletal reason: This is trivial. diff --git a/databases/catdat/data/category-implications/accessible.yaml b/databases/catdat/data/category-implications/accessible.yaml index c0018f04..4d681fbc 100644 --- a/databases/catdat/data/category-implications/accessible.yaml +++ b/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 Makkai-Pare, Prop. 2.2.1. is_equivalence: false - id: small_accessible_characterization diff --git a/databases/catdat/data/category-implications/filtered colimits.yaml b/databases/catdat/data/category-implications/filtered colimits.yaml index 5e3ff90a..5b93a253 100644 --- a/databases/catdat/data/category-implications/filtered colimits.yaml +++ b/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 MO/509853 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 walking idempotent is $\kappa$-filtered. See also Makkai-Pare, Prop. 2.2.1. + is_equivalence: false + - id: sifted_categories_are_connected assumptions: - connected colimits diff --git a/databases/catdat/data/category-properties/aleph1-accessible.yaml b/databases/catdat/data/category-properties/aleph1-accessible.yaml index 23532d7a..6b3d96c2 100644 --- a/databases/catdat/data/category-properties/aleph1-accessible.yaml +++ b/databases/catdat/data/category-properties/aleph1-accessible.yaml @@ -1,6 +1,6 @@ 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 @@ -8,3 +8,4 @@ related_properties: - accessible - finitely accessible - locally ℵ₁-presentable + - ℵ₁-filtered colimits diff --git a/databases/catdat/data/category-properties/aleph1-filtered colimits.yaml b/databases/catdat/data/category-properties/aleph1-filtered colimits.yaml new file mode 100644 index 00000000..0ac19525 --- /dev/null +++ b/databases/catdat/data/category-properties/aleph1-filtered colimits.yaml @@ -0,0 +1,11 @@ +id: ℵ₁-filtered colimits +relation: has +description: A category has $\aleph_1$-filtered colimits if it has colimits of diagrams indexed by small $\aleph_1$-filtered categories. Here, a category is called $\aleph_1$-filtered when every countable diagram has a cocone. +nlab_link: https://ncatlab.org/nlab/show/filtered+colimit +dual_property: null +invariant_under_equivalences: true + +related_properties: + - cocomplete + - filtered colimits + - ℵ₁-accessible diff --git a/databases/catdat/data/category-properties/filtered colimits.yaml b/databases/catdat/data/category-properties/filtered colimits.yaml index ebab748e..9cc8bc4f 100644 --- a/databases/catdat/data/category-properties/filtered colimits.yaml +++ b/databases/catdat/data/category-properties/filtered colimits.yaml @@ -10,3 +10,4 @@ related_properties: - directed colimits - filtered - sifted colimits + - ℵ₁-filtered colimits diff --git a/databases/catdat/scripts/expected-data/Ab.json b/databases/catdat/scripts/expected-data/Ab.json index 5adbeb58..75e28964 100644 --- a/databases/catdat/scripts/expected-data/Ab.json +++ b/databases/catdat/scripts/expected-data/Ab.json @@ -89,6 +89,7 @@ "accessible": true, "finitely accessible": true, "ℵ₁-accessible": true, + "ℵ₁-filtered colimits": true, "generalized variety": true, "locally finitely multi-presentable": true, "locally multi-presentable": true, diff --git a/databases/catdat/scripts/expected-data/Set.json b/databases/catdat/scripts/expected-data/Set.json index 1b231c2e..44644248 100644 --- a/databases/catdat/scripts/expected-data/Set.json +++ b/databases/catdat/scripts/expected-data/Set.json @@ -83,6 +83,7 @@ "accessible": true, "finitely accessible": true, "ℵ₁-accessible": true, + "ℵ₁-filtered colimits": true, "generalized variety": true, "locally finitely multi-presentable": true, "locally multi-presentable": true, diff --git a/databases/catdat/scripts/expected-data/Top.json b/databases/catdat/scripts/expected-data/Top.json index d3febb98..864a05fa 100644 --- a/databases/catdat/scripts/expected-data/Top.json +++ b/databases/catdat/scripts/expected-data/Top.json @@ -137,6 +137,7 @@ "accessible": false, "finitely accessible": false, "ℵ₁-accessible": false, + "ℵ₁-filtered colimits": true, "generalized variety": false, "locally finitely multi-presentable": false, "locally multi-presentable": false, From 3c7f70bf3c021483862c9d50ea632bba40449721 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 14 May 2026 18:25:34 +0200 Subject: [PATCH 2/3] =?UTF-8?q?add=20property:=20=E2=84=B5=E2=82=81-filter?= =?UTF-8?q?ed?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../data/categories/walking_idempotent.yaml | 4 +- .../filtered + sifted.yaml | 53 ++++++++++++++++--- .../aleph1-filtered colimits.yaml | 3 +- .../category-properties/aleph1-filtered.yaml | 11 ++++ .../data/category-properties/filtered.yaml | 6 ++- .../catdat/scripts/expected-data/Ab.json | 1 + .../catdat/scripts/expected-data/Set.json | 1 + .../catdat/scripts/expected-data/Top.json | 1 + 8 files changed, 67 insertions(+), 13 deletions(-) create mode 100644 databases/catdat/data/category-properties/aleph1-filtered.yaml diff --git a/databases/catdat/data/categories/walking_idempotent.yaml b/databases/catdat/data/categories/walking_idempotent.yaml index 68b3a491..ba0e99ce 100644 --- a/databases/catdat/data/categories/walking_idempotent.yaml +++ b/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 diff --git a/databases/catdat/data/category-implications/filtered + sifted.yaml b/databases/catdat/data/category-implications/filtered + sifted.yaml index 1b1f2b3c..ce37ad89 100644 --- a/databases/catdat/data/category-implications/filtered + sifted.yaml +++ b/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 universal 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 universal 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 universal 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 diff --git a/databases/catdat/data/category-properties/aleph1-filtered colimits.yaml b/databases/catdat/data/category-properties/aleph1-filtered colimits.yaml index 0ac19525..1a583f6a 100644 --- a/databases/catdat/data/category-properties/aleph1-filtered colimits.yaml +++ b/databases/catdat/data/category-properties/aleph1-filtered colimits.yaml @@ -1,6 +1,6 @@ id: ℵ₁-filtered colimits relation: has -description: A category has $\aleph_1$-filtered colimits if it has colimits of diagrams indexed by small $\aleph_1$-filtered categories. Here, a category is called $\aleph_1$-filtered when every countable diagram has a cocone. +description: A category has $\aleph_1$-filtered colimits 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 @@ -9,3 +9,4 @@ related_properties: - cocomplete - filtered colimits - ℵ₁-accessible + - ℵ₁-filtered diff --git a/databases/catdat/data/category-properties/aleph1-filtered.yaml b/databases/catdat/data/category-properties/aleph1-filtered.yaml new file mode 100644 index 00000000..52183594 --- /dev/null +++ b/databases/catdat/data/category-properties/aleph1-filtered.yaml @@ -0,0 +1,11 @@ +id: ℵ₁-filtered +relation: is +description: A category is $\aleph_1$-filtered 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 nLab. +nlab_link: https://ncatlab.org/nlab/show/filtered+category +dual_property: null +invariant_under_equivalences: true + +related_properties: + - filtered + - ℵ₁-filtered colimits + - cocomplete diff --git a/databases/catdat/data/category-properties/filtered.yaml b/databases/catdat/data/category-properties/filtered.yaml index 938bdf4a..7ce6254b 100644 --- a/databases/catdat/data/category-properties/filtered.yaml +++ b/databases/catdat/data/category-properties/filtered.yaml @@ -1,10 +1,12 @@ id: filtered relation: is -description: A category is filtered 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 filtered 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 diff --git a/databases/catdat/scripts/expected-data/Ab.json b/databases/catdat/scripts/expected-data/Ab.json index 75e28964..42c0cb6a 100644 --- a/databases/catdat/scripts/expected-data/Ab.json +++ b/databases/catdat/scripts/expected-data/Ab.json @@ -79,6 +79,7 @@ "finite copowers": true, "binary copowers": true, "filtered": true, + "ℵ₁-filtered": true, "cofiltered": true, "sifted": true, "cosifted": true, diff --git a/databases/catdat/scripts/expected-data/Set.json b/databases/catdat/scripts/expected-data/Set.json index 44644248..b2ab6e58 100644 --- a/databases/catdat/scripts/expected-data/Set.json +++ b/databases/catdat/scripts/expected-data/Set.json @@ -77,6 +77,7 @@ "finite copowers": true, "binary copowers": true, "filtered": true, + "ℵ₁-filtered": true, "cofiltered": true, "sifted": true, "cosifted": true, diff --git a/databases/catdat/scripts/expected-data/Top.json b/databases/catdat/scripts/expected-data/Top.json index 864a05fa..f0292620 100644 --- a/databases/catdat/scripts/expected-data/Top.json +++ b/databases/catdat/scripts/expected-data/Top.json @@ -61,6 +61,7 @@ "finite copowers": true, "binary copowers": true, "filtered": true, + "ℵ₁-filtered": true, "cofiltered": true, "sifted": true, "cosifted": true, From 4c98d0489512c2855a9564e4bcee14fdd0c50035 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 15 May 2026 17:20:03 +0200 Subject: [PATCH 3/3] add criterion for countable accessibility (WIP) --- .../category-implications/accessible.yaml | 28 +++++++++++++++++-- 1 file changed, 25 insertions(+), 3 deletions(-) diff --git a/databases/catdat/data/category-implications/accessible.yaml b/databases/catdat/data/category-implications/accessible.yaml index 4d681fbc..92d6d51a 100644 --- a/databases/catdat/data/category-implications/accessible.yaml +++ b/databases/catdat/data/category-implications/accessible.yaml @@ -161,13 +161,35 @@ reason: See Makkai-Pare, 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 Makkai-Pare (which only gives $\aleph_2$-accessibility) and to MO/509853 (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