in a topos, epis are usually not stable under cofiltered limits

Author: ScriptRaccoon

databases/catdat/data/003_category-property-assignments/Haus.sql

@@ -105,5 +105,5 @@ VALUES
 	'Haus',
 	'cofiltered-limit-stable epimorphisms',
 	FALSE,
-	'Our <a href="/category/Set">counterexample for $\mathbf{Set}$</a> (using infinite intersections) also works in $\mathbf{Haus}$ by using discrete topologies. We could also apply a variant of (the dual of) <a href="/lemma/filtered-monos">this lemma</a> to the discrete topology functor $\mathbf{Set} \to \mathbf{Haus}$, which does not preserve all cofiltered limits, but does preserve intersections.'
+	'Recall the counterexample for sets: The unique maps $\mathbb{N}_{\geq n} \to 1$ are surjective, but their limit $0 = \bigcap_{n \geq 0} \mathbb{N}_{\geq n} \to 1$ is not. This also works in $\mathbf{Haus}$ by using discrete topologies. We could also apply a variant of (the dual of) <a href="/lemma/filtered-monos">this lemma</a> to the discrete topology functor $\mathbf{Set} \to \mathbf{Haus}$, which does not preserve all cofiltered limits, but does preserve intersections.'
 );

databases/catdat/data/003_category-property-assignments/M-Set.sql

@@ -31,9 +31,9 @@ VALUES
 ),
 (
 	'M-Set',
-	'cofiltered-limit-stable epimorphisms',
+	'trivial',
 	FALSE,
-	'We know that $\mathbf{Set}$ does not have this property. Now use the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> applied to the functor $\mathbf{Set} \to M{-}\mathbf{Set}$ that equips a set with the trivial $M$-action.'
+	'This is trivial.'
 );
 
 INSERT INTO category_property_comments (category_id, property_id, comment)

databases/catdat/data/003_category-property-assignments/Set.sql

@@ -37,7 +37,7 @@ VALUES
 ),
 (
 	'Set',
-	'cofiltered-limit-stable epimorphisms',
+	'trivial',
 	FALSE,
-	'Pick any decreasing sequence of non-empty sets $X_0 \supseteq X_1 \supseteq \cdots$ with empty intersection, such as $X_n = \mathbb{N}_{\geq n}$. The unique map $X_n \to 1$ is surjective, but their limit $\varnothing \to 1$ is not surjective.'
+	'This is trivial.'
 );

databases/catdat/data/003_category-property-assignments/SetxSet.sql

@@ -40,10 +40,4 @@ VALUES
 	'generator',
 	FALSE,
 	'Assume that $(A,B)$ is a generator. Of course, $A$ and $B$ cannot be both empty. Assume w.l.o.g. that $A$ is non-empty. Then there is no morphism $(A,B) \to (0,1)$, but there are two different morphisms $(0,1) \rightrightarrows (0,2)$.'
-),
-(
-	'SetxSet',
-	'cofiltered-limit-stable epimorphisms',
-	FALSE,
-	'We already know that $\mathbf{Set}$ does not have this property. Now apply the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> to the diagonal functor $\mathbf{Set} \to \mathbf{Set} \times \mathbf{Set}$.'
 );

databases/catdat/data/003_category-property-assignments/Sh(X).sql

@@ -25,7 +25,7 @@ VALUES
 ),
 (
 	'Sh(X)',
-	'cofiltered-limit-stable epimorphisms',
+	'trivial',
 	FALSE,
-	'Our <a href="/category/Set">counterexample for $\mathbf{Set}$</a> (using infinite intersections) also works in $\mathbf{Sh}(X)$ by using constant sheaves. We could also apply a variant of (the dual of) <a href="/lemma/filtered-monos">this lemma</a> to the constant sheaf functor $\mathbf{Set} \to \mathbf{Sh}(X)$, which does not preserve all cofiltered limits, but does preserve intersections.'
+	'This is because $X$ is assumed to be non-empty.'
 );

databases/catdat/data/004_category-implications/008_topos-theory-implications.sql

@@ -229,4 +229,11 @@ VALUES
 	'["natural numbers object"]',
 	'The triple $(1, \mathrm{id}_1, \mathrm{id}_1)$ is clearly a NNO.',
 	FALSE
+),
+(
+	'topos_no_stable_epis',
+	'["elementary topos", "countable coproducts", "cofiltered-limit-stable epimorphisms"]',
+	'["trivial"]',
+	'Let $N := \coprod_{m \in \mathbb{N}} 1$ and consider for every $n \in \mathbb{N}$ the subobject $N_{\geq n} = \coprod_{m \geq n} 1$ of $N$. For $n \leq n''$ we have $N_{\geq n''} \subseteq N_{\geq n}$. There is a (unique, split) epimorphism $N_{\geq n} \to 1$ for every $n$. By assumption, their limit $\lim_n N_{\geq n} \to 1$ is also an epimorphism. But $\lim_n N_{\geq n} = \bigcap_{n} N_{\geq n} = 0$. Thus, $0 \to 1$ is an epimorphism. It must be a regular epimorphism, but $0$ is strict initial, so that $0 \to 1$ is an isomorphism. Hence, $X \cong X \times 1 \cong X \times 0 \cong 0$ for all $X$.',
+	FALSE
 );