It's time for another installment of Wild Spectral Sequences! We shall start our investigations with a classic theorem useful in many applications of homological algebra called Schanuel's lemma, named after Stephen Hoel Schanuel who first proved it.
Consider for a ring $ R$ the category of left $ R$-modules, and let $ A$ be any $ R$-module. Schanuel's lemma states: if $ 0\to K_1\to P_1\to A\to 0$ and $ 0\to K_2\to P_2\to A\to 0$ are exact sequences of $ R$-modules with $ P$ projective, then $ K_1\oplus P_2\cong K_2\oplus P_1$.
We shall prove this using spectral sequences. I came up with this proof while trying to remember the "usual" proof of Schanuel's lemma and I thought that this would be a good illustration of how spectral sequences can be used to eliminate the dearth of clarity in the dangerous world of diagram chasing.
Before I start, I'd like to review a pretty cool fact I which I think of as expanding the kernel, which is pretty useful in working with total complexes (however, to appreciate it you just need a basic grasp of module theory or even just abelian groups). It goes like this: suppose $ f:A\to B$ is a module homomorphism. What is the kernel of $ A\oplus B\to B$ give by $ (a,b)\mapsto f(a) + b$? By just using the definition of kernel, we see that it is $ \{ (a, -f(a)) : a\in A\}$. which is actually just isomorphic to $ A$ itself. This handy fact will come it with our proof of Schanuel's lemma.
The Proof
Let us restate the theorem.
Next, we observe that since the rows are exact, the spectral sequence $ H_p^v(H_q^h(C)\Rightarrow H_{p+q}(\mathrm{Tot}(C))$ has zero $ E^\infty$ terms so that the total complex is exact:
Now we recall that the kernel of $ P_2\oplus A\to A$ is just isomorphic to $ P_2$ via the 'expanding the kernel' trick, and so the image of $ K_2\oplus P_1\to P_2\oplus A$ is isomorphic to $ P_2$. Hence we get a short exact sequence:
Since $ P_2$ is projective, this sequence splits giving us the isomorphism $ K_2\oplus P_1\cong K_1\oplus P_2$.
Notice that once we get used to spectral sequences, they can help remove a lot of the clutter that comes with ridiculous proofs that contain sentences of the form 'let $ x\in X$, then $ f(x)\in Y$ is in the kernel of…', which are exceptionally hard to read.