Mathlib v3 is deprecated. Go to Mathlib v4

# Commit2021-05-11 07:41b4c7654b

View on Github →

feat(algebra/homology): redesign of homological complexes (#7473) This is a complete redesign of our library on homological complexes and homology. This PR replaces the current definition of `chain_complex` which had proved cumbersome to work with. The fundamental change is that chain complexes are now indexed by a type equipped with a `complex_shape`, rather than by a monoid. A `complex_shape ι` contains a relation `r`, with the intent that we will only allow a differential `X i ⟶ X j` when `r i j`. This allows, for example, complexes indexed either by `nat` or `int`, with differentials going either up or down. We set up the initial theory without referring to "successors" and "predecessors" in the type `ι`, to ensure we can avoid dependent type theory hell issues involving arithmetic in the index of a chain group. We achieve this by having a chain complex consist of morphisms `d i j : X i ⟶ X j` for all `i j`, but with an additional axiom saying this map is zero unless `r i j`. This means we can easily talk about, e.g., morphisms from `X (i - 1 + 1)` to `X (i + 1)` when we need to. However after not too long we also set up `option` valued `next` and `prev` functions which make an arbitrary choice of such successors and predecessors if they exist. Using these, we define morphisms `d_to j`, which lands in `X j`, and has source either `X i` for some `r i j`, or the zero object if these isn't such an `i`. These morphisms are very convenient when working "at the edge of a complex", e.g. when indexing by `nat`.