mathlib

mathlib copied to clipboard

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!)