Unfolding the definitions of \(\delta ^i = \operatorname {dualMap}(\partial _{i+1})\) and \(\delta ^{i-1} = \operatorname {dualMap}(\partial _i)\), we apply the identity \(\operatorname {dualMap}(f) \circ \operatorname {dualMap}(g) = \operatorname {dualMap}(g \circ f)\) (i.e., \(\operatorname {dualMap}\) is contravariant). Thus

Rewriting using the chain complex relation \(\partial _i \circ \partial _{i+1} = 0\) (which holds by differential_comp_incomingDifferential), we obtain \(\operatorname {dualMap}(0) = 0\), which follows from the fact that any linear map sends zero to zero.

Unfolding the definitions of \(B^i(C) = \operatorname {im}\, \delta ^{i-1}\) and \(Z^i(C) = \ker \delta ^i\), we apply the standard criterion: \(\operatorname {im}(f) \subseteq \ker (g)\) if and only if \(g \circ f = 0\). Rewriting using the range–kernel inclusion lemma, it suffices to show \(\delta ^i \circ \delta ^{i-1} = 0\), which is exactly the content of coboundaryMap_comp_incomingCoboundaryMap.

Unfolding the definitions \(Z^i(C) = \ker \delta ^i = \ker \bigl(\operatorname {dualMap}(\partial _{i+1})\bigr)\) and \(B_i(C) = \operatorname {im}\, \partial _{i+1}\), the result follows directly from the identity \(\ker (f^{\mathrm{tr}}) = (\operatorname {im}\, f)^{\mathrm{ann}}\), which holds over any commutative ring. Specifically, we apply LinearMap.ker_dualMap_eq_dualAnnihilator_range to the incoming differential \(\partial _{i+1} = C.\operatorname {incomingDifferential}(i)\).

Unfolding the definitions \(B^i(C) = \operatorname {im}\, \delta ^{i-1} = \operatorname {im}\bigl(\operatorname {dualMap}(\partial _i)\bigr)\) and \(Z_i(C) = \ker \, \partial _i\), the result follows from the identity \(\operatorname {im}(f^{\mathrm{tr}}) = (\ker f)^{\mathrm{ann}}\) for linear maps between finite-dimensional vector spaces over a field. Specifically, we apply LinearMap.range_dualMap_eq_dualAnnihilator_ker to the differential \(\partial _i = C.\operatorname {differential}(i)\). Finite-dimensionality of \(C_i\) and \(C_{i-1}\) is used to ensure the field-theoretic transpose identity holds.

Let \(h_{\le }\) denote the inclusion \(B_i(C) \subseteq Z_i(C)\) from boundaries_le_cycles. Unfolding \(B_i(C)|_{Z_i} = \operatorname {comap}(\iota _{Z_i})(B_i(C))\), we apply the identity

using Submodule.finrank_map_subtype_eq. Next, we apply Submodule.map_comap_subtype to obtain \(\operatorname {map}(\iota _{Z_i})(\operatorname {comap}(\iota _{Z_i})(B_i)) = Z_i \sqcap B_i\). Since \(B_i \subseteq Z_i\) (i.e., \(h_{\le }\) holds), we conclude \(Z_i \sqcap B_i = B_i\) by inf_eq_right, completing the proof.

Let \(h_{\le }\) denote the inclusion \(B^i(C) \subseteq Z^i(C)\) from coboundaries_le_cocycles. Unfolding \(B^i(C)|_{Z^i} = \operatorname {comap}(\iota _{Z^i})(B^i(C))\), we apply Submodule.finrank_map_subtype_eq to obtain

By Submodule.map_comap_subtype, this equals \(\operatorname {finrank}(Z^i \sqcap B^i)\). Since \(B^i \subseteq Z^i\), we have \(Z^i \sqcap B^i = B^i\) by inf_eq_right, completing the proof.

We apply the dimension formula \(\operatorname {finrank}(M/N) + \operatorname {finrank}(N) = \operatorname {finrank}(M)\) twice:

By finrank_boundariesSubCycles_eq, \(\operatorname {finrank}(B_i|_{Z_i}) = \operatorname {finrank}(B_i)\). By finrank_coboundariesSubCocycles_eq, \(\operatorname {finrank}(B^i|_{Z^i}) = \operatorname {finrank}(B^i)\).

We then apply the dual annihilator dimension formula \(\operatorname {finrank}(W) + \operatorname {finrank}(W^{\mathrm{ann}}) = \operatorname {finrank}(V)\) (for \(W \subseteq V\) finite-dimensional) to both \(B_i(C)\) and \(Z_i(C)\):

By cocycles_eq_dualAnnihilator_boundaries, \(\operatorname {finrank}(Z^i) = \operatorname {finrank}(B_i^{\mathrm{ann}})\). By coboundaries_eq_dualAnnihilator_cycles, \(\operatorname {finrank}(B^i) = \operatorname {finrank}(Z_i^{\mathrm{ann}})\). Combining all four equations, the equality \(\operatorname {finrank}(H_i) = \operatorname {finrank}(H^i)\) follows by integer arithmetic (omega).