mathlib homological algebra

We'd like to have the basics of homological algebra (complexes, chain maps, homotopy equivalences, exact sequences, homology).

There will be some overlap with the theory of simplicial objects: this issue only addresses the pedestrian approach.

I think it is valuable to work quite generally, and use enriched categories (one doesn't want to have to separately prove that if your morphisms form abelian groups, your chain maps form abelian groups, and that if your morphisms form vector spaces, your chains maps form vector spaces). However if enriched categories aren't ready yet, it's reasonable to start on the special cases.

In any preadditive category:

[x] Chain complexes
[x] Chain maps
[x] Homotopies
[x] Homotopy equivalences
[ ] Retracts

In any additive category:

[ ] Direct sums of complexes

In any monoidal additive category:

[ ] Tensor products of complexes

In an abelian category:

[x] Homology
[x] Exactness
[ ] Short exact sequences
[ ] ... (please feel free to extend these lists!)

May 20 '19 10:05 kim-em

Definitely worth checking out https://github.com/cmu-phil/Spectral which goes all the way through spectral sequences, though only for modules over a ring.

May 24 '19 10:05 rwbarton

Yes, it it worth checking out what was done in the Lean 2 HoTT library (also e.g. https://github.com/leanprover/lean2/blob/master/hott/homotopy/chain_complex.hlean).

What I would do the same:

Have the concept of a "successor structure" (https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/succ_str) to have a common generalization of chain complexes indexed over nat and those over int (or something like int x int)
Index some LESs over types like nat x 3 or int x 3 instead of nat or int. (see the same Zulip discussion for reasons)

Things I would do differently:

Work more generally. We had separate notions of chain complexes of pointed sets and chain complexes of modules. This of course leads to code duplication. It would have been much better (but also more work) to do it generally over a (pre)additive category.
We can use type classes more in Lean 3. For example, I would make succ_str a typeclass

Comments:

In unstable homotopy theory you often have LESs of abelian groups, except that the last 3 terms are pointed sets, and the next 3 terms are just groups. When I just started out, I tried to encode that exact structure as a huge single dependent type, but (to no surprise of any dependent type skeptic) that was a huge mess. In the end I decided to make it a sequence of pointed sets, and then have separate proofs that most of them were groups (and most of the map group homomorphisms): https://github.com/leanprover/lean2/blob/master/hott/homotopy/LES_of_homotopy_groups.hlean#L646-L662
In Lean 2 I didn't really encounter this, but it would be nice to have a genuine common generalization of sequences indexed over nat going upwards and those going downwards. That is, sequences

... -> X n -> X (n+1) -> X (n+2) -> ...

and

... -> X (n+2) -> X (n+1) -> X n -> ...

The approach in Lean 2 HoTT was to always use maps X n -> X (S n) where S was any endofunction (like succ or pred), encapsulated in a "successor structure". This gives you mostly what you want, except in the case where you use pred over nat, because then you have a superfluous function X 0 -> X (pred 0), i.e. X 0 -> X 0.

May 24 '19 18:05 fpvandoorn

@semorrison @TwoFX I guess we have homology and exactness now, right?

Aug 17 '20 03:08 jcommelin

I guess we have homology and exactness now, right?

The definitions are there, yes, though I would say that the API for both is not yet in a shape where you can actually work with them.

Aug 17 '20 03:08 TwoFX