The beginning of homological algebra involves lots of diagram chasing, for proving most of the theorems. This gets repetitive after a while. To make things more interesting and satisfactory, one would like to remove the mechanical dredge work as far as possible.
One possible approach, as advocated in Lang's Algebra book, is to first prove the snake lemma by diagram chasing, and then reduce everything else as much possible to the snake lemma. This is mostly satisfactory. But some proofs, such as that of five lemma(as far as I am able to reconstruct now), require a small amount of diagram chasing in addition to using snake lemma.
There seems to be an alternate approach using the salamander lemma, as given in the references in this question. Salamander lemma can be used to prove the other important lemmas. But according to the description in Anton Geraschenko's post, it is like chasing salamanders around, rather than chasing elements.
Are there other possible approaches to founding homological algebra avoiding extensive diagram chasing? That is, is it possible to base homological algebra on some other lemma/proposition, than the two possibilities mentioned above?
Best Answer
One other way you can prove all diagram chasing results (that I know of) is to first prove that there is a spectral sequence associated with a double complex (actually, there are two!). This involves some diagram chasing, but you only do it once. I guess you could also argue that you still have to chase the spectral sequences.
As an example, here's how you'd prove that a short exact sequence of chain complexes induces a long exact sequence in homology. We start with the double complex with exact rows
↑ ↑ ↑ 0 → Ai+1 → Bi+1 → Ci+1 → 0 ↑ ↑ ↑ 0 → Ai → Bi → Ci → 0 ↑ ↑ ↑(I'm assuming the columns are bounded below, but it doesn't matter since this result is "local": you can truncate above and below the point you're interested in and then prove the result)
We can regard this as the $E_0$ page of two different spectral sequences, depending on whether we decide to start with the vertical or horizontal arrows as our differential. Both spectral sequences have to abut to the homology of the total complex associated to this double complex.
First, use the horizontal arrows. Since the rows are exact, when we take homology, we get zero everywhere, so the $E_1$ page is identically zero. Nothing interesting is going to happen now: we've gotten to $E_\infty$. So the homology of the total complex is zero.
Now what if we use the vertical arrows? We get the $E_1$ page
We'd like to prove that the rows are exact in the middle and that kernel of $H^{i+1}(A)\to H^{i+1}(B)$ is isomorphic to the cokernel of $H^i(B)\to H^i(C)$. Let's flip to the $E_2$ page and see what happens. Let $K^i=\ker(H^{i+1}(A)\to H^{i+1}(B))$, $M^i=\mathrm{cok}(H^i(B)\to H^i(C))$, and let $L^i$ be the homology of the above row at $H^i(B)$. We get the $E_2$ page
0 Ki+1 Li+1 Mi+1 0 ↘ ↘ ↘ ↘ ↘ ↘ 0 Ki Li Mi 0(pardon my ascii art: those are meant to be arrows going two spots to the right and one spot down)
Note that on the $E_{\ge 3}$ pages, the differentials will be too long to connect anything in these three columns to anything other than zero. Since we must abut to zero, this $E_2$ page is the "last chance" for the homology to vanish. It follows that the sequences $0\to L^i\to 0$ and $0\to K^{i+1}\to M^i\to 0$ must be exact, so $L^i=0$ and $K^{i+1}\cong M^i$, which is exactly what we wanted to show.
Note that I was able to completely ignore the question of what the differentials on higher pages were; I just had to know that they exist.
Diagram-chasing results almost always assume that the rows are exact and then make assertions about the homology groups you get from the columns, so you can always run one spectral sequence and immediately get that the homology of the total complex is zero, then run the other spectral sequence and note when the spectral sequence has it's "last chance" to cancel all homology groups.