Two results on finite categories

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',

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 <a href="http://www.tac.mta.ca/tac/volumes/8/n3/8-03abs.html" target="_blank">[AR01, Lemma 3.3]</a> 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',

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 <a href="https://mathoverflow.net/questions/509853" target="_blank">MO/509853</a> 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 <a href="https://mathoverflow.net/questions/509853" target="_blank">MO/509853</a>, where it is in fact shown that the ind-completion of any finite Cauchy-complete category becomes itself.',