SpectralSequence -- the type of all spectral sequences

A (homological, or lower index) spectral sequence consists of:

1. A sequence of modules $\{E^r_{p,q}\}$ for $p,q \in \mathbb{Z}$ and $r \geq 0$;

2. A collection of homomorphisms $\{d^r_{p,q}: E^r_{p,q} \rightarrow E^r_{p-r,q+r-1} \}$, for $p,q \in \mathbb{Z}$ and $ r \geq 0$, such that $d^r_{p,q} d^r_{p+r,q-r+1} = 0$ ;

3. A collection of isomorphisms $E^{r+1}_{p,q} \rightarrow ker d^r_{p,q} / image d^r_{p+r,q-r+1}$.

Alternatively a (cohomological, or upper index) spectral sequence consists of:

1'. A sequence of modules $\{E_r^{p,q}\}$ for $p,q \in \mathbb{Z}$, and $r \geq 0$;

2'. A collection of homomorphisms $\{d_r^{p,q}: E_r^{p,q} \rightarrow E_{r}^{p+r,q-r+1}\}$ for $p,q \in \mathbb{Z}, r \geq 0$ such that $d_r^{p,q} d_r^{p-r,q+r-1} = 0$ ;

3'. A collection of isomorphisms $E_{r+1}^{p,q} $\rightarrow$ ker d_r^{p,q} / image d_r^{p-r,q+r-1}$.

The type SpectralSequence is a data type for working with spectral sequences. In this package, a spectral sequence is represented by a sequence of spectral sequence pages.

All spectral sequences arise from bounded filtrations of bounded chain complexes. Ascending filtrations of degree $-1$ chain complexes determine spectral sequences of the first type. Descending filtrations of degree $1$ chain complex determine spectral sequences of the second type.