Has effective (co)congruences properties

.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/002_category-properties/001_limits-colimits-existence.sql

@@ -343,6 +343,38 @@ VALUES
 	'quotients of congruences',
 	TRUE
 ),
+(
+	'effective congruences',
+	'has',
+	'A congruence $f, g : E \rightrightarrows X$ (see definition <a href="/category-property/quotients_of_congruences">here</a>) is <i>effective</i> if it is the kernel pair of some morphism, i.e. if there is a morphism $h : X \to Y$ such that we have a cartesian square
+	$$
+	\begin{CD}
+	E @> f >> X \\
+	@V g VV @VV h V \\
+	X @>> h > Y.
+	\end{CD}
+	$$
+	A category <i>has effective congruences</i> if every congruence in the category is effective.',
+	'https://ncatlab.org/nlab/show/congruence',
+	'effective cocongruences',
+	TRUE
+),
+(
+	'effective cocongruences',
+	'has',
+	'A cocongruence $f, g : X \rightrightarrows E$ (see definition <a href="/category-property/coquotients_of_cocongruences">here</a>) is <i>effective</i> if it is the cokernel pair of some morphism, i.e. if there is a morphism $h : Y \to X$ such that we have a cocartesian square
+	$$
+	\begin{CD}
+	Y @> h >> X \\
+	@V h VV @VV f V \\
+	X @>> g > E.
+	\end{CD}
+	$$
+	A category <i>has effective cocongruences</i> if every cocongruence in the category is effective.',
+	NULL,
+	'effective congruences',
+	TRUE
+),
 (
 	'cosifted limits',
 	'has',

databases/catdat/data/002_category-properties/100_related-category-properties.sql

@@ -293,9 +293,17 @@ VALUES
 ('quotients of congruences', 'coequalizers'),
 ('quotients of congruences', 'cokernels'),
 ('quotients of congruences', 'regular'),
+('quotients of congruences', 'effective congruences'),
 ('coquotients of cocongruences', 'equalizers'),
 ('coquotients of cocongruences', 'kernels'),
 ('coquotients of cocongruences', 'coregular'),
+('coquotients of cocongruences', 'effective cocongruences'),
+('effective congruences', 'normal'),
+('effective congruences', 'quotients of congruences'),
+('effective congruences', 'mono-regular'),
+('effective cocongruences', 'conormal'),
+('effective cocongruences', 'coquotients of cocongruences'),
+('effective cocongruences', 'epi-regular'),
 ('direct', 'one-way'),
 ('direct', 'skeletal'),
 ('inverse', 'one-way'),
@@ -341,15 +349,19 @@ VALUES
 ('cofiltered', 'finitely complete'),
 ('cofiltered', 'cofiltered limits'),
 ('mono-regular', 'normal'),
+('mono-regular', 'effective congruences'),
 ('mono-regular', 'subobject-trivial'),
 ('epi-regular', 'conormal'),
+('epi-regular', 'effective cocongruences'),
 ('epi-regular', 'quotient-trivial'),
 ('normal', 'zero morphisms'),
 ('normal', 'mono-regular'),
 ('normal', 'kernels'),
+('normal', 'effective congruences'),
 ('conormal', 'zero morphisms'),
 ('conormal', 'epi-regular'),
 ('conormal', 'cokernels'),
+('conormal', 'effective cocongruences'),
 ('multi-complete', 'complete'),
 ('multi-complete', 'multi-terminal object'),
 ('multi-terminal object', 'multi-complete'),

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">$\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">$\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, \C]$ is that $F \sim G$ if and only if $F$ and $G$ send the object of $X$ to the same object of $\C$, and they send the idempotent of $X$ to idempotent morphisms $a, b$ in $\C$ satisfying $ab=b$, $ba=a$. From here, the proof that this gives a cocongruence on $\Cat$ which is not effective is similar to the one in $\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 $\FinGrp$. Since the embedding $\FinGrp \hookrightarrow \Grp$ preserves finite limits, it is also a congruence in $\Grp$. We already know that $\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)_{\Grp}$ in $\Grp$. Also, the quotient $(X/E)_{\Grp}$ is finite; and the forgetful functor $\FinGrp \to \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)_{\Grp}$ in $\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 $\IZ \rightrightarrows E$ given by $1\mapsto a$, $1\mapsto b$. Note that $E$ is free with basis $\{ b, c \}$. Then $\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 $\IZ$.<br>
+	On the other hand, if $E$ were the cokernel pair of $h : H \to \IZ$, that would mean that for $x, y : \IZ \to G$, $x \equiv y \pmod{2G}$ if and only if $x \circ h = y \circ h$. In particular, from the case $G := \IZ$, $x := 2 \id$, $y := 0$, we would have $2h = 0$. That implies $h = 0$, but then that would give $\id_{\IZ} \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 $\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 $\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">$\Top$</a>: Use the trivial $\sigma$-algebra on a two-point set.'
 );

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

