Abelian categories

[Alizter]

Eventually we want to be able to formalize spectral sequences in this library. Floris' thesis and spectral lean library is a proof of concept that it can be done.

When thinking about ways to go about doing this, I have decided that it will be useful for the future to formalize some theory of Abelian categories. In the lean library, only abelian groups (or maybe R-modules) are considered but I think we can do this a bit more abstractly, which will stop unrelated concepts interfering. (In my mind anyway).

I have managed to formalize some basic theory of pointed categories, which doesn't contain anything surprising.

My current plan is to do this following:

1. Formalize some theory of semiadditive categories (i.e. pointed categories with biproducts.

There is something interesting to be said here in that, we can require the isomorphism between coproducts and products to be the canonical one we desire, however Stephan Lack has proven in his paper "Non-canonical isomorphisms (2009)" that any such isomorphism is sufficient.

So far having a zero object is a mere prop, having biproducts is a mere prop. Semiadditive categories allow us to characterize the operation on the hom sets directly without having to give it ourselves.

There are a lot of equivalent ways to characterise the biproduct which should be interesting to investigate.

2. Define the notion of additive category as an additive category with an inverse operation on homsets.

Here it looks like we have to make a choice but this is not the case. We can show that any two inverses are necessarily the same, so a category being additive is a mere proposition.

We can do a lot with additive categories. One thing I have been wanting to do for a while is some linear algebra. Now given an additive category C, and a morphism f : A + B -> X + Y where + is the biproduct, we can completely characterize f as a matrix. Composition of functions then becomes matrix "multiplication". This is the kind of structure I would love to see exploited in a proof assistant.

3. Define abelian categories a semiadditive category where every mono is a kernel and every epi is a cokernel.

This part is pretty standard and requires following any homological algebra text really. We will have to prove some standard results used in homological algebra.

4. Develop results about exactness.

Finally I want to study about exact sequences and various lemmas that come with them. Something to start with would be to show being an epi and a mono is equivalent to being an iso. Then we can start saying things like every mono is the kernel of its cokernel etc.

We will also need to define some sort of (co)homology of a given complex. I have ideas how to do this, but I don't think we can go down the standard route of derived functors. We really only need to form some quotients here.

All of this should be enough groundwork for us to eventually start talking about I-graded objects in an abelian category, spectral sequences and exact couples.

I've created this issue to present my plan of attack if you like. I welcome all discussion about what I am doing. I also welcome any help!