Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes

added theorem'_X_0
added theorem'_X_1
added def
added theorem chain_complex.mk_X_0
added theorem chain_complex.mk_X_1
added theorem chain_complex.mk_X_2
added theorem chain_complex.mk_d_1_0
added theorem chain_complex.mk_d_2_0
added structure chain_complex.mk_struct
added theorem
added def chain_complex.of
added theorem chain_complex.of_X
added theorem chain_complex.of_d
added theorem chain_complex.prev
added def chain_complex
added theorem
added theorem cochain_complex.prev
added def cochain_complex
added structure homological_complex.hom
added structure homological_complex
added def boundaries_map
added def cycles_functor
added def cycles_map
added theorem cycles_map_arrow
added theorem cycles_map_comp
added theorem cycles_map_id
added def homology_functor