Working through Weibel's Introduction to Homological Algebra, I am frequently unsure when it is acceptable to prove results using diagram-chasing and elements, and when Weibel has in mind a category-theoretic proof.
For example, Weibel 1.3.1 asks for a proof of the claim:
If $0 \rightarrow A_{\bullet} \xrightarrow{f} B_{\bullet} \xrightarrow{g} C_{\bullet} \rightarrow 0$ is a short exact sequence of chain complexes, then, whenever two of the three complexes $A_{\bullet}$,$B_{\bullet}$,$C_{\bullet}$ are exact, so is the third.
A complete solution using diagram chasing and elements is available here. However, the wording of the question, and the fact that Exercise 1.3.2 applies the result in a general Abelian category, suggest that a categorical proof is desired. How would such a proof go?
I understand that Freyd-Mitchell's Embedding Theorem implies that any theorems of a certain form which can be proven for R-modules using diagram chasing automatically hold in any Abelian category (Rotman calls this the Metatheorem). I suspect that this embedding should be "constructive" with respect to proofs.
My question is: Does there exist a concrete set of rules for lifting a proof by chasing elements into one by the equivalent category-theoretic properties? For example, how would one go about converting the following small excerpts in the diagram-chasing solution into language suitable for any Abelian category?
Assume $B, C$ are exact and let $x \in \ker d \subseteq A_n$. By commutative square we have $$d(f_n(x)) = f_{n-1}(d(x)) = f_{n-1}(0) = 0$$ Thus $f_n(x) \in \ker d \subseteq B_n$, which is exactly $\operatorname{im} d \subseteq B_n$ by exactness of $B$, and there is some $b \in B_{n+1}$ such that $d(b) = f_n(x)$.
. . .
For $c \in C_{n+2}$ with $d(c) = g_{n+1}(b)$, since $g_{n+2}$ is surjective, there is some $b' \in B_{n+2}$ such that $g_{n+2}(b') = c$.
Consider $b - d(b')$. We have by commutative square that $b - d(b') \in \ker g_{n+1}$: $$g_{n+1}(b - d(b')) = g_{n+1}(b) - g_{n+1}(d(b')) = g_{n+1}(b) - d(g_{n+2}(b')) = g_{n+1}(b) - g_{n+1}(b) = 0$$
I think I understand how some small parts of this conversion would work. For example, you can replace statements like $\ker d = \operatorname{im} d$ with an isomorphism of their embeddings as submodules. But the step which constructs a difference of elements doesn't obviously seem to have a categorical equivalent.
Edit: As Pedro mentioned in a comment, the topic of converting element-proofs in $R\mathbf{-mod}$ or $\mathbf{Ab}$ into categorical proofs is discussed in these notes of Bergman, where he develops exactly this kind of dictionary of terms. The result seems somewhat more involved than I might hope for 1.3.1, so I'll leave open the restricted version of the question: is there an elementary categorical proof of Weibel 1.3.1 (stated above).
This is how I did it: ($B, C$ exact $\Rightarrow A$ is exact)
As per Weibel's notation, for a chain complex $C$, let $Z_{n}(C)$ and $B_{n}(C)$ denote the kernel and image of the morphisms $C_{n}\xrightarrow{d_{n}^{C}}C_{n-1}$ and $C_{n+1}\xrightarrow{d_{n+1}^{C}}C_{n}$ respectively. Then we have the factorization $C_{n+1}\twoheadrightarrow B_{n}(C) \hookrightarrow Z_{n}(C) \hookrightarrow C_{n}$ of the morphism $C_{n+1}\xrightarrow{d_{n+1}^{C}}C_{n}$, which, for an exact complex, reduces to $C_{n+1}\twoheadrightarrow Z_{n}(C) \hookrightarrow C_{n}$.
In the proof I will use the fact that in any abelian category, the pullback of an epimorphism is an epimorphism. (See P.Freyd, Abelian Categories, Prop. 2.54 for a proof)
The map $A\xrightarrow{f}B$ induces morphisms $Z_{n}(A)\rightarrow Z_{n}(B)$ between the kernels. Consider the pullback diagram \begin{eqnarray} E&\twoheadrightarrow& Z_{n}(A)\\ \downarrow &&\downarrow\\ B_{n+1}&\twoheadrightarrow&Z_{n}(B) \end{eqnarray} Here $E\twoheadrightarrow Z_{n}(A)$ is epi as $B_{n+1}\twoheadrightarrow Z_{n}(B)$ is. Now observe that $E\rightarrow B_{n+1} \xrightarrow{g_{n+1}}C_{n+1} \xrightarrow{d_{n+1}^{C}} C_{n}$ = $E \twoheadrightarrow Z_n(A) \hookrightarrow A_n \xrightarrow{f_n}B_n \xrightarrow{g_n} C_{n}$ = $E \xrightarrow{0} C_{n}$. Thus, by the universal property of the kernel $Z_{n+1}(C)$, there exists a unique morphism $E \dashrightarrow Z_{n+1}(C)$ such that $E \dashrightarrow Z_{n+1}(C) \hookrightarrow C_{n+1}$ = $E\rightarrow B_{n+1} \xrightarrow{g_{n+1}}C_{n+1}$. Consider the pullback diagram \begin{eqnarray} P&\twoheadrightarrow& E\\ \downarrow &&\downarrow\\ B_{n+2}&\twoheadrightarrow&Z_{n+1}(C) \end{eqnarray} where the bottom morphism is the composition of the two epi's $B_{n+1} \xrightarrow{g_{n+2}} C_{n+2} \twoheadrightarrow Z_{n+1}(C)$. Let $r: P\rightarrow B_{n+1}$ be the composition $P\twoheadrightarrow E\rightarrow B_{n+1}$ and $s: P\rightarrow B_{n+1}$ be the composition $P\rightarrow B_{n+2} \xrightarrow{d_{n+2}^{B}} B_{n+1}$ and let $h = r-s$. Then, it is easy to see that $g_{n+1} \circ h = 0$. As $0\rightarrow A_{n+1} \xrightarrow{f_{n+1}} B_{n+1} \xrightarrow{g_{n+1}} C_{n+1}\rightarrow 0$ is a short exact sequence, $A_{n+1} \xrightarrow{f_{n+1}} B_{n+1}$ is the kernel of $B_{n+1} \xrightarrow{g_{n+1}} C_{n+1}$ and hence by the universal property of kernel, there exists a unique morphism $k: P \dashrightarrow A_{n+1}$ such that $f_{n+1}\circ k = h$. Composing with the morphism $B_{n+1} \xrightarrow{d_{n+1}^{B}} B_{n}$ we get $d_{n+1}^{B}\circ f_{n+1}\circ k = d_{n+1}^{B}\circ (r-s) = d_{n+1}^{B}\circ r$ which gives $P\xrightarrow{k}A_{n+1}\xrightarrow{d_{n+1}^{A}} A_n\xrightarrow{f_n}B_{n}$ = $P \twoheadrightarrow E\twoheadrightarrow Z_{n}(A) \hookrightarrow A_{n}\xrightarrow{f_n}B_{n}$. Since $f_n$ is a mono, we get $P\xrightarrow{k}A_{n+1}\xrightarrow{d_{n+1}^{A}} A_n$ = $P \twoheadrightarrow E\twoheadrightarrow Z_{n}(A) \hookrightarrow A_{n}$.
Composing with the epimorphism $A_n \twoheadrightarrow coker(d_{n+1}^{A})$, we get $P \twoheadrightarrow E\twoheadrightarrow Z_{n}(A) \hookrightarrow A_{n}\twoheadrightarrow coker(d_{n+1}^{A})$ = $P\xrightarrow{0} coker(d_{n+1}^{A})$ which implies $Z_{n}(A) \hookrightarrow A_{n}\twoheadrightarrow coker(d_{n+1}^{A})$ = $Z_{n}(A)\xrightarrow{0} coker(d_{n+1}^{A})$ (as $P \twoheadrightarrow E\twoheadrightarrow Z_{n}(A)$ is epi). Since by definition $B_{n}(A) \hookrightarrow A_{n}$ is the kernel of the morphism $A_n \twoheadrightarrow coker(d_{n+1}^{A})$, there exists a unique morphism $i: Z_{n}(A)\rightarrow B_{n}(A)$ such that $Z_{n}(A)\xrightarrow{i}B_{n}(A)\hookrightarrow Z_{n}(A)$ = $Z_{n}(A)\xrightarrow{id}Z_{n}(A)$ which implies that $i: Z_{n}(A)\rightarrow B_{n}(A)$ is an isomorphism.