20
$\begingroup$

The question

I would be interested to hear about examples of formalisation of the theory of abelian categories in theorem provers, and in particular formalisations of things like the zig-zag lemma and the snake lemma, together hopefully with applications which show that these formalisations are actually usable in practice.

Details

Categories are very easy objects to define in theorem provers, at least on the face of it. Some objects, some morphisms, and some axioms. But when developing cohomology theories in e.g. algebraic geometry or topology, one needs to use a theory of abelian categories, which are much more complicated to define; the concept of "kernel = image" is easy in a concrete category but I specifically do not want to assume that the abelian categories we're talking about here are concrete.

In the context of abelian categories there are notions of an exact sequence and a complex of objects, and the zig-zag lemma is the construction of a long exact sequence of cohomology groups associated to a short exact sequence of complexes (here by "cohomology group" I just mean "kernel over image", not any exotic cohomology theory). There are also basic facts such as the snake lemma which are valid in all abelian categories.

When I knew nothing about formalisation, I would have guessed that all these things would be pretty easy to do. However this seems not to be the case. Our human ability to draw diagrams which encode a lot of information does not transfer over well to the theorem prover domain. Furthermore most proofs of the snake lemma involve chasing elements around, which is not valid in an arbitrary abelian category until one has proved the Freyd-Mitchell embedding theorem which basically says that many questions about abstract abelian categories can be reduced to the category of abelian groups or more generally the category of modules over a ring; without this theorem, all proofs become a lot more fiddly.

In the ongoing work on the Liquid Tensor Experiment we have had to bite the bullet and engage with this material in Lean, because we need it for the main result, and it has been quite a challenge. Note that we do not have a formalisation of Freyd-Mitchell yet, so we're having to argue abstractly with everything. The reason I'm asking is to see if there are examples of formalisation of results about abelian categories in other theorem provers which we could learn from.

$\endgroup$
5
  • 1
    $\begingroup$ I've participated in the proof of the snake lemma, and it wasn't very hard, or at least not a lot harder than with pen and paper. (I mean, without Freyd-Mitchell is really annoying even on paper). The real problem is when one wants to use it. We usually think that the first row is the "row of kernels", but of course this is not really precise, in the sense that "being the kernel" is an evil notion. We want that the elements of the first row satisfy the universal property of the kernel and so on. It is this kind of difficulties that are really different when working with a theorem prover. $\endgroup$
    – Ricky
    Apr 12, 2022 at 13:03
  • 1
    $\begingroup$ On top of that, you want everything to be functorial wrt maps of short exact sequence (or long exact sequences, or whatever gadget you are considering). On paper that's "obvious". In a theorem prover you can quickly paint yourself in a nasty corner. $\endgroup$
    – jmc
    Apr 12, 2022 at 13:22
  • $\begingroup$ Thanks @GuyCoder . I started tagging explicit provers then realised I'd run out of tags. $\endgroup$ Apr 12, 2022 at 17:09
  • $\begingroup$ @Ricky yes this is somehow the point. One could imagine writing something down and saying it's the snake lemma or whatever, but I was wondering whether there had been some developments of the theory of abelian categories which had attempted to use a formalisation of the snake lemma to do other things; in informal maths it's used all over the place to prove results about cohomology groups for example. Has anyone formalised anything like this in any prover? $\endgroup$ Apr 12, 2022 at 17:11
  • 1
    $\begingroup$ Just to add to what was said above, I want to mention that the argument we have in the liquid tensor experiment for the snake lemma is just a diagram chase, but with pseudoelements. The key construction is the connecting map, and its definition can be found here for those who might be interested: github.com/leanprover-community/lean-liquid/blob/… $\endgroup$
    – Adam Topaz
    Apr 12, 2022 at 19:48

1 Answer 1

5
$\begingroup$

The UniMath library has a formalization on abelian categories and homological algebra (done by Tommi Pannila). See:

The documentation can be found here: An Introduction to Homological Algebra

$\endgroup$
1

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.