Proof.
Proof of (1). Let us say two pairs $p_1 = (f_1 : X \to Y_1, s_1 : Y \to Y_1)$ and $p_2 = (f_2 : X \to Y_2, s_2 : Y \to Y_2)$ are elementary equivalent if there exists a morphism $a : Y_1 \to Y_2$ of $\mathcal{C}$ such that $a \circ f_1 = f_2$ and $a \circ s_1 = s_2$. Diagram:
\[ \xymatrix{ X \ar@{=}[d] \ar[r]_{f_1} & Y_1 \ar[d]^ a & Y \ar[l]^{s_1} \ar@{=}[d] \\ X \ar[r]^{f_2} & Y_2 & Y \ar[l]_{s_2} } \]
Let us denote this property by saying $p_1Ep_2$. Note that $pEp$ and $aEb, bEc \Rightarrow aEc$. (Despite its name, $E$ is not an equivalence relation.) Part (1) claims that the relation $p \sim p' \Leftrightarrow \exists q: pEq \wedge p'Eq$ (where $q$ is supposed to be a pair satisfying the same conditions as $p$ and $p'$) is an equivalence relation. A simple formal argument, using the properties of $E$ above, shows that it suffices to prove $p_3Ep_1, p_3Ep_2 \Rightarrow p_1 \sim p_2$. Thus suppose that we are given a commutative diagram
\[ \xymatrix{ & Y_1 & \\ X \ar[ru]^{f_1} \ar[r]^{f_3} \ar[rd]_{f_2} & Y_3 \ar[u]_{a_{31}} \ar[d]^{a_{32}} & Y \ar[lu]_{s_1} \ar[l]_{s_3} \ar[ld]^{s_2} \\ & Y_2 & } \]
with $s_ i \in S$. First we apply LMS2 to get a commutative diagram
\[ \xymatrix{ Y \ar[d]_{s_1} \ar[r]_{s_2} & Y_2 \ar@{..>}[d]^{a_{24}} \\ Y_1 \ar@{..>}[r]^{a_{14}} & Y_4 } \]
with $a_{24} \in S$. Then, we have
\[ a_{14} \circ a_{31} \circ s_3 = a_{14} \circ s_1 = a_{24} \circ s_2 = a_{24} \circ a_{32} \circ s_3. \]
Hence, by LMS3, there exists a morphism $s_{44} : Y_4 \to Y'_4$ such that $s_{44} \in S$ and $s_{44} \circ a_{14} \circ a_{31} = s_{44} \circ a_{24} \circ a_{32}$. Hence, after replacing $Y_4$, $a_{14}$ and $a_{24}$ by $Y'_4$, $s_{44} \circ a_{14}$ and $s_{44} \circ a_{24}$, we may assume that $a_{14} \circ a_{31} = a_{24} \circ a_{32}$ (and we still have $a_{24} \in S$ and $a_{14} \circ s_1 = a_{24} \circ s_2$). Set
\[ f_4 = a_{14} \circ f_1 = a_{14} \circ a_{31} \circ f_3 = a_{24} \circ a_{32} \circ f_3 = a_{24} \circ f_2 \]
and $s_4 = a_{14} \circ s_1 = a_{24} \circ s_2$. Then, the diagram
\[ \xymatrix{ X \ar@{=}[d] \ar[r]_{f_1} & Y_1 \ar[d]^{a_{14}} & Y \ar[l]^{s_1} \ar@{=}[d] \\ X \ar[r]^{f_4} & Y_4 & Y \ar[l]_{s_4} } \]
commutes, and we have $s_4 \in S$ (by LMS1). Thus, $p_1 E p_4$, where $p_4 = (f_4, s_4)$. Similarly, $p_2 E p_4$. Combining these, we find $p_1 \sim p_2$.
Proof of (2). Let $p = (f : X \to Y', s : Y \to Y')$ and $q = (g : Y \to Z', t : Z \to Z')$ be pairs as in the definition of composition above. To compose we choose a diagram
\[ \xymatrix{ Y \ar[d]_ s \ar[r]_ g & Z' \ar[d]^{u_2} \\ Y' \ar[r]^{h_2} & Z_2 } \]
with $u_2 \in S$. We first show that the equivalence class of the pair $r_2 = (h_2 \circ f : X \to Z_2, u_2 \circ t : Z \to Z_2)$ is independent of the choice of $(Z_2, h_2, u_2)$. Namely, suppose that $(Z_3, h_3, u_3)$ is another choice with corresponding composition $r_3 = (h_3 \circ f : X \to Z_3, u_3 \circ t : Z \to Z_3)$. Then by LMS2 we can choose a diagram
\[ \xymatrix{ Z' \ar[d]_{u_2} \ar[r]_{u_3} & Z_3 \ar[d]^{u_{34}} \\ Z_2 \ar[r]^{h_{24}} & Z_4 } \]
with $u_{34} \in S$. We have $h_2 \circ s = u_2 \circ g$ and similarly $h_3 \circ s = u_3 \circ g$. Now,
\[ u_{34} \circ h_3 \circ s = u_{34} \circ u_3 \circ g = h_{24} \circ u_2 \circ g = h_{24} \circ h_2 \circ s. \]
Hence, LMS3 shows that there exist a $Z'_4$ and an $s_{44} : Z_4 \to Z'_4$ such that $s_{44} \circ u_{34} \circ h_3 = s_{44} \circ h_{24} \circ h_2$. Replacing $Z_4$, $h_{24}$ and $u_{34}$ by $Z'_4$, $s_{44} \circ h_{24}$ and $s_{44} \circ u_{34}$, we may assume that $u_{34} \circ h_3 = h_{24} \circ h_2$. Meanwhile, the relations $u_{34} \circ u_3 = h_{24} \circ u_2$ and $u_{34} \in S$ continue to hold. We can now set $h_4 = u_{34} \circ h_3 = h_{24} \circ h_2$ and $u_4 = u_{34} \circ u_3 = h_{24} \circ u_2$. Then, we have a commutative diagram
\[ \xymatrix{ X \ar@{=}[d] \ar[r]_{h_2\circ f} & Z_2 \ar[d]^{h_{24}} & Z \ar[l]^{u_2 \circ t} \ar@{=}[d] \\ X \ar@{=}[d] \ar[r]^{h_4\circ f} & Z_4 & Z \ar@{=}[d] \ar[l]_{u_4 \circ t} \\ X \ar[r]^{h_3 \circ f} & Z_3 \ar[u]^{u_{34}} & Z \ar[l]_{u_3 \circ t} } \]
Hence we obtain a pair $r_4 = (h_4 \circ f : X \to Z_4, u_4 \circ t : Z \to Z_4)$ and the above diagram shows that we have $r_2Er_4$ and $r_3Er_4$, whence $r_2 \sim r_3$, as desired. Thus it now makes sense to define $p \circ q$ as the equivalence class of all possible pairs $r$ obtained as above.
To finish the proof of (2) we have to show that given pairs $p_1, p_2, q$ such that $p_1Ep_2$ then $p_1 \circ q = p_2 \circ q$ and $q \circ p_1 = q \circ p_2$ whenever the compositions make sense. To do this, write $p_1 = (f_1 : X \to Y_1, s_1 : Y \to Y_1)$ and $p_2 = (f_2 : X \to Y_2, s_2 : Y \to Y_2)$ and let $a : Y_1 \to Y_2$ be a morphism of $\mathcal{C}$ such that $f_2 = a \circ f_1$ and $s_2 = a \circ s_1$. First assume that $q = (g : Y \to Z', t : Z \to Z')$. In this case choose a commutative diagram as the one on the left
\[ \vcenter { \xymatrix{ Y \ar[d]_{s_2} \ar[r]^ g & Z' \ar[d]^ u \\ Y_2 \ar[r]^ h & Z'' } } \quad \Rightarrow \quad \vcenter { \xymatrix{ Y \ar[d]_{s_1} \ar[r]^ g & Z' \ar[d]^ u \\ Y_1 \ar[r]^{h \circ a} & Z'' } } \]
(with $u \in S$), which implies the diagram on the right is commutative as well. Using these diagrams we see that both compositions $q \circ p_1$ and $q \circ p_2$ are the equivalence class of $(h \circ a \circ f_1 : X \to Z'', u \circ t : Z \to Z'')$. Thus $q \circ p_1 = q \circ p_2$. The proof of the other case, in which we have to show $p_1 \circ q = p_2 \circ q$, is omitted. (It is similar to the case we did.)
Proof of (3). We have to prove associativity of composition. Consider a solid diagram
\[ \xymatrix{ & & & Z \ar[d] \\ & & Y \ar[d] \ar[r] & Z' \ar@{..>}[d] \\ & X \ar[d] \ar[r] & Y' \ar@{..>}[d] \ar@{..>}[r] & Z'' \ar@{..>}[d] \\ W \ar[r] & X' \ar@{..>}[r] & Y'' \ar@{..>}[r] & Z''' } \]
(whose vertical arrows belong to $S$) which gives rise to three composable pairs. Using LMS2 we can choose the dotted arrows making the squares commutative and such that the vertical arrows are in $S$. Then it is clear that the composition of the three pairs is the equivalence class of the pair $(W \to Z''', Z \to Z''')$ gotten by composing the horizontal arrows on the bottom row and the vertical arrows on the right column.
We leave it to the reader to check the identity axioms.
$\square$
Comments (2)
Comment #322 by arp on
Comment #323 by arp on
There are also: