Commit 2021-05-11 07:41 b4c7654b

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.