4 Def 1: Chain Complex
Let \(C\) be a chain complex of \(\mathbb {F}_2\)-vector spaces. The differential \(\partial _i : C_i \to C_{i-1}\) is the \(\mathbb {F}_2\)-linear map obtained from the Mathlib differential \(C.d\, i\, (i-1)\) (with respect to the descending complex shape on \(\mathbb {Z}\)) by extracting its underlying linear map via the forgetful functor from \(\mathbf{Mod}_{\mathbb {F}_2}\) to \(\mathbb {F}_2\)-linear maps.
Let \(C\) be a chain complex of \(\mathbb {F}_2\)-vector spaces. The incoming differential at degree \(i\) is the \(\mathbb {F}_2\)-linear map \(\partial _{i+1} : C_{i+1} \to C_i\) extracted from the Mathlib differential \(C.d\, (i+1)\, i\). This formulation avoids definitional issues with \((i+1)-1\) vs. \(i\) in integer arithmetic.
Let \(C\) be a chain complex of \(\mathbb {F}_2\)-vector spaces. The cycles at degree \(i\) are
defined as the kernel submodule of the differential \(\partial _i : C_i \to C_{i-1}\).
Let \(C\) be a chain complex of \(\mathbb {F}_2\)-vector spaces. The boundaries at degree \(i\) are
defined as the image (range) submodule of the incoming differential \(\partial _{i+1} : C_{i+1} \to C_i\).
Let \(C\) be a chain complex of \(\mathbb {F}_2\)-vector spaces. For every \(i \in \mathbb {Z}\),
as a composition of \(\mathbb {F}_2\)-linear maps \(C_{i+1} \to C_{i-1}\).
By extensionality, it suffices to show that \((\partial _i \circ \partial _{i+1})(x) = 0\) for an arbitrary element \(x \in C_{i+1}\). Unfolding the definitions of \(\partial _i\) (i.e., \(\mathtt{differential}\)) and \(\partial _{i+1}\) (i.e., \(\mathtt{incomingDifferential}\)) and simplifying the linear map composition and zero map, we reduce to showing that \((C.d\, (i+1)\, i \gg C.d\, i\, (i-1))(x) = 0\). By the Mathlib chain complex axiom \(C.\mathtt{d\_ comp\_ d}\, (i+1)\, i\, (i-1)\), the composition \(C.d\, (i+1)\, i \gg C.d\, i\, (i-1) = 0\), so after simplification the expression vanishes. Rewriting using the \(\mathbf{Mod}_{\mathbb {F}_2}\) composition application lemma completes the proof.
Let \(C\) be a chain complex of \(\mathbb {F}_2\)-vector spaces. For every \(i \in \mathbb {Z}\),
That is, every boundary is a cycle.
Unfolding the definitions of \(B_i(C)\) (i.e., \(\mathtt{boundaries}\)) and \(Z_i(C)\) (i.e., \(\mathtt{cycles}\)), the inclusion \(\operatorname {im}\partial _{i+1} \subseteq \ker \partial _i\) is equivalent (by the submodule lemma \(\mathtt{LinearMap.range\_ le\_ ker\_ iff}\)) to the condition \(\partial _i \circ \partial _{i+1} = 0\). This follows immediately from \(\mathtt{differential\_ comp\_ incomingDifferential}\).
Let \(C\) be a chain complex of \(\mathbb {F}_2\)-vector spaces. The boundaries \(B_i(C)\), viewed as a submodule of the cycles \(Z_i(C)\), are defined as the preimage of \(B_i(C) \subseteq C_i\) under the canonical subtype embedding \(Z_i(C) \hookrightarrow C_i\). Concretely,
Let \(C\) be a chain complex of \(\mathbb {F}_2\)-vector spaces. The \(i\)-th homology of \(C\) is the quotient \(\mathbb {F}_2\)-module
where \(B_i^{Z}(C)\) is the boundaries viewed as a submodule of the cycles \(Z_i(C)\).