Decide effective (co)congruences for most categories

Note that ScriptRaccoon <scriptraccoon@gmail.com> contributed many enhancements to
the proofs and presentation, and in particular contributed the proof that Grp has
effective cocongruences.

Author: dschepler

.vscode/settings.json

@@ -105,6 +105,7 @@
 		"Diers",
 		"diffeomorphism",
 		"diffeomorphisms",
+		"disjointness",
 		"dualizable",
 		"Dualization",
 		"Eilenberg",
@@ -135,6 +136,7 @@
 		"hypercategory",
 		"hypercollection",
 		"hypercollections",
+		"idempotents",
 		"infima",
 		"infimum",
 		"infinitary",
@@ -185,6 +187,7 @@
 		"Prerendering",
 		"presheaf",
 		"presheaves",
+		"pretopos",
 		"procyclic",
 		"proset",
 		"prosets",

databases/catdat/data/001_categories/100_related-categories.sql

@@ -85,6 +85,7 @@ VALUES
 ('Met_oo', 'Met_c'),
 ('Mon', 'CMon'),
 ('Mon', 'Grp'),
+('Mon', 'Cat'),
 ('N', 'N_oo'),
 ('N', 'On'),
 ('N', 'Z_div'),

databases/catdat/data/003_category-property-assignments/Alg(R).sql

@@ -96,4 +96,10 @@ VALUES
 	'cofiltered-limit-stable epimorphisms',
 	FALSE,
 	'We already know that $\CAlg(R)$ does not have this property. Now apply the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> to the forgetful functor $\CAlg(R) \to \Alg(R)$. It preserves epimorphisms by <a href="https://math.stackexchange.com/questions/5133488" target="_blank">MSE/5133488</a>.'
+),
+(
+	'Alg(R)',
+	'effective cocongruences',
+	FALSE,
+	'The counterexample is similar to the one for <a href="/category/Ring">$\mathbf{Ring}$</a>: Let $X := R[p] / (p^2-p)$ with cocongruence $E := R \langle p, q \rangle / (p^2-p, q^2-q, pq-q, qp-p)$.'
 );

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

@@ -88,4 +88,12 @@ VALUES
 	'cofiltered-limit-stable epimorphisms',
 	FALSE,
 	'We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> to the functor $\Set \to \Cat$ that maps a set to its discrete category.'
-);
+),
+(
+	'Cat',
+	'effective cocongruences',
+	FALSE,
+	'The counterexample is similar to the one for <a href="/category/Mon">$\mathbf{Mon}$</a>: Let $X$ be the <a href="/category/walking_idempotent">walking idempotent</a>, and let $E$ be the delooping of the monoid with presentation
+	$$\langle p, q \mid p^2=p,\, q^2=q,\, pq=q,\, qp=p \rangle.$$
+	The induced relation on functors in $[X, \mathcal{C}]$ is that $F \sim G$ if and only if $F$ and $G$ send the object of $X$ to the same object of $\mathcal{C}$, and they send the idempotent of $X$ to idempotent morphisms $a, b$ in $\mathcal{C}$ satisfying $ab=b$, $ba=a$. From here, the proof that this gives a cocongruence on $\mathbf{Cat}$ which is not effective is similar to the one in $\mathbf{Mon}$.'
+);

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

@@ -65,6 +65,12 @@ VALUES
 	TRUE,
 	'The proof works exactly as for the <a href="/category/FinSet">category of finite sets</a>.'
 ),
+(
+	'FinGrp',
+	'effective congruences',
+	TRUE,
+	'Suppose we have a congruence $f, g : E \rightrightarrows X$ in $\mathbf{FinGrp}$. Since the embedding $\mathbf{FinGrp} \hookrightarrow \mathbf{Grp}$ preserves finite limits, it is also a congruence in $\mathbf{Grp}$. We already know that $\mathbf{Grp}$ has effective congruences since it is algebraic. Using <a href="/lemma/effective-congruence-quotients">this result</a>, we see that $E$ is the kernel pair of $X \to (X/E)_{\mathbf{Grp}}$ in $\mathbf{Grp}$. Also, the quotient $(X/E)_{\mathbf{Grp}}$ is finite; and the forgetful functor $\mathbf{FinGrp} \to \mathbf{Grp}$ is fully faithful <a href="https://ncatlab.org/nlab/show/reflected+limit#FullSubcategoryInclusionReflectCoLimits" target="_blank">and therefore reflects limits</a>. Thus, we conclude that $E$ is the kernel pair of $X \to (X/E)_{\mathbf{Grp}}$ in $\mathbf{FinGrp}$ as well.'
+),
 (
 	'FinGrp',
 	'normal',
@@ -118,4 +124,4 @@ VALUES
 	'countable',
 	FALSE,
 	'This is trivial.'
-);
+);

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

