various minor adjustments

Author: ScriptRaccoon

.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

@@ -83,6 +83,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/Cat.sql

@@ -93,5 +93,7 @@ VALUES
 	'Cat',
 	'effective cocongruences',
 	FALSE,
-	'The counterexample is similar to the one for <a href="/category/Mon">$\mathbf{Mon}$</a>: Let $X$ be the walking idempotent, 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 idempotents $a, b$ 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}$.'
+	'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

@@ -69,8 +69,7 @@ VALUES
 	'FinGrp',
 	'effective congruences',
 	TRUE,
-	'Suppose we have a congruence $f, g : E \rightrightarrows X$. This induces a monomorphism $(f, g) : E \hookrightarrow X \times X$, which is thus an injective group homomorphism (see below). The image is also clearly a reflexive and symmetric relation. Furthermore, since the forgetful functor to $\mathbf{Set}$ preserves pullbacks, and transitivity gives a morphism $E \times_{p_2, X, p_1} E \to E$ in $\mathbf{FinGrp}$, it also gives a transitivity morphism in $\mathbf{Set}$, showing that the image is transitive.<br>
-	Therefore, the image of $E \hookrightarrow X \times X$ induces a congruence in $\mathbf{Grp}$. We already know that $\mathbf{Grp}$ has effective congruences since it is multi-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.'
+	'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',

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

@@ -89,7 +89,7 @@ VALUES
 	'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) \simeq \{ (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>
+	'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.'
 );
 

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

@@ -155,7 +155,11 @@ VALUES
 	'Met',
 	'effective cocongruences',
 	FALSE,
-	'We will define a cocongruence on $(0,1)$ where $E := (-1, 0) \cup (0, 1)$ with the standard subspace metric from $\mathbb{R}$, 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>
+	'We will define a cocongruence on the interval $(0,1) \subseteq \mathbb{R}$ where $E := (-1, 0) \cup (0, 1) \subseteq \mathbb{R}$, 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 $\mathbf{Met}$.'
 );
 

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

@@ -69,7 +69,7 @@ VALUES
 	'Met_c',
 	'effective cocongruences',
 	TRUE,
-	'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\mathbf{Met}_\mathrm{c}$. Then the image in $\mathbf{Haus}$ is a coreflexive corelation. 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 $\mathbf{Met}_\mathrm{c} \to \mathbf{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 $\mathbf{Met}_\mathrm{c}$.'
+	'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\mathbf{Met}_\mathrm{c}$. Then the image in $\mathbf{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 $\mathbf{Met}_\mathrm{c} \to \mathbf{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 $\mathbf{Met}_\mathrm{c}$.'
 ),
 (
 	'Met_c',

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

@@ -105,6 +105,11 @@ VALUES
 	'Mon',
 	'effective cocongruences',
 	FALSE,
-	'We adapt the counterexample from <a href="https://mathoverflow.net/a/510809" target="_blank">MO/510744</a> for $\mathbf{Ring}$. Namely, let $X$ be the multiplicative monoid of $\{ 0, 1 \}$, which has presentation $\langle p \mid p^2 = p \rangle$, and let $E$ be the monoid with presentation $\langle p, q \mid p^2 = p, q^2 = q, pq = q, qp = p \rangle$. 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$. This is clearly reflexive and symmetric. For transitivity, suppose $ab = b, ba = a, bc = c, cb = b$. Then $ac = a(bc) = (ab)c = bc = c$ and $ca = c(ba) = (cb)a = ba = a$. Therefore, $E$ is a cocongruence on $X$.<br>
-	On the other hand, using the map of $E$ to the multiplicative monoid of $M_{2\times 2}(\mathbb{Z})$ with $p \mapsto \begin{bmatrix} 1 & 0 \\ 0 & 0 \end{bmatrix}, q \mapsto \begin{bmatrix} 1 & 1 \\ 0 & 0 \end{bmatrix}$, 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$, which can be expressed as the set of words in $p,q$ with $p,q$ strictly alternating. In particular, in this coproduct, $pq \ne q$.'
+	'We adapt the counterexample from <a href="https://mathoverflow.net/a/510809" target="_blank">MO/510744</a> for $\mathbf{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}(\mathbb{Z}), \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/Pos.sql

@@ -99,6 +99,6 @@ VALUES
 	'Pos',
 	'effective cocongruences',
 	FALSE,
-	'Let $X$ be $\mathbb{R}$ with the standard (total) order, and let $E$ be the poset with underlying set $\mathbb{R} \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 $\mathbb{R} \rightrightarrows E$ will be $x \mapsto (x, 0)$ and $x \mapsto (x, 1)$ respectively. For any partial order $(\mathbb{P}, \le)$, the induced equivalence relation on the set of order-preserving functions $\mathbb{R} \to \mathbb{P}$ 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 whenver $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>
+	'Let $X$ be $\mathbb{R}$ with the standard (total) order, and let $E$ be the poset with underlying set $\mathbb{R} \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 $\mathbb{R} \rightrightarrows E$ will be $x \mapsto (x, 0)$ and $x \mapsto (x, 1)$ respectively. For any partial order $(\mathbb{P}, \le)$, the induced equivalence relation on the set of order-preserving functions $\mathbb{R} \to \mathbb{P}$ 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 $\mathbb{R}$ 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 $\mathbb{R} \rightrightarrows E$. However, that equalizer is the empty poset, so $E$ would have to be the coproduct poset $\mathbb{R} + \mathbb{R}$, giving a contradiction.'
 );

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

@@ -101,5 +101,11 @@ VALUES
 	'Rng',
 	'effective cocongruences',
 	FALSE,
-	'The counterexample is similar to the one at <a href="https://mathoverflow.net/a/510809" target="_blank">MO/510744</a> for $\mathbf{Ring}$: in this case, $X := \langle p \mid p^2 = p \rangle$ is isomorphic to the rng $\mathbb{Z}$, and $E := \langle p, q \mid p^2 = p, q^2 = q, pq = q, qp = p \rangle$ is isomorphic to the rng $\begin{bmatrix} \mathbb{Z} & \mathbb{Z} \\ 0 & 0 \end{bmatrix}$ via $p \mapsto \begin{bmatrix} 1 & 0 \\ 0 & 0 \end{bmatrix}$, $q \mapsto \begin{bmatrix} 1 & 1 \\ 0 & 0 \end{bmatrix}$. From here, the rest of the proof is similar to the one for $\mathbf{Ring}$.'
+	'The counterexample is similar to the one at <a href="https://mathoverflow.net/a/510809" target="_blank">MO/510744</a> for $\mathbf{Ring}$: in this case,
+	$$X := \langle p \mid p^2 = p \rangle_{\mathbf{Rng}} \cong \mathbb{Z}$$
+	and
+	$$E := \langle p, q \mid p^2 = p, q^2 = q, pq = q, qp = p \rangle_{\mathbf{Rng}}  \cong \begin{pmatrix} \mathbb{Z} & \mathbb{Z} \\ 0 & 0 \end{pmatrix}$$
+	via
+	$$p \mapsto \begin{pmatrix} 1 & 0 \\ 0 & 0 \end{pmatrix}, \quad q \mapsto \begin{pmatrix} 1 & 1 \\ 0 & 0 \end{pmatrix}.$$
+	From here, the rest of the proof is similar to the one for $\mathbf{Ring}$.'
 );