# FilteredComplex -- the type of all filtered complexes

## Description

An ascending filtration of a bounded (homological, lower index, or degree $-1$) chain complex $C : \dots \rightarrow C_i \rightarrow C_{i - 1} \rightarrow \dots$ is an ordered family of chain subcomplexes $FC : \dots \subseteq F_{n - 1} C \subseteq F_n C \subseteq \dots$. Such a filtration is said to be bounded if $F_s C = C$ for all sufficiently large $s$ and $F_t C = 0$ for all sufficiently small $t$.

Alternatively, a descending filtration of a bounded (cohomological, or upper index, or degree $1$) chain complex $C : \dots \rightarrow C^i \rightarrow C^{i + 1} \rightarrow \dots$ is an ordered family of subchain complexes $FC : \dots \subseteq F^{n + 1} C \subseteq F^n C \subseteq \dots$. Such a filtration is said to be bounded if $F^s C = 0$ for all sufficiently large $s$ and $F^t C = C$ for all sufficiently small $t$.

The type FilteredComplex is a data type for working with bounded filtrations of bounded chain complexes.

## Caveat

By assumption all filtered complexes arise from bounded filtrations of bounded chain complexes. Filtrations on degree $-1$ chain complexes are ascending. Filtrations on degree $1$ chain complexes are descending.