Let \(v\) be arbitrary. By extensionality it suffices to show \(\varepsilon (\psi .\alpha _0\, v) = \varepsilon (v)\).

Since \(\psi \) acts as the identity on homology at degree 0, we have \(\psi .\alpha _0\, v - v \in \operatorname {im}(d_F)\). Obtaining \(w\) such that \(d_F(w) = \psi .\alpha _0\, v - v\), we compute:

using the hypothesis \(\varepsilon \circ d_F = 0\). Applying \(\operatorname {map_sub}\) and \(\operatorname {sub_eq_zero}\), we conclude \(\varepsilon (\psi .\alpha _0\, v) = \varepsilon (v)\).

We proceed by induction on \(x\) using the tensor product induction principle.

Zero case: Both sides vanish trivially.

Additivity: Both sides are linear, so the identity extends from simple tensors.

Simple tensor case \(x = b \otimes f\): Expanding \(\widetilde{d}_h^0(b \otimes f)\) via twistedDhLin_tmul and simplifying autAtDeg, we obtain

For each term, by epsilon_comp_alpha0_eq (when \(d_B(e_{b_1})(b_0) \neq 0\), the chain automorphism \(\varphi (b_1,b_0)\) acts as the identity on homology), we replace \(\varepsilon (\alpha _0^{\varphi (b_1,b_0)} f)\) by \(\varepsilon (f)\). After this substitution the sum becomes

Proceeding pointwise and applying the basis expansion \(d_B(b) = \sum _{b_1} b(b_1) \cdot d_B(e_{b_1})\), we obtain \(\varepsilon (f) \cdot d_B(b) = d_B(\varepsilon (f) \cdot b)\), which equals \(d_B((\operatorname {rid} \circ (\operatorname {id} \otimes \varepsilon ))(b \otimes f))\).

We must show \(d_B(\pi _*^{(1)}(z)) = 0\). Since \(z \in \operatorname {totZ}_1 = \ker (d_1)\), we have \(d_1(z) = 0\), i.e. \(\widetilde{d}_h^0(z_1) + d_v^0(z_2) = 0\) (as \(d_1 = \operatorname {coprod}(\widetilde{d}_h^0, d_v^0)\)).

Applying \(\operatorname {rid} \circ (\operatorname {id} \otimes \varepsilon )\) to this equation:

The \(d_v^0\)-term vanishes since \(d_v^0 = \operatorname {lTensor}(d_F)\), and \((\operatorname {id} \otimes \varepsilon ) \circ (\operatorname {id} \otimes d_F) = \operatorname {id} \otimes (\varepsilon \circ d_F) = 0\) by hypothesis. Thus:

By the chain map property (Lemma 228), this equals \(d_B((\operatorname {rid} \circ (\operatorname {id} \otimes \varepsilon ))(z_1)) = d_B(\pi _*^{(1)}(z)) = 0\).

Let \(z \in \operatorname {totB}_1^{Z_1}\). Rewriting \(\operatorname {totB}_1^{Z_1}\) as the preimage under inclusion of \(\operatorname {totB}_1 = \operatorname {im}(d_2)\), we obtain \(w\) such that \(d_2(w) = z.\operatorname {val}\). In particular, \(z.\operatorname {val}.1 = d_v^1(w)\) (from the first component of \(d_2\)).

We must show \(\pi _*^{(1)}(z.\operatorname {val}) = 0\). By definition of \(\pi _*^{(1)}\) as \(\operatorname {coprod}(\operatorname {rid} \circ (\operatorname {id} \otimes \varepsilon ),\; 0)\), it suffices to show

Substituting \(z.\operatorname {val}.1 = d_v^1(w) = \operatorname {lTensor}(d_F)(w)\):

since \(\varepsilon \circ d_F = 0\) by hypothesis.

Since \(\varepsilon \) is surjective, there exists \(f_0 \in \mathbb {F}_2^{m_2}\) with \(\varepsilon (f_0) = 1\).

