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.
