Use of snake lemma vs long exact sequence

Stream: condensed mathematics

[David Michael Roberts]

I've been wondering about if the snake lemma is used in any other capacity other than to do the analogue of the standard proof of the long exact sequence in (co)homology. Because someone in the not too distant past showed me a novel proof of the long exact sequence that constructs a sequence of complexes directly, except the connecting homomorphism is a span consisting of a degreewise-surjective quasi-isomorphism in the backwards direction and a projection map in the forwards direction. The proof then that this is exact after applying (co)homology is much more modular and conceptual than the proof using the snake lemma. It's non-standard, but might people might be interested in seeing a paper version? I only have rough notes at present, but can make a neat version.

[David Michael Roberts]

I should say it uses the shift functor, with an extra minus sign on d, a minor lemma about detecting isomorphisms of quotient modules, quasi-isomorphisms, and the result that a short exact sequence of complexes is exact in the middle after applying (co)homology. The diagram chasing is broken up/reduced compared to the proof of the snake lemma.

[Johan Commelin]

@David Michael Roberts As far as I can see, normed_snake (9.10 in the PDF) is only used in the proof of normed_spectral (9.6). On the other hand, 9.10 doesn't really look much like the classical snake lemma. It seems much closer to what you are already describing.

[David Michael Roberts]

Hmm, calling 9.10 the snake lemma seems quite a stretch ;-), though I trust that's what it's supposed to be.
I might just, when I have time, try using the chain complex stuff developed here to do the proof I was given, as an exercise, then, for my own benefit.

As you all were!

[Kevin Buzzard]

One thing which has been confusing me about the snake lemma recently is that the boundary map seems to be "canonical" in the same way that if you want to write down a map from a vector space to its double dual, you choose the obvious evaluation one (which makes sense for monoids) and don't throw in a random minus sign and send v to the map sending phi to -phi(v). Similarly the diagram chase to get from Ker(f3) to coker(f1) feels quite natural. This is contrast to the connecting homomorphism in a cohomology theory which is in some sense only defined up to sign

[David Michael Roberts]

I guess the sign comes from how one defines the mapping cone (which the proof I've got uses). When you see it, the choice of the extra sign feels absolutely natural. However, one can either write the connecting homomorphism in this "long sequence of complexes" as a span or a cospan (a right or left fraction), which is really just a specific natural presentation of the resulting map in the derived category. These two maps in the derived category are not equal, but differ by a sign. The thing about exactness is that the image of a map and the image of the negative of that map are equal, so it doesn't really matter. I should check which one of the span and cospan give the map that arises as in the usual snake lemma proof. The signs were definitely bugging me a little, because I thought these two connecting homomorphisms where equal, for a little bit, and stuff wasn't working!