Let \(v \in \ker (d_B)\). We construct a preimage in \(\operatorname {totH}_1\) mapping to \(v\).

First, we show \(\widetilde{d}_h^0(v \otimes f_0) \in \operatorname {im}(d_v^0)\): since \(v \in \ker (d_B)\) and the connection acts as the identity on homology, for each basis vector \(e_{b_1}\) with \(d_B(e_{b_1})(b_0) \neq 0\), the automorphism \((\varphi (b_1,b_0)).\alpha _0\, f_0 - f_0 \in \operatorname {im}(d_F)\). After expanding via twistedDhLin_tmul, the sum splits into a term \(d_B(v) \otimes f_0 = 0\) (since \(v \in \ker (d_B)\)) and a sum of terms of the form \(e_{b_0} \otimes d_F(g)\), each lying in \(\operatorname {im}(\operatorname {lTensor}(d_F))\).

Obtaining \(y\) with \(d_v^0(y) = \widetilde{d}_h^0(v \otimes f_0)\), we set \(z = (v \otimes f_0,\; y)\). Over \(\mathbb {F}_2\), \(\widetilde{d}_h^0(v \otimes f_0) + d_v^0(y) = 0\), so \(z \in \operatorname {totZ}_1\).

The class \([z] \in \operatorname {totH}_1\) satisfies \(H_1(\pi _*)([z]) = \pi _*|_{\operatorname {cycles}}(z)\). By definition, this equals \((\operatorname {rid} \circ (\operatorname {id} \otimes \varepsilon ))(v \otimes f_0) = \varepsilon (f_0) \cdot v = 1 \cdot v = v\).

By Theorem 212, there is a linear equivalence

Hence \(\dim \operatorname {totH}_1 = \dim (\ker (d_B) \otimes H_0(F)) + \dim (H_0(B) \otimes \ker (d_F))\).

Since \(\operatorname {im}(d_B) = \top \), the cokernel \(H_0(B) = \mathbb {F}_2^{m_1} / \operatorname {im}(d_B)\) is the quotient by \(\top \), which is subsingleton. Therefore \(H_0(B) \otimes \ker (d_F)\) is also subsingleton (as a tensor product with a zero module), and its dimension is \(0\).

Since \(\bar{\varepsilon } : H_0(F) \simeq \mathbb {F}_2\), we have

using \(\operatorname {lTensor}(\bar{\varepsilon })\) and the right-unit isomorphism \(\ker (d_B) \otimes \mathbb {F}_2 \simeq \ker (d_B)\).

Combining: \(\dim \operatorname {totH}_1 = \dim \ker (d_B) + 0 = \dim \ker (d_B)\).

Surjectivity follows from Lemma 233. By Lemma 234, \(\dim \operatorname {totH}_1 = \dim \ker (d_B)\).

We verify that both spaces are finite-dimensional: \(\operatorname {totH}_1\) is finite-dimensional because by Theorem 212 it is linearly equivalent to a product of tensor products of finite-dimensional spaces; \(\ker (d_B)\) is finite-dimensional as a submodule of a finite-dimensional space.

Since \(H_1(\pi _*)\) is a surjective linear map between finite-dimensional spaces of equal dimension, it is also injective by the rank-nullity theorem (as applied via LinearMap.injective_iff_surjective_of_finrank_eq_finrank). Hence \(H_1(\pi _*)\) is bijective.

The map \(H^1(\pi ^*)\) is defined as \(H^1(\pi ^*) = H_1(\pi _*)^{\simeq ,\operatorname {dual}}\), the dual of the linear equivalence \(H_1(\pi _*)^{\simeq }\). Since \(H_1(\pi _*)^{\simeq }\) is a linear equivalence (and in particular bijective), its dual \(H^1(\pi ^*)\) is also a linear equivalence, and its underlying linear map is bijective. This follows directly from LinearEquiv.bijective applied to \(H^1(\pi ^*)\).