@@ -144,4 +144,22 @@ VALUES
 	'If $(N,z,s)$ is a natural numbers object in $\Met$, then
 	$$1 \xrightarrow{z} N \xleftarrow{s} N$$
 	is a coproduct cocone by <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, Part A, Lemma 2.5.5. Since there is a map $1 \to N$, we have $N \neq \varnothing$. However, the coproduct of two non-empty metric spaces does not exist, see <a href="https://math.stackexchange.com/questions/1778408" target="_blank">MSE/1778408</a>.'
-);
+),
+(
+	'Met',
+	'effective congruences',
+	FALSE,
+	'Any kernel pair of $h : X \to Z$ in $\Met$ corresponds to a closed subset of $X\times X$. However, there are plenty of non-closed congruences, such as $\Delta \cup (\IQ \times \IQ) \subseteq \IR \times \IR$ with the subspace metric.'
+),
+(
+	'Met',
+	'effective cocongruences',
+	FALSE,
+	'We will define a cocongruence on the interval $(0,1) \subseteq \IR$ where $E := (-1, 0) \cup (0, 1) \subseteq \IR$, and the two maps $(0, 1) \rightrightarrows E$ are the inclusion map and $x \mapsto -x$. Then for any metric space $X$, the induced relation on non-expansive maps $(0, 1) \to X$ is that $f \sim g$ if and only if
+	$$d(f(x), g(y)) \le x+y$$
+	for each $x, y \in (0, 1)$. This is reflexive since $d(f(x), f(y)) \le |x-y| < x+y$, and it is clearly symmetric. For transitivity, suppose $f\sim g$ and $g\sim h$.  Then for any $\varepsilon > 0$, we have
+	$$d(f(x), h(y)) \le d(f(x), g(\varepsilon)) + d(g(\varepsilon), h(y)) \le (x + \varepsilon) + (y + \varepsilon).$$
+	Since this holds for every $\varepsilon > 0$, we conclude $d(f(x), h(y)) \le x+y$.<br>
+	On the other hand, if this cocongruence were effective, then by the dual of <a href="/lemma/effective-congruence-quotients">this result</a>, it would be the cokernel pair of the equalizer of the two inclusion maps. However, that equalizer is empty, so $E$ would have to be a binary copower of $(0,1)$, which does not exist in $\Met$.'
+);
+

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

@@ -65,6 +65,12 @@ VALUES
 	TRUE,
 	'Every non-empty metric space is weakly terminal (by using constant maps).'
 ),
