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 a29adac7..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 @@ -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", "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 +), +( + '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.',