From 0f46f03567a1a6296cbc0de355754ee05ff83587 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 27 Apr 2026 19:04:04 +0200 Subject: [PATCH 1/2] add back: finite + cauchy complete => filtered colimits this was already in the database, but then was "improved" to => finitely accessible, which however is not dualized, since we do not have finitely coaccessible. --- .../001_limits-colimits-existence-implications.sql | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/databases/catdat/data/004_category-implications/001_limits-colimits-existence-implications.sql b/databases/catdat/data/004_category-implications/001_limits-colimits-existence-implications.sql index a29adac7..44756c51 100644 --- a/databases/catdat/data/004_category-implications/001_limits-colimits-existence-implications.sql +++ b/databases/catdat/data/004_category-implications/001_limits-colimits-existence-implications.sql @@ -181,6 +181,15 @@ VALUES ), ( 'finite_filtered_colimits', + -- TODO: combine this with "finitely accessible" below + -- once its dual is added to the database. + '["essentially finite", "Cauchy complete"]', + '["filtered colimits"]', + 'See MO/509853.', + FALSE +), +( + 'finite_accessible', '["essentially finite", "Cauchy complete"]', '["finitely accessible"]', 'See MO/509853, where it is in fact shown that the ind-completion of any finite Cauchy-complete category becomes itself.', From b5bc07ace9cc58ad7cd329dbff7748920fe88e21 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 27 Apr 2026 19:11:42 +0200 Subject: [PATCH 2/2] finite + cauchy complete => monos are stable under filtered colimits --- .../data/003_category-property-assignments/walking_fork.sql | 6 ------ .../003_category-property-assignments/walking_splitting.sql | 6 ------ .../001_limits-colimits-existence-implications.sql | 4 ++-- 3 files changed, 2 insertions(+), 14 deletions(-) diff --git a/databases/catdat/data/003_category-property-assignments/walking_fork.sql b/databases/catdat/data/003_category-property-assignments/walking_fork.sql index 89ccd76e..9cb538b1 100644 --- a/databases/catdat/data/003_category-property-assignments/walking_fork.sql +++ b/databases/catdat/data/003_category-property-assignments/walking_fork.sql @@ -71,12 +71,6 @@ VALUES TRUE, 'This is trivial.' ), -( - 'walking_fork', - 'cofiltered-limit-stable epimorphisms', - TRUE, - 'Let $(X_p)$ and $(Y_p)$ be diagrams in the walking fork indexed by a cofiltered poset $P$. Let $(X_p \to Y_p)_{p \in P}$ be compatible epimorphisms, we need to show that $\lim_p X_p \to \lim_p Y_p$ is an epimorphism as well. Assume it is not. The only non-epimorphism is $i : 0 \to 1$. Hence, $\lim_p X_p = 0$ and $\lim_p Y_p = 1$. So for every $p$ there is a morphism $1 \to Y_p$, meaning $Y_p \in \{1,2\}$. If $Y_p = 2$ for all $p$, the transition morphisms between them must be identities, so that $\lim_p Y_p = 2$, a contradiction. Choose $p$ with $Y_p = 1$. Then for all $q \leq p$ the morphism $Y_q \to Y_p$ shows that $Y_q = 1$ as well. Since $X_q \to Y_q = 1$ is an epimorphism by assumption, it cannot be $i : 0 \to 1$, and we see that $X_q = 1$. Then the transitions between the $X_q$ are identities, and we get the contradiction $\lim_p X_p = \lim_q X_q = 1$.' -), ( 'walking_fork', 'terminal object', diff --git a/databases/catdat/data/003_category-property-assignments/walking_splitting.sql b/databases/catdat/data/003_category-property-assignments/walking_splitting.sql index 5e934e2e..c17abe80 100644 --- a/databases/catdat/data/003_category-property-assignments/walking_splitting.sql +++ b/databases/catdat/data/003_category-property-assignments/walking_splitting.sql @@ -73,12 +73,6 @@ VALUES TRUE, 'Again we work with $\mathbf{Vect}^{\leq 1}_{\mathbb{F}_2}$. We already know that it has sifted colimits and that the embedding to $\mathbf{Vect}_{\mathbb{F}_2}$ preserves them. The object $0$ is initial and hence strongly finitely presentable. The object $\mathbb{F}_2$ is strongly finitely presentable in $\mathbf{Vect}^{\leq 1}_{\mathbb{F}_2}$ since its hom-functor is the composition of the embedding and the forgetful functor $\mathbf{Vect}_{\mathbb{F}_2} \to \mathbf{Set}$, and the latter preserves sifted colimits by [AR01, Lemma 3.3] applied to $\mathbb{F}_2 \in \mathbf{Vect}_{\mathbb{F}_2}$.' ), -( - 'walking_splitting', - 'filtered-colimit-stable monomorphisms', - TRUE, - 'We saw above that the embedding $\mathbf{Vect}^{\leq 1}_{\mathbb{F}_2} \hookrightarrow \mathbf{Vect}_{\mathbb{F}_2}$ is closed under sifted colimits, hence under filtered colimits. Hence, it preserves filtered colimits. Moreover, it preserves and reflects monomorphisms. Therefore, the claim follows from $\mathbf{Vect}_{\mathbb{F}_2}$.' -), ( 'walking_splitting', 'one-way', diff --git a/databases/catdat/data/004_category-implications/001_limits-colimits-existence-implications.sql b/databases/catdat/data/004_category-implications/001_limits-colimits-existence-implications.sql index 44756c51..b47dfad3 100644 --- a/databases/catdat/data/004_category-implications/001_limits-colimits-existence-implications.sql +++ b/databases/catdat/data/004_category-implications/001_limits-colimits-existence-implications.sql @@ -184,8 +184,8 @@ VALUES -- TODO: combine this with "finitely accessible" below -- once its dual is added to the database. '["essentially finite", "Cauchy complete"]', - '["filtered colimits"]', - 'See MO/509853.', + '["filtered colimits", "filtered-colimit-stable monomorphisms"]', + 'We may assume that the category $\mathcal{C}$ is finite and Cauchy complete. The answer at MO/509853 shows that every filtered colimit in $\mathcal{C}$ exists, in fact it is a retract of one of the objects in the diagram. Now apply this to the morphism category of $\mathcal{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.', FALSE ), (