Unify the notation and definition of congruences and cocongruences

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 <i>regular corelation</i> 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 <i>regular corelation</i> 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,23 +168,23 @@ $$
 \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}
 $$
 
 However, under the canonical isomorphism $(X+Y)+(Y+X) \cong X+Y+Y+X$, we see that $(\id; e) + (e; \id)$ corresponds to
 $$(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
 In an extensive and regular category with quotients of congruences, every cocongruence is effective.
 :::
 
 ::: 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).
 :::

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

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,25 +76,25 @@ 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}
 $$
 
 :::
 
 ::: 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$.
 :::