+(
+	'Met_c',
+	'effective cocongruences',
+	TRUE,
+	'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Met_\c$. Then the image in $\Haus$ is a coreflexive corelation (since epimorphisms in both categories are continuous maps with dense image). By <a href="https://mathoverflow.net/a/509582/2841" target="_blank">MO/509548</a>, that implies that image is of the form $X +_S X$ for a closed subset $S$ of $X$. Since $S$ is metrizable, and the functor $\Met_\c \to \Haus$ is fully faithful <a href="https://ncatlab.org/nlab/show/reflected+limit#FullSubcategoryInclusionReflectCoLimits" target="_blank">and therefore reflects colimits</a>, we conclude that $E$ is effective in $\Met_\c$.'
+),
 (
 	'Met_c',
 	'powers',

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

@@ -88,4 +88,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 \Met_{\infty}$ that equips a set with the discrete topology.'
+),
+(
+	'Met_oo',
+	'effective cocongruences',
+	FALSE,
+	'The same counterexample as for <a href="/category/Met">$\Met$</a> works here. The difference in this case is that a binary copower of two copies of $(0,1)$ does exist in $\Met_\infty$. However, this would assign a distance of $\infty$ between points in $(-1,0)$ and points in $(0,1)$, which does not agree with the chosen subspace metric on $(-1,0) \cup (0,1)$.'
 );

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

@@ -100,5 +100,16 @@ VALUES
 	'CSP',
 	FALSE,
 	'If $M \to N$ is an epimorphism in $\Mon$ and $M$ is infinite, then $\card(N) \leq \card(M)$ (see <a href="https://mathoverflow.net/questions/510431/" target="_blank">MO/510431</a>). This implies that in $\Mon$ the canonical homomorphism $\coprod_{n \geq 0} \IN \to \prod_{n \geq 0} \IN$ is not an epimorphism because its domain is countable and its codomain is uncountable.'
+),
+(
+	'Mon',
+	'effective cocongruences',
+	FALSE,
+	'We adapt the counterexample from <a href="https://mathoverflow.net/a/510809" target="_blank">MO/510744</a> for $\Ring$. Namely, consider the monoids
+	$$\begin{align*} X & := \langle p \mid p^2 = p \rangle \cong (\{ 0, 1 \}, \cdot),\\
+	E & := \langle p, q \mid p^2 = p,\, q^2 = q,\, pq = q,\, qp = p \rangle. \end{align*}$$
+	Then $X$ represents the functor sending a monoid $M$ to its idempotents, and $E$ represents the relation on idempotents $a, b$ of $M$ that $ab = b$, $ba = a$. The equations are equivalent to $aM = bM$, showing that the relation is indeed an equivalence relation.<br>
+	On the other hand, using the multiplicative map
+	$$E \to M_{2\times 2}(\IZ), \quad p \mapsto \begin{pmatrix} 1 & 0 \\ 0 & 0 \end{pmatrix},\quad q \mapsto \begin{pmatrix} 1 & 1 \\ 0 & 0 \end{pmatrix},$$
+	we can see that $p \ne q$ in $E$, so the equalizer of the two maps $X \rightrightarrows E$ is the trivial submonoid $\{ 1 \}$. Therefore, if $E$ were effective, it would be isomorphic to the coproduct $X \sqcup X$, whose underlying set consists of words in $p,q$ with $p,q$ strictly alternating. In particular, in this coproduct, $pq \ne q$.'
 );
-

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

@@ -138,4 +138,10 @@ VALUES
 	'If $(N,z,s)$ is a natural numbers object in $\PMet$, then
 	$$1 \xrightarrow{z} N \xleftarrow{s} N$$
 	is a coproduct cocone by <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, Part A, Lemma 2.5.5. Since there is a map $1 \to N$, we have $N \neq \varnothing$. However, the coproduct of two non-empty pseudo-metric spaces does not exist, see <a href="https://math.stackexchange.com/questions/1778408" target="_blank">MSE/1778408</a>.'
+),
+(
+	'PMet',
+	'effective cocongruences',
+	FALSE,
+	'The proof is similar to the one for <a href="/category/Top">$\Top$</a>: Equip a two-point set with the zero metric; this pseudo-metric space represents the functor taking a pseudo-metric space to the pairs of points with $d(x,y) = 0$. In this case, once you conclude $Z = \varnothing$, the map $h : Z \to 1$ does not have any cokernel pair, since that would have to be a coproduct $1+1$, which does not exist.'
 );

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

