Homological algebra lemmas

[Alizter]

Now that we have abelian categories in #1929, its time to think about how we can go proving various items in the toolbox of homological algebra.

We can prove the short 5-lemma and then the rest, but I thought it might also be a good time to introduce a different abstract approach.

We say a category is regular when it admits a good notion of image factorization. There is an abstract notion of "homological category" in which the short 5-lemma holds. A homological category is a pointed regular protomodular category. Now the definition of protomodular is a bit of a rabbit hole so I would propose an equivalent definition that is normally a theorem:

A homological category is a pointed regular category in which the short 5-lemma holds.

Now I am fairly certain that from this definition we can prove the salamander lemma and from that all other diagram lemmas in homological algebra.

Examples of homological categories include abelian categories, pType and Group. I would also assume that categories of extensions of abelian groups also form homological categories (though I haven't checked).

Another advantage of homological categories is that they are regular by definition. Regular categories have their own internal logic which is very simple. This logic is essentially the language of diagram chasing which might be interesting to make practical.

[jdchristensen]

Can you give a reference for how the short 5-lemma + regularity is enough to get all the other standard homological results?

Also, is it really true that pType will satisfy this? How do you define exactness in that generality? E.g. I have sequences

   1 → 2 → 2

and

   1 → 3 → 2

where in both cases the second map sends the base point to the base point and the other point(s) to the non-base point in 2. In both cases, the preimage of the base point agrees with the image of the previous map. Are both sequences exact? There's a map from the second to the first that isn't an equivalence in the middle.

[Alizter]

@jdchristensen I think i misremembered pType. I believe it might work for connected spaces however.

[Alizter]

Can you give a reference for how the short 5-lemma + regularity is enough to get all the other standard homological results?

In Borceux's book "Mal'cev, Protomodular, Homological and Semi-Abelian Categories" a "homological category is defined as a pointed regular protomodular category (4.1.1). Theorem 4.1.10 states that a pointed regular category is homological iff the short 5-lemma holds.

Here is Bergman's Salamander Lemma which is general enough to produce most other homological lemmas. Here is a slick proof by Jonathan Wise that avoids talking about elements.

Now the five lemma, snake lemma and nine lemma are all proven in Borceux's book, so I don't think it would be a huge stretch to prove the salamander lemma and derive the rest from that. This is a bit flaky as I haven't actually checked it and there is a chance there might be some property of abelian categories that remains essential.

[ThomatoTomato]

There is a paper by Goswami that describes five axioms you need to prove the salamander lemma, and then proves it. I haven't checked the details, but it looks plausible that these axioms are satisfied by homological categories. At least the homological categories we care about.

In a follow up paper, this framework is further expanded upon, and many diagram lemmas that we want are shown or claimed to be true. The salamander lemma is one of them. I'm not sure what framework will be the easiest/best to implement, but this gives us another option to tackle this problem.