@@ -84,6 +84,13 @@ VALUES
 	'sequential colimits',
 	FALSE,
 	'See <a href="https://mathoverflow.net/questions/509715" target="_blank">MO/509715</a>.'
+),
+(
+	'FreeAb',
+	'effective cocongruences',
+	FALSE,
+	'We will let $E$ be the abelian group with presentation $\langle a, b, c \mid a - b = 2c \rangle$, with two morphisms $\mathbb{Z} \rightrightarrows E$ given by $1\mapsto a$, $1\mapsto b$. Note that $E$ is free with basis $\{ b, c \}$. Then $\operatorname{Hom}(E, G) \cong \{ (x, y, z) \in G^3 \mid x - y = 2z \}$. Observe that since $G$ is torsion-free, the projection onto the first two coordinates is injective; and $(x, y)$ is in the image precisely when $x \equiv y \pmod{2G}$, which gives an equivalence relation. Therefore, $E$ gives a cocongruence on $\mathbb{Z}$.<br>
+	On the other hand, if $E$ were the cokernel pair of $h : H \to \mathbb{Z}$, that would mean that for $x, y : \mathbb{Z} \to G$, $x \equiv y \pmod{2G}$ if and only if $x \circ h = y \circ h$. In particular, from the case $G := \mathbb{Z}$, $x := 2 \operatorname{id}$, $y := 0$, we would have $2h = 0$. That implies $h = 0$, but then that would give $\operatorname{id}_{\mathbb{Z}} \equiv 0 \pmod{2}$, resulting in a contradiction.'
 );
 
 INSERT INTO category_property_comments (category_id, property_id, comment)
@@ -92,4 +99,4 @@ VALUES
     'FreeAb',
     'accessible',
     'The question if this category is accessible is undecidable in ZFC. See <a href="https://math.stackexchange.com/questions/720885" target="_blank">MSE/720885</a>.'
-);
+);

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

@@ -47,6 +47,12 @@ VALUES
 	TRUE,
 	'Since epimorphisms are surjective (see below), this is the first isomorphism theorem for groups.'
 ),
+(
+	'Grp',
+	'effective cocongruences',
+	TRUE,
+	'A proof can be found <a href="/pdf/cocongruences_of_groups.pdf">here</a>.'
+),
 (
 	'Grp',
 	'normal',

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

@@ -65,6 +65,12 @@ VALUES
     TRUE,
     'See <a href="https://mathoverflow.net/a/509582/2841" target="_blank">MO/509548</a>.'
 ),
+(
+	'Haus',
+	'effective cocongruences',
+	TRUE,
+	'As the proof at <a href="https://mathoverflow.net/a/509582/2841" target="_blank">MO/509548</a> shows, in fact any coreflexive corelation on $X$ in $\mathbf{Haus}$ is of the form $X +_S X$ for a closed subset $S$ of $X$. Such a cocongruence is clearly effective.'
+),
 (
 	'Haus',
 	'cartesian filtered colimits',

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

@@ -80,6 +80,12 @@ VALUES
 	Because $r \circ (p \circ i_1) : X \to X$ is the identity, the image of $p \circ i_1$ is the equalizer of $\id_E$ and $(p \circ i_1) \circ r$, hence closed. Likewise, the image of $p \circ i_2$ is closed. Thus, the image of $p$, which is the union of these images, is closed.<br>
 	Now, since the pushforward maps of tangent spaces compose to the identity, we see that $p$ must be a local immersion and $r$ must be a submersion.  Also, since the fibers of $r$ have one or two points each, we see that the dimension of $E$ must locally be the same as the dimension of $X$.  This implies that in fact $p$ and $r$ are local diffeomorphisms.  Therefore, the cardinality of the fiber of $r$ is locally constant.  Thus, if $U$ is the subset of $X$ where $r$ has fiber of a single point, with the subspace topology, then $U$ is a clopen submanifold of $X$ which serves as the equalizer of $p \circ i_1$ and $p \circ i_2$.'
 ),
+(
+	'Man',
+	'effective cocongruences',
+	TRUE,
+	'From the proof that $\mathbf{Man}$ has coquotients of cocongruences, we know that for any cocongruence $X \rightrightarrows E$, there is a clopen submanifold $U$ of $X$ such that the fibers of $r : E \twoheadrightarrow X$ have one point on $U$, and two points on $X \setminus U$. Therefore, $E$ is the cokernel pair of the inclusion map $U \hookrightarrow X$.'
+),
 (
 	'Man',
 	'small',

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

@@ -100,4 +100,10 @@ VALUES
 	'cofiltered-limit-stable epimorphisms',
 	FALSE,
 	'We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> to the functor $\Set \to \Meas$ which equips a set with the trivial $\sigma$-algebra.'
+),
+(
+	'Meas',
+	'effective cocongruences',
+	FALSE,
+	'The proof is similar to the one for <a href="/category/Top">$\mathbf{Top}$</a>: Use the trivial $\sigma$-algebra on a two-point set.'
 );