@@ -94,4 +94,11 @@ VALUES
 	'cofiltered-limit-stable epimorphisms',
 	FALSE,
 	'Pick any poset $X$ which has a decreasing sequence of non-empty sets $X = X_0 \supseteq X_1 \supseteq \cdots$ with empty intersection, such as $X_n = \IN_{\geq n}$ with the natural ordering. The unique map $X_n \to 1$ is surjective, but their limit $\varnothing \to 1$ is not surjective.'
+),
+(
+	'Pos',
+	'effective cocongruences',
+	FALSE,
+	'Let $X$ be $\IR$ with the standard (total) order, and let $E$ be the poset with underlying set $\IR \times \{ 0, 1 \}$ and partial order such that $(x, m) \le (y, n)$ if and only if $x < y$ or $(x, m) = (y, n)$. The two maps $\IR \rightrightarrows E$ will be $x \mapsto (x, 0)$ and $x \mapsto (x, 1)$ respectively. For any partial order $(\IP, \le)$, the induced equivalence relation on the set of order-preserving functions $\IR \to \IP$ is that $f \sim g$ if and only if $f(x) \le g(y)$ and $g(x) \le f(y)$ whenever $x < y$. This relation is clearly reflexive and symmetric; for transitivity, if $f \sim g$ and $g \sim h$, then whenever $x < y$, we have $f(x) \le g(\frac{x+y}{2}) \le h(y)$ and similarly $h(x) \le g(\frac{x+y}{2}) \le f(y)$, showing that $f \sim h$.<br>
+	On the other hand, if this cocongruence on $\IR$ were effective, then by the dual of <a href="/lemma/effective-congruence-quotients">this result</a>, $E$ would be the cokernel pair of the equalizer of the two maps $\IR \rightrightarrows E$. However, that equalizer is the empty poset, so $E$ would have to be the coproduct poset $\IR + \IR$, giving a contradiction.'
 );

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

@@ -100,4 +100,10 @@ VALUES
 	'cofiltered-limit-stable epimorphisms',
 	FALSE,
 	'We know that $\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 $\Set \to \Prost$ that equips a set with the chaotic preorder.'
+),
+(
+	'Prost',
+	'effective cocongruences',
+	FALSE,
+	'Consider the proset $E := \{ a, b \}$ with the chaotic preorder. This represents the functor which sends a proset to the pairs of elements $x,y$ with $x \le y$ and $y \le x$. Therefore, it defines a cocongruence $1 \rightrightarrows E$, where the maps are the two possible functions. However, this cannot be effective: for any map $h : Z \to 1$ which equalizes the two functions, $Z$ must be empty. But that means the cokernel pair of $h$ is the two-element proset with the trivial preorder.'
 );

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

@@ -71,6 +71,12 @@ VALUES
 	TRUE,
 	'A proof can be found <a href="/pdf/congruences_in_rel.pdf">here</a>.'
 ),
+(
+	'Rel',
+	'effective congruences',
+	TRUE,
+	'A proof can be found <a href="/pdf/congruences_in_rel.pdf">here</a>.'
+),
 (
 	'Rel',
 	'preadditive',

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

@@ -96,4 +96,10 @@ VALUES
 	'cofiltered-limit-stable epimorphisms',
 	FALSE,
 	'We know that $\CRing$ does not have this property. Now use the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> applied to the forgetful functor $\CRing \to \Ring$. It preserves epimorphisms by <a href="https://math.stackexchange.com/questions/5133488" target="_blank">MSE/5133488</a>.'
-);
+),
+(
+	'Ring',
+	'effective cocongruences',
+	FALSE,
+	'See <a href="https://mathoverflow.net/a/510809" target="_blank">MO/510744</a>.'
+);