diff --git a/.vscode/settings.json b/.vscode/settings.json
index 76b8493e..9074afb3 100644
--- a/.vscode/settings.json
+++ b/.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",
diff --git a/databases/catdat/data/001_categories/100_related-categories.sql b/databases/catdat/data/001_categories/100_related-categories.sql
index 5fc756f0..2b76e80a 100644
--- a/databases/catdat/data/001_categories/100_related-categories.sql
+++ b/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'),
diff --git a/databases/catdat/data/002_category-properties/001_limits-colimits-existence.sql b/databases/catdat/data/002_category-properties/001_limits-colimits-existence.sql
index 69f42efd..91b81257 100644
--- a/databases/catdat/data/002_category-properties/001_limits-colimits-existence.sql
+++ b/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 here) is effective 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 has effective congruences 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 here) is effective 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 has effective cocongruences if every cocongruence in the category is effective.',
+ NULL,
+ 'effective congruences',
+ TRUE
+),
(
'cosifted limits',
'has',
diff --git a/databases/catdat/data/002_category-properties/100_related-category-properties.sql b/databases/catdat/data/002_category-properties/100_related-category-properties.sql
index c609e74e..35053691 100644
--- a/databases/catdat/data/002_category-properties/100_related-category-properties.sql
+++ b/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'),
diff --git a/databases/catdat/data/003_category-property-assignments/Alg(R).sql b/databases/catdat/data/003_category-property-assignments/Alg(R).sql
index 4db5c6c4..5b615ef0 100644
--- a/databases/catdat/data/003_category-property-assignments/Alg(R).sql
+++ b/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 this lemma to the forgetful functor $\CAlg(R) \to \Alg(R)$. It preserves epimorphisms by MSE/5133488.'
+),
+(
+ 'Alg(R)',
+ 'effective cocongruences',
+ FALSE,
+ 'The counterexample is similar to the one for $\Ring$: 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)$.'
);
diff --git a/databases/catdat/data/003_category-property-assignments/Cat.sql b/databases/catdat/data/003_category-property-assignments/Cat.sql
index 2c5f4d36..7e63e0ac 100644
--- a/databases/catdat/data/003_category-property-assignments/Cat.sql
+++ b/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 this lemma to the functor $\Set \to \Cat$ that maps a set to its discrete category.'
-);
\ No newline at end of file
+),
+(
+ 'Cat',
+ 'effective cocongruences',
+ FALSE,
+ 'The counterexample is similar to the one for $\Mon$: 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, \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$.'
+);
diff --git a/databases/catdat/data/003_category-property-assignments/FinGrp.sql b/databases/catdat/data/003_category-property-assignments/FinGrp.sql
index f711ffbd..a412f578 100644
--- a/databases/catdat/data/003_category-property-assignments/FinGrp.sql
+++ b/databases/catdat/data/003_category-property-assignments/FinGrp.sql
@@ -65,6 +65,12 @@ VALUES
TRUE,
'The proof works exactly as for the category of finite sets.'
),
+(
+ '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 this result, 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 and therefore reflects limits. 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.'
-);
\ No newline at end of file
+);
diff --git a/databases/catdat/data/003_category-property-assignments/FreeAb.sql b/databases/catdat/data/003_category-property-assignments/FreeAb.sql
index d6e0aa76..a9e7c494 100644
--- a/databases/catdat/data/003_category-property-assignments/FreeAb.sql
+++ b/databases/catdat/data/003_category-property-assignments/FreeAb.sql
@@ -84,6 +84,13 @@ VALUES
'sequential colimits',
FALSE,
'See MO/509715.'
+),
+(
+ '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$.
+ 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 MSE/720885.'
-);
\ No newline at end of file
+);
diff --git a/databases/catdat/data/003_category-property-assignments/Grp.sql b/databases/catdat/data/003_category-property-assignments/Grp.sql
index d15de7c1..ddbfa9b3 100644
--- a/databases/catdat/data/003_category-property-assignments/Grp.sql
+++ b/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 here.'
+),
(
'Grp',
'normal',
diff --git a/databases/catdat/data/003_category-property-assignments/Haus.sql b/databases/catdat/data/003_category-property-assignments/Haus.sql
index 8d70a7ec..5de2f067 100644
--- a/databases/catdat/data/003_category-property-assignments/Haus.sql
+++ b/databases/catdat/data/003_category-property-assignments/Haus.sql
@@ -65,6 +65,12 @@ VALUES
TRUE,
'See MO/509548.'
),
+(
+ 'Haus',
+ 'effective cocongruences',
+ TRUE,
+ 'As the proof at MO/509548 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',
diff --git a/databases/catdat/data/003_category-property-assignments/Man.sql b/databases/catdat/data/003_category-property-assignments/Man.sql
index 883066c1..8153e7a4 100644
--- a/databases/catdat/data/003_category-property-assignments/Man.sql
+++ b/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.
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',
diff --git a/databases/catdat/data/003_category-property-assignments/Meas.sql b/databases/catdat/data/003_category-property-assignments/Meas.sql
index 3cd30515..3ece3480 100644
--- a/databases/catdat/data/003_category-property-assignments/Meas.sql
+++ b/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 this lemma 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 $\Top$: Use the trivial $\sigma$-algebra on a two-point set.'
);
diff --git a/databases/catdat/data/003_category-property-assignments/Met.sql b/databases/catdat/data/003_category-property-assignments/Met.sql
index f3ab4aa0..f997bce5 100644
--- a/databases/catdat/data/003_category-property-assignments/Met.sql
+++ b/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 Johnstone, 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 MSE/1778408.'
-);
\ No newline at end of file
+),
+(
+ '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$.
+ On the other hand, if this cocongruence were effective, then by the dual of this result, 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$.'
+);
+
diff --git a/databases/catdat/data/003_category-property-assignments/Met_c.sql b/databases/catdat/data/003_category-property-assignments/Met_c.sql
index 855e50ec..ac615a5b 100644
--- a/databases/catdat/data/003_category-property-assignments/Met_c.sql
+++ b/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 MO/509548, 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 and therefore reflects colimits, we conclude that $E$ is effective in $\Met_\c$.'
+),
(
'Met_c',
'powers',
diff --git a/databases/catdat/data/003_category-property-assignments/Met_oo.sql b/databases/catdat/data/003_category-property-assignments/Met_oo.sql
index f46a0963..89723a17 100644
--- a/databases/catdat/data/003_category-property-assignments/Met_oo.sql
+++ b/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 this lemma 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 $\Met$ 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)$.'
);
diff --git a/databases/catdat/data/003_category-property-assignments/Mon.sql b/databases/catdat/data/003_category-property-assignments/Mon.sql
index 6361a214..d45a83be 100644
--- a/databases/catdat/data/003_category-property-assignments/Mon.sql
+++ b/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 MO/510431). 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 MO/510744 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.
+ 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$.'
);
-
diff --git a/databases/catdat/data/003_category-property-assignments/PMet.sql b/databases/catdat/data/003_category-property-assignments/PMet.sql
index 6085d837..bc184c83 100644
--- a/databases/catdat/data/003_category-property-assignments/PMet.sql
+++ b/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 Johnstone, 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 MSE/1778408.'
+),
+(
+ 'PMet',
+ 'effective cocongruences',
+ FALSE,
+ 'The proof is similar to the one for $\Top$: 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.'
);
diff --git a/databases/catdat/data/003_category-property-assignments/Pos.sql b/databases/catdat/data/003_category-property-assignments/Pos.sql
index 9609edef..352856d9 100644
--- a/databases/catdat/data/003_category-property-assignments/Pos.sql
+++ b/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$.
+ On the other hand, if this cocongruence on $\IR$ were effective, then by the dual of this result, $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.'
);
diff --git a/databases/catdat/data/003_category-property-assignments/Prost.sql b/databases/catdat/data/003_category-property-assignments/Prost.sql
index f229c8db..50170fde 100644
--- a/databases/catdat/data/003_category-property-assignments/Prost.sql
+++ b/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 this lemma 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.'
);
diff --git a/databases/catdat/data/003_category-property-assignments/Rel.sql b/databases/catdat/data/003_category-property-assignments/Rel.sql
index f7337d53..353689ba 100644
--- a/databases/catdat/data/003_category-property-assignments/Rel.sql
+++ b/databases/catdat/data/003_category-property-assignments/Rel.sql
@@ -71,6 +71,12 @@ VALUES
TRUE,
'A proof can be found here.'
),
+(
+ 'Rel',
+ 'effective congruences',
+ TRUE,
+ 'A proof can be found here.'
+),
(
'Rel',
'preadditive',
diff --git a/databases/catdat/data/003_category-property-assignments/Ring.sql b/databases/catdat/data/003_category-property-assignments/Ring.sql
index efd9a051..d80d7c72 100644
--- a/databases/catdat/data/003_category-property-assignments/Ring.sql
+++ b/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 this lemma applied to the forgetful functor $\CRing \to \Ring$. It preserves epimorphisms by MSE/5133488.'
-);
\ No newline at end of file
+),
+(
+ 'Ring',
+ 'effective cocongruences',
+ FALSE,
+ 'See MO/510744.'
+);
diff --git a/databases/catdat/data/003_category-property-assignments/Rng.sql b/databases/catdat/data/003_category-property-assignments/Rng.sql
index 1bcfc6a8..a4bcc88b 100644
--- a/databases/catdat/data/003_category-property-assignments/Rng.sql
+++ b/databases/catdat/data/003_category-property-assignments/Rng.sql
@@ -96,4 +96,16 @@ VALUES
'cofiltered-limit-stable epimorphisms',
FALSE,
'We know that $\Ring$ does not have this property. Now use the contrapositive of the dual of this lemma applied to the forgetful functor $\Ring \to \Rng$. We only need to verify that it preserves epimorphisms: Let $f : R \to S$ be an epimorphism in $\Ring$ and let $g,h : S \rightrightarrows T$ be two homomorphisms of rngs with $gf = hf$. The element $e = g(1) = h(1) \in T$ is idempotent, and $g,h$ become homomorphisms of rings $S \rightrightarrows eTe$. Hence, $g=h$.'
+),
+(
+ 'Rng',
+ 'effective cocongruences',
+ FALSE,
+ 'The counterexample is similar to the one at MO/510744 for $\Ring$: in this case,
+ $$X := \langle p \mid p^2 = p \rangle_{\Rng} \cong \IZ$$
+ and
+ $$E := \langle p, q \mid p^2 = p, q^2 = q, pq = q, qp = p \rangle_{\Rng} \cong \begin{pmatrix} \IZ & \IZ \\ 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 $\Ring$.'
);
diff --git a/databases/catdat/data/003_category-property-assignments/Set_c.sql b/databases/catdat/data/003_category-property-assignments/Set_c.sql
index b11d2b96..40d282fd 100644
--- a/databases/catdat/data/003_category-property-assignments/Set_c.sql
+++ b/databases/catdat/data/003_category-property-assignments/Set_c.sql
@@ -77,6 +77,12 @@ VALUES
TRUE,
'This is because $\{0,1\}$ is a subobject classifier in $\Set$, which is countable, and the monomorphisms coincide.'
),
+(
+ 'Set_c',
+ 'effective congruences',
+ TRUE,
+ 'Let $f, g : E \rightrightarrows X$ be a congruence in $\Set_\c$. Then using $1$ as a test object, we see that this induces an equivalence relation on $X$. We already know that $\Set$ has effective congruences (as does every topos). Using this result, we see that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set$. Also, the quotient $(X/E)_{\Set}$ is countable; and the forgetful functor $\Set_\c \to \Set$ is fully faithful and therefore reflects limits. Thus, we conclude that $E$ is the kernel pair of $X \to (X/E)_{\Set}$ in $\Set_\c$ as well.'
+),
(
'Set_c',
'small',
diff --git a/databases/catdat/data/003_category-property-assignments/Set_f.sql b/databases/catdat/data/003_category-property-assignments/Set_f.sql
index 075caa4d..92880ab6 100644
--- a/databases/catdat/data/003_category-property-assignments/Set_f.sql
+++ b/databases/catdat/data/003_category-property-assignments/Set_f.sql
@@ -41,6 +41,18 @@ VALUES
TRUE,
'A congruence on a set $X$ in $\Set_\f$ is the same as an equivalence relation $R$ on $X$ whose equivalence classes are finite. In that case, the usual quotient map $p : X \to X/R$ is finite-to-one. Moreover, if $h : X/R \to Y$ is a map such that $h \circ p : X \to Y$ is finite-to-one, then $h$ is finite-to-one as well because $h^*(\{y\}) \subseteq p^*((h \circ p)^*(\{y\}))$ for all $y \in Y$. Therefore, $p$ is also the quotient in $\Set_\f$.'
),
+(
+ 'Set_f',
+ 'effective congruences',
+ TRUE,
+ 'Let $f, g : E \rightrightarrows X$ be a congruence in $\Set_\f$. From the proof on quotients of congruences in $\Set_\f$, we have a quotient map $p : X \to X/E$ in $\Set_\f$, and $E$ is the kernel pair of $p$ in $\Set$. It remains to see that $E$ is also the kernel pair of $p$ in $\Set_f$. Thus, suppose we have $x_1, x_2 : T \rightrightarrows X$ with $p \circ x_1 = p \circ x_2$. Then there is a unique $e : T \to E$ in $\Set$ with $x_1 = f\circ e$ and $x_2 = g\circ e$. Since $f\circ e$ is finite-to-one, we must have $e$ is finite-to-one as well.'
+),
+(
+ 'Set_f',
+ 'effective cocongruences',
+ TRUE,
+ 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Set_f$. Then it is a coreflexive corelation in $\Set$. Since $\Set$ is co-Malcev and has effective cocongruences, that implies $E$ is the cokernel pair of some function $h : Z \to X$ in $\Set$. By the dual of this result, if $\inc_Y : Y \hookrightarrow X$ is the equalizer of $f$ and $g$, then $E$ is also the cokernel pair of $\inc_Y$ in $\Set$. It remains to see that $E$ is the cokernel pair of $\inc_Y$ in $\Set_\f$ as well. Thus, suppose $a, b : X \rightrightarrows T$ are such that $a |_Y = b |_Y$. Then there is a unique $c : E\to T$ in $\Set$ with $a = c\circ f$ and $b = c\circ g$. Since $(f;g) : X + X \to E$ is surjective and $c \circ (f;g) = (a;b)$ is finite-to-one, we see $c$ is finite-to-one as well.'
+),
(
'Set_f',
'locally cartesian closed',
@@ -132,4 +144,4 @@ VALUES
FALSE,
'We will prove that the family of singleton sets $(1)_{n \in \IN}$ has no multi-coproduct, generalizing the proof that the family does not have a coproduct given above. A cocone is just a map of sets $f : \IN \to X$. A morphism from $f : \IN \to X$ to $g : \IN \to Y$ is a finite-to-one map $h : X \to Y$ with $g = h \circ f$. This describes the category of cocones, and we need to show that it has no multi-initial object. To this end, we claim that the connected component of the unique map $! : \IN \to 1$ consists precisely of the maps $f : \IN \to X$ with finite image. Once that is established, we can recycle the proof for missing coproducts since there we have only used finite codomains.
Let $g = h \circ f$ be as above. If $\im(f)$ is finite, then $\im(g) = h_*(\im(f))$ is finite as well. Conversely, if $\im(g)$ is finite, then $\im(f) \subseteq \bigcup_{y \in \im(g)} h^*(\{y\})$ is finite as well. This shows that the connected component of $!$ is contained in the collection of maps with finite image. Conversely, if $f$ has finite image, then there is a morphism from the corestriction $f'' : \IN \to \im(f)$ to $f$, and also a morphism from $f''$ to $!$. This proves the remaining inclusion.'
-);
\ No newline at end of file
+);
diff --git a/databases/catdat/data/003_category-property-assignments/Set_pointed.sql b/databases/catdat/data/003_category-property-assignments/Set_pointed.sql
index 948787ef..cc41e9dc 100644
--- a/databases/catdat/data/003_category-property-assignments/Set_pointed.sql
+++ b/databases/catdat/data/003_category-property-assignments/Set_pointed.sql
@@ -67,6 +67,13 @@ VALUES
TRUE,
'The coproduct (wedge sum) of a family of pointed sets $(X_i)_{i \in I}$ can be realized as the subset of $\prod_{i \in I} X_i$ consisting of those tuples $x$ such that $x_i = 0$ for all but (at most) one index.'
),
+(
+ -- TODO: rework this when Barr-exact is added
+ 'Set*',
+ 'effective cocongruences',
+ TRUE,
+ 'We have that $\Set_*^{\op}$ is a slice category of $\Set^{\op}$, which in turn is monadic over $\Set$. Therefore, by combining results from Borceux and Bourn Appendix A and nLab, $\Set_*^{\op}$ is Barr-exact, and in particular it has effective congruences.'
+),
(
'Set*',
'skeletal',
diff --git a/databases/catdat/data/003_category-property-assignments/Setne.sql b/databases/catdat/data/003_category-property-assignments/Setne.sql
index b66a7605..83c35dfe 100644
--- a/databases/catdat/data/003_category-property-assignments/Setne.sql
+++ b/databases/catdat/data/003_category-property-assignments/Setne.sql
@@ -114,6 +114,12 @@ VALUES
TRUE,
'This follows from this lemma applied to the forgetful functor to $\Set$.'
),
+(
+ 'Setne',
+ 'effective congruences',
+ TRUE,
+ 'If a congruence $E \rightrightarrows X$ is the kernel pair of $h : X \to Z$, with both $E$ and $X$ non-empty, then certainly $Z$ must also be non-empty.'
+),
(
'Setne',
'sequential limits',
@@ -137,4 +143,11 @@ VALUES
'coquotients of cocongruences',
FALSE,
'The two maps $\{0\} \rightrightarrows \{0,1\}$ form a cocongruence on $\{0\}$ — namely the cofull cocongruence on $\{0\}$ — but they do not have an equalizer.'
-)
+),
+(
+ 'Setne',
+ 'effective cocongruences',
+ FALSE,
+ 'The two maps $\{0\} \rightrightarrows \{0,1\}$ form a cocongruence on $\{0\}$ — namely the cofull cocongruence on $\{0\}$ — but there is no map $Z \to \{0\}$ making the required commutative diagram, much less a cocartesian square.'
+);
+
diff --git a/databases/catdat/data/003_category-property-assignments/SetxSet.sql b/databases/catdat/data/003_category-property-assignments/SetxSet.sql
index b55ea360..c9228c13 100644
--- a/databases/catdat/data/003_category-property-assignments/SetxSet.sql
+++ b/databases/catdat/data/003_category-property-assignments/SetxSet.sql
@@ -23,6 +23,12 @@ VALUES
TRUE,
'Take the two-sorted algebraic theory with no operations and no equations.'
),
+(
+ 'SetxSet',
+ 'effective cocongruences',
+ TRUE,
+ 'Suppose we have a cocongruence $X \rightrightarrows E$ in $\Set \times \Set$. Then each component is a cocongruence, so they are the kernel pairs of some maps $Z_1\to X_1$, $Z_2 \to X_2$. Then $E$ is the cokernel pair of $(Z_1, Z_2) \to (X_1, X_2)$.'
+),
(
'SetxSet',
'skeletal',
diff --git a/databases/catdat/data/003_category-property-assignments/Top.sql b/databases/catdat/data/003_category-property-assignments/Top.sql
index 273bbdc2..6cc47954 100644
--- a/databases/catdat/data/003_category-property-assignments/Top.sql
+++ b/databases/catdat/data/003_category-property-assignments/Top.sql
@@ -130,4 +130,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 this lemma to the functor $\Set \to \Top$ which equips a set with the indiscrete topology.'
+),
+(
+ 'Top',
+ 'effective cocongruences',
+ FALSE,
+ 'Consider the indiscrete topological space $I$ on two points. This represents the functor which takes a topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $1 \rightrightarrows I$, where the maps are the two possible functions. However, this cannot be effective: if we have $h : Z\to 1$ which equalizes the two maps, then $Z$ must be empty. But that means the cokernel pair of $h$ is the discrete space on two points.'
);
diff --git a/databases/catdat/data/003_category-property-assignments/Top_pointed.sql b/databases/catdat/data/003_category-property-assignments/Top_pointed.sql
index df67cfa8..c69eaeec 100644
--- a/databases/catdat/data/003_category-property-assignments/Top_pointed.sql
+++ b/databases/catdat/data/003_category-property-assignments/Top_pointed.sql
@@ -168,7 +168,16 @@ VALUES
'cofiltered-limit-stable epimorphisms',
FALSE,
'We already know that $\Set_*$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\Set_* \to \Top_*$ that equips a pointed set with the indiscrete topology.'
+),
+(
+ 'Top*',
+ 'effective congruences',
+ FALSE,
+ 'Suppose that $\Top_*$ had effective congruences. Then by this result, $\Top$ would also have effective congruences, which we know is not the case (see here).'
+),
+(
+ 'Top*',
+ 'effective cocongruences',
+ FALSE,
+ 'This counterexample is adapted from the counterexample for $\Top$. Consider the pointed topological space $I := \{ *, a, b \}$ with topology $\{ \varnothing, \{ * \}, \{ a, b \}, \{ *, a, b \} \}$. This represents the functor which sends a pointed topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $\{ *, a \} \rightrightarrows I$ on the discrete space $\{ *, a \}$, where the maps are $*\mapsto *, a\mapsto a$ and $*\mapsto *, a\mapsto b$ respectively. However, this cannot be effective: if we have $h : Z \to \{ *, a \}$ which equalizes the cocongruence, then $h$ must be the constant function with value $*$. But that means the cokernel pair of $h$ is the discrete space on $\{ *, a, b \}$.'
);
-
-
-
diff --git a/databases/catdat/data/003_category-property-assignments/TorsFreeAb.sql b/databases/catdat/data/003_category-property-assignments/TorsFreeAb.sql
index d44b6edf..dc355d3a 100644
--- a/databases/catdat/data/003_category-property-assignments/TorsFreeAb.sql
+++ b/databases/catdat/data/003_category-property-assignments/TorsFreeAb.sql
@@ -72,11 +72,4 @@ VALUES
'CSP',
FALSE,
'The canonical homomorphism $\bigoplus_{n \geq 0} \IZ \to \prod_{n \geq 0} \IZ$ is injective, but not an epimorphism, since the quotient $\prod_{n \geq 0} \IZ / \bigoplus_{n \geq 0} \IZ$ is not torsion. In fact, it is torsion-free and non-zero.'
-),
-(
- -- TODO: rework this when effective congruences are added to the database
- 'TorsFreeAb',
- 'multi-algebraic',
- FALSE,
- 'Every multi-algebraic category has effective congruences, but the congruence $E = \{(x,y) \in \IZ^2 : 2 \mid x-y \}$ on $\IZ$ is not effective in $\TorsFreeAb$: Otherwise, the inclusion $E \hookrightarrow \IZ^2$ would be a regular monomorphism. By their classification below, $\IZ^2 / E$ would be torsion-free. But $(1,0) \notin E$ and $2 (1,0) \in E$.'
);
diff --git a/databases/catdat/data/003_category-property-assignments/Z.sql b/databases/catdat/data/003_category-property-assignments/Z.sql
index cd86a8f6..1be53edd 100644
--- a/databases/catdat/data/003_category-property-assignments/Z.sql
+++ b/databases/catdat/data/003_category-property-assignments/Z.sql
@@ -53,6 +53,18 @@ VALUES
TRUE,
'This follows immediately from the fact for $\Set$.'
),
+(
+ 'Z',
+ 'effective congruences',
+ TRUE,
+ 'If we have a congruence $E \rightrightarrows X$ in $[\CRing, \Set]$, then evaluating at any commutative ring gives a congruence in $\Set$. Defining $Y$ pointwise to be the quotient of this congruence, we get a morphism of functors $h : X \to Y$, and by this result applied pointwise, the kernel pair of $h$ is $E$.'
+),
+(
+ 'Z',
+ 'effective cocongruences',
+ TRUE,
+ 'If we have a cocongruence $X\rightrightarrows E$ in $[\CRing, \Set]$, then evaluating at any commutative gives a cocongruence in $\Set$. Defining $Y$ pointwise to be the equalizer of the pair, we get a morphism of functors $h : Y \to X$, and by the dual of this result applied pointwise, the cokernel pair of $h$ is $E$.'
+),
(
'Z',
'locally essentially small',
@@ -100,4 +112,4 @@ VALUES
'cofiltered-limit-stable epimorphisms',
FALSE,
'We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of this lemma to the functor $\Set \to [\CRing, \Set]$ that maps a set to its constant functor.'
-);
\ No newline at end of file
+);
diff --git a/databases/catdat/data/004_category-implications/004_morphism-behavior-implications.sql b/databases/catdat/data/004_category-implications/004_morphism-behavior-implications.sql
index 5b83b6b4..4196ec49 100644
--- a/databases/catdat/data/004_category-implications/004_morphism-behavior-implications.sql
+++ b/databases/catdat/data/004_category-implications/004_morphism-behavior-implications.sql
@@ -37,8 +37,8 @@ VALUES
(
'reflexive_pair_trivial',
'["left cancellative"]',
- '["reflexive coequalizers", "coreflexive equalizers"]',
- 'Any parallel pair of morphisms with a common section (or retraction) must be a pair of equal isomorphisms.',
+ '["reflexive coequalizers", "coreflexive equalizers", "effective congruences", "effective cocongruences"]',
+ 'Any parallel pair of morphisms with a common section (or retraction) must be a pair of equal isomorphisms. In particular, they are the kernel pair of the identity morphism on the target, and the cokernel pair of the identity morphism on the source.',
FALSE
),
(
@@ -192,8 +192,8 @@ VALUES
(
'core-hin_quotients',
'["core-thin"]',
- '["quotients of congruences"]',
- 'If $p_1, p_2 : E \rightrightarrows X$ is a congruence, the symmetry morphism $s : E \to E$ is an automorphism of $E$, hence equal to $\id_E$ by assumption. But then $p_1 = p_2 \circ s = p_2$, and simply $\id_X$ is a coequalizer.',
+ '["quotients of congruences", "effective congruences"]',
+ 'If $p_1, p_2 : E \rightrightarrows X$ is a congruence, the symmetry morphism $s : E \to E$ is an automorphism of $E$, hence equal to $\id_E$ by assumption. But then $p_1 = p_2 \circ s = p_2$, and simply $\id_X$ is a coequalizer. Also, for the reflexivity morphism $r : X \to E$, we have $p_1 \circ r = \id$. For the reverse composition, $p_1 \circ r \circ p_1 = p_1 \circ \id$ and $p_2 \circ r \circ p_1 = p_2 \circ \id$, so since $p_1, p_2$ are jointly monomorphic, we get $r \circ p_1 = \id$. Therefore, $p_1 = p_2$ is an isomorphism, so $E$ is the kernel pair of $\id_X$.',
FALSE
),
(
@@ -230,4 +230,4 @@ VALUES
'["subobject-trivial"]',
'This is because a monomorphism which is also a regular epimorphism is an isomorphism.',
FALSE
-);
\ No newline at end of file
+);
diff --git a/databases/catdat/data/004_category-implications/005_additional-structure-implications.sql b/databases/catdat/data/004_category-implications/005_additional-structure-implications.sql
index 24b71cdb..3cece9fb 100644
--- a/databases/catdat/data/004_category-implications/005_additional-structure-implications.sql
+++ b/databases/catdat/data/004_category-implications/005_additional-structure-implications.sql
@@ -27,6 +27,30 @@ VALUES
'This is trivial.',
FALSE
),
+(
+ 'preadditive_kernels_normal_imply_effective_congruences',
+ '["preadditive", "kernels", "normal"]',
+ '["effective congruences"]',
+ 'Let $f, g : E \rightrightarrows X$ be a congruence. Then let $E_0$ be the kernel of $g$. We see that $f|_{E_0} : E_0 \to X$ is a monomorphism. Let $f|_{E_0}$ be the kernel of a morphism $h : X \to Y$. We claim that $E$ is also the kernel pair of $h$.
+ To see this, suppose we have a pair of generalized elements $x_1, x_2 \in X(T)$. Then we have
+ $$\begin{align*}
+ (x_1,x_2) \in E & \iff (x_1 - x_2,0) \in E \\
+ & \iff x_1 - x_2 \in E_0 \\
+ & \iff h(x_1 - x_2) = 0 \\
+ & \iff h(x_1) = h(x_2).
+ \end{align*}$$
+ In particular, applying the forward implications in the case $T := E$, $x_1 := f$, $x_2 := g$, we conclude that $h \circ f = h \circ g$, so we get the required commutative diagram. From there, the reverse implications show this diagram is a cartesian square.',
+ FALSE
+),
+(
+ 'additive_effective_congruences_imply_normal',
+ '["additive", "finitely complete", "effective congruences"]',
+ '["normal"]',
+ 'Let $i : Y \hookrightarrow X$ be a monomorphism. Then the pullback $E$ of
+ $$X \times X \xrightarrow{p_1 - p_2} X \xhookleftarrow{~~~i~~~} Y$$
+ is a congruence on $X$. This is because for generalized elements $x_1, x_2 \in X(T)$, $(x_1, x_2)$ factors through $E$ if and only if $x_1 - x_2$ factors through $Y$. In other words, the relation on $X(T)$ is exactly $x_1 \equiv x_2 \pmod{Y(T)}$, which is an equivalence relation on $X(T)$ (and in fact a congruence in $\Ab$). Now by assumption, $E$ is the kernel pair of some morphism $h : X \to Z$; in other words, $(x_1, x_2)$ factors through $E$ if and only if $h(x_1) = h(x_2)$. In particular, for $x \in X(T)$, $x$ factors through $Y$ if and only if $(x, 0)$ factors through $E$, which is equivalent to $h(x) = h(0) = 0$. We have thus shown that $Y$ is the kernel of $h$.',
+ FALSE
+),
(
'additive_definition',
'["additive"]',
@@ -110,4 +134,4 @@ VALUES
'["trivial"]',
'This follows since the dual of a non-trivial Grothendieck abelian category cannot be Grothendieck abelian. See Peter Freyd, Abelian categories, p. 116.',
FALSE
-);
\ No newline at end of file
+);
diff --git a/databases/catdat/data/004_category-implications/007_locally-presentable-implications.sql b/databases/catdat/data/004_category-implications/007_locally-presentable-implications.sql
index e9555508..b801b7bc 100644
--- a/databases/catdat/data/004_category-implications/007_locally-presentable-implications.sql
+++ b/databases/catdat/data/004_category-implications/007_locally-presentable-implications.sql
@@ -223,10 +223,17 @@ VALUES
'This follows from one of equivalent formulations of multi-algebraic categories.',
TRUE
),
+(
+ 'multi-algebraic_implies_effective_congruences',
+ '["multi-algebraic"]',
+ '["effective congruences"]',
+ 'This is Thm. 4.0 in Yves Diers, Catégories Multialgébriques or its English translation.',
+ FALSE
+),
(
'locally-finitely-multi-presentable_stable-monos',
'["locally finitely multi-presentable"]',
'["filtered-colimit-stable monomorphisms"]',
'Every locally finitely multi-presentable category is a multi-reflective full subcategory of a presheaf category closed under filtered colimits (Adamek-Rosicky, 4.30). Since multi-reflective full subcategories are in general closed under connected limits (Adamek-Rosicky, Thm. 4.26), in particular, we can calculate not only filtered colimits but also kernel pairs as well as in a presheaf category.',
FALSE
-);
\ No newline at end of file
+);
diff --git a/databases/catdat/data/004_category-implications/008_topos-theory-implications.sql b/databases/catdat/data/004_category-implications/008_topos-theory-implications.sql
index ced55c45..c6d07917 100644
--- a/databases/catdat/data/004_category-implications/008_topos-theory-implications.sql
+++ b/databases/catdat/data/004_category-implications/008_topos-theory-implications.sql
@@ -121,8 +121,8 @@ VALUES
(
'topos_consequence',
'["elementary topos"]',
- '["finitely cocomplete", "disjoint finite coproducts", "epi-regular"]',
- 'See Mac Lane & Moerdijk, Cor. IV.5.4, Cor. IV.10.5, Thm. 4.7.8.',
+ '["finitely cocomplete", "disjoint finite coproducts", "epi-regular", "effective congruences"]',
+ 'See Mac Lane & Moerdijk, Cor. IV.5.4, Cor. IV.10.5, Thm. 4.7.8; and Johnstone, Part A, Proposition 2.4.1.',
FALSE
),
(
@@ -167,6 +167,41 @@ VALUES
'This is proven in Johnstone, A2.6.3 (for every quasitopos).',
FALSE
),
+(
+ 'regular_effective_congruences_implies_quotients',
+ '["regular", "effective congruences"]',
+ '["quotients of congruences"]',
+ 'We assume that every congruence is effective, and the regularity condition implies that every effective congruence has a quotient.',
+ FALSE
+),
+(
+ 'regular_epi-regular_extensive_consequences',
+ '["regular", "epi-regular", "extensive"]',
+ '["effective cocongruences", "co-Malcev"]',
+ 'Suppose we have a coreflexive corelation
+ $$X+X'' \xtwoheadrightarrow{p} E \xtwoheadrightarrow{r} X$$
+ on $X$, where we let $X''$ be an isomorphic copy of $X$ for clarity below. Let $Y$ be the equalizer of $p\circ i_1, p\circ i_2 : X \rightrightarrows E$. That means that for a generalized element $x \in X(T)$, $x \in Y(T)$ if and only if $p(x) = p(x'')$. Then by the assumptions $p$ is a regular epimorphism. By regularity, $p$ is the coequalizer of its kernel pair, which can be expressed as the equalizer $K$ of
+ $$p \circ \pi_1,\, p\circ \pi_2 : (X+X'') \times (X+X'') \rightrightarrows E,$$
+ where $\pi_1, \pi_2$ are the projections. By distributivity and extensivity, it is sufficient to calculate the equalizer on each "quadrant" of $(X+X'') \times (X+X'')$, i.e. the four copies of $X \times X$.
+ On the $X\times X$ quadrant, for generalized elements $x_1, x_2 \in X(T)$, we have $(x_1, x_2) \in K(T)$ if and only if $p(x_1) = p(x_2)$. Since $p\circ i_1$ is a split monomorphism, this is equivalent to $x_1 = x_2$. Thus, the $X\times X$ quadrant of $K$ is the diagonal of $X$. On the $X\times X''$ quadrant, we have $(x_1, x_2'')\in K(T)$ if and only if $p(x_1) = p(x_2'')$. Since $r(p(x_1)) = x_1$ and $r(p(x_2'')) = x_2$, this condition implies $x_1 = x_2$; and then by definition of $Y$, $x_1 = x_2 \in Y(T)$. The converse is straightforward. Thus, the $X\times X''$ quadrant of $K$ is the diagonal of $Y$. Similarly, the $X''\times X$ quadrant of $K$ is the diagonal of $Y$, and the $X''\times X''$ quadrant of $K$ is the diagonal of $X$.
+
+ Thus, we get that a morphism $h : X+X'' \to Z$ factors through $E$ if and only if $h(x) = h(x)$ for every generalized element $x \in X$; $h(y) = h(y'')$ for every $y \in Y$; $h(y'') = h(y)$ for every $y\in Y$; and $h(x'') = h(x'')$ for every $x \in X$. Clearly this is equivalent to $h(y) = h(y'')$ for every $y\in Y$, so in fact $E$ is the cokernel pair of $i_1 \circ \inc_Y$ and $i_2 \circ \inc_Y$. This means that $E$ is an effective cocongruence.
+
+ Remark: The assumptions are satisfied in particular for every elementary topos. Therefore, every elementary topos has effective cocongruences and is co-Malcev. This special case is Example 2.2.18 in Malcev, protomodular, homological and semi-abelian categories. An alternative proof of this special case is given later in A.5.17.',
+ FALSE
+),
+(
+ 'pretopos_balanced',
+ '["effective congruences", "extensive"]',
+ '["mono-regular"]',
+ 'Let $\alpha : A \hookrightarrow B$ be a monomorphism. Let $B''$ be a copy of $B$, and likewise let $A''$ be a copy of $A$. Consider the congruence on $B + B''$ generated by $y \sim y''$ for $y \in A$. Formally, we define $E := B + B'' + A + A''$ and define the two morphisms $f, g : E \rightrightarrows B + B''$ by extending the identity on $B + B''$ and
+ $$\begin{align*}
+ f(y) & = \alpha(y), & f(y'') & = \alpha(y)'', \\
+ g(y) & = \alpha(y)'', & g(y'') & = \alpha(y),
+ \end{align*}$$
+ on generalized elements. Extensivity can be used to show that $f, g$ are jointly monomorphic. Clearly, the pair $f, g$ is reflexive and symmetric. For transitivity, one once again uses extensivity. By assumption, there is a morphism $h : B + B'' \to C$ such that $f, g$ is the kernel pair of $h$, that is, two generalized elements $x, y \in B + B''$ satisfy $h(x) = h(y)$ if and only if $x = f(e)$, $y = g(e)$ for some $e \in E$. In particular, for $x \in B$, we have $h(x) = h(x'')$ if and only if $x = f(e)$, $x'' = g(e)$ for some $e \in E$. By disjointness of coproducts, we must necessarily have $e \in A$, and $x = \alpha(e)$. This shows that $\alpha$ is the equalizer of $h \circ i_1, h \circ i_2 : B \rightrightarrows C$.',
+ FALSE
+),
(
'lcc_implies_extensive',
'["locally cartesian closed", "disjoint finite coproducts"]',
@@ -181,18 +216,11 @@ VALUES
'The pullback functor preserves coproducts because it has a right adjoint. See also Remark 2.6 at the nLab.',
FALSE
),
-(
- 'topos_is_co-malcev',
- '["elementary topos"]',
- '["co-Malcev"]',
- 'This is Example 2.2.18 in Malcev, protomodular, homological and semi-abelian categories. An alternative proof is given later in A.5.17.',
- FALSE
-),
(
'subobject_classifier_disallows_malcev',
'["subobject classifier", "Malcev"]',
- '["thin"]',
- 'The subobject classifier $\Omega$ is an internal poset (cf. Mac Lane & Moerdijk, IV.8). Concretely, the intersection of subobjects yields a morphism $\wedge : \Omega \times \Omega \to \Omega$, and the internal relation ${\leq_{\Omega}} \subseteq \Omega \times \Omega$ is the equalizer of $\wedge, p_1 : \Omega \times \Omega \rightrightarrows \Omega$. The relation ${\leq_{\Omega}}$ is reflexive, hence symmetric by assumption. Since it also antisymmetric and has a largest element $\top$, every monomorphism must be an isomorphism. Applying this to equalizers, we see that the category is thin. (And from here, we can infer that it is trivial.)',
+ '["subobject-trivial"]',
+ 'The subobject classifier $\Omega$ is an internal poset (cf. Mac Lane & Moerdijk, IV.8). Concretely, the intersection of subobjects yields a morphism $\wedge : \Omega \times \Omega \to \Omega$, and the internal relation ${\leq_{\Omega}} \subseteq \Omega \times \Omega$ is the equalizer of $\wedge, p_1 : \Omega \times \Omega \rightrightarrows \Omega$. The relation ${\leq_{\Omega}}$ is reflexive, hence symmetric by assumption. Since it also antisymmetric and has a largest element $\top$, every monomorphism must be an isomorphism. (From here, we can infer that the category is trivial.)',
FALSE
),
(
@@ -236,4 +264,4 @@ VALUES
'["trivial"]',
'Let $N := \coprod_{m \in \IN} 1$ and consider for every $n \in \IN$ 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
-);
\ No newline at end of file
+);
diff --git a/databases/catdat/data/009_lemmas/001_lemmas.sql b/databases/catdat/data/009_lemmas/001_lemmas.sql
index dbb92647..8dd7794a 100644
--- a/databases/catdat/data/009_lemmas/001_lemmas.sql
+++ b/databases/catdat/data/009_lemmas/001_lemmas.sql
@@ -129,4 +129,36 @@ INSERT INTO lemmas (
'Construction of a colimit of a sequence of monomorphisms as a quotient of a congruence',
'Let $\C$ be a countably extensive category with quotients of congruences. Then $\C$ has colimits of sequences of monomorphisms.',
'Suppose we have a sequence $X_1 \hookrightarrow X_2 \hookrightarrow \cdots$ with corresponding monomorphisms $f_{m,n} : X_m \hookrightarrow X_n$ for $m \le n$. Define $Y$ to be the coproduct of all $X_n$. Now for each $m\le n$, define $E_{m,n} := X_m$ with two maps $i_m, i_n \circ f_{m,n} : E_{m,n} \rightrightarrows Y$, and similarly for $m \ge n$ define $E_{m,n} := X_n$ with two maps $i_m \circ f_{n,m}, i_n : E_{m,n} \rightrightarrows Y$. Then the coproduct of all $E_{m,n}$, with the induced morphisms to $Y$, forms a congruence. Here to prove the maps are jointly monomorphic, and again in proving transitivity, we use extensivity to split the domain of the generalized elements of $\sum_{m,n=1}^\infty E_{m,n}$ so that without loss of generality we may assume each factors through one of the coproduct inclusions. Now a quotient of this congruence must be a colimit of the sequence.'
+),
+(
+ 'effective-congruence-quotients',
+ 'Quotients of effective congruences are strict quotients',
+ 'Let $f, g : E \rightrightarrows X$ be an effective congruence. If $f, g$ have a coequalizer $p : X \to X/E$, then in fact we have a cartesian square
+ $$\begin{CD}
+ E @> f >> X \\
+ @V g VV @VV p V \\
+ X @>> p > X/E.
+ \end{CD}$$',
+ 'Suppose we have $h : X \to Z$ so that we have a cartesian square
+ $$\begin{CD}
+ E @> f >> X \\
+ @V g VV @VV h V \\
+ X @>> h > Z.
+ \end{CD}$$
+ Then by the universal property of the coequalizer, there is a unique morphism $$\bar h : X/E \to Z$$
+ such that $h = \bar h \circ p$. Now suppose we have generalized elements $x_1, x_2 : T \rightrightarrows X$ such that $p \circ x_1 = p \circ x_2$. Then
+ $$h \circ x_1 = \bar h \circ p \circ x_1 = \bar h \circ p \circ x_2 = h \circ x_2,$$
+ so the pair $x_1, x_2$ factors through $f, g : E \rightrightarrows X$. The uniqueness of the factorization follows from the assumption that $E$ is a congruence, so $f, g$ are jointly monomorphic.'
+),
+(
+ 'coslice-effective-congruences',
+ 'Inheritance of effective congruences in coslice categories',
+ 'Let $\C$ be an extensive category, and $A$ an object of $\C$. If the coslice category $A \backslash \C$ has effective congruences, then so does $\C$.',
+ 'Let $f, g : E \rightrightarrows X$ be a congruence in $\C$. We then construct a congruence on $A+X$ in $A \backslash \C$. On an intuitive level, this will be the congruence generated by $a \sim a$ for $a\in A$ and $x \sim y$ for $(x, y) \in E$. More precisely, we will show the two maps
+ $$\id_A + f,\, \id_A + g : A+E \rightrightarrows A+X$$
+ form a congruence. To show the pair of maps is jointly monomorphic, we use extensivity to split the domains of the generalized elements, so without loss of generality we may assume each comes from either $A$ or $E$. Reflexivity and symmetry are straightforward; and for transitivity, we again use extensivity to split the domains of the generalized elements, and provide an argument on each subdomain where the three generalized elements all come from either $A$ or $E$.
+ Now if this congruence is the kernel pair of $h : A+X \to Z$ in $A \backslash \C$, then $E$ is the kernel pair of $h \circ i_2 : X \to Z$ in $\C$. Namely, if we have two generalized elements $x_1, x_2 : T \rightrightarrows X$ such that $h \circ i_2 \circ x_1 = h \circ i_2 \circ x_2$, then we can construct a map pair
+ $$\id_A + x_1,\, \id_A + x_2 : A+T \rightrightarrows A+X$$
+ in $A \backslash \C$ with $h \circ (\id_A + x_1) = h \circ (\id_A + x_2)$. Therefore, $\id_A + x_1, \id_A + x_2$ factors through $A+E$ in $A \backslash \C$, so $x_1, x_2$ factors through $A+E$ in $\C$; and using disjoint coproducts, we may conclude $x_1, x_2$ factors through $E$.'
);
+
diff --git a/databases/catdat/scripts/expected-data/Ab.json b/databases/catdat/scripts/expected-data/Ab.json
index 409d8281..adf0df41 100644
--- a/databases/catdat/scripts/expected-data/Ab.json
+++ b/databases/catdat/scripts/expected-data/Ab.json
@@ -104,6 +104,8 @@
"filtered-colimit-stable monomorphisms": true,
"quotients of congruences": true,
"coquotients of cocongruences": true,
+ "effective congruences": true,
+ "effective cocongruences": true,
"cartesian closed": false,
"locally cartesian closed": false,
diff --git a/databases/catdat/scripts/expected-data/Set.json b/databases/catdat/scripts/expected-data/Set.json
index 7fe66a78..45f66146 100644
--- a/databases/catdat/scripts/expected-data/Set.json
+++ b/databases/catdat/scripts/expected-data/Set.json
@@ -99,6 +99,8 @@
"filtered-colimit-stable monomorphisms": true,
"quotients of congruences": true,
"coquotients of cocongruences": true,
+ "effective congruences": true,
+ "effective cocongruences": true,
"Grothendieck abelian": false,
"Malcev": false,
diff --git a/databases/catdat/scripts/expected-data/Top.json b/databases/catdat/scripts/expected-data/Top.json
index 6806592d..93cc5571 100644
--- a/databases/catdat/scripts/expected-data/Top.json
+++ b/databases/catdat/scripts/expected-data/Top.json
@@ -155,5 +155,7 @@
"gaunt": false,
"core-thin": false,
"subobject-trivial": false,
- "quotient-trivial": false
+ "quotient-trivial": false,
+ "effective congruences": false,
+ "effective cocongruences": false
}
diff --git a/src/lib/server/macros.ts b/src/lib/server/macros.ts
index ad50c81b..f6c1356d 100644
--- a/src/lib/server/macros.ts
+++ b/src/lib/server/macros.ts
@@ -49,6 +49,7 @@ export const MACROS = {
'\\Quot': '\\operatorname{Quot}',
'\\supp': '\\operatorname{supp}',
'\\Coexp': '\\operatorname{Coexp}',
+ '\\inc': '\\operatorname{inc}',
// categories
'\\Set': '\\mathbf{Set}',
'\\Rel': '\\mathbf{Rel}',
diff --git a/static/pdf/.gitignore b/static/pdf/.gitignore
new file mode 100644
index 00000000..372e1325
--- /dev/null
+++ b/static/pdf/.gitignore
@@ -0,0 +1,7 @@
+# Files from Latex Workshop
+*.aux
+*.fdb_latexmk
+*.fls
+*.log
+*.synctex.gz
+*.out
\ No newline at end of file
diff --git a/static/pdf/cocongruences_of_groups.pdf b/static/pdf/cocongruences_of_groups.pdf
new file mode 100644
index 00000000..f5bdf0b6
Binary files /dev/null and b/static/pdf/cocongruences_of_groups.pdf differ
diff --git a/static/pdf/cocongruences_of_groups.tex b/static/pdf/cocongruences_of_groups.tex
new file mode 100644
index 00000000..c6957f45
--- /dev/null
+++ b/static/pdf/cocongruences_of_groups.tex
@@ -0,0 +1,108 @@
+\documentclass[a4paper,12pt,reqno]{amsart}
+\usepackage[utf8]{inputenc}
+\usepackage[top=25truemm,bottom=25truemm,left=20truemm,right=20truemm]{geometry}
+\usepackage{parskip}
+\usepackage{tikz-cd}
+
+\usepackage{amsmath, amssymb, amsfonts, amscd, amsthm, mathtools}
+\usepackage{hyperref}
+
+\theoremstyle{plain}
+\newtheorem{prop}{Proposition}
+\newtheorem{cor}[prop]{Corollary}
+
+\theoremstyle{definition}
+\newtheorem{defi}[prop]{Definition}
+
+\DeclareMathOperator{\id}{id}
+\DeclareMathOperator{\eq}{eq}
+\DeclareMathOperator{\Grp}{\mathbf{Grp}}
+
+\newcommand{\C}{\mathcal{C}}
+
+\title{Cocongruences on groups are effective}
+\author{Martin Brandenburg}
+\date{\today}
+
+\begin{document}
+\maketitle
+
+Our goal is to prove that every cocongruence in the category $\Grp$ is effective. We will establish a more general result for categories in which pushouts and monomorphisms interact in a suitable way.
+
+\begin{defi}
+We shall say that a category $\C$ has \emph{good pushouts of monomorphisms} if it has pushouts of monomorphisms and if, for every diagram of monomorphisms
+\[\begin{tikzcd}
+B \ar{r} & B' \\
+A \ar{r} \ar{u} \ar{d} & A' \ar{u} \ar{d} \\
+C \ar{r} & C'
+\end{tikzcd}\]
+in which each square is a pullback, the induced morphism
+\[B \sqcup_A C \to B' \sqcup_{A'} C'\]
+is also a monomorphism.
+\end{defi}
+
+\begin{prop}
+The category $\Grp$ has good pushouts of monomorphisms.
+\end{prop}
+
+\begin{proof}
+Consider a diagram as above. We regard every monomorphism in it as an inclusion. Choose a system of representatives $S \subseteq B$ for the right $A$-cosets in $B$, meaning that the multiplication map $\cdot : A \times S \to B$ is bijective. Likewise, choose $T \subseteq C$ such that the multiplication map $\cdot : A \times T \to C$ is bijective. We may assume that $1 \in S$ and $1 \in T$.
+
+It is well known (see, for example, Serre's book \emph{Trees}, Ch.\ I, §1, Thm.\ 1) that every element of the amalgamated free product $B \sqcup_A C$ has a unique representation of the form
+\[w = a \cdot x_1 \cdots x_n,\]
+where $a \in A$, each $x_i$ lies either in $S \setminus \{1\}$ or in $T \setminus \{1\}$, and these choices alternate.
+
+The map
+\[A \backslash B \to A' \backslash B', \, Ab \mapsto A'b\]
+is injective. Indeed, if $b_1,b_2 \in B$ satisfy $A' b_1 = A' b_2$, then $b_1 b_2^{-1} \in A'$. Since $B \cap A' = A$, it follows that $b_1 b_2^{-1} \in A$, and hence $A b_1 = A b_2$.
+
+Therefore, we may extend $S$ to a system of representatives $S' \subseteq B'$ for the right $A'$-cosets in $B'$. Likewise, we may extend $T$ to a system of representatives $T' \subseteq C'$ for the right $A'$-cosets in $C'$.
+
+With respect to these systems, an element $w \in B \sqcup_A C$ written in normal form as above remains in normal form after being mapped to $B' \sqcup_{A'} C'$. This shows that the induced map is injective.
+\end{proof}
+
+\begin{prop}
+Let $\C$ be a balanced category with good pushouts of monomorphisms and equalizers of monomorphisms. Then every cocongruence in $\C$ is effective.
+\end{prop}
+
+\begin{proof}
+Let $X \in \C$ be an object, and let $i_1,i_2 : X \rightrightarrows Y$ be a cocongruence. Since it is coreflexive, there exists a morphism $r : Y \to X$ satisfying
+\[r \circ i_1 = \id_X, \quad r \circ i_2 = \id_X.\]
+In particular, $i_1$ and $i_2$ are monomorphisms. Since the cocongruence is cotransitive, there exists a morphism
+\[c : Y \to Y \sqcup_{i_2,X,i_1} Y\]
+satisfying
+\[c \circ i_1 = u_1 \circ i_1, \quad c \circ i_2 = u_2 \circ i_2,\]
+where $u_1,u_2 : Y \rightrightarrows Y \sqcup_{i_2,X,i_1} Y$ are the pushout inclusions satisfying $u_1 i_2 = u_2 i_1$. We will not use the fact that the cocongruence is cosymmetric; this will follow automatically. Define the monomorphism
+\[E := \eq(i_1,i_2) \hookrightarrow X.\]
+
+Since $i_1$ and $i_2$ agree on $E$, there exists a unique morphism
+\[\varphi : X \sqcup_E X \to Y\]
+defined by $\varphi \circ j_1 = i_1$ and $\varphi \circ j_2 = i_2$, where $j_1,j_2 : X \rightrightarrows X \sqcup_E X$ are the two inclusions.
+
+We must show that $\varphi$ is an isomorphism. It is clearly an epimorphism, since $i_1$ and $i_2$ are jointly epimorphic by assumption. Since $\C$ is balanced, it therefore suffices to prove that $\varphi$ is a monomorphism.
+
+We will show that even the morphism
+\[\gamma := c \circ \varphi : X \sqcup_E X \to Y \sqcup_{i_2,X,i_1} Y\]
+is a monomorphism. It is characterized by
+\[\gamma \circ j_1 = c \circ \varphi \circ j_1 = c \circ i_1 = u_1 \circ i_1,\]
+\[\gamma \circ j_2 = c \circ \varphi \circ j_2 = c \circ i_2 = u_2 \circ i_2.\]
+
+In other words, $\gamma$ is induced by the diagram of monomorphisms
+\[\begin{tikzcd}
+X \ar{r}{i_1} & Y \\
+E \ar{r} \ar{u} \ar{d} & X \ar{u}[swap]{i_2} \ar{d}{i_1} \\
+X \ar{r}[swap]{i_2} & Y
+\end{tikzcd}\]
+
+Since $\C$ has good pushouts of monomorphisms, it suffices to verify that both squares are pullbacks. Observe that the two squares are symmetric, so it is enough to consider one of them. To verify the universal property, let $a : T \to X$ and $b : T \to X$ be morphisms satisfying $i_1 \circ a = i_2 \circ b$. Applying $r : Y \to X$, we obtain
+\[a = r \circ i_1 \circ a = r \circ i_2 \circ b = b.\]
+
+Thus, $a$ is simply a morphism equalizing $i_1$ and $i_2$, so it factors uniquely through $E \hookrightarrow X$.
+\end{proof}
+
+\begin{cor}
+Every cocongruence in the category $\Grp$ is effective.
+\end{cor}
+
+
+\end{document}