10 Def 7: Cell Complex
A regular cell complex \(X\) consists of:
A family of types \(X_n\) (for each \(n \in \mathbb {Z}\)), whose elements are called \(n\)-cells, each equipped with a Fintype instance and a DecidableEq instance.
A boundary map \(\partial \): for each \(n\)-cell \(\sigma \in X_n\), a finite set \(\partial \sigma \subseteq X_{n-1}\) of \((n-1)\)-cells in the boundary of \(\sigma \).
The chain complex condition: for every \(n \in \mathbb {Z}\), every \(n\)-cell \(\sigma \in X_n\), and every \((n-2)\)-cell \(\rho \in X_{n-2}\), the cardinality
\[ \left|\{ \, \tau \in \partial \sigma \mid \rho \in \partial \tau \, \} \right| \]is even (i.e., \(\equiv 0 \pmod{2}\)).
Let \(X\) be a cell complex and let \(C_i(X) = (X_i \to \mathbb {F}_2)\) denote the free \(\mathbb {F}_2\)-vector space on the \(i\)-cells (i.e., functions from \(X_i\) to \(\mathbb {F}_2\)). The differential
is the \(\mathbb {F}_2\)-linear map defined for \(f \in C_n(X)\) and \(\tau \in X_{n-1}\) by
Equivalently, on a basis element \(e_\sigma \) (the indicator function of \(\sigma \)), we have \(\partial _n(e_\sigma ) = \sum _{\tau \in \partial \sigma } e_\tau \), extended linearly.
Let \(X\) be a cell complex. For every \(n \in \mathbb {Z}\),
Let \(f \in C_n(X)\) and \(\rho \in X_{n-2}\) be arbitrary. By extensionality, it suffices to show
Simplifying using the definition of \(\partial _{n-1}\), \(\partial _n\), and the zero map, the left-hand side becomes
We rewrite the inner filtered sum using the identity \(\sum _{\sigma \in S,\, P(\sigma )} f(\sigma ) = \sum _{\sigma \in S} \mathbf{1}_{P(\sigma )}\, f(\sigma )\), converting to a sum over all of \(X_n\) with an indicator. Then we swap the order of summation (both index sets are finite), obtaining
It suffices to show each inner summand (over \(\sigma \)) is zero. For fixed \(\sigma \in X_n\), we apply the identity for sums of if-then-else expressions: the sum over \(\tau \) splits as
Combining the two filter conditions with filter_filter, we identify the counting set as
whose cardinality equals \(\left|\{ \tau \in \partial \sigma \mid \rho \in \partial \tau \} \right|\). By the chain complex condition (bdry_bdry) applied to \(\sigma \) and \(\rho \), this cardinality is even. Since the cardinality of an even set, cast to \(\mathbb {F}_2\), equals \(0\) (by Even.natCast_zmod_two), we have \(f(\sigma ) \cdot 0 = 0\). Hence the entire sum is zero.
Let \(X\) be a cell complex. The associated chain complex \(C(X) = (C_\bullet (X), \partial )\) is the \(\mathbb {F}_2\)-chain complex defined as follows:
In degree \(i \in \mathbb {Z}\), the chain module is \(C_i(X) = (X_i \to \mathbb {F}_2)\), the free \(\mathbb {F}_2\)-vector space on the \(i\)-cells.
The differential \(d_{i,j} : C_i(X) \to C_j(X)\) is the linear map \(\partial _{j+1}\) when \(j + 1 = i\), and zero otherwise.
The chain complex condition \(d_{j} \circ d_{j+1} = 0\) is verified by composing the differentials and applying differentialMap_comp, after cancelling the coherence isomorphisms (eqToHom) that arise from the ModuleCat packaging.
Let \(X\) be a cell complex. The homology of \(X\) in degree \(i \in \mathbb {Z}\) is
where \(H_i(C(X))\) is the \(i\)-th homology of the associated chain complex \(C(X)\) (as defined in the chain complex homology construction of Definition 1).