Revise proof in terms of generalized elements, to address review comments

Author: dschepler

databases/catdat/data/004_category-implications/008_topos-theory-implications.sql

@@ -179,13 +179,13 @@ VALUES
 	'["regular", "epi-regular", "extensive"]',
 	'["effective cocongruences", "co-Malcev"]',
 	'Suppose we have a coreflexive corelation
-	$$X+X \xtwoheadrightarrow{p} E \xtwoheadrightarrow{r} X$$
-	on $X$. Let $Y$ be the equalizer of $p\circ i_1, p\circ i_2 : X \rightrightarrows E$. Then by the assumptions $p$ is a regular epimorphism. By regularity, $p$ is the coequalizer of its kernel pair, which can be expressed as the equalizer of
-	$$p \circ \pi_1,\, p\circ \pi_2 : (X+X) \times (X+X) \rightrightarrows E,$$
-	where $\pi_1, \pi_2$ are the projections. By distributivity and extensivity, it is sufficient to calculate the equalizer on each "quadrant" of $(X+X) \times (X+X)$, i.e. the four copies of $X \times X$.<br>
-	On the $(1,1)$ quadrant, this is the equalizer of $p\circ i_1\circ \pi_1, p\circ i_1\circ \pi_2$, which is isomorphic to $X$ since $p\circ i_1$ is a split monomorphism. On the $(1,2)$ quadrant, it is the equalizer of $p\circ i_1\circ \pi_1, p\circ i_2\circ \pi_2$. Since $r$ is a common retraction of $p\circ i_1$ and $p\circ i_2$, any generalized element of this equalizer has equal components; thus, the equalizer is isomorphic to the equalizer $Y$ of $p\circ i_1, p\circ i_2$. Similarly, on the $(2,1)$ quadrant, it is isomorphic to $Y$, and on the $(2,2)$ quadrant, it is isomorphic to $X$.<br>
+	$$X+X'' \xtwoheadrightarrow{p} E \xtwoheadrightarrow{r} X$$
+	on $X$, where we let $X''$ be an isomorphic copy of $X$ for clarity below. Let $Y$ be the equalizer of $p\circ i_1, p\circ i_2 : X \rightrightarrows E$. That means that for a generalized element $x \in X(T)$, $x \in Y(T)$ if and only if $p(x) = p(x'')$. Then by the assumptions $p$ is a regular epimorphism. By regularity, $p$ is the coequalizer of its kernel pair, which can be expressed as the equalizer $K$ of
+	$$p \circ \pi_1,\, p\circ \pi_2 : (X+X'') \times (X+X'') \rightrightarrows E,$$
+	where $\pi_1, \pi_2$ are the projections. By distributivity and extensivity, it is sufficient to calculate the equalizer on each "quadrant" of $(X+X'') \times (X+X'')$, i.e. the four copies of $X \times X$.<br>
+	On the $X\times X$ quadrant, for generalized elements $x_1, x_2 \in X(T)$, we have $(x_1, x_2) \in K(T)$ if and only if $p(x_1) = p(x_2)$. Since $p\circ i_1$ is a split monomorphism, this is equivalent to $x_1 = x_2$. Thus, the $X\times X$ quadrant of $K$ is the diagonal of $X$. On the $X\times X''$ quadrant, we have $(x_1, x_2'')\in K(T)$ if and only if $p(x_1) = p(x_2'')$. Since $r(p(x_1)) = x_1$ and $r(p(x_2'')) = x_2$, this condition implies $x_1 = x_2$; and then by definition of $Y$, $x_1 = x_2 \in Y(T)$. The converse is straightforward. Thus, the $X\times X''$ quadrant of $K$ is the diagonal of $Y$. Similarly, the $X''\times X$ quadrant of $K$ is the diagonal of $Y$, and the $X''\times X''$ quadrant of $K$ is the diagonal of $X$.<br>
 
-	Since the $X$ pieces are already equalized by the kernel pair of $p$, and the second $Y$ piece is redundant, we thus get that $p$ is the coequalizer of $i_1 \circ \mathrm{inc}_Y$ and $i_2 \circ \mathrm{inc}_Y$, which is equivalent to the cokernel pair of $\mathrm{inc}_Y$ and thus an effective cocongruence.<br><br>
+	Thus, we get that a morphism $h : X+X'' \to Z$ factors through $E$ if and only if $h(x) = h(x)$ for every generalized element $x \in X$; $h(y) = h(y'')$ for every $y \in Y$; $h(y'') = h(y)$ for every $y\in Y$; and $h(x'') = h(x'')$ for every $x \in X$. Clearly this is equivalent to $h(y) = h(y'')$ for every $y\in Y$, so in fact $E$ is the cokernel pair of $i_1 \circ \operatorname{inc}_Y$ and $i_2 \circ \operatorname{inc}_Y$. This means that $E$ is an effective cocongruence.<br><br>
 
 	Remark: The assumptions are satisfied in particular for every elementary topos. Therefore, every elementary topos has effective cocongruences and is co-Malcev.
 	',