malcev + topos => trivial

Author: ScriptRaccoon

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

@@ -71,12 +71,6 @@ VALUES
 	FALSE,
 	'This is trivial.'
 ),
-(
-	'FinSet',
-	'Malcev',
-	FALSE,
-	'There are lots of non-symmetric reflexive relations.'
-),
 (
 	'FinSet',
 	'countable',

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

@@ -29,12 +29,6 @@ VALUES
 	FALSE,
 	'This is trivial.'
 ),
-(
-	'M-Set',
-	'Malcev',
-	FALSE,
-	'Endow the set $\mathbb{N}$ with the trivial $M$-action, and consider the subset $\{(a,b) : a \leq b \}$ of $\mathbb{N}^2$.'
-),
 (
 	'M-Set',
 	'cofiltered-limit-stable epimorphisms',

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

@@ -35,12 +35,6 @@ VALUES
 	FALSE,
 	'This is trivial.'
 ),
-(
-	'Set',
-	'Malcev',
-	FALSE,
-	'There are lots of non-symmetric reflexive relations, for example $\leq$ on $\mathbb{N}$.'
-),
 (
 	'Set',
 	'cofiltered-limit-stable epimorphisms',

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

@@ -29,12 +29,6 @@ VALUES
 	FALSE,
 	'This is trivial.'
 ),
-(
-	'SetxSet',
-	'Malcev',
-	FALSE,
-	'There are lots of pairs of non-symmetric reflexive relations.'
-),
 (
 	'SetxSet',
 	'semi-strongly connected',

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

@@ -17,12 +17,6 @@ VALUES
 	TRUE,
 	'This holds by definition of a Grothendieck topos.'
 ),
-(
-	'Sh(X)',
-	'Malcev',
-	FALSE,
-	'Consider the subsheaf of $\underline{\mathbb{N}} \times \underline{\mathbb{N}}$ consisting of locally constant functions $(f,g) : X \to \mathbb{N} \times \mathbb{N}$ with $f \leq g$ pointwise. This is reflexive, but not symmetric.'
-),
 (
 	'Sh(X)',
 	'skeletal',

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

@@ -47,12 +47,6 @@ VALUES
 	FALSE,
 	'This is trivial.'
 ),
-(
-	'Sp',
-	'Malcev',
-	FALSE,
-	'Since $\mathbf{FinSet}$ is not Malcev, there is some finite set $X$ with a non-symmetric reflexive relation $R \subseteq X^2$. Now consider these as constant functors $\mathbb{B} \to \mathbf{FinSet}$.'
-),
 (
 	'Sp',
 	'semi-strongly connected',

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

@@ -41,12 +41,6 @@ VALUES
 	FALSE,
 	'This is trivial.'
 ),
-(
-	'sSet',
-	'Malcev',
-	FALSE,
-	'Any counterexample for $\mathbf{Set}$ (i.e., any non-symmetric reflexive relation) yields one for this category by taking constant simplicial sets.'
-),
 (
 	'sSet',
 	'finitary algebraic',

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

@@ -188,6 +188,13 @@ VALUES
 	'This is Example 2.2.18 in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>. An alternative proof is given later in A.5.17.',
 	FALSE
 ),
+(
+	'topos_is_never_malcev',
+	'["elementary topos", "Malcev"]',
+	'["trivial"]',
+	'The subobject classifier $\Omega$ is an internal Heyting algebra and hence an internal poset (see <a href="https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic" target="_blank">Mac Lane & Moerdijk</a>, IV.8). The relation $\leq$ on $\Omega$ is reflexive, hence symmetric by assumption. But then $\bot \leq \top$ in $\Omega$ implies $\top \leq \bot$, and hence $\bot = \top$. This means $1 \cong 0$ and hence $X \cong X \times 1 \cong X \times 0 \cong 0$ for all $X$.',
+	FALSE
+),
 (
 	'nno_assumption',
 	'["natural numbers object"]',