# Commit 2021-05-11 07:41 b4c7654b

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`

.