Cocongruences in extensive categories

Proof. Suppose we have a commutative square

$$\begin{CD} E \times_X E @> p_1 >> E \\ @V t VV @VV f V \\ E @> 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 $$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)$.

This concludes the proof that the first diagram is a pushout diagram; the proof for the second is similar. $\square$

Proof. Suppose we have compatible maps $T \to B$ and $T \to C_1 + C_2$. Then using extensivity, we can find a decomposition of the latter into morphisms $T_1 \to C_1$ and $T_2 \to C_2$ where $T \cong T_1 + T_2$. Using the individual pullback diagrams, we can then construct morphisms $T_1 \to A_1$ and $T_2 \to A_2$ with the corresponding projections to $B, C_1, C_2$. The sum $T \cong T_1 + T_2 \to A_1 + A_2$ then gives the required morphism for the desired pullback diagram.

For uniqueness, suppose we have two generalized elements $s, s' \in (A_1 + A_2)(T)$ such that $$(f_1; f_2)(s) = (f_1; f_2)(s')$$ and $$(g_1 + g_2)(s) = (g_1 + g_2)(s').$$ Then we can find a decomposition of $s$ into generalized elements $a_1 \in A_1(T_1)$ and $a_2 \in A_2(T_2)$ where $T \cong T_1 + T_2$, and similarly a decomposition of $s'$ into generalized elements $a_1' \in A_1(T_1')$ and $a_2' \in A_2(T_2')$ where $T \cong T_1' + T_2'$. From the condition $(g_1 + g_2)(s) = (g_1 + g_2)(s')$, we get that $$T \cong T_1 + T_2 \xrightarrow{g_1(a_1) + g_2(a_2)} C_1 + C_2$$ and $$T \cong T_1' + T_2' \xrightarrow{g_1(a_1') + g_2(a_2')} C_1 + C_2$$ are equal. From the equivalence of categories $\C / C_1 \times \C / C_2 \cong \C / (C_1 + C_2)$, we can conclude that the slices $T_1 \xrightarrow{g_1(a_1)} C_1$ and $T_1' \xrightarrow{g_1(a_1')} C_1$ are isomorphic, and similarly for the slices $T_2 \xrightarrow{g_2(a_2)} C_2$ and $T_2' \xrightarrow{g_2(a_2')} C_2$. Without loss of generality, then, we may assume that $T_1 = T_1'$ and $T_2 = T_2'$; the isomorphism $T_1 + T_2 \cong T \cong T_1' + T_2'$ is the identity; and $g_1(a_1) = g_1(a_1')$ and $g_2(a_2) = g_2(a_2')$.

On the other hand, from $(f_1; f_2)(s) = (f_1; f_2)(s')$, we conclude $f_1(a_1) = f_1(a_1')$ and $f_2(a_2) = f_2(a_2')$. Therefore, from the uniqueness conditions on the given pullback diagrams, we get $a_1 = a_1'$ and $a_2 = a_2'$. Hence, $s = (a_1; a_2) = (a_1'; a_2') = s'$. $\square$

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). $\square$

Proof. Let $e : Y \hookrightarrow X$ be the equalizer of $j_1$ and $j_2$. We will prove that the parallel pair

$$\begin{align*} (i_1; i_1 \circ e; i_2 \circ e; i_2) & ,\\ (i_1; i_2 \circ e; i_1 \circ e; i_2) & : X + Y + Y + X \rightrightarrows X + X \end{align*}$$

is a kernel pair of $(j_1; j_2) : X + X \to E$. 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

$$\begin{CD} X @> \id >> X \\ @V \id VV @VV j_1 V \\ X @>> j_1 > E. \end{CD}$$

Similarly, since $e$ is formed as a coreflexive equalizer, we have a pullback diagram

$$\begin{CD} Y @> e >> X \\ @V e VV @VV j_1 V \\ X @>> j_2 > E. \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 $$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),$$ so $x_1 = x_2$ factors uniquely through $e$. (See also here; in particular, that result, along with the uniqueness of equalizers and pullbacks, would give an alternate proof with an additional hypothesis that the pullback exists.)

Combining these using Lemma 2, we get a pullback diagram

$$\begin{CD} X+Y @> (\id; e) >> X \\ @V \id + e VV @VV j_1 V \\ X+X @>> (j_1; j_2) > E. \end{CD}$$

Similarly, we get a pullback diagram

$$\begin{CD} Y+X @> (e; \id) >> X \\ @V e + \id VV @VV j_2 V \\ X+X @>> (j_1; j_2) > E. \end{CD}$$

Now, combining those two using Lemma 2 (transposed), we get a pullback diagram

$$\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. \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$.

Therefore, since $(j_1; j_2) : X + X \to E$ is a regular epimorphism, by this result, it is a coequalizer of this kernel pair. However, this coequalizer is exactly the congruence quotient in the construction of $X +_Y X$ here. Thus, we see that the original corelation is equivalent to the cokernel pair of $e$. $\square$

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. $\square$