diff --git a/content/cocongruences_in_extensive_categories.md b/content/cocongruences_in_extensive_categories.md
index 6b66d92b9..31aa5a27e 100644
--- a/content/cocongruences_in_extensive_categories.md
+++ b/content/cocongruences_in_extensive_categories.md
@@ -8,13 +8,13 @@ description: This gives some results on cocongruences in extensive categories wi
We start with a general fact which is easier to visualize for the dual case of congruences.
::: Lemma 1
-Let $q_1, q_2 : E \rightrightarrows X$ be a congruence such that the pullback $E \times_X E$ of $q_2$ and $q_1$ exists, and let $t : E \times_X E \to E$ be the transitivity morphism. Then we have pushout diagrams
+Let $q_1, q_2 : R \rightrightarrows X$ be a congruence such that the pullback $R \times_X R$ of $q_2$ and $q_1$ exists, and let $t : R \times_X R \to R$ be the transitivity morphism. Then we have pushout diagrams
$$
\begin{CD}
-E \times_X E @> p_1 >> E @. \quad @. E \times_X E @> p_2 >> E \\
+R \times_X R @> p_1 >> R @. \quad @. R \times_X R @> p_2 >> R \\
@V t VV @VV q_1 V @. @V t VV @VV q_2 V \\
-E @> q_1 >> X @. \quad @. E @> q_2 >> X.
+R @> q_1 >> X @. \quad @. R @> q_2 >> X.
\end{CD}
$$
@@ -25,17 +25,17 @@ Suppose we have a commutative square
$$
\begin{CD}
-E \times_X E @> p_1 >> E \\
+R \times_X R @> p_1 >> R \\
@V t VV @VV f V \\
-E @> g >> T.
+R @> g >> T.
\end{CD}
$$
-Then for any generalized element $(x, y)$ of $E$, consider the generalized elements $((x, x), (x, y))$ and $((x, y), (y, y))$ of $E \times_X E$. From the commutativity of the square acting on these generalized elements, we have
+Then for any generalized element $(x, y)$ of $R$, consider the generalized elements $((x, x), (x, y))$ and $((x, y), (y, y))$ of $R \times_X R$. From the commutativity of the square acting on these generalized elements, we have
$$f(x, x) = g(x, y)$$
and
$$f(x, y) = g(x, y).$$
-Therefore, if we define $h : X \to T$ on generalized elements by $h(x) \coloneqq f(x, x)$, we must have $f = h \circ q_1$ and $g = h \circ q_1$. Conversely, if $h$ is a morphism with $f = h \circ q_1$, we have $h(x)=f(x,y)$ for all $(x,y) \in E$, which for $y=x$ yields $h(x)=f(x,x)$.
+Therefore, if we define $h : X \to T$ on generalized elements by $h(x) \coloneqq f(x, x)$, we must have $f = h \circ q_1$ and $g = h \circ q_1$. Conversely, if $h$ is a morphism with $f = h \circ q_1$, we have $h(x)=f(x,y)$ for all $(x,y) \in R$, which for $y=x$ yields $h(x)=f(x,x)$.
This concludes the proof that the first diagram is a pushout diagram; the proof for the second is similar.
:::
@@ -80,27 +80,27 @@ On the other hand, from $(f_1; f_2)(s) = (f_1; f_2)(s')$, we conclude $f_1(a_1)
:::
::: Corollary 3
-Let $j_1, j_2 : X \rightrightarrows E$ be a cocongruence in an extensive category such that the pushout $E +_X E$ of $j_2$ and $j_1$ exists, and let $t : E \to E +_X E$ be the corresponding cotransitivity morphism. Then we have a pullback diagram
+Let $j_1, j_2 : X \rightrightarrows C$ be a cocongruence in an extensive category such that the pushout $C +_X C$ of $j_2$ and $j_1$ exists, and let $t : C \to C +_X C$ be the corresponding cotransitivity morphism. Then we have a pullback diagram
$$
\begin{CD}
-X + X @> (j_1; j_2) >> E \\
+X + X @> (j_1; j_2) >> C \\
@V j_1 + j_2 VV @VV t V \\
-E + E @>>> E +_X E.
+C + C @>>> C +_X C.
\end{CD}
$$
-In particular, if the category also has pullback-stable regular epimorphisms, then for any cocongruence $j_1, j_2 : X \rightrightarrows E$ such that the pushout of $j_2$ and $j_1$ exists, the corresponding morphism $(j_1; j_2) : X + X \to E$ is a regular epimorphism.
+In particular, if the category also has pullback-stable regular epimorphisms, then for any cocongruence $j_1, j_2 : X \rightrightarrows C$ such that the pushout of $j_2$ and $j_1$ exists, the corresponding morphism $(j_1; j_2) : X + X \to C$ is a regular epimorphism.
:::
::: Proof
-The pullback diagram comes from using Lemma 2 on the two pullback diagrams from the dual of Lemma 1. For the other conclusion, all we need to establish is that $E + E \to E +_X E$ is a regular epimorphism. However, this is immediate from the fact that the pushout $E +_X E$ is also a coequalizer of $i_1 \circ j_2, i_2 \circ j_1 : X \rightrightarrows E + E$ (cf. [this implication](/category-implication/dual_pullbacks_criterion)).
+The pullback diagram comes from using Lemma 2 on the two pullback diagrams from the dual of Lemma 1. For the other conclusion, all we need to establish is that $C + C \to C +_X C$ is a regular epimorphism. However, this is immediate from the fact that the pushout $C +_X C$ is also a coequalizer of $i_1 \circ j_2, i_2 \circ j_1 : X \rightrightarrows C + C$ (cf. [this implication](/category-implication/dual_pullbacks_criterion)).
:::
-In the following results, define a regular corelation to be a corelation $j_1, j_2 : X \rightrightarrows E$ such that the binary copower of $X$ exists, and $(j_1; j_2) : X + X \to E$ is a regular epimorphism.
+In the following results, define a regular corelation to be a corelation $j_1, j_2 : X \rightrightarrows C$ such that the binary copower of $X$ exists, and $(j_1; j_2) : X + X \to C$ is a regular epimorphism.
::: Lemma 4
-In an extensive category, every regular coreflexive corelation $j_1, j_2 : X \rightrightarrows E$ such that the equalizer of $j_1$ and $j_2$ exists is an effective cocongruence.
+In an extensive category, every regular coreflexive corelation $j_1, j_2 : X \rightrightarrows C$ such that the equalizer of $j_1$ and $j_2$ exists is an effective cocongruence.
:::
::: Proof
@@ -113,7 +113,7 @@ $$
\end{align*}
$$
-is a kernel pair of $(j_1; j_2) : X + X \to E$.
+is a kernel pair of $(j_1; j_2) : X + X \to C$.
Informally, we can think of this as the subobject of $(X + X)^2 \cong \sum_{i,j=1}^2 X^2$ which is the diagonal of $X$ in the first and fourth quadrants, and the diagonal of $Y$ in the second and third quadrants.
To see this, note that since $j_1$ is a (split) monomorphism, we have a pullback diagram
@@ -122,7 +122,7 @@ $$
\begin{CD}
X @> \id >> X \\
@V \id VV @VV j_1 V \\
-X @>> j_1 > E.
+X @>> j_1 > C.
\end{CD}
$$
@@ -132,11 +132,11 @@ $$
\begin{CD}
Y @> e >> X \\
@V e VV @VV j_1 V \\
-X @>> j_2 > E.
+X @>> j_2 > C.
\end{CD}
$$
-To see this, suppose we have two generalized elements $x_1, x_2 \in X(T)$ such that $j_1(x_1) = j_2(x_2)$. Then letting $r : E \to X$ be the coreflexivity morphism, we see
+To see this, suppose we have two generalized elements $x_1, x_2 \in X(T)$ such that $j_1(x_1) = j_2(x_2)$. Then letting $r : C \to X$ be the coreflexivity morphism, we see
$$x_1 = r(j_1(x_1)) = r(j_2(x_2)) = x_2$$
and
$$j_1(x_1) = j_2(x_2) = j_2(x_1),$$
@@ -148,7 +148,7 @@ $$
\begin{CD}
X+Y @> (\id; e) >> X \\
@V \id + e VV @VV j_1 V \\
-X+X @>> (j_1; j_2) > E.
+X+X @>> (j_1; j_2) > C.
\end{CD}
$$
@@ -158,7 +158,7 @@ $$
\begin{CD}
Y+X @> (e; \id) >> X \\
@V e + \id VV @VV j_2 V \\
-X+X @>> (j_1; j_2) > E.
+X+X @>> (j_1; j_2) > C.
\end{CD}
$$
@@ -168,7 +168,7 @@ $$
\begin{CD}
(X+Y)+(Y+X) @> (\id; e) + (e; \id) >> X+X \\
@V (\id+e; e+\id) VV @VV (j_1; j_2) V \\
-X+X @>> (j_1; j_2) > E.
+X+X @>> (j_1; j_2) > C.
\end{CD}
$$
@@ -176,9 +176,9 @@ However, under the canonical isomorphism $(X+Y)+(Y+X) \cong X+Y+Y+X$, we see tha
$$(i_1; i_1\circ e; i_2\circ e; i_2) : X+Y+Y+X \to X+X,$$
whereas $(\id+e; e+\id)$ corresponds to
$$(i_1; i_2\circ e; i_1\circ e; i_2) : X+Y+Y+X \to X+X.$$
-This completes the proof that these two morphisms form a kernel pair of $(j_1; j_2) : X + X \to E$.
+This completes the proof that these two morphisms form a kernel pair of $(j_1; j_2) : X + X \to C$.
-Therefore, since $(j_1; j_2) : X + X \to E$ is a regular epimorphism, by [this result](/content/regular-epis-kernel-pairs), it is a coequalizer of this kernel pair. However, this coequalizer is exactly the congruence quotient in the construction of $X +_Y X$ [here](/content/pushouts-of-monos-via-congruence-quotients). Thus, we see that the original corelation is equivalent to the cokernel pair of $e$.
+Therefore, since $(j_1; j_2) : X + X \to C$ is a regular epimorphism, by [this result](/content/regular-epis-kernel-pairs), it is a coequalizer of this kernel pair. However, this coequalizer is exactly the congruence quotient in the construction of $X +_Y X$ [here](/content/pushouts-of-monos-via-congruence-quotients). Thus, we see that the original corelation is equivalent to the cokernel pair of $e$.
:::
::: Corollary 5
@@ -186,5 +186,5 @@ In an extensive and regular category with quotients of congruences, every cocong
:::
::: Proof
-This follows by combining Corollary 3 and Lemma 4, using the existence of quotients of congruences so that $E +_X E$ always exists by [this result](/content/pushouts-of-monos-via-congruence-quotients).
+This follows by combining Corollary 3 and Lemma 4, using the existence of quotients of congruences so that $C +_X C$ always exists by [this result](/content/pushouts-of-monos-via-congruence-quotients).
:::
diff --git a/content/cocongruences_of_groups.md b/content/cocongruences_of_groups.md
index eb86f6bc1..99e567070 100644
--- a/content/cocongruences_of_groups.md
+++ b/content/cocongruences_of_groups.md
@@ -50,56 +50,56 @@ Let $\C$ be a balanced category with good pushouts of monomorphisms and equalize
:::
::: 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
+Let $X \in \C$ be an object, and let $j_1,j_2 : X \rightrightarrows C$ be a cocongruence. Since it is coreflexive, there exists a morphism $r : C \to X$ satisfying
-$$r \circ i_1 = \id_X, \quad r \circ i_2 = \id_X.$$
+$$r \circ j_1 = \id_X, \quad r \circ j_2 = \id_X.$$
-In particular, $i_1$ and $i_2$ are monomorphisms. Since the cocongruence is cotransitive, there exists a morphism
+In particular, $j_1$ and $j_2$ are monomorphisms. Since the cocongruence is cotransitive, there exists a morphism
-$$c : Y \to Y \sqcup_{i_2,X,i_1} Y$$
+$$t : C \to C \sqcup_{j_2,X,j_1} C$$
satisfying
-$$c \circ i_1 = u_1 \circ i_1, \quad c \circ i_2 = u_2 \circ i_2,$$
+$$t \circ j_1 = u_1 \circ j_1, \quad t \circ j_2 = u_2 \circ j_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. Consider the equalizer
+where $u_1,u_2 : C \rightrightarrows C \sqcup_{j_2,X,j_1} C$ are the pushout inclusions satisfying $u_1 j_2 = u_2 j_1$. We will not use the fact that the cocongruence is cosymmetric; this will follow automatically. Consider the equalizer
$$e : E \hookrightarrow X$$
-of $i_1$ and $i_2$. Since $i_1$ and $i_2$ agree on $E$, there exists a unique morphism
+of $j_1$ and $j_2$. Since $j_1$ and $j_2$ agree on $E$, there exists a unique morphism
-$$\varphi : X \sqcup_E X \to Y$$
+$$\varphi : X \sqcup_E X \to C$$
-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.
+defined by $\varphi \circ i_1 = j_1$ and $\varphi \circ i_2 = j_2$, where $i_1,i_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 must show that $\varphi$ is an isomorphism. It is clearly an epimorphism, since $j_1$ and $j_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 \coloneqq c \circ \varphi : X \sqcup_E X \to Y \sqcup_{i_2,X,i_1} Y$$
+$$\gamma \coloneqq t \circ \varphi : X \sqcup_E X \to C \sqcup_{j_2,X,j_1} C$$
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.$$
+$$\gamma \circ i_1 = t \circ \varphi \circ i_1 = t \circ j_1 = u_1 \circ j_1,$$
+$$\gamma \circ i_2 = t \circ \varphi \circ i_2 = t \circ j_2 = u_2 \circ j_2.$$
In other words, $\gamma$ is induced by the diagram of monomorphisms
$$
\begin{CD}
-X @>{i_1}>> Y \\
-@A{e}AA @AA{i_2}A \\
+X @>{j_1}>> C \\
+@A{e}AA @AA{j_2}A \\
E @>>{e}> X \\
-@V{e}VV @VV{i_1}V \\
-X @>>{i_2}> Y
+@V{e}VV @VV{j_1}V \\
+X @>>{j_2}> C
\end{CD}
$$
-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
+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 $j_1 \circ a = j_2 \circ b$. Applying $r : C \to X$, we obtain
-$$a = r \circ i_1 \circ a = r \circ i_2 \circ b = b.$$
+$$a = r \circ j_1 \circ a = r \circ j_2 \circ b = b.$$
-Thus, $a$ is simply a morphism equalizing $i_1$ and $i_2$, so it factors uniquely through $e$.
+Thus, $a$ is simply a morphism equalizing $j_1$ and $j_2$, so it factors uniquely through $e$.
:::
::: Corollary 3
diff --git a/content/congruences_in_rel.md b/content/congruences_in_rel.md
index 7160ffbe5..5bd5807b9 100644
--- a/content/congruences_in_rel.md
+++ b/content/congruences_in_rel.md
@@ -7,12 +7,12 @@ description: The classification will prove in particular that the category of se
We will give a classification of congruences in $\Rel$, the [category of sets and relations](/category/Rel). This classification will prove in particular that $\Rel$ has quotients of congruences and that congruences are effective.
-Let $i : E \hookrightarrow X \times X$ be a congruence in $\Rel$. Recall that products in $\Rel$ are actually given by disjoint unions at the level of underlying sets. Also, recall that a morphism $R : X \to Y$ in $\Rel$ is a monomorphism if and only if
+Let $q_1, q_2 : E \rightrightarrows X$ be a congruence in $\Rel$, and let $i \coloneqq (q_1,q_2) : E \hookrightarrow X \times X$ be the induced monomorphism. Recall that products in $\Rel$ are actually given by disjoint unions at the level of underlying sets. Also, recall that a morphism $R : X \to Y$ in $\Rel$ is a monomorphism if and only if
$$R_* : P(X) \to P(Y),\, S \mapsto \bigl\{ y\in Y \mid \exists x\in S, (x, y) \in R \bigr\}$$
is injective, and it is an isomorphism if and only if $R$ is the graph of a bijection $X \to Y$ in $\Set$.
In particular, we get
$$i_* : P(E) \to P(X + X) \cong P(X) \times P(X)$$
-which must be injective. It must also preserve arbitrary unions and in particular be inclusion-preserving. From the assumption that $i$ is a congruence, since the functor $(P, {-}_*) : \Rel \to \Set$ is representable by the object 1, we see that $i_*$ must have image given by an equivalence relation $\sim$ on $P(X)$. Note also that since $i_*$ preserves arbitrary unions, we must have that $\sim$ respects arbitrary unions.
+which must be injective. It must also preserve arbitrary unions and in particular be inclusion-preserving. From the assumption that $q_1, q_2$ is a congruence, since the functor $(P, {-}_*) : \Rel \to \Set$ is representable by the object 1, we see that $i_*$ must have image given by an equivalence relation $\sim$ on $P(X)$. Note also that since $i_*$ preserves arbitrary unions, we must have that $\sim$ respects arbitrary unions.
Since the symmetry morphism $s : E \to E$ satisfies $s^2 = \id$, it must be the graph of an involution $s_0$ on $E$, where $s_0$ is a morphism in $\Set$.
@@ -76,19 +76,19 @@ We can define a bijection $E \to E'$ as follows: let $e \in E$. If $i_*(\{ e \})
Now, without loss of generality we will assume from now on that the congruence is of exactly this form.
-With this classification, we can show that $A$ is a quotient for the congruence, with quotient morphism $\Delta_A \subseteq A \times A \subseteq X \times A$. In fact, we can define a morphism $\Delta_A^\circ : A \to X$ as the inverse relation to $\Delta_A$, and a morphism $X \to E$ as the graph of $i_1$. It is then straightforward to verify that these maps together make $A$ a split coequalizer of $p_1 \circ i$ and $p_2 \circ i$.
+With this classification, we can show that $A$ is a quotient for the congruence, with quotient morphism $\Delta_A \subseteq A \times A \subseteq X \times A$. In fact, we can define a morphism $\Delta_A^\circ : A \to X$ as the inverse relation to $\Delta_A$, and a morphism $X \to E$ as the graph of $i_1$. It is then straightforward to verify that these maps together make $A$ a split coequalizer of $q_1$ and $q_2$.
We can also conclude that $E$ is the kernel pair of this quotient, by the general result below.
::: Lemma
-Suppose we have a congruence $f, g : E \rightrightarrows X$ with a contractible coequalizer
-$$ E \, \overset{f}{\underset{g}{\rightrightarrows}} \, X \overset{e}{\rightarrow} Q $$
+Suppose we have a congruence $q_1, q_2 : E \rightrightarrows X$ with a contractible coequalizer
+$$ E \, \overset{q_1}{\underset{q_2}{\rightrightarrows}} \, X \overset{e}{\rightarrow} Q $$
with maps in the reverse direction $s : Q \to X$ and $t : X \to E$. Then $E$ is the kernel pair of this quotient, i.e. we have a pullback square
$$
\begin{CD}
-E @> f >> X \\
-@V g VV @V e VV \\
+E @> q_1 >> X \\
+@V q_2 VV @V e VV \\
X @> e >> Q.
\end{CD}
$$
@@ -96,5 +96,5 @@ $$
:::
::: Proof
-Suppose we have generalized elements $x_1, x_2 : U \rightrightarrows X$ with $e x_1 = e x_2$. Then $f t x_1 = x_1$ and $g t x_1 = s e x_1$, so the pair $x_1, s e x_1$ factors through $E$. Similarly, the pair $x_2, s e x_2$ factors through $E$. However, by the assumption, we also have $s e x_1 = s e x_2$. Therefore, since $E$ is a congruence, we conclude that the pair $x_1, x_2$ factors through $E$.
+Suppose we have generalized elements $x_1, x_2 : U \rightrightarrows X$ with $e x_1 = e x_2$. Then $q_1 t x_1 = x_1$ and $q_2 t x_1 = s e x_1$, so the pair $x_1, s e x_1$ factors through $E$. Similarly, the pair $x_2, s e x_2$ factors through $E$. However, by the assumption, we also have $s e x_1 = s e x_2$. Therefore, since $E$ is a congruence, we conclude that the pair $x_1, x_2$ factors through $E$.
:::
diff --git a/content/coslice-effective-congruences.md b/content/coslice-effective-congruences.md
index 730e5aa0f..4f8afe3cc 100644
--- a/content/coslice-effective-congruences.md
+++ b/content/coslice-effective-congruences.md
@@ -10,15 +10,15 @@ Let $\C$ be an extensive category, and $A$ an object of $\C$. If the coslice cat
:::
::: Proof
-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
+Let $q_1, q_2 : R \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 R$. More precisely, we will show the two maps
-$$\id_A + f,\, \id_A + g : A+E \rightrightarrows A+X$$
+$$\id_A + q_1,\, \id_A + q_2 : A+R \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$.
+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 $R$. 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 $R$.
-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 pair of maps
+Now if this congruence is the kernel pair of $h : A+X \to Z$ in $A \backslash \C$, then $R$ 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 pair of maps
$$\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$ factor through $A+E$ in $A \backslash \C$, so $x_1, x_2$ factor through $A+E$ in $\C$; and using disjoint coproducts, we may conclude that $x_1, x_2$ factor through $E$.
+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$ factor through $A+R$ in $A \backslash \C$, so $x_1, x_2$ factor through $A+R$ in $\C$; and using disjoint coproducts, we may conclude that $x_1, x_2$ factor through $R$.
:::
diff --git a/content/effective-congruence-quotients.md b/content/effective-congruence-quotients.md
index 5e21d597a..0c90be83f 100644
--- a/content/effective-congruence-quotients.md
+++ b/content/effective-congruence-quotients.md
@@ -5,20 +5,20 @@ description: If an effective congruence has a quotient, it is the kernel pair of
# Quotients of effective congruences
-Recall that a congruence $E \rightrightarrows X$ is called effective if it is the kernel pair of some morphism with domain $X$. The next result shows that, in many situations, this morphism can be chosen canonically, namely as the quotient of the congruence, provided that it exists.
+Recall that a congruence $R \rightrightarrows X$ is called effective if it is the kernel pair of some morphism with domain $X$. The next result shows that, in many situations, this morphism can be chosen canonically, namely as the quotient of the congruence, provided that it exists.
::: Lemma
-An effective congruence whose coequalizer exists is the kernel pair of its coequalizer. More precisely, let $f,g : E \rightrightarrows X$ be an effective congruence. If $f,g$ have a coequalizer $p : X \to X/E$, then $f,g$ is the kernel pair of $p$. That is, the square
-$$\begin{CD} E @> f >> X \\ @V g VV @VV p V \\ X @>> p > X/E \end{CD}$$
+An effective congruence whose coequalizer exists is the kernel pair of its coequalizer. More precisely, let $q_1,q_2 : R \rightrightarrows X$ be an effective congruence. If $q_1,q_2$ have a coequalizer $p : X \to X/R$, then $q_1,q_2$ is the kernel pair of $p$. That is, the square
+$$\begin{CD} R @> q_1 >> X \\ @V q_2 VV @VV p V \\ X @>> p > X/R \end{CD}$$
is a pullback.
:::
::: Proof
-Let $h : X \to Z$ be a morphism such that $f,g$ is the kernel pair of $h$. By the universal property of the coequalizer, there is a unique morphism
-$$\bar h : X/E \to Z$$
+Let $h : X \to Z$ be a morphism such that $q_1,q_2$ is the kernel pair of $h$. By the universal property of the coequalizer, there is a unique morphism
+$$\bar h : X/R \to Z$$
such that $h = \bar h \circ p$. Now suppose we have morphisms $a, b : T \rightrightarrows X$ such that $p \circ a = p \circ b$. Then
$$h \circ a = \bar h \circ p \circ a = \bar h \circ p \circ b = h \circ b.$$
-Since $f,g$ is the kernel pair of $h$, this means that the pair $a, b$ factors uniquely through the pair $f,g$.
+Since $q_1,q_2$ is the kernel pair of $h$, this means that the pair $a, b$ factors uniquely through the pair $q_1,q_2$.
:::
This result is similar to the [lemma](/content/regular-epis-kernel-pairs) that a regular monomorphism is the equalizer of its cokernel pair, provided that the cokernel pair exists.
diff --git a/content/free-cocompletion.md b/content/free-cocompletion.md
index f8fcb128d..d80b862f2 100644
--- a/content/free-cocompletion.md
+++ b/content/free-cocompletion.md
@@ -161,7 +161,7 @@ Let $\C$ be a locally small category. Then $\widehat{\C}$ has effective congruen
:::
::: Proof
-Let $f,g : F \rightrightarrows G$ be a congruence in $\widehat{\C}$. Let $p : G \twoheadrightarrow Q$ be its quotient (i.e. coequalizer) in $\widehat{\C}$, which is constructed objectwise. Applying the functorial definition of a congruence to representable functors in $\widehat{\C}$, we see that for every object $X \in \C$, $f(X),g(X) : F(X) \rightrightarrows G(X)$ is a congruence in $\Set$. Since congruences in $\Set$ are effective, $f(X),g(X)$ is the kernel pair of $p(X)$; we are also using [this result](/content/effective-congruence-quotients). Therefore, $f,g$ is the kernel pair of $p$ in the category of all presheaves, _a fortiori_ in the category of small presheaves.
+Let $q_1,q_2 : R \rightrightarrows G$ be a congruence in $\widehat{\C}$. Let $p : G \twoheadrightarrow Q$ be its quotient (i.e. coequalizer) in $\widehat{\C}$, which is constructed objectwise. Applying the functorial definition of a congruence to representable functors in $\widehat{\C}$, we see that for every object $X \in \C$, $q_1(X),q_2(X) : R(X) \rightrightarrows G(X)$ is a congruence in $\Set$. Since congruences in $\Set$ are effective, $q_1(X),q_2(X)$ is the kernel pair of $p(X)$; we are also using [this result](/content/effective-congruence-quotients). Therefore, $q_1,q_2$ is the kernel pair of $p$ in the category of all presheaves, _a fortiori_ in the category of small presheaves.
:::
::: Proposition 12
diff --git a/content/monic_sequential_colimits.md b/content/monic_sequential_colimits.md
index e48cfae8e..de1264c67 100644
--- a/content/monic_sequential_colimits.md
+++ b/content/monic_sequential_colimits.md
@@ -10,48 +10,48 @@ Let $\C$ be a countably extensive category with quotients of congruences. Then $
:::
::: Proof
-Suppose we have a sequence $X_0 \hookrightarrow X_1 \hookrightarrow \cdots$ with corresponding monomorphisms $f_{m,n} : X_m \hookrightarrow X_n$ for $m \le n$. Let $Y \coloneqq \coprod_{n \geq 0} X_n$ with coproduct inclusions $i_n : X_n \hookrightarrow Y$. For $m,n \geq 0$, define $E_{m,n} \coloneqq X_{\min(m,n)}$. Let $R \coloneqq \coprod_{m,n \geq 0} E_{m,n}$ with coproduct inclusions $j_{m,n} : E_{m,n} \hookrightarrow R$, and let $r_1, r_2 : R \rightrightarrows Y$ be the morphisms defined by
-$$r_1 \circ j_{m,n} = \begin{cases} i_m & \text{if } m \leq n, \\ i_m \circ f_{n,m} & \text{if } m \geq n, \end{cases} \qquad r_2 \circ j_{m,n} = \begin{cases} i_n \circ f_{m,n} & \text{if } m \leq n, \\ i_n & \text{if } m \geq n. \end{cases}$$
-For $m = n$, both cases agree. In particular, $r_1 \circ j_{m,n}$ factors through $i_m$, and $r_2 \circ j_{m,n}$ factors through $i_n$.
+Suppose we have a sequence $X_0 \hookrightarrow X_1 \hookrightarrow \cdots$ with corresponding monomorphisms $f_{m,n} : X_m \hookrightarrow X_n$ for $m \le n$. Let $Y \coloneqq \coprod_{n \geq 0} X_n$ with coproduct inclusions $i_n : X_n \hookrightarrow Y$. For $m,n \geq 0$, define $E_{m,n} \coloneqq X_{\min(m,n)}$. Let $R \coloneqq \coprod_{m,n \geq 0} E_{m,n}$ with coproduct inclusions $j_{m,n} : E_{m,n} \hookrightarrow R$, and let $q_1, q_2 : R \rightrightarrows Y$ be the morphisms defined by
+$$q_1 \circ j_{m,n} = \begin{cases} i_m & \text{if } m \leq n, \\ i_m \circ f_{n,m} & \text{if } m \geq n, \end{cases} \qquad q_2 \circ j_{m,n} = \begin{cases} i_n \circ f_{m,n} & \text{if } m \leq n, \\ i_n & \text{if } m \geq n. \end{cases}$$
+For $m = n$, both cases agree. In particular, $q_1 \circ j_{m,n}$ factors through $i_m$, and $q_2 \circ j_{m,n}$ factors through $i_n$.
-A morphism $h : Y \to T$ corresponds to a family of morphisms $h_n : X_n \to T$, and $h \circ r_1 = h \circ r_2$ holds if and only if $h \circ r_1 \circ j_{m,n} = h \circ r_2 \circ j_{m,n}$ for all $m,n \geq 0$. For $m \leq n$, we have
-$$h \circ r_1 \circ j_{m,n} = h \circ i_m = h_m, \qquad h \circ r_2 \circ j_{m,n} = h \circ i_n \circ f_{m,n} = h_n \circ f_{m,n},$$
-so the condition means $h_m = h_n \circ f_{m,n}$; the case $m \geq n$ gives the same condition with $m$ and $n$ exchanged. This is precisely the cocone condition. Hence, it suffices to show that $r_1, r_2$ is a congruence on $Y$, since then its quotient is a colimit of the sequence.
+A morphism $h : Y \to T$ corresponds to a family of morphisms $h_n : X_n \to T$, and $h \circ q_1 = h \circ q_2$ holds if and only if $h \circ q_1 \circ j_{m,n} = h \circ q_2 \circ j_{m,n}$ for all $m,n \geq 0$. For $m \leq n$, we have
+$$h \circ q_1 \circ j_{m,n} = h \circ i_m = h_m, \qquad h \circ q_2 \circ j_{m,n} = h \circ i_n \circ f_{m,n} = h_n \circ f_{m,n},$$
+so the condition means $h_m = h_n \circ f_{m,n}$; the case $m \geq n$ gives the same condition with $m$ and $n$ exchanged. This is precisely the cocone condition. Hence, it suffices to show that $q_1, q_2$ is a congruence on $Y$, since then its quotient is a colimit of the sequence.
-We will repeatedly use the following consequence of extensivity: if $a : T \to \coprod_{k \in K} A_k$ is a morphism into a countable coproduct, then pulling back the coproduct inclusions along $a$ yields a decomposition $T \cong \coprod_{k \in K} T_k$ such that the restriction of $a$ to each $T_k$ factors through the inclusion $A_k \hookrightarrow \coprod_{k \in K} A_k$. Applying this successively to finitely many morphisms $a_1,\dotsc,a_p$ from $T$ into countable coproducts (and their restrictions to the pieces obtained so far), we obtain a decomposition $T \cong \coprod_{l \in L} T_l$ with $L$ countable such that each restriction of each $a_q$ to each $T_l$ factors through a coproduct inclusion. Morphisms out of $T$ agree if and only if their restrictions to all $T_l$ agree, and morphisms out of the $T_l$ glue to a morphism out of $T$.
+We will repeatedly use the following consequence of extensivity: if $a : T \to \coprod_{k \in K} A_k$ is a morphism into a countable coproduct, then pulling back the coproduct inclusions along $a$ yields a decomposition $T \cong \coprod_{k \in K} T_k$ such that the restriction of $a$ to each $T_k$ factors through the inclusion $A_k \hookrightarrow \coprod_{k \in K} A_k$. Applying this successively to finitely many morphisms $a_1,\dotsc,a_p$ from $T$ into countable coproducts (and their restrictions to the pieces obtained so far), we obtain a decomposition $T \cong \coprod_{l \in L} T_l$ with $L$ countable such that each restriction of each of these morphisms to each $T_l$ factors through a coproduct inclusion. Morphisms out of $T$ agree if and only if their restrictions to all $T_l$ agree, and morphisms out of the $T_l$ glue to a morphism out of $T$.
Say that a morphism $x : T \to Y$ _lies in_ $X_m$ if $x = i_m \circ x'$ for some $x' : T \to X_m$, which is unique since coproduct inclusions in an extensive category are monomorphisms. If $x$ lies in $X_m$ and in $X_n$ for some $m \neq n$, then $x$ factors through $X_m \times_Y X_n$, which is initial since coproducts in an extensive category are disjoint. Hence, $T$ is initial since initial objects in an extensive category are strict. $(\ast)$
-First, $r_1, r_2$ are jointly monomorphic. Let $e, e' : T \rightrightarrows R$ with $r_1 \circ e = r_1 \circ e'$ and $r_2 \circ e = r_2 \circ e'$. Decompose $T$ such that on each piece $S$ we have $e|_S = j_{m,n} \circ a$ and $e'|_S = j_{m',n'} \circ a'$ for some $m,n,m',n'$ and some $a : S \to E_{m,n}$, $a' : S \to E_{m',n'}$. Then $r_1 \circ e|_S = r_1 \circ j_{m,n} \circ a$ lies in $X_m$, and
-$$r_1 \circ e|_S = r_1 \circ e'|_S = r_1 \circ j_{m',n'} \circ a'$$
-lies in $X_{m'}$, so that $S$ is initial by $(\ast)$ if $m \neq m'$; likewise, using $r_2$, if $n \neq n'$. On initial pieces, $e$ and $e'$ trivially agree. If $(m,n) = (m',n')$ and $m \leq n$, then
-$$i_m \circ a = r_1 \circ j_{m,n} \circ a = r_1 \circ e|_S = r_1 \circ e'|_S = r_1 \circ j_{m,n} \circ a' = i_m \circ a',$$
-hence $a = a'$ since $i_m$ is a monomorphism; if $m \geq n$, use $r_2$ and $i_n$ instead. Thus, $e|_S = e'|_S$ for all pieces $S$, and therefore $e = e'$.
+First, $q_1, q_2$ are jointly monomorphic. Let $e, e' : T \rightrightarrows R$ with $q_1 \circ e = q_1 \circ e'$ and $q_2 \circ e = q_2 \circ e'$. Decompose $T$ such that on each piece $S$ we have $e|_S = j_{m,n} \circ a$ and $e'|_S = j_{m',n'} \circ a'$ for some $m,n,m',n'$ and some $a : S \to E_{m,n}$, $a' : S \to E_{m',n'}$. Then $q_1 \circ e|_S = q_1 \circ j_{m,n} \circ a$ lies in $X_m$, and
+$$q_1 \circ e|_S = q_1 \circ e'|_S = q_1 \circ j_{m',n'} \circ a'$$
+lies in $X_{m'}$, so that $S$ is initial by $(\ast)$ if $m \neq m'$; likewise, using $q_2$, if $n \neq n'$. On initial pieces, $e$ and $e'$ trivially agree. If $(m,n) = (m',n')$ and $m \leq n$, then
+$$i_m \circ a = q_1 \circ j_{m,n} \circ a = q_1 \circ e|_S = q_1 \circ e'|_S = q_1 \circ j_{m,n} \circ a' = i_m \circ a',$$
+hence $a = a'$ since $i_m$ is a monomorphism; if $m \geq n$, use $q_2$ and $i_n$ instead. Thus, $e|_S = e'|_S$ for all pieces $S$, and therefore $e = e'$.
-It remains to show that for every object $T$, the image of $\Hom(T,R) \to \Hom(T,Y)^2$, $e \mapsto (r_1 \circ e, r_2 \circ e)$ is an equivalence relation. We call a pair of morphisms $x,y : T \rightrightarrows Y$ _related_ if it lies in this image, that is, if there is a morphism $e : T \to R$ with $r_1 \circ e = x$ and $r_2 \circ e = y$.
+It remains to show that for every object $T$, the image of $\Hom(T,R) \to \Hom(T,Y)^2$, $e \mapsto (q_1 \circ e, q_2 \circ e)$ is an equivalence relation. We call a pair of morphisms $x,y : T \rightrightarrows Y$ _related_ if it lies in this image, that is, if there is a morphism $e : T \to R$ with $q_1 \circ e = x$ and $q_2 \circ e = y$.
-For reflexivity, let $\delta : Y \to R$ be the morphism with $\delta \circ i_n = j_{n,n}$ for all $n$. Since $r_1 \circ j_{n,n} = i_n = r_2 \circ j_{n,n}$, we have $r_1 \circ \delta = \id_Y = r_2 \circ \delta$. Hence, for every $x : T \to Y$, the morphism $\delta \circ x$ witnesses that $(x,x)$ is related. For symmetry, let $\sigma : R \to R$ be the morphism with $\sigma \circ j_{m,n} = j_{n,m}$, which makes sense since $E_{m,n} = E_{n,m}$. The formulas for $r_1$ and $r_2$ above show that $r_1 \circ j_{n,m} = r_2 \circ j_{m,n}$ for all $m,n$. Hence, we have $r_1 \circ \sigma = r_2$, and likewise $r_2 \circ \sigma = r_1$. Thus, if $e$ witnesses that $(x,y)$ is related, then $\sigma \circ e$ witnesses that $(y,x)$ is related.
+For reflexivity, let $\delta : Y \to R$ be the morphism with $\delta \circ i_n = j_{n,n}$ for all $n$. Since $q_1 \circ j_{n,n} = i_n = q_2 \circ j_{n,n}$, we have $q_1 \circ \delta = \id_Y = q_2 \circ \delta$. Hence, for every $x : T \to Y$, the morphism $\delta \circ x$ witnesses that $(x,x)$ is related. For symmetry, let $\sigma : R \to R$ be the morphism with $\sigma \circ j_{m,n} = j_{n,m}$, which makes sense since $E_{m,n} = E_{n,m}$. The formulas for $q_1$ and $q_2$ above show that $q_1 \circ j_{n,m} = q_2 \circ j_{m,n}$ for all $m,n$. Hence, we have $q_1 \circ \sigma = q_2$, and likewise $q_2 \circ \sigma = q_1$. Thus, if $e$ witnesses that $(x,y)$ is related, then $\sigma \circ e$ witnesses that $(y,x)$ is related.
For transitivity, we use the following auxiliary relation. For morphisms $x' : T \to X_m$ and $y' : T \to X_n$, write $x' \sim y'$ if $f_{m,k} \circ x' = f_{n,k} \circ y'$ for all $k \geq m,n$. Since the equation for $k = \max(m,n)$ implies the equation for all larger $k$, we have $x' \sim y'$ if and only if $y' = f_{m,n} \circ x'$ in case $m \leq n$, and if and only if $x' = f_{n,m} \circ y'$ in case $m \geq n$. Clearly, $\sim$ is symmetric. It is also transitive: if $x' \sim y'$ and $y' \sim z'$ with $z' : T \to X_p$, then the equation $f_{m,k} \circ x' = f_{p,k} \circ z'$ holds for all $k \geq m,n,p$, and hence for all $k \geq m,p$ by cancelling the monomorphisms $f_{k,k'}$.
We claim that if $x' : T \to X_m$ and $y' : T \to X_n$, then $(i_m \circ x', i_n \circ y')$ is related if and only if $x' \sim y'$. Since $\sim$ and relatedness are symmetric, we may assume $m \leq n$. If $x' \sim y'$, then $y' = f_{m,n} \circ x'$, and we may regard $x'$ as a morphism $T \to E_{m,n} = X_m$. Then $e \coloneqq j_{m,n} \circ x' : T \to R$ satisfies
-$$r_1 \circ e = i_m \circ x', \qquad r_2 \circ e = i_n \circ f_{m,n} \circ x' = i_n \circ y'.$$
-Conversely, let $e : T \to R$ with $r_1 \circ e = i_m \circ x'$ and $r_2 \circ e = i_n \circ y'$. Decompose $T \cong \coprod_{k,l \geq 0} T_{k,l}$ such that $e|_{T_{k,l}} = j_{k,l} \circ e_{k,l}$ for some $e_{k,l} : T_{k,l} \to E_{k,l}$. Then
-$$i_m \circ x'|_{T_{k,l}} = r_1 \circ e|_{T_{k,l}} = r_1 \circ j_{k,l} \circ e_{k,l},$$
-and this morphism also lies in $X_k$ since $r_1 \circ j_{k,l}$ factors through $i_k$. So $T_{k,l}$ is initial by $(\ast)$ when $k \neq m$. Likewise,
-$$i_n \circ y'|_{T_{k,l}} = r_2 \circ e|_{T_{k,l}} = r_2 \circ j_{k,l} \circ e_{k,l}$$
+$$q_1 \circ e = i_m \circ x', \qquad q_2 \circ e = i_n \circ f_{m,n} \circ x' = i_n \circ y'.$$
+Conversely, let $e : T \to R$ with $q_1 \circ e = i_m \circ x'$ and $q_2 \circ e = i_n \circ y'$. Decompose $T \cong \coprod_{k,l \geq 0} T_{k,l}$ such that $e|_{T_{k,l}} = j_{k,l} \circ e_{k,l}$ for some $e_{k,l} : T_{k,l} \to E_{k,l}$. Then
+$$i_m \circ x'|_{T_{k,l}} = q_1 \circ e|_{T_{k,l}} = q_1 \circ j_{k,l} \circ e_{k,l},$$
+and this morphism also lies in $X_k$ since $q_1 \circ j_{k,l}$ factors through $i_k$. So $T_{k,l}$ is initial by $(\ast)$ when $k \neq m$. Likewise,
+$$i_n \circ y'|_{T_{k,l}} = q_2 \circ e|_{T_{k,l}} = q_2 \circ j_{k,l} \circ e_{k,l}$$
also lies in $X_l$, so that $T_{k,l}$ is initial when $l \neq n$. On initial pieces, the equation $y' = f_{m,n} \circ x'$ holds trivially. On $T_{m,n}$, since $m \leq n$, we have
$$
\begin{align*}
-i_m \circ x'|_{T_{m,n}} & = r_1 \circ j_{m,n} \circ e_{m,n} = i_m \circ e_{m,n}, \\
-i_n \circ y'|_{T_{m,n}} & = r_2 \circ j_{m,n} \circ e_{m,n} = i_n \circ f_{m,n} \circ e_{m,n}.
+i_m \circ x'|_{T_{m,n}} & = q_1 \circ j_{m,n} \circ e_{m,n} = i_m \circ e_{m,n}, \\
+i_n \circ y'|_{T_{m,n}} & = q_2 \circ j_{m,n} \circ e_{m,n} = i_n \circ f_{m,n} \circ e_{m,n}.
\end{align*}
$$
Cancelling the monomorphisms $i_m$ and $i_n$ gives $y'|_{T_{m,n}} = f_{m,n} \circ x'|_{T_{m,n}}$. Therefore, $y' = f_{m,n} \circ x'$.
-Now let $x,y,z : T \to Y$ such that $(x,y)$ and $(y,z)$ are related. Decompose $T$ such that on each piece $S$, the restrictions of $x,y,z$ lie in some $X_m, X_n, X_p$, respectively, say $x|_S = i_m \circ x'$, $y|_S = i_n \circ y'$, $z|_S = i_p \circ z'$. Restricting the witnesses to $S$ shows that $(x|_S, y|_S)$ and $(y|_S, z|_S)$ are related, so the claim gives $x' \sim y'$ and $y' \sim z'$, hence $x' \sim z'$ by transitivity of $\sim$, and therefore $(x|_S, z|_S)$ is related by the claim again. Gluing the morphisms $S \to R$ witnessing this, we obtain a morphism $T \to R$ witnessing that $(x,z)$ is related. This finishes the proof that $r_1, r_2$ is a congruence.
+Now let $x,y,z : T \to Y$ such that $(x,y)$ and $(y,z)$ are related. Decompose $T$ such that on each piece $S$, the restrictions of $x,y,z$ lie in some $X_m, X_n, X_p$, respectively, say $x|_S = i_m \circ x'$, $y|_S = i_n \circ y'$, $z|_S = i_p \circ z'$. Restricting the witnesses to $S$ shows that $(x|_S, y|_S)$ and $(y|_S, z|_S)$ are related, so the claim gives $x' \sim y'$ and $y' \sim z'$, hence $x' \sim z'$ by transitivity of $\sim$, and therefore $(x|_S, z|_S)$ is related by the claim again. Gluing the morphisms $S \to R$ witnessing this, we obtain a morphism $T \to R$ witnessing that $(x,z)$ is related. This finishes the proof that $q_1, q_2$ is a congruence.
:::
::: Lemma 2
diff --git a/content/pushouts-of-monos-via-congruence-quotients.md b/content/pushouts-of-monos-via-congruence-quotients.md
index 8b31f08a9..6aad837ca 100644
--- a/content/pushouts-of-monos-via-congruence-quotients.md
+++ b/content/pushouts-of-monos-via-congruence-quotients.md
@@ -10,5 +10,5 @@ Let $\C$ be an extensive category with quotients of congruences. Then $\C$ has p
:::
::: Proof
-Let $f : S \hookrightarrow X$, $g : S \hookrightarrow Y$ be monomorphisms. We construct a congruence on $X+Y$ via the maps $p_1, p_2 : X + Y + S + S \rightrightarrows X+Y$ which act as the identity on $X+Y$, $i_1 \circ f, i_2 \circ g$ on the first copy of $S$, and $i_2 \circ g, i_1 \circ f$ on the second copy of $S$, respectively. To show that $p_1, p_2$ are jointly monomorphic, and again in proving transitivity of the congruence, we use extensivity to split the domain of the generalized elements of $X+Y+S+S$ so that without loss of generality we may assume each factors through one of the coproduct inclusions. Now a quotient of the congruence must be a pushout of $f$ and $g$.
+Let $f : S \hookrightarrow X$, $g : S \hookrightarrow Y$ be monomorphisms. We construct a congruence on $X+Y$ via the maps $q_1, q_2 : X + Y + S + S \rightrightarrows X+Y$ which act as the identity on $X+Y$, $i_1 \circ f, i_2 \circ g$ on the first copy of $S$, and $i_2 \circ g, i_1 \circ f$ on the second copy of $S$, respectively. To show that $q_1, q_2$ are jointly monomorphic, and again in proving transitivity of the congruence, we use extensivity to split the domain of the generalized elements of $X+Y+S+S$ so that without loss of generality we may assume each factors through one of the coproduct inclusions. Now a quotient of the congruence must be a pushout of $f$ and $g$.
:::
diff --git a/database/data/categories/Alg(R).yaml b/database/data/categories/Alg(R).yaml
index 6e068f9cf..9135878a8 100644
--- a/database/data/categories/Alg(R).yaml
+++ b/database/data/categories/Alg(R).yaml
@@ -53,7 +53,7 @@ unsatisfied_properties:
proof: 'If $\sqcup$ denotes the coproduct of $R$-algebras (see MSE/625874 for their description) and $A$ is an $R$-algebra, the canonical morphism $A \sqcup R^2 \to (A \sqcup R)^2 = A^2$ is usually not an isomorphism. For example, for $A = R[X]$ the coproduct on the LHS is not commutative; it has the algebra presentation $\langle X,E : E^2=E \rangle$.'
- property: co-Malcev
- proof: 'See MO/509552: Consider the forgetful functor $U : \Alg(R) \to \Set$ and the relation $S \subseteq U^2$ defined by $S(A) \coloneqq \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by $R[X]$ and $S$ by $R \langle X,Y \rangle / \langle XY-X^2 \rangle$. It is clear that $S$ is reflexive, but not symmetric.'
+ proof: 'See MO/509552: Consider the forgetful functor $U : \Alg(R) \to \Set$ and the relation $E \subseteq U^2$ defined by $E(A) \coloneqq \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by $R[X]$ and $E$ by $R \langle X,Y \rangle / \langle XY-X^2 \rangle$. It is clear that $E$ is reflexive, but not symmetric.'
- property: pushout-stable regular monomorphisms
proof: 'Since $R \neq 0$, there is an infinite field $K$ with a homomorphism $R \to K$. Since $K$ is infinite, we may choose some $\lambda \in K \setminus \{0,1\}$. Let $B \coloneqq M_2(K)$ and $A \coloneqq K \times K$. Then $A \to B$, $(x,y) \mapsto \diag(x,y)$ is a regular monomorphism: A direct calculation shows that a matrix is diagonal iff it commutes with $M \coloneqq \bigl(\begin{smallmatrix} 1 & 0 \\ 0 & \lambda \end{smallmatrix}\bigr)$, so that $A \to B$ is the equalizer of the identity $B \to B$ and the conjugation $B \to B$, $X \mapsto M X M^{-1}$. Consider the homomorphism $A \to K$, $(a,b) \mapsto a$. We claim that $K \to K \sqcup_A B$ is not a monomorphism, because in fact, the pushout $K \sqcup_A B$ is zero: Since $A \to K$ is surjective with kernel $0 \times K$, the pushout is $B/\langle 0 \times K \rangle$, which is $0$ because $B$ is simple (proof) or via a direct calculation with elementary matrices.'
@@ -74,7 +74,7 @@ unsatisfied_properties:
proof: We already know that $\CAlg(R)$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the forgetful functor $\CAlg(R) \to \Alg(R)$. It preserves epimorphisms by MSE/5133488.
- property: effective cocongruences
- proof: 'MO/510744 presents a counterexample for $\Ring$, and it can be easily generalized to $\Alg(R)$: Let $X \coloneqq R[p] / (p^2-p)$ with cocongruence $E \coloneqq R \langle p, q \rangle / (p^2-p, q^2-q, pq-q, qp-p)$.'
+ proof: 'MO/510744 presents a counterexample for $\Ring$, and it can be easily generalized to $\Alg(R)$: Let $X \coloneqq R[p] / (p^2-p)$ with cocongruence $C \coloneqq R \langle p, q \rangle / (p^2-p, q^2-q, pq-q, qp-p)$.'
special_objects:
initial object:
diff --git a/database/data/categories/Ban.yaml b/database/data/categories/Ban.yaml
index 6311a5453..bc577fb59 100644
--- a/database/data/categories/Ban.yaml
+++ b/database/data/categories/Ban.yaml
@@ -69,7 +69,7 @@ satisfied_properties:
- property: effective congruences
proof: >-
- Let $R \hookrightarrow X \times X$ be a congruence in $\Ban$. We may assume that it is an inclusion of vector spaces. Since the forgetful functor $\Ban \to \Vect$ preserves finite limits, the congruence yields a congruence in $\Vect$, which we understand well:
+ Let $q_1,q_2 : R \rightrightarrows X$ be a congruence in $\Ban$. We may assume that the induced map $R \hookrightarrow X \times X$ is an inclusion of vector spaces. Since the forgetful functor $\Ban \to \Vect$ preserves finite limits, the congruence yields a congruence in $\Vect$, which we understand well:
It is fully classified by the subspace $U \coloneqq \{x \in X : (x,0) \in R\}$ via $R = \{(x,y) \in X \times X : x-y \in U\}$.
Since $R \hookrightarrow X \times X$ is a linear contraction, the norm $|{-}|_R$ on $R$ satisfies
diff --git a/database/data/categories/Bin.yaml b/database/data/categories/Bin.yaml
index 975cf900c..a250a303c 100644
--- a/database/data/categories/Bin.yaml
+++ b/database/data/categories/Bin.yaml
@@ -114,7 +114,7 @@ unsatisfied_properties:
- property: co-Malcev
proof: >-
- Consider the set $X = \{x\}$ with the relation $R_X = \{(x,x)\}$ and the set $Y = \{x,x'\}$ with the relation $R_Y = \{(x,x),(x',x'),(x,x')\}$. There are two canonical morphisms $q,q' : (X,R_X) \rightrightarrows (Y,R_Y)$ defined by $q(x)=x$ and $q'(x)=x'$. They are jointly surjective and have a common retraction $(Y,R_Y) \to (X,R_X)$, namely the unique map $Y \to X$ sending both $x$ and $x'$ to $x$. Thus, $q,q'$ form a coreflexive corelation. It is not cosymmetric, since otherwise there would be a morphism $s : (Y,R_Y) \to (Y,R_Y)$ satisfying $s(x)=x'$ and $s(x')=x$, which would imply $(x',x) \in R_Y$, contrary to the definition of $R_Y$.
+ Consider the set $X = \{x\}$ with the relation $R_X = \{(x,x)\}$ and the set $C = \{x,x'\}$ with the relation $R_C = \{(x,x),(x',x'),(x,x')\}$. There are two canonical morphisms $j_1,j_2 : (X,R_X) \rightrightarrows (C,R_C)$ defined by $j_1(x)=x$ and $j_2(x)=x'$. They are jointly surjective and have a common retraction $(C,R_C) \to (X,R_X)$, namely the unique map $C \to X$ sending both $x$ and $x'$ to $x$. Thus, $j_1,j_2$ form a coreflexive corelation. It is not cosymmetric, since otherwise there would be a morphism $s : (C,R_C) \to (C,R_C)$ satisfying $s(x)=x'$ and $s(x')=x$, which would imply $(x',x) \in R_C$, contrary to the definition of $R_C$.
label: Bin_not_co-Malcev
special_objects:
diff --git a/database/data/categories/Bin_irr.yaml b/database/data/categories/Bin_irr.yaml
index b361d2aca..9e10def00 100644
--- a/database/data/categories/Bin_irr.yaml
+++ b/database/data/categories/Bin_irr.yaml
@@ -72,7 +72,7 @@ satisfied_properties:
- property: effective cocongruences
proof: >-
- Let $q_1, q_2 : X \rightrightarrows Y$ be a cocongruence in $\Bin_{\irr}$. Then $(q_1;q_2) : X \sqcup X \to Y$ is an epimorphism, i.e. surjective on underlying sets, and hence an epimorphism in $\Bin$. The pushout $Y \sqcup_{q_2,X,q_1} Y$ in $\Bin$ has no loops since, using the common retraction $Y \to X$ of $q_1,q_2$ (the coreflexivity morphism), it admits a morphism to $X$. Therefore, we obtain coreflexivity, cosymmetry, and cotransitivity morphisms in $\Bin_{\irr}$, and these are also such morphisms in $\Bin$. Hence, $q_1, q_2 : X \rightrightarrows Y$ is a cocongruence in $\Bin$. Since $\Bin$ has effective cocongruences, there is a morphism $T \to X$ whose cokernel pair is $X \rightrightarrows Y$ in $\Bin$. Since $T$ admits a morphism to $X \in \Bin_{\irr}$, we have $T \in \Bin_{\irr}$. It follows that $T \to X$ also has cokernel pair $X \rightrightarrows Y$ in $\Bin_{\irr}$.
+ Let $j_1, j_2 : X \rightrightarrows C$ be a cocongruence in $\Bin_{\irr}$. Then $(j_1;j_2) : X \sqcup X \to C$ is an epimorphism, i.e. surjective on underlying sets, and hence an epimorphism in $\Bin$. The pushout $C \sqcup_{j_2,X,j_1} C$ in $\Bin$ has no loops since, using the common retraction $C \to X$ of $j_1,j_2$ (the coreflexivity morphism), it admits a morphism to $X$. Therefore, we obtain coreflexivity, cosymmetry, and cotransitivity morphisms in $\Bin_{\irr}$, and these are also such morphisms in $\Bin$. Hence, $j_1, j_2 : X \rightrightarrows C$ is a cocongruence in $\Bin$. Since $\Bin$ has effective cocongruences, there is a morphism $T \to X$ whose cokernel pair is $X \rightrightarrows C$ in $\Bin$. Since $T$ admits a morphism to $X \in \Bin_{\irr}$, we have $T \in \Bin_{\irr}$. It follows that $T \to X$ also has cokernel pair $X \rightrightarrows C$ in $\Bin_{\irr}$.
unsatisfied_properties:
- property: skeletal
diff --git a/database/data/categories/Bin_symm.yaml b/database/data/categories/Bin_symm.yaml
index 4fcd80a7c..2458b2b4b 100644
--- a/database/data/categories/Bin_symm.yaml
+++ b/database/data/categories/Bin_symm.yaml
@@ -106,7 +106,7 @@ unsatisfied_properties:
Consider these two objects of $\Bin_{\symm}$:
$$\begin{align*}
G & = (\{a,b\},\{(a,b),(b,a)\}) \\
- H & = (\{a,b,a',b'\},\{(a,b),(b,a),(a',b'),(b',a'),(a,b'),(b',a)\})
+ C & = (\{a,b,a',b'\},\{(a,b),(b,a),(a',b'),(b',a'),(a,b'),(b',a)\})
\end{align*}$$
As undirected (loop-)graphs, these look as follows:
$$\begin{array}{cccc}
@@ -114,10 +114,10 @@ unsatisfied_properties:
\end{array}$$
$$\begin{array}{cccc}
& a & \longleftrightarrow & b \\[1ex]
- H : & & \searrow \!\!\!\!\!\! \nwarrow & \\[1ex]
+ C : & & \searrow \!\!\!\!\!\! \nwarrow & \\[1ex]
& a' & \longleftrightarrow & b' \\
\end{array}$$
- There are two canonical morphisms $G \rightrightarrows H$. They are jointly epimorphic and have a common retraction $H \to G$ mapping $a,a' \mapsto a$ and $b,b' \mapsto b$. Thus, $G \rightrightarrows H$ is a coreflexive corelation. But it is not cosymmetric, since there is no edge $a' \leftrightarrow b$ in $H$.
+ There are two canonical morphisms $G \rightrightarrows C$. They are jointly epimorphic and have a common retraction $C \to G$ mapping $a,a' \mapsto a$ and $b,b' \mapsto b$. Thus, $G \rightrightarrows C$ is a coreflexive corelation. But it is not cosymmetric, since there is no edge $a' \leftrightarrow b$ in $C$.
label: Bin_symm_not_co-Malcev
special_objects:
diff --git a/database/data/categories/Bin_symm_irr.yaml b/database/data/categories/Bin_symm_irr.yaml
index 1aaa2c2e2..978c7636a 100644
--- a/database/data/categories/Bin_symm_irr.yaml
+++ b/database/data/categories/Bin_symm_irr.yaml
@@ -79,7 +79,7 @@ satisfied_properties:
- property: effective cocongruences
proof: >-
- Let $q_1, q_2 : X \rightrightarrows Y$ be a cocongruence in $\Bin_{\symm,\irr}$. Then $(q_1;q_2) : X \sqcup X \to Y$ is an epimorphism, i.e. surjective on underlying sets, and hence an epimorphism in $\Bin$. The pushout $Y \sqcup_{q_2,X,q_1} Y$ in $\Bin$ belongs to $\Bin_{\irr}$ since, using the common retraction $Y \to X$ of $q_1,q_2$ (the coreflexivity morphism), it admits a morphism to $X$. It also belongs to $\Bin_{\symm}$ since $Y$ belongs to $\Bin_{\symm}$ and every relation comes from one of the two copies of $Y$. Therefore, we obtain coreflexivity, cosymmetry, and cotransitivity morphisms in $\Bin_{\symm,\irr}$, and these are also such morphisms in $\Bin$. Hence, $q_1, q_2 : X \rightrightarrows Y$ is a cocongruence in $\Bin$. Since $\Bin$ has effective cocongruences and equalizers, there is a monomorphism $T \to X$ whose cokernel pair is $X \rightrightarrows Y$ in $\Bin$. Since $T$ admits a monomorphism to $X \in \Bin_{\symm,\irr}$, we have $T \in \Bin_{\symm,\irr}$. It follows that $T \to X$ also has cokernel pair $X \rightrightarrows Y$ in $\Bin_{\symm,\irr}$.
+ Let $j_1, j_2 : X \rightrightarrows C$ be a cocongruence in $\Bin_{\symm,\irr}$. Then $(j_1;j_2) : X \sqcup X \to C$ is an epimorphism, i.e. surjective on underlying sets, and hence an epimorphism in $\Bin$. The pushout $C \sqcup_{j_2,X,j_1} C$ in $\Bin$ belongs to $\Bin_{\irr}$ since, using the common retraction $C \to X$ of $j_1,j_2$ (the coreflexivity morphism), it admits a morphism to $X$. It also belongs to $\Bin_{\symm}$ since $C$ belongs to $\Bin_{\symm}$ and every relation comes from one of the two copies of $C$. Therefore, we obtain coreflexivity, cosymmetry, and cotransitivity morphisms in $\Bin_{\symm,\irr}$, and these are also such morphisms in $\Bin$. Hence, $j_1, j_2 : X \rightrightarrows C$ is a cocongruence in $\Bin$. Since $\Bin$ has effective cocongruences and equalizers, there is a monomorphism $T \to X$ whose cokernel pair is $X \rightrightarrows C$ in $\Bin$. Since $T$ admits a monomorphism to $X \in \Bin_{\symm,\irr}$, we have $T \in \Bin_{\symm,\irr}$. It follows that $T \to X$ also has cokernel pair $X \rightrightarrows C$ in $\Bin_{\symm,\irr}$.
unsatisfied_properties:
- property: skeletal
diff --git a/database/data/categories/CAlg(R).yaml b/database/data/categories/CAlg(R).yaml
index bfd77c3aa..e252158c6 100644
--- a/database/data/categories/CAlg(R).yaml
+++ b/database/data/categories/CAlg(R).yaml
@@ -67,7 +67,7 @@ unsatisfied_properties:
proof: See MSE/3745302.
- property: co-Malcev
- proof: 'See MO/509552: Consider the forgetful functor $U : \CAlg(R) \to \Set$ and the relation $S \subseteq U^2$ defined by $S(A) \coloneqq \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by $R[X]$ and $S$ by $R[X,Y] / \langle XY-X^2 \rangle$. It is clear that $S$ is reflexive, but not symmetric.'
+ proof: 'See MO/509552: Consider the forgetful functor $U : \CAlg(R) \to \Set$ and the relation $E \subseteq U^2$ defined by $E(A) \coloneqq \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by $R[X]$ and $E$ by $R[X,Y] / \langle XY-X^2 \rangle$. It is clear that $E$ is reflexive, but not symmetric.'
- property: regular quotient object classifier
proof: 'Assume that $P \to R$ is a regular quotient object classifier. If $J$ denotes the kernel of $P \to R$, every ideal $I \subseteq A$ of any commutative $R$-algebra has the form $I = \langle \varphi(J) \rangle$ for a unique homomorphism $\varphi : P \to A$. If $\sigma : A \to A$ is an automorphism with $\sigma(I)=I$, then uniqueness gives us $\sigma \circ \varphi = \varphi$, which means that $\varphi(J)$ lies in $A^{\sigma}$, the fixed algebra of $\sigma$. But then $I$ is generated by elements in $A^{\sigma} \cap I$. If $K$ is a residue field of $R$, this fails for $A = K[X,Y]$, $I = \langle X,Y \rangle$, $\sigma(X)=Y$, $\sigma(Y)=X$. The fixed algebra is the subalgebra of symmetric polynomials, which is $K[X+Y,XY]$. So $\langle X,Y \rangle$ is generated by symmetric polynomials without constant term, which implies $\langle X,Y \rangle \subseteq \langle X+Y,XY \rangle$ in $K[X,Y]$. But reducing an equation like $X = a(X,Y) \cdot (X+Y) + b(X,Y) \cdot (XY)$ modulo $\langle X^2,Y^2,XY \rangle$ yields a contradiction.'
diff --git a/database/data/categories/Euclid_coprod.yaml b/database/data/categories/Euclid_coprod.yaml
index 6f12bc0c5..b3bcd1526 100644
--- a/database/data/categories/Euclid_coprod.yaml
+++ b/database/data/categories/Euclid_coprod.yaml
@@ -51,25 +51,25 @@ satisfied_properties:
- property: effective cocongruences
proof: >-
- Let $i_1,i_2 : X \rightrightarrows E$ be a coreflexive corelation in $\Euclidsqcup$. (We will not need to assume cosymmetry or cotransitivity, as both properties will follow.) This means that the induced map $(i_1;i_2) : X \sqcup X \to E$ is an epimorphism, i.e. has dense image, and that there is a continuous map $r : E \to X$ satisfying
- $$r \circ i_1 = r \circ i_2 = \id_X.$$
- It follows that, in $\Top$, $i_1$ is the equalizer of $\id_E$ and $i_1 \circ r : E \rightrightarrows E$. Since $E$ is Hausdorff, this implies that $i_1$ is an embedding with closed image $i_1(X)$. Likewise, $i_2$ is an embedding with closed image $i_2(X)$. Their union $i_1(X) \cup i_2(X)$ is also closed. On the other hand, since $(i_1;i_2)$ has dense image, $i_1(X) \cup i_2(X)$ is dense. Thus,
- $$E = i_1(X) \cup i_2(X),$$
- i.e. $i_1,i_2$ are jointly surjective. It follows that the underlying maps of $i_1,i_2$ form a coreflexive corelation in $\Set$. Therefore, by this result, if we define the equalizer
- $$U \coloneqq \{x \in X : i_1(x) = i_2(x)\},$$
+ Let $j_1,j_2 : X \rightrightarrows C$ be a coreflexive corelation in $\Euclidsqcup$. (We will not need to assume cosymmetry or cotransitivity, as both properties will follow.) This means that the induced map $(j_1;j_2) : X \sqcup X \to C$ is an epimorphism, i.e. has dense image, and that there is a continuous map $r : C \to X$ satisfying
+ $$r \circ j_1 = r \circ j_2 = \id_X.$$
+ It follows that, in $\Top$, $j_1$ is the equalizer of $\id_C$ and $j_1 \circ r : C \rightrightarrows C$. Since $C$ is Hausdorff, this implies that $j_1$ is an embedding with closed image $j_1(X)$. Likewise, $j_2$ is an embedding with closed image $j_2(X)$. Their union $j_1(X) \cup j_2(X)$ is also closed. On the other hand, since $(j_1;j_2)$ has dense image, $j_1(X) \cup j_2(X)$ is dense. Thus,
+ $$C = j_1(X) \cup j_2(X),$$
+ i.e. $j_1,j_2$ are jointly surjective. It follows that the underlying maps of $j_1,j_2$ form a coreflexive corelation in $\Set$. Therefore, by this result, if we define the equalizer
+ $$U \coloneqq \{x \in X : j_1(x) = j_2(x)\},$$
then the induced continuous map
- $$X \sqcup_U X \to E$$
- is a bijection. Since the maps $i_1,i_2$ are closed embeddings, $(i_1;i_2) : X + X \to E$ is closed, and therefore a quotient map. It follows that $X \sqcup_U X \cong E$ is an isomorphism of topological spaces. In other words, $i_1,i_2$ is the cokernel pair of $U \hookrightarrow X$ in $\Top$.
+ $$X \sqcup_U X \to C$$
+ is a bijection. Since the maps $j_1,j_2$ are closed embeddings, $(j_1;j_2) : X + X \to C$ is closed, and therefore a quotient map. It follows that $X \sqcup_U X \cong C$ is an isomorphism of topological spaces. In other words, $j_1,j_2$ is the cokernel pair of $U \hookrightarrow X$ in $\Top$.
- It remains to prove that $U$ belongs to $\Euclidsqcup$, since then $i_1,i_2$ is also a cokernel pair in $\Euclidsqcup$. In fact, we will prove that $U$ is a union of connected components of $X$.
+ It remains to prove that $U$ belongs to $\Euclidsqcup$, since then $j_1,j_2$ is also a cokernel pair in $\Euclidsqcup$. In fact, we will prove that $U$ is a union of connected components of $X$.
- Suppose that $U$ intersects a connected component $X' \subseteq X$. Choose a point $x \in U \cap X'$ and let $e \coloneqq i_1(x) = i_2(x)$. Let $E' \subseteq E$ be the connected component containing $e$. Then $i_1(X') \subseteq E'$ and $i_2(X') \subseteq E'$. Since $r(e)=x$, we also have $r(E') \subseteq X'$. We claim that
- $$E' = i_1(X') \cup i_2(X').$$
- The inclusion $\supseteq$ is clear. To show the inclusion $\subseteq$, pick any point $p \in E'$. We have either $p \in i_1(X)$ or $p \in i_2(X)$. Assume without loss of generality that $p \in i_1(X)$, say $p = i_1(y)$ for some $y \in X$. Then $y = r(p) \in r(E') \subseteq X'$, and hence $p \in i_1(X')$.
+ Suppose that $U$ intersects a connected component $X' \subseteq X$. Choose a point $x \in U \cap X'$ and let $e \coloneqq j_1(x) = j_2(x)$. Let $C' \subseteq C$ be the connected component containing $e$. Then $j_1(X') \subseteq C'$ and $j_2(X') \subseteq C'$. Since $r(e)=x$, we also have $r(C') \subseteq X'$. We claim that
+ $$C' = j_1(X') \cup j_2(X').$$
+ The inclusion $\supseteq$ is clear. To show the inclusion $\subseteq$, pick any point $p \in C'$. We have either $p \in j_1(X)$ or $p \in j_2(X)$. Assume without loss of generality that $p \in j_1(X)$, say $p = j_1(y)$ for some $y \in X$. Then $y = r(p) \in r(C') \subseteq X'$, and hence $p \in j_1(X')$.
- The space $E'$ is Euclidean and therefore a Baire space. Thus, it cannot be the union of two closed sets with empty interior. Assume without loss of generality that $i_1(X')$ has non-empty interior in $E'$. Since $i_1(X') \cong X'$ is also Euclidean, the Invariance of Domain theorem implies that $X'$ and $E'$ have the same dimension and that $i_1(X')$ is open in $E'$. Since $i_1$ is a closed embedding, $i_1(X')$ is also closed in $E'$, and it is non-empty. Since $E'$ is connected, this implies
- $$i_1(X') = E'.$$
- Hence, for every $y \in X'$, we have $i_2(y) = i_1(z)$ for some $z \in X'$. Applying $r$, we obtain $y=z$, and hence $y \in U$. This proves that $U$ contains the entire component $X'$ and finishes the proof.
+ The space $C'$ is Euclidean and therefore a Baire space. Thus, it cannot be the union of two closed sets with empty interior. Assume without loss of generality that $j_1(X')$ has non-empty interior in $C'$. Since $j_1(X') \cong X'$ is also Euclidean, the Invariance of Domain theorem implies that $X'$ and $C'$ have the same dimension and that $j_1(X')$ is open in $C'$. Since $j_1$ is a closed embedding, $j_1(X')$ is also closed in $C'$, and it is non-empty. Since $C'$ is connected, this implies
+ $$j_1(X') = C'.$$
+ Hence, for every $y \in X'$, we have $j_2(y) = j_1(z)$ for some $z \in X'$. Applying $r$, we obtain $y=z$, and hence $y \in U$. This proves that $U$ contains the entire component $X'$ and finishes the proof.
label: Euclid_coprod_cocongruence_classification
- property: coquotients of cocongruences
diff --git a/database/data/categories/FinGrp.yaml b/database/data/categories/FinGrp.yaml
index da53ca2fc..77079f517 100644
--- a/database/data/categories/FinGrp.yaml
+++ b/database/data/categories/FinGrp.yaml
@@ -42,7 +42,7 @@ satisfied_properties:
proof: A direct argument is possible, but this can also be derived from the observation that $\FinGrp$ is the category of group objects in $(\FinSet,\times)$ and Borceux–Bourn, Example 2.2.16.
- property: effective congruences
- proof: '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.'
+ proof: 'Suppose we have a congruence $R \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 $R$ is the kernel pair of $X \to (X/R)_{\Grp}$ in $\Grp$. Also, the quotient $(X/R)_{\Grp}$ is finite; and the forgetful functor $\FinGrp \to \Grp$ is fully faithful and therefore reflects limits. Thus, we conclude that $R$ is the kernel pair of $X \to (X/R)_{\Grp}$ in $\FinGrp$ as well.'
- property: effective cocongruences
proof: 'A proof can be found in MO/511516. It even shows that every cocongruence in $\FinGrp$ is trivial. In short, the proof goes like this: We know that $\Grp$ has effective cocongruences. Using the fact that amalgamated sums of finite groups are residually finite, one can show that every cocongruence in $\FinGrp$ is also a cocongruence in $\Grp$.'
diff --git a/database/data/categories/FinSet_even.yaml b/database/data/categories/FinSet_even.yaml
index ab39306d5..b956f1e5a 100644
--- a/database/data/categories/FinSet_even.yaml
+++ b/database/data/categories/FinSet_even.yaml
@@ -59,10 +59,10 @@ satisfied_properties:
proof: In fact, every small diagram has a cocone in $\FinSet_{\even}$. We take the colimit in $\Set$ and then map it to $\{0,1\}$ via a constant map.
- property: effective congruences
- proof: Let $E \rightrightarrows X$ be a congruence in $\FinSet_{\even}$. This means that the induced map of sets $E \to X \times X$ is a monomorphism, i.e. injective, and that for every test object $T$ of $\FinSet_{\even}$, the induced injective map $\Hom(T,E) \to \Hom(T,X) \times \Hom(T,X)$ is an equivalence relation in $\Set$. By applying this to $T = \{0,1\}$ and constant maps, it is easy to check that $E \rightrightarrows X$ is a congruence in $\Set$. It is therefore the kernel pair of the projection $X \twoheadrightarrow X/E$ in $\Set$, and hence also in $\FinSet$. If $X/E$ has even cardinality, this remains true in $\FinSet_{\even}$, and we are done. If not, we simply compose the projection with the inclusion $X/E \hookrightarrow X/E + \{\ast\}$. The resulting map $X \to X/E + \{\ast\}$ is a morphism in $\FinSet_{\even}$ with kernel pair $E \rightrightarrows X$. (The last step is also an indication that quotients of congruences do not exist in general, which we will see later.)
+ proof: Let $R \rightrightarrows X$ be a congruence in $\FinSet_{\even}$. This means that the induced map of sets $R \to X \times X$ is a monomorphism, i.e. injective, and that for every test object $T$ of $\FinSet_{\even}$, the induced injective map $\Hom(T,R) \to \Hom(T,X) \times \Hom(T,X)$ is an equivalence relation in $\Set$. By applying this to $T = \{0,1\}$ and constant maps, it is easy to check that $R \rightrightarrows X$ is a congruence in $\Set$. It is therefore the kernel pair of the projection $X \twoheadrightarrow X/R$ in $\Set$, and hence also in $\FinSet$. If $X/R$ has even cardinality, this remains true in $\FinSet_{\even}$, and we are done. If not, we simply compose the projection with the inclusion $X/R \hookrightarrow X/R + \{\ast\}$. The resulting map $X \to X/R + \{\ast\}$ is a morphism in $\FinSet_{\even}$ with kernel pair $R \rightrightarrows X$. (The last step is also an indication that quotients of congruences do not exist in general, which we will see later.)
- property: effective cocongruences
- proof: Let $X \rightrightarrows Q$ be a cocongruence in $\FinSet_{\even}$. In particular, it is a coreflexive corelation. Then $X+X \to Q$ is an epimorphism, hence surjective. It follows that $X \rightrightarrows Q$ is also a coreflexive corelation in $\Set$. Since $\Set$ is co-Malcev and has effective cocongruences (by this result), there is a subset $Y \subseteq X$ such that $Q \cong X \sqcup_Y X$ in $\Set$, with $X \rightrightarrows Q$ corresponding to the two pushout inclusions. We have $\card(Q) = 2 \card(X) - \card(Y)$, so $\card(Y)$ is even. Hence, $Q \cong X \sqcup_Y X$ remains true in $\FinSet_{\even}$.
+ proof: Let $X \rightrightarrows C$ be a cocongruence in $\FinSet_{\even}$. In particular, it is a coreflexive corelation. Then $X+X \to C$ is an epimorphism, hence surjective. It follows that $X \rightrightarrows C$ is also a coreflexive corelation in $\Set$. Since $\Set$ is co-Malcev and has effective cocongruences (by this result), there is a subset $Y \subseteq X$ such that $C \cong X \sqcup_Y X$ in $\Set$, with $X \rightrightarrows C$ corresponding to the two pushout inclusions. We have $\card(C) = 2 \card(X) - \card(Y)$, so $\card(Y)$ is even. Hence, $C \cong X \sqcup_Y X$ remains true in $\FinSet_{\even}$.
label: FinSet_even_effective_cocongruences
- property: coquotients of cocongruences
diff --git a/database/data/categories/FinSet_odd.yaml b/database/data/categories/FinSet_odd.yaml
index 3997bef5e..a78849b86 100644
--- a/database/data/categories/FinSet_odd.yaml
+++ b/database/data/categories/FinSet_odd.yaml
@@ -52,13 +52,13 @@ satisfied_properties:
proof: The set $\{0,1,2\}$ is an extremal cogenerator even in $\Set$. Now apply Lemma 10 here.
- property: effective congruences
- proof: Let $E \rightrightarrows X$ be a congruence in $\FinSet_{\odd}$. By applying the (functorial) definition to the test object $T = \{\ast\}$, we see that it is a congruence in $\Set$, i.e. an equivalence relation, such that $E$ and $X$ are finite sets of odd cardinality. The finite set $X/E$ embeds into a finite set $Q$ of odd cardinality (either $X/E$ or $X/E + \{\ast\}$). Then $E \rightrightarrows X$ is the kernel pair of $X \twoheadrightarrow X/E \hookrightarrow Q$ in $\FinSet_{\odd}$.
+ proof: Let $R \rightrightarrows X$ be a congruence in $\FinSet_{\odd}$. By applying the (functorial) definition to the test object $T = \{\ast\}$, we see that it is a congruence in $\Set$, i.e. an equivalence relation, such that $R$ and $X$ are finite sets of odd cardinality. The finite set $X/R$ embeds into a finite set $Q$ of odd cardinality (either $X/R$ or $X/R + \{\ast\}$). Then $R \rightrightarrows X$ is the kernel pair of $X \twoheadrightarrow X/R \hookrightarrow Q$ in $\FinSet_{\odd}$.
- property: effective cocongruences
proof: >-
- Let $X \rightrightarrows Q$ be a cocongruence in $\FinSet_{\odd}$. The induced map
- $$\Hom(Q,\{0,1,2\}) \to \Hom(X,\{0,1,2\})^2 \cong \Hom(X+X, \{0,1,2\})$$
- is injective, which implies that $X+X \to Q$ is surjective (where $X+X$ denotes the coproduct in $\Set$, which does not exist in $\FinSet_{\odd}$). It follows that $X \rightrightarrows Q$ is a coreflexive corelation in $\Set$. Since $\Set$ is co-Malcev and has effective cocongruences (by this result), there is a subset $Y \subseteq X$ such that $Q \cong X \sqcup_Y X$ in $\Set$, with $X \rightrightarrows Q$ corresponding to the two pushout inclusions. We have $\card(Q) = 2 \card(X) - \card(Y)$, so $\card(Y)$ is odd. Hence, $Q \cong X \sqcup_Y X$ remains true in $\FinSet_{\odd}$.
+ Let $X \rightrightarrows C$ be a cocongruence in $\FinSet_{\odd}$. The induced map
+ $$\Hom(C,\{0,1,2\}) \to \Hom(X,\{0,1,2\})^2 \cong \Hom(X+X, \{0,1,2\})$$
+ is injective, which implies that $X+X \to C$ is surjective (where $X+X$ denotes the coproduct in $\Set$, which does not exist in $\FinSet_{\odd}$). It follows that $X \rightrightarrows C$ is a coreflexive corelation in $\Set$. Since $\Set$ is co-Malcev and has effective cocongruences (by this result), there is a subset $Y \subseteq X$ such that $C \cong X \sqcup_Y X$ in $\Set$, with $X \rightrightarrows C$ corresponding to the two pushout inclusions. We have $\card(C) = 2 \card(X) - \card(Y)$, so $\card(Y)$ is odd. Hence, $C \cong X \sqcup_Y X$ remains true in $\FinSet_{\odd}$.
label: FinSet_odd_effective_cocongruences
- property: coquotients of cocongruences
diff --git a/database/data/categories/FinSet_power_3.yaml b/database/data/categories/FinSet_power_3.yaml
index 6395bfd73..343519875 100644
--- a/database/data/categories/FinSet_power_3.yaml
+++ b/database/data/categories/FinSet_power_3.yaml
@@ -43,13 +43,13 @@ satisfied_properties:
proof: The set $\{0,1,2\}$ is an extremal cogenerator even in $\Set$. Now apply Lemma 10 here.
- property: effective congruences
- proof: Let $E \rightrightarrows X$ be a congruence in $\FinSet_{3^\bullet}$. By applying the (functorial) definition to the test object $T = \{\ast\}$, we see that it is a congruence in $\Set$, i.e. an equivalence relation, such that $E$ and $X$ are finite sets of cardinality a power of $3$. Since for every $n \in \IN$ we have $n \leq 3^n$, the finite set $X/E$ embeds into a finite set $Q$ of cardinality a power of $3$. Then $E \rightrightarrows X$ is the kernel pair of $X \twoheadrightarrow X/E \hookrightarrow Q$ in $\FinSet_{3^\bullet}$.
+ proof: Let $R \rightrightarrows X$ be a congruence in $\FinSet_{3^\bullet}$. By applying the (functorial) definition to the test object $T = \{\ast\}$, we see that it is a congruence in $\Set$, i.e. an equivalence relation, such that $R$ and $X$ are finite sets of cardinality a power of $3$. Since for every $n \in \IN$ we have $n \leq 3^n$, the finite set $X/R$ embeds into a finite set $Q$ of cardinality a power of $3$. Then $R \rightrightarrows X$ is the kernel pair of $X \twoheadrightarrow X/R \hookrightarrow Q$ in $\FinSet_{3^\bullet}$.
- property: effective cocongruences
proof: >-
- We will prove that, in fact, every cocongruence is trivial. Let $X \rightrightarrows Q$ be a cocongruence in $\FinSet_{3^\bullet}$. The induced map
- $$\Hom(Q,\{0,1,2\}) \to \Hom(X,\{0,1,2\})^2 \cong \Hom(X+X, \{0,1,2\})$$
- is injective, which implies that $X+X \to Q$ is surjective (where $X+X$ denotes the coproduct in $\Set$, which does not exist in $\FinSet_{3^\bullet}$). It follows that $X \rightrightarrows Q$ is a coreflexive corelation in $\Set$. Since $\Set$ is co-Malcev and has effective cocongruences (by this result), there is a subset $Y \subseteq X$ such that $Q \cong X \sqcup_Y X$ in $\Set$, with $X \rightrightarrows Q$ corresponding to the two pushout inclusions. If $X$ has cardinality $3^n$, the cardinality of $Q$ lies in the interval $[3^n,2 \cdot 3^n]$ and is a power of $3$. Thus, $Q$ also has cardinality $3^n$. It follows that $Y=X$ and that the cocongruence is isomorphic to $\id_X,\id_X : X \rightrightarrows X$. In particular, it is the cokernel pair of $\id_X : X \to X$.
+ We will prove that, in fact, every cocongruence is trivial. Let $X \rightrightarrows C$ be a cocongruence in $\FinSet_{3^\bullet}$. The induced map
+ $$\Hom(C,\{0,1,2\}) \to \Hom(X,\{0,1,2\})^2 \cong \Hom(X+X, \{0,1,2\})$$
+ is injective, which implies that $X+X \to C$ is surjective (where $X+X$ denotes the coproduct in $\Set$, which does not exist in $\FinSet_{3^\bullet}$). It follows that $X \rightrightarrows C$ is a coreflexive corelation in $\Set$. Since $\Set$ is co-Malcev and has effective cocongruences (by this result), there is a subset $Y \subseteq X$ such that $C \cong X \sqcup_Y X$ in $\Set$, with $X \rightrightarrows C$ corresponding to the two pushout inclusions. If $X$ has cardinality $3^n$, the cardinality of $C$ lies in the interval $[3^n,2 \cdot 3^n]$ and is a power of $3$. Thus, $C$ also has cardinality $3^n$. It follows that $Y=X$ and that the cocongruence is isomorphic to $\id_X,\id_X : X \rightrightarrows X$. In particular, it is the cokernel pair of $\id_X : X \to X$.
label: FinSet_power_3_trivial_cocongruences
- property: coquotients of cocongruences
@@ -89,9 +89,9 @@ unsatisfied_properties:
- property: quotients of congruences
proof: >-
- Partition a finite set $X$ of cardinality $9$ into sets of cardinalities $1,1,3,4$. This yields an equivalence relation $E \subseteq X \times X$ with
- $$\card(E) = 1^2 + 1^2 + 3^2 + 4^2 = 27 = 3^3.$$
- Thus, $E \rightrightarrows X$ is a congruence in $\FinSet_{3^\bullet}$. We already know that the inclusion functor $\FinSet_{3^\bullet} \hookrightarrow \Set$ is cocontinuous, so a quotient in $\FinSet_{3^\bullet}$ must be the quotient taken in $\Set$. However, since there are $4$ equivalence classes, the set $X/E$ has cardinality $4$. Thus, the quotient does not exist in $\FinSet_{3^\bullet}$.
+ Partition a finite set $X$ of cardinality $9$ into sets of cardinalities $1,1,3,4$. This yields an equivalence relation $R \subseteq X \times X$ with
+ $$\card(R) = 1^2 + 1^2 + 3^2 + 4^2 = 27 = 3^3.$$
+ Thus, $R \rightrightarrows X$ is a congruence in $\FinSet_{3^\bullet}$. We already know that the inclusion functor $\FinSet_{3^\bullet} \hookrightarrow \Set$ is cocontinuous, so a quotient in $\FinSet_{3^\bullet}$ must be the quotient taken in $\Set$. However, since there are $4$ equivalence classes, the set $X/R$ has cardinality $4$. Thus, the quotient does not exist in $\FinSet_{3^\bullet}$.
references:
- FinSet_power_3_inclusion_cocontinuous
diff --git a/database/data/categories/Free_fg(ZxZ).yaml b/database/data/categories/Free_fg(ZxZ).yaml
index a83a993a4..effaba0d4 100644
--- a/database/data/categories/Free_fg(ZxZ).yaml
+++ b/database/data/categories/Free_fg(ZxZ).yaml
@@ -36,17 +36,17 @@ satisfied_properties:
proof: >-
Since $(\IZ \times \IZ){-}\Mod$ is equivalent to $\Ab \times \Ab$ via $M \mapsto ((1,0) M, (0,1) M)$, and the equivalence maps $(\IZ \times \IZ)^n$ to $(\IZ^n,\IZ^n)$, the category $\Free_{\fg}(\IZ \times \IZ)$ is equivalent to the full subcategory of $\FreeAb_{\fg} \times \FreeAb_{\fg}$ consisting of those pairs of finitely generated free abelian groups $(A,B)$ such that $\rank(A)=\rank(B)$, i.e. $A \cong B$. We denote these equivalences by $M \mapsto (M_1,M_2)$.
- Let $E \rightrightarrows M$ be a congruence in $\Free_{\fg}(\IZ \times \IZ)$. By applying the definition to the test object $\IZ \times \IZ$, we see that it is a congruence in $(\IZ \times \IZ){-}\Mod$. Thus, we have
- $$E = \{(x,y) \in M \times M : x - y \in U\}$$
+ Let $R \rightrightarrows M$ be a congruence in $\Free_{\fg}(\IZ \times \IZ)$. By applying the definition to the test object $\IZ \times \IZ$, we see that it is a congruence in $(\IZ \times \IZ){-}\Mod$. Thus, we have
+ $$R = \{(x,y) \in M \times M : x - y \in U\}$$
for some $\IZ \times \IZ$-submodule $U \subseteq M$ (up to isomorphism), namely
- $$U = \{x \in M : (x,0) \in E\}.$$
+ $$U = \{x \in M : (x,0) \in R\}.$$
This implies
- $$E \cong M \oplus U.$$
- The pair $(U_1,U_2)$ of $\IZ$-modules corresponding to $U$ therefore satisfies $E_i \cong M_i \oplus U_i$ for $i=1,2$. Since $E_i$ is finitely generated and free, we see that $U_i$ is a finitely generated projective $\IZ$-module, which is therefore free. Moreover, the rank of $U_i$ is
- $$\rank(U_i) = \rank(E_i) - \rank(M_i).$$
- Since $\rank(E_1) = \rank(E_2)$ and $\rank(M_1) = \rank(M_2)$, we conclude that $\rank(U_1) = \rank(U_2)$. We have shown that $U$ belongs to $\Free_{\fg}(\IZ \times \IZ)$.
+ $$R \cong M \oplus U.$$
+ The pair $(U_1,U_2)$ of $\IZ$-modules corresponding to $U$ therefore satisfies $R_i \cong M_i \oplus U_i$ for $i=1,2$. Since $R_i$ is finitely generated and free, we see that $U_i$ is a finitely generated projective $\IZ$-module, which is therefore free. Moreover, the rank of $U_i$ is
+ $$\rank(U_i) = \rank(R_i) - \rank(M_i).$$
+ Since $\rank(R_1) = \rank(R_2)$ and $\rank(M_1) = \rank(M_2)$, we conclude that $\rank(U_1) = \rank(U_2)$. We have shown that $U$ belongs to $\Free_{\fg}(\IZ \times \IZ)$.
- The quotient of the congruence $E \rightrightarrows M$ in $(\IZ \times \IZ){-}\Mod$ is $M/U$, but this will not be the quotient in the subcategory of free modules. Instead, consider the congruences $E_i \rightrightarrows M_i$ for $i=1,2$ in $\Ab$, whose quotients in $\TorsFreeAb$ and hence also in $\FreeAb_{\fg}$ are the torsion-free reflections $(M_i / U_i) / T(M_i / U_i)$. The rank of this abelian group is $\rank(M_i) - \rank(U_i)$, which therefore does not depend on $i$. Thus, the pair of these quotients belongs to $\Free_{\fg}(\IZ \times \IZ)$.
+ The quotient of the congruence $R \rightrightarrows M$ in $(\IZ \times \IZ){-}\Mod$ is $M/U$, but this will not be the quotient in the subcategory of free modules. Instead, consider the congruences $R_i \rightrightarrows M_i$ for $i=1,2$ in $\Ab$, whose quotients in $\TorsFreeAb$ and hence also in $\FreeAb_{\fg}$ are the torsion-free reflections $(M_i / U_i) / T(M_i / U_i)$. The rank of this abelian group is $\rank(M_i) - \rank(U_i)$, which therefore does not depend on $i$. Thus, the pair of these quotients belongs to $\Free_{\fg}(\IZ \times \IZ)$.
unsatisfied_properties:
- property: skeletal
diff --git a/database/data/categories/Grp.yaml b/database/data/categories/Grp.yaml
index e5d7c4136..e50670434 100644
--- a/database/data/categories/Grp.yaml
+++ b/database/data/categories/Grp.yaml
@@ -37,7 +37,7 @@ satisfied_properties:
- property: Malcev
proof: >-
See Borceux–Bourn, Example 2.2.4.
- Alternatively, here is a direct proof: let $G$ be a group and let $U \subseteq G^2$ be a subgroup containing the diagonal. Then $N \coloneqq \{g \in G : (g,1) \in U\}$ is clearly a subgroup of $G$. It is a normal subgroup because, if $g \in N$ and $h \in G$, then $U$ contains $(h,h) (g,1) (h,h)^{-1} = (h g h^{-1},1)$, i.e. $h g h^{-1} \in N$. Moreover, $U$ contains $(g,g')$ if and only if it contains $(g,g') (g',g')^{-1} = (g g'^{-1},1)$, i.e. $g g'^{-1} \in N$. This means that $U$ is the congruence induced by the normal subgroup $N \subseteq G$ and is therefore transitive and symmetric.
+ Alternatively, here is a direct proof: let $q_1, q_2 : R \rightrightarrows G$ be a reflexive relation. Since the induced homomorphism $(q_1,q_2) : R \to G^2$ is a monomorphism, hence injective, we may assume that $R \subseteq G^2$ is a subgroup and that $q_1,q_2$ are the two projections. By reflexivity, $R$ contains the diagonal. Then $N \coloneqq \{g \in G : (g,1) \in R\}$ is clearly a subgroup of $G$. It is a normal subgroup because, if $g \in N$ and $h \in G$, then $R$ contains $(h,h) (g,1) (h,h)^{-1} = (h g h^{-1},1)$, i.e. $h g h^{-1} \in N$. Moreover, $R$ contains $(g,g')$ if and only if it contains $(g,g') (g',g')^{-1} = (g g'^{-1},1)$, i.e. $g g'^{-1} \in N$. This means that $R$ is the congruence induced by the normal subgroup $N \subseteq G$ and is therefore transitive and symmetric.
label: Grp_malcev
- property: effective cocongruences
diff --git a/database/data/categories/Grp_c.yaml b/database/data/categories/Grp_c.yaml
index b2bf5ceb2..1b198df6c 100644
--- a/database/data/categories/Grp_c.yaml
+++ b/database/data/categories/Grp_c.yaml
@@ -63,11 +63,11 @@ satisfied_properties:
proof: This follows from Lemma 7 here applied to the inclusion functor $\Grp_\c \hookrightarrow \Grp$ into the regular category $\Grp$ and the description of regular epimorphisms below.
- property: effective congruences
- proof: 'A congruence on a countable group $G$ has the form $\{(g,h) \in G^2 : g^{-1} h \in N \}$ for some normal subgroup $N \subseteq G$. It is the kernel pair of the projection $p : G \twoheadrightarrow G/N$ in $\Grp$, but also in $\Grp_\c$ since $G/N$ is countable.'
+ proof: 'Let $q_1,q_2 : R \rightrightarrows G$ be a congruence in $\Grp_\c$. Since the induced homomorphism $(q_1,q_2) : R \to G \times G$ is a monomorphism, hence injective (see below). Thus, we may assume that $R \subseteq G \times G$ is a subgroup and that $q_1,q_2$ are the two projections. By reflexivity, $R$ contains the diagonal of $G$. We know from the proof that $\Grp$ is Malcev that $R = \{(g,h) \in G^2 : g^{-1} h \in N \}$ for some normal subgroup $N \subseteq G$. It is the kernel pair of the projection $p : G \twoheadrightarrow G/N$ in $\Grp$, but also in $\Grp_\c$ since $G/N$ is countable.'
- property: effective cocongruences
proof: >-
- Let $G + G \twoheadrightarrow H$ be a cocongruence in $\Grp_\c$. Since $\Grp_\c \hookrightarrow \Grp$ is closed under finite colimits, this is the same as a cocongruence in $\Grp$ where $G,H \in \Grp$ happen to be countable groups. Since we already know that $\Grp$ has effective cocongruences, the cocongruence is the cokernel pair of some homomorphism of groups $K \to H$. If $K' \subseteq H$ denotes the image of $K$, it is then also the cokernel pair of the inclusion $K' \hookrightarrow H$, and $K'$ is countable.
+ Let $G \rightrightarrows C$ be a cocongruence in $\Grp_\c$. Since $\Grp_\c \hookrightarrow \Grp$ is closed under finite colimits, this is the same as a cocongruence in $\Grp$ where $G,C \in \Grp$ happen to be countable groups. Since we already know that $\Grp$ has effective cocongruences, the cocongruence is the cokernel pair of some homomorphism of groups $K \to C$. If $K' \subseteq C$ denotes the image of $K$, it is then also the cokernel pair of the inclusion $K' \hookrightarrow C$, and $K'$ is countable.
unsatisfied_properties:
- property: skeletal
diff --git a/database/data/categories/Grp_fg.yaml b/database/data/categories/Grp_fg.yaml
index c4fa55fe9..1322ecb32 100644
--- a/database/data/categories/Grp_fg.yaml
+++ b/database/data/categories/Grp_fg.yaml
@@ -48,7 +48,7 @@ satisfied_properties:
- property: effective congruences
proof: >-
- Let $p_1,p_2 : E \rightrightarrows G$ be a congruence in $\Grp_\fg$. Since the pair is jointly monomorphic, the induced homomorphism $(p_1,p_2) : E \to G \times G$ is a monomorphism, hence injective (see below). Thus, $E$ is isomorphic to a subgroup $R \subseteq G \times G$, which contains the diagonal of $G$. We know from the proof that $\Grp$ is Malcev that $R$ is the congruence induced by the normal subgroup $N \coloneqq \{x \in G : (x,1) \in R\}$, i.e. $R$ is the kernel pair of the projection $h : G \to G/N$ in $\Grp$. Since $G/N$ and $R \cong E$ are finitely generated and $\Grp_\fg \hookrightarrow \Grp$ is fully faithful, $R$ is also the kernel pair of $h$ in $\Grp_\fg$.
+ Let $q_1,q_2 : R \rightrightarrows G$ be a congruence in $\Grp_\fg$. Since the induced homomorphism $(q_1,q_2) : R \to G \times G$ is a monomorphism, hence injective (see below). Thus, we may assume that $R \subseteq G \times G$ is a subgroup and that $q_1,q_2$ are the two projections. By reflexivity, $R$ contains the diagonal of $G$. We know from the proof that $\Grp$ is Malcev that $R$ is the congruence induced by the normal subgroup $N \coloneqq \{x \in G : (x,1) \in R\}$, i.e. $R$ is the kernel pair of the projection $h : G \to G/N$ in $\Grp$. Since $G/N$ and $R$ are finitely generated and $\Grp_\fg \hookrightarrow \Grp$ is fully faithful, $R$ is also the kernel pair of $h$ in $\Grp_\fg$.
references:
- Grp_malcev
@@ -122,7 +122,7 @@ unsatisfied_properties:
proof: >-
We show that if $G$ is a finitely generated group and $L \subseteq G$ is a subgroup that is not finitely generated, then the cokernel pair of $L \hookrightarrow G$ in $\Grp$ is a cocongruence in $\Grp_\fg$ without an equalizer. Such subgroups exist, for example the kernel $L \subseteq F_2$ from the proof that $\Grp_\fg$ has no kernels.
- Let $E \coloneqq G \sqcup_L G$ be the pushout in $\Grp$ with its two inclusions $i_1,i_2 : G \rightrightarrows E$. Then $E$ is finitely generated, since it is generated by $i_1(G) \cup i_2(G)$, and $i_1,i_2$ is a cocongruence in $\Grp$. Since $\Grp_\fg$ is a full subcategory containing $G$ and $E$, it is also a cocongruence in $\Grp_\fg$.
+ Let $C \coloneqq G \sqcup_L G$ be the pushout in $\Grp$ with its two inclusions $j_1,j_2 : G \rightrightarrows C$. Then $C$ is finitely generated, since it is generated by $j_1(G) \cup j_2(G)$, and $j_1,j_2$ is a cocongruence in $\Grp$. Since $\Grp_\fg$ is a full subcategory containing $G$ and $C$, it is also a cocongruence in $\Grp_\fg$.
Since $\Grp$ is mono-regular, $L \hookrightarrow G$ is a regular monomorphism in $\Grp$. By this lemma, it is therefore the equalizer of its cokernel pair $i_1,i_2$ in $\Grp$. Now assume that $i_1,i_2$ have an equalizer $e : K \to G$ in $\Grp_\fg$. Since the inclusion $\Grp_\fg \hookrightarrow \Grp$ preserves limits (see the proof that $\Grp_\fg$ has no kernels), $e$ is also an equalizer of $i_1,i_2$ in $\Grp$. So $K \cong L$, which is not finitely generated, a contradiction.
references:
diff --git a/database/data/categories/LRS_R.yaml b/database/data/categories/LRS_R.yaml
index 02890a01f..55e0863eb 100644
--- a/database/data/categories/LRS_R.yaml
+++ b/database/data/categories/LRS_R.yaml
@@ -74,7 +74,7 @@ unsatisfied_properties:
proof: This is because already the full subcategory $\Sch_R$ of $R$-schemes is not Malcev.
- property: co-Malcev
- proof: 'We can adjust the proof for $\Top$ (see MO/509548) as follows: Let $K$ be a residue field of $R$, let $X$ be a singleton and $Y = \{u,v\}$ be the Sierpiński space where $\{u\}$ is open, but $\{v\}$ is not. Endow both with the sheaf of locally constant functions to $K$. Thus, $\O_X(X) = K$, $\O_Y(Y) = \O_Y(\{u\}) = K$. There is a canonical morphism $p : X + X \to Y$. It is a coreflexive corelation that is not cosymmetric.'
+ proof: 'We can adjust the proof for $\Top$ (see MO/509548) as follows: Let $K$ be a residue field of $R$, let $X$ be a singleton and $C = \{u,v\}$ be the Sierpiński space where $\{u\}$ is open, but $\{v\}$ is not. Endow both with the sheaf of locally constant functions to $K$. Thus, $\O_X(X) = K$, $\O_C(C) = \O_C(\{u\}) = K$. Let $j_1, j_2 : X \rightrightarrows C$ be the two canonical morphisms with images $u$ and $v$, respectively. They form a coreflexive corelation that is not cosymmetric.'
references:
- Top_not_co-malcev
diff --git a/database/data/categories/Man.yaml b/database/data/categories/Man.yaml
index 8bb754c49..6572969fa 100644
--- a/database/data/categories/Man.yaml
+++ b/database/data/categories/Man.yaml
@@ -41,13 +41,13 @@ satisfied_properties:
- property: coquotients of cocongruences
proof: >-
- Let $p : X + X \twoheadrightarrow E$ be a cocongruence with coreflexivity morphism $r : E \to X$, so that $r \circ p : X + X \to X$ is the codiagonal. Since $p$ is an epimorphism, it has dense image (see below). We first claim that in fact $p$ also has closed image and therefore is surjective. 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.
+ Let $j_1, j_2 : X \rightrightarrows C$ be a cocongruence with coreflexivity morphism $r : C \to X$, so that $r \circ j_1 = r \circ j_2 = \id_X$. Since $(j_1;j_2) : X + X \to C$ is an epimorphism, it has dense image (see below). We first claim that in fact $(j_1;j_2)$ also has closed image and therefore is surjective. Because $r \circ j_1 = \id_X$, the image of $j_1$ is the equalizer of $\id_C$ and $j_1 \circ r$, hence closed. Likewise, the image of $j_2$ is closed. Thus, the image of $(j_1;j_2)$, 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$.
+ Now, since the pushforward maps of tangent spaces compose to the identity, we see that $(j_1;j_2)$ 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 $C$ must locally be the same as the dimension of $X$. This implies that in fact $(j_1;j_2)$ 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 $j_1$ and $j_2$.
label: Man_coquotients_congruences
- property: effective cocongruences
- proof: '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$.'
+ proof: 'From the proof that $\Man$ has coquotients of cocongruences, we know that for any cocongruence $X \rightrightarrows C$, there is a clopen submanifold $U$ of $X$ such that the fibers of $r : C \twoheadrightarrow X$ have one point on $U$, and two points on $X \setminus U$. Therefore, $C$ is the cokernel pair of the inclusion map $U \hookrightarrow X$.'
references:
- Man_coquotients_congruences
diff --git a/database/data/categories/Meas.yaml b/database/data/categories/Meas.yaml
index 073a4aa90..040e6a84c 100644
--- a/database/data/categories/Meas.yaml
+++ b/database/data/categories/Meas.yaml
@@ -76,43 +76,43 @@ satisfied_properties:
- property: co-Malcev
proof: >-
- Let $i_1,i_2 : X \rightrightarrows R$ be a coreflexive corelation of measurable spaces. Thus, $i_1,i_2$ are jointly surjective measurable maps with a common retraction $r : R \twoheadrightarrow X$.
- To show that $(i_1,i_2)$ is cosymmetric, define the map of sets $s : R \to R$ by
- $$s(i_1(x)) \coloneqq i_2(x), \quad s(i_2(x)) \coloneqq i_1(x).$$
- This is well-defined by a direct calculation or by using the fact that $\Set$ is co-Malcev. We need to show that $s$ is measurable. To this end, let $B \subseteq R$ be a measurable subset. Its preimages
- $$A_1 \coloneqq i_1^*(B), \quad A_2 \coloneqq i_2^*(B)$$
+ Let $j_1,j_2 : X \rightrightarrows C$ be a coreflexive corelation of measurable spaces. Thus, $j_1,j_2$ are jointly surjective measurable maps with a common retraction $r : C \twoheadrightarrow X$.
+ To show that $(j_1,j_2)$ is cosymmetric, define the map of sets $s : C \to C$ by
+ $$s(j_1(x)) \coloneqq j_2(x), \quad s(j_2(x)) \coloneqq j_1(x).$$
+ This is well-defined by a direct calculation or by using the fact that $\Set$ is co-Malcev. We need to show that $s$ is measurable. To this end, let $B \subseteq C$ be a measurable subset. Its preimages
+ $$A_1 \coloneqq j_1^*(B), \quad A_2 \coloneqq j_2^*(B)$$
are measurable subsets of $X$. We claim that
$$s^*(B) = \bigl((r^*(A_1) \cup r^*(A_2)) \setminus B\bigr) \cup r^*(A_1 \cap A_2), \tag{1}$$
- which will prove in particular that $s^*(B)$ is measurable, as required. Let $y \in R$. Since $R = i_1(X) \cup i_2(X)$, we may assume without loss of generality that $y = i_1(x)$ for some $x \in X$. The following are equivalent:
+ which will prove in particular that $s^*(B)$ is measurable, as required. Let $y \in C$. Since $C = j_1(X) \cup j_2(X)$, we may assume without loss of generality that $y = j_1(x)$ for some $x \in X$. The following are equivalent:
$$y \in (r^*(A_1) \cup r^*(A_2)) \setminus B \iff x \in (A_1 \cup A_2) \setminus A_1,$$
$$y \in r^*(A_1 \cap A_2) \iff x \in A_1 \cap A_2.$$
Hence, $y$ lies in the RHS of $(1)$ if and only if
- $$x \in ((A_1 \cup A_2) \setminus A_1) \cup (A_1 \cap A_2) = A_2 = i_2^*(B),$$
- which means that $s(y) = i_2(x)$ lies in $B$. This proves $(1)$.
-
- It remains to show that $(i_1,i_2)$ is cotransitive. We adopt the functorial point of view (simply to avoid talking about pushouts) and show that the subfunctor $\Hom(R,-) \hookrightarrow \Hom(X,-)^2$ is transitive. That is, given three measurable maps $u,v,w : X \rightrightrightarrows T$ into some measurable space $T$ and two measurable maps $f,g : R \rightrightarrows T$ such that
- $$f i_1 = u, \quad f i_2 = v = g i_1, \quad g i_2 = w,$$
- we need to show that there is a measurable map $h : R \to T$ with $h i_1 = u$ and $h i_2 = w$. We can certainly define $h$ as a map of sets by
- $$h(i_1(x)) \coloneqq u(x), \quad h(i_2(x)) \coloneqq w(x),$$
- which is well-defined by a direct calculation or again by using the fact that $\Set$ is co-Malcev. We need to show that $h$ is measurable. Let $C \subseteq T$ be a measurable subset. Its preimages
- $$B_1 \coloneqq f^*(C), \quad B_2 \coloneqq g^*(C)$$
- are measurable subsets of $R$. Notice that $f i_2 = g i_1$ implies
- $$A \coloneqq i_2^*(B_1) = i_1^*(B_2) \subseteq X.$$
+ $$x \in ((A_1 \cup A_2) \setminus A_1) \cup (A_1 \cap A_2) = A_2 = j_2^*(B),$$
+ which means that $s(y) = j_2(x)$ lies in $B$. This proves $(1)$.
+
+ It remains to show that $(j_1,j_2)$ is cotransitive. We adopt the functorial point of view (simply to avoid talking about pushouts) and show that the subfunctor $\Hom(C,-) \hookrightarrow \Hom(X,-)^2$ is transitive. That is, given three measurable maps $u,v,w : X \rightrightrightarrows T$ into some measurable space $T$ and two measurable maps $f,g : C \rightrightarrows T$ such that
+ $$f j_1 = u, \quad f j_2 = v = g j_1, \quad g j_2 = w,$$
+ we need to show that there is a measurable map $h : C \to T$ with $h j_1 = u$ and $h j_2 = w$. We can certainly define $h$ as a map of sets by
+ $$h(j_1(x)) \coloneqq u(x), \quad h(j_2(x)) \coloneqq w(x),$$
+ which is well-defined by a direct calculation or again by using the fact that $\Set$ is co-Malcev. We need to show that $h$ is measurable. Let $M \subseteq T$ be a measurable subset. Its preimages
+ $$B_1 \coloneqq f^*(M), \quad B_2 \coloneqq g^*(M)$$
+ are measurable subsets of $C$. Notice that $f j_2 = g j_1$ implies
+ $$A \coloneqq j_2^*(B_1) = j_1^*(B_2) \subseteq X.$$
We claim that
- $$h^*(C) = \bigl((B_1 \cup B_2) \setminus r^*(A)\bigr) \cup (B_1 \cap B_2), \tag{2}$$
- which will prove that $h^*(C)$ is measurable. Let $y \in R$. There are two cases to consider.
+ $$h^*(M) = \bigl((B_1 \cup B_2) \setminus r^*(A)\bigr) \cup (B_1 \cap B_2), \tag{2}$$
+ which will prove that $h^*(M)$ is measurable. Let $y \in C$. There are two cases to consider.
- Case 1: We have $y = i_1(x)$ for some $x \in X$. The following are equivalent:
- $$y \in (B_1 \cup B_2) \setminus r^*(A) \iff (u(x) \in C \vee v(x) \in C) \wedge v(x) \notin C,$$
- $$y \in B_1 \cap B_2 \iff (u(x) \in C \wedge v(x) \in C).$$
- Hence, $y$ lies in the RHS of $(2)$ if and only if $h(y) = u(x) \in C$, i.e. $y \in h^*(C)$.
+ Case 1: We have $y = j_1(x)$ for some $x \in X$. The following are equivalent:
+ $$y \in (B_1 \cup B_2) \setminus r^*(A) \iff (u(x) \in M \vee v(x) \in M) \wedge v(x) \notin M,$$
+ $$y \in B_1 \cap B_2 \iff (u(x) \in M \wedge v(x) \in M).$$
+ Hence, $y$ lies in the RHS of $(2)$ if and only if $h(y) = u(x) \in M$, i.e. $y \in h^*(M)$.
- Case 2: We have $y = i_2(x)$ for some $x \in X$. The following are equivalent:
- $$y \in (B_1 \cup B_2) \setminus r^*(A) \iff (v(x) \in C \vee w(x) \in C) \wedge v(x) \notin C,$$
- $$y \in B_1 \cap B_2 \iff (v(x) \in C \wedge w(x) \in C).$$
- Hence, $y$ lies in the RHS of $(2)$ if and only if $h(y) = w(x) \in C$, i.e. $y \in h^*(C)$.
+ Case 2: We have $y = j_2(x)$ for some $x \in X$. The following are equivalent:
+ $$y \in (B_1 \cup B_2) \setminus r^*(A) \iff (v(x) \in M \vee w(x) \in M) \wedge v(x) \notin M,$$
+ $$y \in B_1 \cap B_2 \iff (v(x) \in M \wedge w(x) \in M).$$
+ Hence, $y$ lies in the RHS of $(2)$ if and only if $h(y) = w(x) \in M$, i.e. $y \in h^*(M)$.
- This proves $(2)$. We conclude that the corelation $(i_1,i_2)$ is both cosymmetric and cotransitive.
+ This proves $(2)$. We conclude that the corelation $(j_1,j_2)$ is both cosymmetric and cotransitive.
unsatisfied_properties:
- property: skeletal
diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml
index 080f398a7..b9b5ae06a 100644
--- a/database/data/categories/Met.yaml
+++ b/database/data/categories/Met.yaml
@@ -151,12 +151,12 @@ unsatisfied_properties:
- property: effective cocongruences
proof: >-
- We will define a cocongruence on the interval $(0,1) \subseteq \IR$ where $E \coloneqq (-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
+ We will define a cocongruence on the interval $(0,1) \subseteq \IR$ where $C \coloneqq (-1, 0) \cup (0, 1) \subseteq \IR$, and the two maps $(0, 1) \rightrightarrows C$ 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$.
+ 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 $C$ would have to be a binary copower of $(0,1)$, which does not exist in $\Met$.
label: Met_no_effective_cocongruences
- property: pullback-stable regular epimorphisms
diff --git a/database/data/categories/Met_c.yaml b/database/data/categories/Met_c.yaml
index a6a92f71d..9bf98d2a1 100644
--- a/database/data/categories/Met_c.yaml
+++ b/database/data/categories/Met_c.yaml
@@ -49,7 +49,7 @@ satisfied_properties:
A more direct proof that $X \sqcup_C X$ is metrizable can be found at MSE/5147463.
- property: effective cocongruences
- proof: '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$.'
+ proof: 'Suppose we have a cocongruence $X \rightrightarrows C$ 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 $C$ is effective in $\Met_c$.'
- property: well-powered
proof: This follows easily from the fact that monomorphisms are injective in this category.
diff --git a/database/data/categories/Mon.yaml b/database/data/categories/Mon.yaml
index 85188b939..a1d6fc92a 100644
--- a/database/data/categories/Mon.yaml
+++ b/database/data/categories/Mon.yaml
@@ -77,11 +77,11 @@ unsatisfied_properties:
- property: effective cocongruences
proof: >-
We adapt the counterexample from MO/510744 for $\Ring$. Namely, consider the monoids
- $$\begin{align*} X & \coloneqq \langle p \mid p^2 = p \rangle \cong (\{ 0, 1 \}, \cdot),\\ E & \coloneqq \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.
+ $$\begin{align*} X & \coloneqq \langle p \mid p^2 = p \rangle \cong (\{ 0, 1 \}, \cdot),\\ C & \coloneqq \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 $C$ 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$.
+ $$C \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 $C$, so the equalizer of the two maps $X \rightrightarrows C$ is the trivial submonoid $\{ 1 \}$. Therefore, if $C$ 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$.
label: Mon_no_effective_cocongruences
special_objects:
diff --git a/database/data/categories/Mono.yaml b/database/data/categories/Mono.yaml
index 9b4b72aab..19cee9374 100644
--- a/database/data/categories/Mono.yaml
+++ b/database/data/categories/Mono.yaml
@@ -87,10 +87,10 @@ satisfied_properties:
- property: co-Malcev
proof: >-
- Suppose we have a coreflexive corelation $p : (X \sqcup X, X' \sqcup X') \twoheadrightarrow (E, E')$ with coreflexivity morphism $r : (E, E') \to (X, X')$. From the assumption that $p$ is an epimorphism, we have that $p : X \sqcup X \to E$ is a surjective function. Since $\Set$ is co-Malcev, it follows that $E \cong X \sqcup_Y X$ for some subset $Y \subseteq X$. It remains to show that $E' = (i_1)_*(X') \cup (i_2)_*(X') \subseteq X \sqcup_Y X$. Certainly, since we have a morphism $(X \sqcup_Y X, (i_1)_*(X') \cup (i_2)_*(X')) \to (E, E')$ induced by $p$, we must have $(i_1)_*(X') \cup (i_2)_*(X') \subseteq E'$. On the other hand, any element of $E'$ is an element of $E$ and hence is equal to either $i_1(x)$ or $i_2(x)$ for $x \in X$. In the first case, we must have $x = r(i_1(x)) \in X'$, so $i_1(x) \in i_1(X')$; and similarly for the second case.
+ Suppose we have a coreflexive corelation $j_1, j_2 : (X, X') \rightrightarrows (C, C')$ with coreflexivity morphism $r : (C, C') \to (X, X')$. From the assumption that $(j_1;j_2)$ is an epimorphism, we have that $(j_1;j_2) : X \sqcup X \to C$ is a surjective function. Since $\Set$ is co-Malcev, it follows that we may assume $C = X \sqcup_Y X$ for some subset $Y \subseteq X$, where $j_1, j_2$ are the two inclusions. It remains to show that $C' = j_1(X') \cup j_2(X')$. Certainly, since $j_1, j_2$ are morphisms in $\Mono$, we have $j_1(X') \cup j_2(X') \subseteq C'$. On the other hand, any element of $C'$ is an element of $C$ and hence is equal to either $j_1(x)$ or $j_2(x)$ for $x \in X$. In the first case, we must have $x = r(j_1(x)) \in X'$, so $j_1(x) \in j_1(X')$; and similarly for the second case.
- property: effective cocongruences
- proof: 'See the proof that $\Mono$ is co-Malcev: It shows that in fact any coreflexive corelation is equivalent to an effective cocongruence $X \sqcup X \twoheadrightarrow X \sqcup_Y X$.'
+ proof: 'See the proof that $\Mono$ is co-Malcev: It shows that in fact any coreflexive corelation is equivalent to an effective cocongruence $X \rightrightarrows X \sqcup_Y X$.'
check_redundancy: false
unsatisfied_properties:
diff --git a/database/data/categories/Pos.yaml b/database/data/categories/Pos.yaml
index 1e62c5a75..bfa9cf633 100644
--- a/database/data/categories/Pos.yaml
+++ b/database/data/categories/Pos.yaml
@@ -73,9 +73,9 @@ unsatisfied_properties:
- property: effective cocongruences
proof: >-
- 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$.
+ Let $X$ be $\IR$ with the standard (total) order, and let $C$ 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 C$ 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, i.e. the cokernel pair of some order-preserving map $P \to \IR$, then $P$ must be empty since the two maps $\IR \rightrightarrows E$ agree nowhere. So $E$ would have to be the coproduct poset $\IR + \IR$, giving a contradiction.
+ On the other hand, if this cocongruence on $\IR$ were effective, i.e. the cokernel pair of some order-preserving map $P \to \IR$, then $P$ must be empty since the two maps $\IR \rightrightarrows C$ agree nowhere. So $C$ would have to be the coproduct poset $\IR + \IR$, giving a contradiction.
label: Pos_no_effective_cocongruences
special_objects:
diff --git a/database/data/categories/PreOrd.yaml b/database/data/categories/PreOrd.yaml
index 24069bf17..af746df49 100644
--- a/database/data/categories/PreOrd.yaml
+++ b/database/data/categories/PreOrd.yaml
@@ -67,7 +67,7 @@ unsatisfied_properties:
proof: We know that $\Set$ does not have this property. Now use the contrapositive of the dual of Lemma 2 here applied to the functor $\Set \to \PreOrd$ that equips a set with the chaotic preorder.
- property: effective cocongruences
- proof: 'Consider the preordered set $E \coloneqq \{ a, b \}$ with the chaotic preorder. This represents the functor which sends a preordered set 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 preordered set with the trivial preorder.'
+ proof: 'Consider the preordered set $C \coloneqq \{ a, b \}$ with the chaotic preorder. This represents the functor which sends a preordered set to the pairs of elements $x,y$ with $x \le y$ and $y \le x$. Therefore, it defines a cocongruence $1 \rightrightarrows C$, 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 preordered set with the trivial preorder.'
special_objects:
initial object:
diff --git a/database/data/categories/Proj_fg(Re).yaml b/database/data/categories/Proj_fg(Re).yaml
index 70326f38d..f789032d8 100644
--- a/database/data/categories/Proj_fg(Re).yaml
+++ b/database/data/categories/Proj_fg(Re).yaml
@@ -46,11 +46,11 @@ satisfied_properties:
label: Proj_fg(Re)_self-dual
- property: quotients of congruences
- proof: 'Let $p_1,p_2 : E \rightrightarrows M$ be a congruence in $\Proj_\fg(R)$. In particular, it is a reflexive relation in $R{-}\Mod$. Thus, there is some submodule $U \subseteq M$ such that $E$ is isomorphic to the module $\{(x,y) \in M^2 : x-y \in U\}$, where $p_1,p_2$ are the two evident projections. Since $E \cong U \oplus M$ and $E$ is finitely generated and projective, it follows that $U$ is finitely generated and projective. Moreover, the coequalizer of $p_1,p_2$ in $R{-}\Mod$ is given by $M/U$, which is clearly finitely generated, and we claim that $M/U$ is also projective. For this, it suffices to prove that the monomorphism $U \hookrightarrow M$ splits, since then $M/U$ is a direct summand of $M$. But every monomorphism splits in this category since it is self-dual and every epimorphism splits by their classification below.'
+ proof: 'Let $q_1,q_2 : E \rightrightarrows M$ be a congruence in $\Proj_\fg(R)$. In particular, it is a reflexive relation in $R{-}\Mod$. Thus, there is some submodule $U \subseteq M$ such that $E$ is isomorphic to the module $\{(x,y) \in M^2 : x-y \in U\}$, where $q_1,q_2$ are the two evident projections. Since $E \cong U \oplus M$ and $E$ is finitely generated and projective, it follows that $U$ is finitely generated and projective. Moreover, the coequalizer of $q_1,q_2$ in $R{-}\Mod$ is given by $M/U$, which is clearly finitely generated, and we claim that $M/U$ is also projective. For this, it suffices to prove that the monomorphism $U \hookrightarrow M$ splits, since then $M/U$ is a direct summand of $M$. But every monomorphism splits in this category since it is self-dual and every epimorphism splits by their classification below.'
label: Proj_fg(Re)_dual_numbers_quotients_congruences
- property: effective congruences
- proof: 'We saw before that every congruence $p_1,p_2 : E \rightrightarrows M$ in $\Proj_\fg(R)$ is isomorphic to $\{(x,y) \in M^2 : x-y \in U\}$ for some direct summand $U \subseteq M$, where $p_1,p_2$ are the two projections. Thus, it is the kernel pair of the projection $M \to M/U$, which indeed lies in $\Proj_\fg(R)$.'
+ proof: 'We saw before that every congruence $q_1,q_2 : E \rightrightarrows M$ in $\Proj_\fg(R)$ is isomorphic to $\{(x,y) \in M^2 : x-y \in U\}$ for some direct summand $U \subseteq M$, where $q_1,q_2$ are the two projections. Thus, it is the kernel pair of the projection $M \to M/U$, which indeed lies in $\Proj_\fg(R)$.'
references:
- Proj_fg(Re)_dual_numbers_quotients_congruences
diff --git a/database/data/categories/Quiv_fc.yaml b/database/data/categories/Quiv_fc.yaml
index 2580437da..97ee12a17 100644
--- a/database/data/categories/Quiv_fc.yaml
+++ b/database/data/categories/Quiv_fc.yaml
@@ -72,7 +72,7 @@ satisfied_properties:
- FinSet_aleph1-cofiltered-limits
- property: effective cocongruences
- proof: More generally, let $G \rightrightarrows H$ be a coreflexive corelation in $\Quiv_{\fc}$. Since binary coproducts exist and the inclusion functor $\Quiv_{\fc} \hookrightarrow \Quiv$ preserves epimorphisms, it is a coreflexive corelation in $\Quiv$. Since $\Quiv$ is co-Malcev and has effective cocongruences (by this result), the pair $G \rightrightarrows H$ is the cokernel pair of some morphism $E \to G$ in $\Quiv$, namely (since equalizers exist, see here) the equalizer of $G \rightrightarrows H$. Since $G$ belongs to $\Quiv_{\fc}$, also $E$ belongs to $\Quiv_{\fc}$. It follows that $G \rightrightarrows H$ is also the cokernel pair of $E \to G$ in $\Quiv_{\fc}$.
+ proof: More generally, let $G \rightrightarrows C$ be a coreflexive corelation in $\Quiv_{\fc}$. Since binary coproducts exist and the inclusion functor $\Quiv_{\fc} \hookrightarrow \Quiv$ preserves epimorphisms, it is a coreflexive corelation in $\Quiv$. Since $\Quiv$ is co-Malcev and has effective cocongruences (by this result), the pair $G \rightrightarrows C$ is the cokernel pair of some morphism $E \to G$ in $\Quiv$, namely (since equalizers exist, see here) the equalizer of $G \rightrightarrows C$. Since $G$ belongs to $\Quiv_{\fc}$, also $E$ belongs to $\Quiv_{\fc}$. It follows that $G \rightrightarrows C$ is also the cokernel pair of $E \to G$ in $\Quiv_{\fc}$.
unsatisfied_properties:
- property: skeletal
diff --git a/database/data/categories/SemiGrp.yaml b/database/data/categories/SemiGrp.yaml
index 62fe4a2ee..de14f8144 100644
--- a/database/data/categories/SemiGrp.yaml
+++ b/database/data/categories/SemiGrp.yaml
@@ -63,8 +63,8 @@ unsatisfied_properties:
- property: effective cocongruences
proof: >-
The proof is similar to $\Mon$, i.e. we adapt the counterexample from MO/510744. Namely, consider the semigroups
- $$\begin{align*} X & \coloneqq \langle p \mid p^2 = p \rangle,\\ E & \coloneqq \langle p, q \mid p^2 = p,\, q^2 = q,\, pq = q,\, qp = p \rangle, \end{align*}$$
- whose underlying sets are $\{p\}$ and $\{p,q\}$, respectively. Then $X$ represents the functor sending a semigroup $A$ to its idempotents, and $E$ represents the relation on idempotents $a, b$ of $A$ that $ab = b$, $ba = a$. It is easy to check that this defines an equivalence relation (see MO/510744 for details). Since $p \ne q$ in $E$, the equalizer of the two maps $X \rightrightarrows E$ is the empty semigroup. Therefore, if $E$ were effective, it would be isomorphic to the coproduct $X \sqcup X$, whose underlying set consists of non-empty words in $p,q$ with $p,q$ strictly alternating. In particular, in this coproduct, $pq \ne q$.
+ $$\begin{align*} X & \coloneqq \langle p \mid p^2 = p \rangle,\\ C & \coloneqq \langle p, q \mid p^2 = p,\, q^2 = q,\, pq = q,\, qp = p \rangle, \end{align*}$$
+ whose underlying sets are $\{p\}$ and $\{p,q\}$, respectively. Then $X$ represents the functor sending a semigroup $A$ to its idempotents, and $C$ represents the relation on idempotents $a, b$ of $A$ that $ab = b$, $ba = a$. It is easy to check that this defines an equivalence relation (see MO/510744 for details). Since $p \ne q$ in $C$, the equalizer of the two maps $X \rightrightarrows C$ is the empty semigroup. Therefore, if $C$ were effective, it would be isomorphic to the coproduct $X \sqcup X$, whose underlying set consists of non-empty words in $p,q$ with $p,q$ strictly alternating. In particular, in this coproduct, $pq \ne q$.
references:
- Mon_no_effective_cocongruences
diff --git a/database/data/categories/Set_c.yaml b/database/data/categories/Set_c.yaml
index 343ec7801..f6f891358 100644
--- a/database/data/categories/Set_c.yaml
+++ b/database/data/categories/Set_c.yaml
@@ -51,7 +51,7 @@ satisfied_properties:
proof: This follows from Lemma 11 here since $\Set$ is countably extensive (even infinitary extensive) and its full subcategory $\Set_\c$ is closed under pullbacks and countable coproducts in $\Set$.
- property: effective congruences
- proof: '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.'
+ proof: 'Let $R \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 $R$ is the kernel pair of $X \to (X/R)_{\Set}$ in $\Set$. Also, the quotient $(X/R)_{\Set}$ is countable; and the forgetful functor $\Set_\c \to \Set$ is fully faithful and therefore reflects limits. Thus, we conclude that $R$ is the kernel pair of $X \to (X/R)_{\Set}$ in $\Set_\c$ as well.'
- property: regular
proof: This follows from Lemma 7 here applied to the inclusion functor $\Set_\c \hookrightarrow \Set$ into the regular category $\Set$ and the description of regular epimorphisms below.
diff --git a/database/data/categories/Set_c_inf.yaml b/database/data/categories/Set_c_inf.yaml
index ae6aae43c..b97355107 100644
--- a/database/data/categories/Set_c_inf.yaml
+++ b/database/data/categories/Set_c_inf.yaml
@@ -35,7 +35,7 @@ satisfied_properties:
proof: 'Let $f : X \to Y$ be a map of countably infinite sets. Its cokernel pair in $\Set$ is $Y \sqcup_X Y$. It is countable as a quotient of $Y \sqcup Y$, and infinite since the coprojections $Y \rightrightarrows Y \sqcup_X Y$ are injective, having the codiagonal $Y \sqcup_X Y \to Y$ as a left inverse. Hence, it is also a cokernel pair in the full subcategory $\Set_{\c,\infty}$.'
- property: effective congruences
- proof: 'Let $q_1,q_2 : E \rightrightarrows X$ be a congruence. Since $q_1,q_2$ are jointly monomorphic, the map $(q_1,q_2) : E \to X \times X$ is a monomorphism, hence injective (see below). Using constant maps $\IN \to X$, we see that its image $R \subseteq X \times X$ is an equivalence relation on $X$. Let $h : X \to (X/R) \sqcup \IN$ be the composite of the projection $X \to X/R$ with the coproduct inclusion (we add $\IN$ since $X/R$ may be finite). Its kernel pair in $\Set$ is $R \cong E$, hence also in the full subcategory $\Set_{\c,\infty}$.'
+ proof: 'Let $q_1,q_2 : R \rightrightarrows X$ be a congruence. Since $q_1,q_2$ are jointly monomorphic, the map $(q_1,q_2) : R \to X \times X$ is a monomorphism, hence injective (see below). Thus, we may assume that $R \subseteq X \times X$ and that $q_1,q_2$ are the two projections. Using constant maps $\IN \to X$, we see that $R$ is an equivalence relation on $X$. Let $h : X \to (X/R) \sqcup \IN$ be the composite of the projection $X \to X/R$ with the coproduct inclusion (we add $\IN$ since $X/R$ may be finite). Its kernel pair in $\Set$ is $R$, hence also in the full subcategory $\Set_{\c,\infty}$.'
- property: ℵ₁-filtered
proof: 'Every diagram $(X_i)_{i \in I}$ in $\Set_{\c,\infty}$ admits a cocone with vertex $\IN$, given by the constant maps $X_i \to \IN$ with value $0$.'
diff --git a/database/data/categories/Set_family_mostly_1.yaml b/database/data/categories/Set_family_mostly_1.yaml
index dde08e42e..cce361162 100644
--- a/database/data/categories/Set_family_mostly_1.yaml
+++ b/database/data/categories/Set_family_mostly_1.yaml
@@ -53,7 +53,7 @@ satisfied_properties:
proof: Let $R \rightrightarrows X$ be a congruence in $\Set^{(I)}_1$. We claim that it is the kernel pair of its coequalizer $X \twoheadrightarrow X/R$. This certainly holds in $\Set$, and for every $i \in I$, the pair $R_i \rightrightarrows X_i$ is a congruence in $\Set$. Therefore, the claim follows since kernel pairs (in fact, all limits) and coequalizers (in fact, all connected colimits) are constructed pointwise.
- property: effective cocongruences
- proof: Let $X \rightrightarrows R$ be a cocongruence in $\Set^{(I)}_1$. We claim that it is the cokernel pair of its equalizer $E \hookrightarrow X$. This certainly holds in $\Set$, and for every $i \in I$, the pair $X_i \rightrightarrows R_i$ is a cocongruence in $\Set$. Therefore, the claim follows since cokernel pairs (in fact, all connected colimits) and equalizers (in fact, all limits) are constructed pointwise.
+ proof: Let $X \rightrightarrows C$ be a cocongruence in $\Set^{(I)}_1$. We claim that it is the cokernel pair of its equalizer $E \hookrightarrow X$. This certainly holds in $\Set$, and for every $i \in I$, the pair $X_i \rightrightarrows C_i$ is a cocongruence in $\Set$. Therefore, the claim follows since cokernel pairs (in fact, all connected colimits) and equalizers (in fact, all limits) are constructed pointwise.
unsatisfied_properties:
- property: skeletal
diff --git a/database/data/categories/Set_ff.yaml b/database/data/categories/Set_ff.yaml
index 87ac2b5f1..392390a7d 100644
--- a/database/data/categories/Set_ff.yaml
+++ b/database/data/categories/Set_ff.yaml
@@ -69,12 +69,12 @@ satisfied_properties:
label: Set_ff_quotients_congruences
- property: effective congruences
- proof: 'Let $f, g : E \rightrightarrows X$ be a congruence in $\Set_\ff$. From the proof on quotients of congruences in $\Set_\ff$, we have a quotient map $p : X \to X/E$ in $\Set_\ff$, 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_\ff$. 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, $e$ must be finite-to-one as well.'
+ proof: 'Let $q_1, q_2 : R \rightrightarrows X$ be a congruence in $\Set_\ff$. From the proof on quotients of congruences in $\Set_\ff$, we have a quotient map $p : X \to X/R$ in $\Set_\ff$, and $R$ is the kernel pair of $p$ in $\Set$. It remains to see that $R$ is also the kernel pair of $p$ in $\Set_\ff$. 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 R$ in $\Set$ with $x_1 = q_1 \circ e$ and $x_2 = q_2 \circ e$. Since $q_1 \circ e$ is finite-to-one, $e$ must be finite-to-one as well.'
references:
- Set_ff_quotients_congruences
- property: effective cocongruences
- proof: 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Set_\ff$. 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_\ff$ 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 that $c$ is finite-to-one as well.'
+ proof: 'Suppose we have a cocongruence $j_1, j_2 : X \rightrightarrows C$ in $\Set_\ff$. Then it is a coreflexive corelation in $\Set$. Since $\Set$ is co-Malcev and has effective cocongruences, that implies $C$ 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 $j_1$ and $j_2$, then $C$ is also the cokernel pair of $\inc_Y$ in $\Set$. It remains to see that $C$ is the cokernel pair of $\inc_Y$ in $\Set_\ff$ as well. Thus, suppose $a, b : X \rightrightarrows T$ are such that $a |_Y = b |_Y$. Then there is a unique $u : C \to T$ in $\Set$ with $a = u \circ j_1$ and $b = u \circ j_2$. Since $(j_1;j_2) : X + X \to C$ is surjective and $u \circ (j_1;j_2) = (a;b)$ is finite-to-one, we see that $u$ is finite-to-one as well.'
- property: ℵ₁-accessible
proof: 'We first show that $\aleph_1$-directed colimits exist and are preserved by the forgetful functor to $\Set$. Let $(X_i)_{i \in I}$ be a diagram in $\Set_\ff$ indexed by an $\aleph_1$-directed poset $I$. Let $(u_i : X_i \to X)$ be the colimit in $\Set$. Each map $u_i$ is finite-to-one: Otherwise, some fiber $u_i^*(\{x\}) \subseteq X_i$ contains infinitely many elements $a_1,a_2,\dotsc$. For every $n \geq 1$ we find $i_n \geq i$ such that $a_1,a_n$ have the same image in $X_{i_n}$. Let $i_\infty \in I$ be an upper bound of all $i_n$. Then all $a_n$ have the same image in $X_{i_\infty}$. This is a contradiction since $X_i \to X_{i_\infty}$ is finite-to-one. Now if $f : X \to Y$ is a map such that each $f \circ u_i$ is finite-to-one, then $f$ is finite-to-one as well: If a fiber $f^*(\{y\})$ contains infinitely many distinct elements $x_1,x_2,\dotsc$, there is some index $i$ such that all have a preimage in $X_i$, but then $(f \circ u_i)^*(\{y\})$ would be infinite. This concludes the proof that $\aleph_1$-directed colimits exist. In $\Set$, every set $X$ is the $\aleph_1$-directed colimit of its countable subsets. This remains true in $\Set_\ff$ because a map $X \to Y$ is finite-to-one as long as each restriction to a countable subset of $X$ is finite-to-one. Moreover, every countable set is $\aleph_1$-presentable in $\Set$, but also in $\Set_\ff$.'
diff --git a/database/data/categories/SetxSet_0_fin.yaml b/database/data/categories/SetxSet_0_fin.yaml
index 93091d59d..1876d1ce5 100644
--- a/database/data/categories/SetxSet_0_fin.yaml
+++ b/database/data/categories/SetxSet_0_fin.yaml
@@ -60,7 +60,7 @@ satisfied_properties:
proof: Let $(R,S) \rightrightarrows (A,B)$ be a congruence in $(\Set \times \Set)_{\varnothing,\fin}$. Since finite limits are constructed pointwise, it is also a congruence in $\Set \times \Set$, and therefore a pair of congruences in $\Set$. Thus, the congruence is the kernel pair of $(A,B) \to (A/R,B/S)$ in $\Set \times \Set$. It remains to show that $(A/R,B/S)$ belongs to $(\Set \times \Set)_{\varnothing,\fin}$. If $A$ is empty, then $A/R$ is empty, and the claim holds. Otherwise, $B$ is finite, and hence $B/S$ is finite.
- property: effective cocongruences
- proof: More generally, let $(A,B) \rightrightarrows (R,S)$ be a coreflexive corelation in $(\Set \times \Set)_{\varnothing,\fin}$. Since binary copowers exist and the forgetful functor to $\Set \times \Set$ preserves epimorphisms (see their classification below), it is a coreflexive corelation in $\Set \times \Set$. Any coreflexive corelation in $\Set \times \Set$ is an effective cocongruence (by this result). Therefore, using this result, $(A,B) \rightrightarrows (R,S)$ is the cokernel pair of its equalizer. Since the equalizer belongs to $(\Set \times \Set)_{\varnothing,\fin}$, we are done.
+ proof: More generally, let $(A,B) \rightrightarrows (C,D)$ be a coreflexive corelation in $(\Set \times \Set)_{\varnothing,\fin}$. Since binary copowers exist and the forgetful functor to $\Set \times \Set$ preserves epimorphisms (see their classification below), it is a coreflexive corelation in $\Set \times \Set$. Any coreflexive corelation in $\Set \times \Set$ is an effective cocongruence (by this result). Therefore, using this result, $(A,B) \rightrightarrows (C,D)$ is the cokernel pair of its equalizer. Since the equalizer belongs to $(\Set \times \Set)_{\varnothing,\fin}$, we are done.
- property: ℵ₁-accessible
proof: >-
diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml
index e51e99ac4..8eb4cee3b 100644
--- a/database/data/categories/Unif.yaml
+++ b/database/data/categories/Unif.yaml
@@ -70,37 +70,37 @@ satisfied_properties:
- property: co-Malcev
proof: >-
- Let $i_1,i_2 : X \rightrightarrows Y$ be a coreflexive corelation of uniform spaces, i.e. $i_1,i_2$ are jointly surjective uniform maps and there is a uniform map $r : Y \to X$ satisfying
- $$r \circ i_1 = r \circ i_2 = \id_X.$$
- In particular, $i_1,i_2$ are injective and satisfy $Y = i_1(X) \cup i_2(X)$ as sets. Moreover, $i_1(x) = i_1(x')$ implies $x = x'$ after applying $r$. First, we show that $(i_1,i_2)$ is cosymmetric, i.e. that there is a uniform map
- $$s : Y \to Y$$
+ Let $j_1,j_2 : X \rightrightarrows C$ be a coreflexive corelation of uniform spaces, i.e. $j_1,j_2$ are jointly surjective uniform maps and there is a uniform map $r : C \to X$ satisfying
+ $$r \circ j_1 = r \circ j_2 = \id_X.$$
+ In particular, $j_1,j_2$ are injective and satisfy $C = j_1(X) \cup j_2(X)$ as sets. Moreover, $j_1(x) = j_1(x')$ implies $x = x'$ after applying $r$. First, we show that $(j_1,j_2)$ is cosymmetric, i.e. that there is a uniform map
+ $$s : C \to C$$
such that
- $$s \circ i_1 = i_2, \quad s \circ i_2 = i_1.$$
- We define the map of sets $s : Y \to Y$ by $s(i_1(x)) \coloneqq i_2(x)$ and $s(i_2(x)) \coloneqq i_1(x)$. This is well-defined by a direct calculation using the above properties of $i_1,i_2$, but we can also use the fact that $\Set$ is co-Malcev. It remains to verify that $s$ is uniform. To this end, let $V$ be an entourage of $Y$. Since $Y$ is a uniform space, there is an entourage $W$ with
+ $$s \circ j_1 = j_2, \quad s \circ j_2 = j_1.$$
+ We define the map of sets $s : C \to C$ by $s(j_1(x)) \coloneqq j_2(x)$ and $s(j_2(x)) \coloneqq j_1(x)$. This is well-defined by a direct calculation using the above properties of $j_1,j_2$, but we can also use the fact that $\Set$ is co-Malcev. It remains to verify that $s$ is uniform. To this end, let $V$ be an entourage of $C$. Since $C$ is a uniform space, there is an entourage $W$ with
$$W \circ W \circ W \subseteq V.$$
- (This is the $\varepsilon/3$-trick in uniform space theory.) Since $i_1,i_2,r$ are uniform, the set
- $$U \coloneqq W^{\op} \cap (r \times r)^*(i_1 \times i_1)^*(W) \cap (r \times r)^*(i_2 \times i_2)^*(W)$$
- is an entourage of $Y$. We claim that $U \subseteq (s \times s)^*(V)$, which will establish that $(s \times s)^*(V)$ is an entourage, as required. For the proof, let $(a,b) \in U$. Up to symmetry, there are two cases to consider:
+ (This is the $\varepsilon/3$-trick in uniform space theory.) Since $j_1,j_2,r$ are uniform, the set
+ $$U \coloneqq W^{\op} \cap (r \times r)^*(j_1 \times j_1)^*(W) \cap (r \times r)^*(j_2 \times j_2)^*(W)$$
+ is an entourage of $C$. We claim that $U \subseteq (s \times s)^*(V)$, which will establish that $(s \times s)^*(V)$ is an entourage, as required. For the proof, let $(a,b) \in U$. Up to symmetry, there are two cases to consider:
- Case 1: We have $a = i_1(x)$ and $b = i_1(x')$ for some $x,x' \in X$. Since $(a,b) \in U$, we have $(a,b) \in (r \times r)^*(i_2 \times i_2)^*(W)$. Thus, $W$ contains the pair
- $$(i_2(r(a)),i_2(r(b))) = (i_2(x),i_2(x')) = (s(a),s(b)).$$
+ Case 1: We have $a = j_1(x)$ and $b = j_1(x')$ for some $x,x' \in X$. Since $(a,b) \in U$, we have $(a,b) \in (r \times r)^*(j_2 \times j_2)^*(W)$. Thus, $W$ contains the pair
+ $$(j_2(r(a)),j_2(r(b))) = (j_2(x),j_2(x')) = (s(a),s(b)).$$
Since $W \subseteq V$, we conclude that $(s(a),s(b)) \in V$.
- Case 2: We have $a = i_1(x)$ and $b = i_2(x')$ for some $x,x' \in X$. Since $(a,b) \in U$, the entourage $W$ contains $(b,a)= (i_2(x'),i_1(x))$, and it also contains the pairs $(i_1(r(a)), i_1(r(b))) = (i_1(x),i_1(x'))$ and $(i_2(r(a)), i_2(r(b))) = (i_2(x),i_2(x'))$. Thus, using infix notation,
- $$i_2(x) \; W \; i_2(x') \; W \; i_1(x) \; W \; i_1(x')$$
+ Case 2: We have $a = j_1(x)$ and $b = j_2(x')$ for some $x,x' \in X$. Since $(a,b) \in U$, the entourage $W$ contains $(b,a)= (j_2(x'),j_1(x))$, and it also contains the pairs $(j_1(r(a)), j_1(r(b))) = (j_1(x),j_1(x'))$ and $(j_2(r(a)), j_2(r(b))) = (j_2(x),j_2(x'))$. Thus, using infix notation,
+ $$j_2(x) \; W \; j_2(x') \; W \; j_1(x) \; W \; j_1(x')$$
which shows that
- $$(s(a),s(b)) = (i_2(x),i_1(x')) \in W \circ W \circ W \subseteq V.$$
- It remains to prove that $(i_1,i_2)$ is cotransitive. We adopt the functorial point of view and prove that the representable subfunctor $\Hom(Y,-) \hookrightarrow \Hom(X,-)^2$ is transitive. This means that for every uniform space $T$ and every triple of uniform maps $u,v,w : X \rightrightrightarrows T$ such that there are uniform maps $y_1,y_2 : Y \rightrightarrows T$ with
- $$y_1 i_1 = u, \quad y_1 i_2 = v = y_2 i_1, \quad y_2 i_2 = w,$$
- there is a uniform map $y_3 : Y \to T$ with $y_3 i_1 = u$ and $y_3 i_2 = w$. As before, we can easily define $y_3$ as a map of sets by
- $$y_3(i_1(x)) \coloneqq u(x), \quad y_3(i_2(x)) \coloneqq w(x)$$
+ $$(s(a),s(b)) = (j_2(x),j_1(x')) \in W \circ W \circ W \subseteq V.$$
+ It remains to prove that $(j_1,j_2)$ is cotransitive. We adopt the functorial point of view and prove that the representable subfunctor $\Hom(C,-) \hookrightarrow \Hom(X,-)^2$ is transitive. This means that for every uniform space $T$ and every triple of uniform maps $u,v,w : X \rightrightrightarrows T$ such that there are uniform maps $y_1,y_2 : C \rightrightarrows T$ with
+ $$y_1 j_1 = u, \quad y_1 j_2 = v = y_2 j_1, \quad y_2 j_2 = w,$$
+ there is a uniform map $y_3 : C \to T$ with $y_3 j_1 = u$ and $y_3 j_2 = w$. As before, we can easily define $y_3$ as a map of sets by
+ $$y_3(j_1(x)) \coloneqq u(x), \quad y_3(j_2(x)) \coloneqq w(x)$$
and verify that $y_3$ is well-defined, either by a direct calculation or using the fact that $\Set$ is co-Malcev. To prove that $y_3$ is uniform, let $E$ be an entourage of $T$. As in the proof of symmetry, choose an entourage $W$ of $T$ with $W \circ W \circ W \subseteq E$. Then
$$V \coloneqq (y_1 \times y_1)^*(W) \cap (y_2 \times y_2)^*(W) \cap (r \times r)^* (v \times v)^*(W)^{\op}$$
- is an entourage of $Y$, and we claim that $V \subseteq (y_3 \times y_3)^*(E)$, which will prove, as required, that $(y_3 \times y_3)^*(E)$ is an entourage. If $(a,b) \in V$, there are again two cases to consider:
+ is an entourage of $C$, and we claim that $V \subseteq (y_3 \times y_3)^*(E)$, which will prove, as required, that $(y_3 \times y_3)^*(E)$ is an entourage. If $(a,b) \in V$, there are again two cases to consider:
- Case 1: We have $a = i_1(x)$ and $b = i_1(x')$ for some $x,x' \in X$. Since $(a,b) \in V \subseteq (y_1 \times y_1)^*(W)$, we have $(y_1(a),y_1(b)) \in W$. Then
+ Case 1: We have $a = j_1(x)$ and $b = j_1(x')$ for some $x,x' \in X$. Since $(a,b) \in V \subseteq (y_1 \times y_1)^*(W)$, we have $(y_1(a),y_1(b)) \in W$. Then
$$(y_3(a),y_3(b)) = (u(x),u(x')) = (y_1(a), y_1(b)) \in W \subseteq E.$$
- Case 2: We have $a = i_1(x)$ and $b = i_2(x')$ for some $x,x' \in X$. Since $(a,b) \in V \subseteq (y_1 \times y_1)^*(W)$, the entourage $W$ contains $(y_1(a),y_1(b)) = (u(x),v(x'))$, and similarly it contains $(y_2(a),y_2(b)) = (v(x),w(x'))$. Furthermore, $W$ contains $(v(r(b)),v(r(a))) = (v(x'),v(x))$. Thus,
+ Case 2: We have $a = j_1(x)$ and $b = j_2(x')$ for some $x,x' \in X$. Since $(a,b) \in V \subseteq (y_1 \times y_1)^*(W)$, the entourage $W$ contains $(y_1(a),y_1(b)) = (u(x),v(x'))$, and similarly it contains $(y_2(a),y_2(b)) = (v(x),w(x'))$. Furthermore, $W$ contains $(v(r(b)),v(r(a))) = (v(x'),v(x))$. Thus,
$$u(x) \; W \; v(x') \; W \; v(x) \; W \; w(x'),$$
which shows
$$(y_3(a),y_3(b)) = (u(x),w(x')) \in W \circ W \circ W \subseteq E.$$
diff --git a/database/data/categories/Z.yaml b/database/data/categories/Z.yaml
index 84b59d4e3..a170d7d80 100644
--- a/database/data/categories/Z.yaml
+++ b/database/data/categories/Z.yaml
@@ -36,7 +36,7 @@ satisfied_properties:
proof: This follows immediately from the fact for $\Set$.
- property: effective congruences
- proof: '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$.'
+ proof: 'If we have a congruence $R \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 $R$.'
unsatisfied_properties:
- property: skeletal
diff --git a/database/data/categories/omega-Set.yaml b/database/data/categories/omega-Set.yaml
index 1f90354e8..8caf6addc 100644
--- a/database/data/categories/omega-Set.yaml
+++ b/database/data/categories/omega-Set.yaml
@@ -205,7 +205,7 @@ unsatisfied_properties:
- property: co-Malcev
proof: >-
- Consider the two possible morphisms $f, g : \nabla 1 \rightrightarrows \nabla 2$. This defines a corelation representing the functor which to $(X, R_X)$ assigns the binary relation on $X$ of two elements having a common realizer. That shows that this corelation is coreflexive, since by definition any element of an $\omega$-set has a realizer. However, it is easy to see that it is not cotransitive; for example, in the $\omega$-set
+ Consider the two possible morphisms $j_1, j_2 : \nabla 1 \rightrightarrows \nabla 2$. This defines a corelation representing the functor which to $(X, R_X)$ assigns the binary relation on $X$ of two elements having a common realizer. That shows that this corelation is coreflexive, since by definition any element of an $\omega$-set has a realizer. However, it is easy to see that it is not cotransitive; for example, in the $\omega$-set
$$\bigl(\{0,1,2\}, \{ (0, 0), (0, 1), (1, 1), (1, 2) \}\bigr),$$
the elements $0$ and $1$ have a common realizer, as do $1$ and $2$; but $0$ and $2$ do not have a common realizer.
diff --git a/database/data/category-implications/algebraic.yaml b/database/data/category-implications/algebraic.yaml
index af7725ebd..9af175a4f 100644
--- a/database/data/category-implications/algebraic.yaml
+++ b/database/data/category-implications/algebraic.yaml
@@ -84,8 +84,8 @@
$$Y : \C \to [G^{\op},\Set], \quad X \mapsto \Hom(-,X)|_{G^{\op}}.$$
It preserves all limits and, since the objects of $G$ are strongly finitely presentable, all sifted colimits. By Adámek–Rosický, Lemma 3.8, $Y$ is fully faithful.
- Now let $q_1, q_2 : E \rightrightarrows X$ be a congruence in $\C$. In particular, it is a reflexive pair. Since $\C$ has sifted colimits, it has reflexive coequalizers. In particular, $q_1, q_2$ have a coequalizer $h : X \to Q$. Let $T \in G$. Since $Y$ preserves this coequalizer and colimits in $[G^{\op},\Set]$ are computed pointwise, the map $h_* : \Hom(T,X) \to \Hom(T,Q)$ is a coequalizer of
- $$(q_1)_*, (q_2)_* : \Hom(T,E) \rightrightarrows \Hom(T,X)$$
+ Now let $q_1, q_2 : R \rightrightarrows X$ be a congruence in $\C$. In particular, it is a reflexive pair. Since $\C$ has sifted colimits, it has reflexive coequalizers. In particular, $q_1, q_2$ have a coequalizer $h : X \to Q$. Let $T \in G$. Since $Y$ preserves this coequalizer and colimits in $[G^{\op},\Set]$ are computed pointwise, the map $h_* : \Hom(T,X) \to \Hom(T,Q)$ is a coequalizer of
+ $$(q_1)_*, (q_2)_* : \Hom(T,R) \rightrightarrows \Hom(T,X)$$
in $\Set$. By definition of a congruence, $(q_1)_*, (q_2)_*$ are jointly injective and their image in $\Hom(T,X)^2$ is an equivalence relation, i.e. they form a congruence in $\Set$. Since $\Set$ has effective congruences, this lemma shows that $(q_1)_*, (q_2)_*$ is a kernel pair of $h_*$. Since $T \in G$ was arbitrary and limits in $[G^{\op},\Set]$ are computed pointwise, $Y(q_1), Y(q_2)$ is a kernel pair of $Y(h)$. Since $Y$ is fully faithful, it reflects limits. Hence, $q_1, q_2$ is a kernel pair of $h$.
Remark: For multi-algebraic categories, this result is also proven in Diers, Thm. 4.0 (see also its English translation).
diff --git a/database/data/category-implications/congruences.yaml b/database/data/category-implications/congruences.yaml
index c84a3a47a..6ce0c6732 100644
--- a/database/data/category-implications/congruences.yaml
+++ b/database/data/category-implications/congruences.yaml
@@ -5,7 +5,7 @@
- reflexive coequalizers
conclusions:
- quotients of congruences
- proof: A congruence $E \rightrightarrows X$ has a common section $X \to E$ given by the reflexivity morphism.
+ proof: A congruence $R \rightrightarrows X$ has a common section $X \to R$ given by the reflexivity morphism.
- id: congruences_include_kernel_pairs
assumptions:
@@ -39,7 +39,8 @@
- preadditive
conclusions:
- quotients of congruences
- proof: 'For any congruence $E$ on an object $X$ of a preadditive category, let $E_0$ be the kernel of $p_2 : E \to X$. The restriction of $p_1$ to $E_0$ is a monomorphism. We can then see that $E$ must be the pullback of $p_1 - p_2 : E \to X$ and $E_0 \hookrightarrow X$. Then the cokernel of $E_0 \hookrightarrow X$ is a quotient of $E$.'
+ proof: >-
+ Let $q_1, q_2 : R \rightrightarrows X$ be a congruence, let $k : R_0 \hookrightarrow R$ be the kernel of $q_2$, and let $m \coloneqq q_1 \circ k : R_0 \to X$. We claim that the cokernel of $m$ is a coequalizer of $q_1, q_2$. If $h \circ q_1 = h \circ q_2$, then $h \circ m = h \circ q_2 \circ k = 0$. Conversely, the image of $\Hom(R,R) \to \Hom(R,X)^2$, $e \mapsto (q_1 \circ e, q_2 \circ e)$ is a subgroup containing $(q_1, q_2)$ and, by reflexivity, $(q_2, q_2)$, hence also $(q_1 - q_2, 0)$. So $q_1 - q_2 = q_1 \circ e$ for some $e : R \to R$ with $q_2 \circ e = 0$. Then $e$ factors through $k$, so $q_1 - q_2$ factors through $m$, and $h \circ m = 0$ implies $h \circ q_1 = h \circ q_2$.
- id: core-thin_quotients
assumptions:
@@ -47,8 +48,7 @@
conclusions:
- effective congruences
- quotients of congruences
- # TODO: rename congruences consistently to q_1, q_2 (and cocongruences to j_1, j_2)
- proof: '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$.'
+ proof: 'If $q_1, q_2 : R \rightrightarrows X$ is a congruence, the symmetry morphism $s : R \to R$ is an automorphism of $R$, hence equal to $\id_R$ by assumption. But then $q_1 = q_2 \circ s = q_2$, and simply $\id_X$ is a coequalizer. Also, for the reflexivity morphism $r : X \to R$, we have $q_1 \circ r = \id$. For the reverse composition, $q_1 \circ r \circ q_1 = q_1 \circ \id$ and $q_2 \circ r \circ q_1 = q_2 \circ \id$, so since $q_1, q_2$ are jointly monomorphic, we get $r \circ q_1 = \id$. Therefore, $q_1 = q_2$ is an isomorphism, so $R$ is the kernel pair of $\id_X$.'
- id: core-connected_locally_finite_congruences
assumptions:
@@ -59,7 +59,7 @@
- quotients of congruences
# TODO: refactor this once we add "split-mono-trivial", cf. #383
proof: >-
- Let $q_1, q_2 : E \rightrightarrows X$ be a congruence. Since the category is core-connected, we may assume $E = X$. The reflexivity morphism $r : X \to X$ satisfies $q_1 \circ r = q_2 \circ r = \id_X$. Since the monoid $\End(X)$ is finite, every right inverse in it is a two-sided inverse (see the remark below), so that $q_1 = r^{-1} = q_2$. It follows that $\id_X$ is a coequalizer of $q_1, q_2$, and that $q_1, q_2$ is a kernel pair of $\id_X$, since $\id_X, \id_X$ is one.
+ Let $q_1, q_2 : R \rightrightarrows X$ be a congruence. Since the category is core-connected, we may assume $R = X$. The reflexivity morphism $r : X \to X$ satisfies $q_1 \circ r = q_2 \circ r = \id_X$. Since the monoid $\End(X)$ is finite, every right inverse in it is a two-sided inverse (see the remark below), so that $q_1 = r^{-1} = q_2$. It follows that $\id_X$ is a coequalizer of $q_1, q_2$, and that $q_1, q_2$ is a kernel pair of $\id_X$, since $\id_X, \id_X$ is one.
Remark: In a finite monoid $M$, every right inverse is a two-sided inverse. Indeed, let $x,y \in M$ with $xy = 1$. The map $M \to M$, $z \mapsto yz$ is injective, since $x(yz) = (xy)z = z$. Since $M$ is finite, it is also surjective, so there is some $z \in M$ with $yz = 1$. Then $x = x(yz) = (xy)z = z$, and hence $yx = yz = 1$.
@@ -71,11 +71,11 @@
conclusions:
- effective congruences
proof: >-
- 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$.
+ Let $q_1, q_2 : R \rightrightarrows X$ be a congruence. Then let $R_0$ be the kernel of $q_2$. We see that $q_1|_{R_0} : R_0 \to X$ is a monomorphism. Let $q_1|_{R_0}$ be the kernel of a morphism $h : X \to Y$. We claim that $R$ 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 \coloneqq E$, $x_1 \coloneqq f$, $x_2 \coloneqq 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 pullback square.
+ $$\begin{align*} (x_1,x_2) \in R & \iff (x_1 - x_2,0) \in R \\ & \iff x_1 - x_2 \in R_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 \coloneqq R$, $x_1 \coloneqq q_1$, $x_2 \coloneqq q_2$, we conclude that $h \circ q_1 = h \circ q_2$, so we get the required commutative diagram. From there, the reverse implications show this diagram is a pullback square.
- id: additive_effective_congruences_imply_normal
assumptions:
@@ -84,7 +84,7 @@
conclusions:
- normal
proof: >-
- Let $i : Y \hookrightarrow X$ be a monomorphism. Then we define a relation on $X$ via $E \coloneqq X \times Y$ with maps $f, g : E \rightrightarrows X$ defined by $f : (x, y) \mapsto x+i(y)$ and $g : (x, y) \mapsto x$. It is straightforward to check that $f$ and $g$ are jointly monomorphic. Now $E$ is a congruence 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$.
+ Let $i : Y \hookrightarrow X$ be a monomorphism. Then we define a relation on $X$ via $R \coloneqq X \times Y$ with maps $q_1, q_2 : R \rightrightarrows X$ defined by $q_1 : (x, y) \mapsto x+i(y)$ and $q_2 : (x, y) \mapsto x$. It is straightforward to check that $q_1$ and $q_2$ are jointly monomorphic. Now $R$ is a congruence because for generalized elements $x_1, x_2 \in X(T)$, $(x_1, x_2)$ factors through $R$ 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, $R$ is the kernel pair of some morphism $h : X \to Z$; in other words, $(x_1, x_2)$ factors through $R$ 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 $R$, which is equivalent to $h(x) = h(0) = 0$. We have thus shown that $Y$ is the kernel of $h$.
# TODO: The "finitely cocomplete" assumption is only needed to satisfy the preconditions of co-Malcev; thus, if we
# revise the definition of "Malcev" not to require a finitely complete category, then that condition can be dropped.
@@ -122,12 +122,12 @@
- mono-regular
proof: >-
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 \coloneqq B + B' + A + A'$$
+ $$R \coloneqq B + B' + A + A'$$
and define the two morphisms
- $$f, g : E \rightrightarrows B + B'$$
+ $$q_1, q_2 : R \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),
+ q_1(y) & = \alpha(y), & q_1(y') & = \alpha(y)', \\
+ q_2(y) & = \alpha(y)', & q_2(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$.
+ on generalized elements. Extensivity can be used to show that $q_1, q_2$ are jointly monomorphic. Clearly, the pair $q_1, q_2$ is reflexive and symmetric. For transitivity, one once again uses extensivity. By assumption, there is a morphism $h : B + B' \to C$ such that $q_1, q_2$ 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 = q_1(e)$, $y = q_2(e)$ for some $e \in R$. In particular, for $x \in B$, we have $h(x) = h(x')$ if and only if $x = q_1(e)$, $x' = q_2(e)$ for some $e \in R$. 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$.
diff --git a/database/data/category-implications/subobject-trivial.yaml b/database/data/category-implications/subobject-trivial.yaml
index 6258063ab..7424cdefc 100644
--- a/database/data/category-implications/subobject-trivial.yaml
+++ b/database/data/category-implications/subobject-trivial.yaml
@@ -77,7 +77,7 @@
- regular-subobject-trivial
conclusions:
- effective congruences
- proof: 'Let $f,g : E \rightrightarrows X$ be a congruence. In particular, there is a morphism $r : X \to E$ with $f r = g r = \id_X$. Since $r$ is a split monomorphism, it is a regular monomorphism. By assumption, $r$ must be an isomorphism. Thus, $f = g = r^{-1}$, and $f,g$ is a kernel pair of $\id_X$.'
+ proof: 'Let $q_1,q_2 : R \rightrightarrows X$ be a congruence. In particular, there is a morphism $r : X \to R$ with $q_1 r = q_2 r = \id_X$. Since $r$ is a split monomorphism, it is a regular monomorphism. By assumption, $r$ must be an isomorphism. Thus, $q_1 = q_2 = r^{-1}$, and $q_1,q_2$ is a kernel pair of $\id_X$.'
- id: regular_subobject_trivial_reflexive_coequalizers
# TODO: refactor this once we add "split-mono-trivial", cf. #383
@@ -93,7 +93,7 @@
- regular-subobject-trivial
conclusions:
- effective cocongruences
- proof: 'Let $f,g : X \rightrightarrows E$ be a cocongruence. In particular, there is a morphism $r : E \to X$ with $r f = r g = \id_X$. Since $f$ is a split monomorphism, it is a regular monomorphism. By assumption, $f$ must be an isomorphism. Then $r f = \id_X$ implies that $r = f^{-1}$, and $r g = \id_X$ implies $g = f$. Hence, $f,g$ is a cokernel pair of $\id_X$.'
+ proof: 'Let $j_1,j_2 : X \rightrightarrows C$ be a cocongruence. In particular, there is a morphism $r : C \to X$ with $r j_1 = r j_2 = \id_X$. Since $j_1$ is a split monomorphism, it is a regular monomorphism. By assumption, $j_1$ must be an isomorphism. Then $r j_1 = \id_X$ implies that $r = j_1^{-1}$, and $r j_2 = \id_X$ implies $j_2 = j_1$. Hence, $j_1,j_2$ is a cokernel pair of $\id_X$.'
- id: regular_subobject_trivial_coreflexive_equalizers
# TODO: refactor this once we add "split-mono-trivial", cf. #383
diff --git a/database/data/category-properties/Malcev.yaml b/database/data/category-properties/Malcev.yaml
index 84d618694..d9312f4ca 100644
--- a/database/data/category-properties/Malcev.yaml
+++ b/database/data/category-properties/Malcev.yaml
@@ -1,6 +1,7 @@
id: Malcev
relation: is
-description: A category is Malcev (also spelled Mal'cev or Maltsev) when it has finite limits and every internal reflexive relation is an internal equivalence relation. That is, if $R \subseteq X^2$ is a subobject with $\Delta_X \subseteq R$, then $R$ is symmetric and transitive.
+description: >-
+ A category is Malcev (also spelled Mal'cev or Maltsev) when it has finite limits and every internal reflexive relation is an internal equivalence relation. That is, if $q_1, q_2 : R \rightrightarrows X$ is a jointly monomorphic pair with a common section $X \to R$, then $q_1, q_2$ is also symmetric and transitive, i.e. a congruence (see the definition here).
nlab_link: https://ncatlab.org/nlab/show/Malcev+category
dual: co-Malcev
invariant_under_equivalences: true
diff --git a/database/data/category-properties/co-Malcev.yaml b/database/data/category-properties/co-Malcev.yaml
index c32a80e9c..a31162a76 100644
--- a/database/data/category-properties/co-Malcev.yaml
+++ b/database/data/category-properties/co-Malcev.yaml
@@ -1,7 +1,7 @@
id: co-Malcev
relation: is
description: >-
- A category is co-Malcev when its dual is Malcev, i.e., it has finite colimits and if $X \sqcup X \twoheadrightarrow R$ is a coreflexive corelation, then it is cosymmetric and cotransitive.
+ A category is co-Malcev when its dual is Malcev, i.e. when it has finite colimits and every internal coreflexive corelation is an internal equivalence corelation. That is, if $j_1, j_2 : X \rightrightarrows C$ is a jointly epimorphic pair with a common retraction $C \to X$, then $j_1, j_2$ is also cosymmetric and cotransitive, i.e. a cocongruence (see the definition here).
This terminology is not standard, but we have added it to properly formulate the interesting theorem that the dual of an elementary topos is Malcev, i.e., that every elementary topos is co-Malcev.
diff --git a/database/data/category-properties/coquotients of cocongruences.yaml b/database/data/category-properties/coquotients of cocongruences.yaml
index 460cb25f1..f3fee0590 100644
--- a/database/data/category-properties/coquotients of cocongruences.yaml
+++ b/database/data/category-properties/coquotients of cocongruences.yaml
@@ -1,11 +1,11 @@
id: coquotients of cocongruences
relation: has
description: >-
- A cocongruence (or internal equivalence corelation) on an object $X$ of a category is a parallel pair $j_1, j_2 : X \rightrightarrows E$ which is jointly epimorphic, and such that for every object $T$, the image of $({-} \circ j_1, {-} \circ j_2) : \Hom(E, T) \to \Hom(X, T)^2$ is an equivalence relation. If pushouts exist (or at least the pushout displayed below), the latter condition is equivalent to the existence of morphisms
+ A cocongruence (or internal equivalence corelation) on an object $X$ of a category is a parallel pair $j_1, j_2 : X \rightrightarrows C$ which is jointly epimorphic, and such that for every object $T$, the image of $({-} \circ j_1, {-} \circ j_2) : \Hom(C, T) \to \Hom(X, T)^2$ is an equivalence relation. If pushouts exist (or at least the pushout displayed below), the latter condition is equivalent to the existence of morphisms
$$\begin{align*}
- r & : E \to X & \quad \text{(coreflexivity)} \\
- s & : E \to E & \quad \text{(cosymmetry)} \\
- t & : E \to E \sqcup_{j_2,X,j_1} E & \quad \text{(cotransitivity)}
+ r & : C \to X & \quad \text{(coreflexivity)} \\
+ s & : C \to C & \quad \text{(cosymmetry)} \\
+ t & : C \to C \sqcup_{j_2,X,j_1} C & \quad \text{(cotransitivity)}
\end{align*}$$
satisfying the following equations:
$$\begin{align*}
@@ -13,7 +13,7 @@ description: >-
s \circ j_1 & = j_2 & s \circ j_2 & = j_1 \\
t \circ j_1 & = \iota_1 \circ j_1 & t \circ j_2 & = \iota_2 \circ j_2
\end{align*}$$
- In particular, $j_1,j_2$ is a coreflexive pair. A coquotient of $j_1,j_2$ is an equalizer of $j_1,j_2$. We say that a category has coquotients of cocongruences if every cocongruence has a coquotient. Note that in the case of a category with binary copowers, the corresponding quotient objects $X + X \twoheadrightarrow E$ are also commonly referred to as cocongruences, or as internal equivalence corelations.
+ In particular, $j_1,j_2$ is a coreflexive pair. A coquotient of $j_1,j_2$ is an equalizer of $j_1,j_2$. We say that a category has coquotients of cocongruences if every cocongruence has a coquotient. Note that in the case of a category with binary copowers, the corresponding quotient objects $X + X \twoheadrightarrow C$ are also commonly referred to as cocongruences, or as internal equivalence corelations.
nlab_link: null
dual: quotients of congruences
invariant_under_equivalences: true
diff --git a/database/data/category-properties/effective cocongruences.yaml b/database/data/category-properties/effective cocongruences.yaml
index bb4bbf21d..0bce1b016 100644
--- a/database/data/category-properties/effective cocongruences.yaml
+++ b/database/data/category-properties/effective cocongruences.yaml
@@ -1,8 +1,8 @@
id: effective cocongruences
relation: has
description: >-
- A cocongruence $j_1,j_2 : 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 pushout square
- $$\begin{CD} Y @> h >> X \\ @V h VV @VV j_1 V \\ X @>> j_2 > E. \end{CD}$$
+ A cocongruence $j_1,j_2 : X \rightrightarrows C$ (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 pushout square
+ $$\begin{CD} Y @> h >> X \\ @V h VV @VV j_1 V \\ X @>> j_2 > C. \end{CD}$$
A category has effective cocongruences if every cocongruence in the category is effective.
nlab_link: null
dual: effective congruences
diff --git a/database/data/category-properties/effective congruences.yaml b/database/data/category-properties/effective congruences.yaml
index 078412177..41b3a9f07 100644
--- a/database/data/category-properties/effective congruences.yaml
+++ b/database/data/category-properties/effective congruences.yaml
@@ -1,8 +1,8 @@
id: effective congruences
relation: has
description: >-
- A congruence $q_1, q_2 : 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 pullback square
- $$\begin{CD} E @> q_1 >> X \\ @V q_2 VV @VV h V \\ X @>> h > Y. \end{CD}$$
+ A congruence $q_1, q_2 : R \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 pullback square
+ $$\begin{CD} R @> q_1 >> X \\ @V q_2 VV @VV h V \\ X @>> h > Y. \end{CD}$$
A category has effective congruences if every congruence in the category is effective. Since congruences are also called internal equivalence relations, this property is also known as having effective equivalence relations.
nlab_link: https://ncatlab.org/nlab/show/congruence
dual: effective cocongruences
diff --git a/database/data/category-properties/quotients of congruences.yaml b/database/data/category-properties/quotients of congruences.yaml
index cfef33f56..40726156f 100644
--- a/database/data/category-properties/quotients of congruences.yaml
+++ b/database/data/category-properties/quotients of congruences.yaml
@@ -1,11 +1,11 @@
id: quotients of congruences
relation: has
description: >-
- A congruence (or internal equivalence relation) on an object $X$ of a category is a parallel pair $q_1, q_2 : E \rightrightarrows X$ which is jointly monomorphic, and such that for every object $T$, the image of $(q_1 \circ {-}, q_2 \circ {-}) : \Hom(T, E) \to \Hom(T, X)^2$ is an equivalence relation. If pullbacks exist (or at least the pullback displayed below), the latter condition is equivalent to the existence of morphisms
+ A congruence (or internal equivalence relation) on an object $X$ of a category is a parallel pair $q_1, q_2 : R \rightrightarrows X$ which is jointly monomorphic, and such that for every object $T$, the image of $(q_1 \circ {-}, q_2 \circ {-}) : \Hom(T, R) \to \Hom(T, X)^2$ is an equivalence relation. If pullbacks exist (or at least the pullback displayed below), the latter condition is equivalent to the existence of morphisms
$$\begin{align*}
- r & : X \to E & \quad \text{(reflexivity)} \\
- s & : E \to E & \quad \text{(symmetry)} \\
- t & : E \times_{q_2,X,q_1} E \to E & \quad \text{(transitivity)}
+ r & : X \to R & \quad \text{(reflexivity)} \\
+ s & : R \to R & \quad \text{(symmetry)} \\
+ t & : R \times_{q_2,X,q_1} R \to R & \quad \text{(transitivity)}
\end{align*}$$
satisfying the following equations:
$$\begin{align*}
@@ -13,7 +13,7 @@ description: >-
q_1 \circ s & = q_2 & q_2 \circ s & = q_1 \\
q_1 \circ t & = q_1 \circ p_1 & q_2 \circ t & = q_2 \circ p_2
\end{align*}$$
- In particular, $q_1,q_2$ is a reflexive pair. A quotient of $q_1,q_2$ is a coequalizer of $q_1,q_2$. We say that a category has quotients of congruences if every congruence has a quotient. Note that in the case of a category with binary powers, the corresponding subobjects $E \hookrightarrow X \times X$ are also commonly referred to as congruences, or as internal equivalence relations.
+ In particular, $q_1,q_2$ is a reflexive pair. A quotient of $q_1,q_2$ is a coequalizer of $q_1,q_2$. We say that a category has quotients of congruences if every congruence has a quotient. Note that in the case of a category with binary powers, the corresponding subobjects $R \hookrightarrow X \times X$ are also commonly referred to as congruences, or as internal equivalence relations.
nlab_link: https://ncatlab.org/nlab/show/congruence
dual: coquotients of cocongruences
invariant_under_equivalences: true