Since \(M\) is free over \(\mathbb {F}_2\), it is flat. Flatness implies that \(\operatorname {id}_M \otimes \iota _{\ker f}\) is injective, where \(\iota _{\ker f} : \ker (f) \hookrightarrow \mathbb {F}_2^{n_2}\) is the inclusion. Moreover, by flatness applied to the exact sequence \(\ker (f) \hookrightarrow \mathbb {F}_2^{n_2} \xrightarrow {f} \mathbb {F}_2^{m_2}\), the sequence

is exact, so \(\ker (\operatorname {id}_M \otimes f) = \operatorname {im}(\operatorname {id}_M \otimes \iota )\). Combining the equality of submodules with the injectivity of \(\operatorname {id}_M \otimes \iota \), we obtain the desired linear equivalence by composing \(\operatorname {LinearEquiv.ofEq}\) with \((\operatorname {LinearEquiv.ofInjective})^{-1}\).

This follows from \(\operatorname {lTensor.equiv}\) applied to the exact sequence \(\mathbb {F}_2^{n_2} \xrightarrow {f} \mathbb {F}_2^{m_2} \xrightarrow {\pi } \mathbb {F}_2^{m_2}/\operatorname {im}(f) \to 0\) (where \(\pi \) is surjective), giving the canonical identification of the left-tensored quotient with the tensor product of the quotient.

Analogously to the left-tensor case: flatness of \(M\) gives injectivity of \(\iota _{\ker f} \otimes \operatorname {id}_M\) and the exact sequence \(\ker (f) \otimes M \to \mathbb {F}_2^{n_1} \otimes M \xrightarrow {f \otimes \operatorname {id}} \mathbb {F}_2^{m_1} \otimes M\). Combining via \(\operatorname {LinearEquiv.ofEq}\) and \((\operatorname {LinearEquiv.ofInjective})^{-1}\) yields the result.

This follows from \(\operatorname {rTensor.equiv}\) applied to the exact sequence \(\mathbb {F}_2^{n_1} \xrightarrow {f} \mathbb {F}_2^{m_1} \xrightarrow {\pi } \mathbb {F}_2^{m_1}/\operatorname {im}(f) \to 0\).

Writing \(g = \sum _i g(i) \cdot e_i\) (by evaluating both sides at each \(j\) using \(\operatorname {Pi.single}\)), we substitute into the left-hand side and use \(\operatorname {TensorProduct.sum_tmul}\) to distribute the sum, obtaining the stated equality.

Expanding by \(\operatorname {twistedDhLin_tmul}\), the left-hand side becomes a double sum over \(b^1 \in \operatorname {Fin}(n_1)\) and \(b^0 \in \operatorname {Fin}(m_1)\). Since \(e_i = \operatorname {Pi.single}\, i\, 1\) vanishes at all \(b^1 \neq i\), only the \(b^1 = i\) term survives. For that term, the inner sum is \(\sum _{b^0} d_B(e_i)(b^0) \cdot (e_{b^0} \otimes \alpha _1^\varphi (i, b^0)(f))\). For each \(b^0\) with \(d_B(e_i)(b^0) \neq 0\), the identity-on-homology hypothesis gives \(\alpha _1^\varphi (i, b^0)(f) = f\) (since \(f \in \ker (d_F)\)). For \(b^0\) with \(d_B(e_i)(b^0) = 0\), the term vanishes. Hence the sum equals \(\sum _{b^0} d_B(e_i)(b^0) \cdot (e_{b^0} \otimes f) = d_B(e_i) \otimes f\) by Lemma 201 (applied in reverse).

By \(\operatorname {TensorProduct.ext’}\), it suffices to check on pure tensors \(b \otimes \langle f, h_f \rangle \) for arbitrary \(b \in \mathbb {F}_2^{n_1}\) and \(f \in \ker (d_F)\). Writing \(b = \sum _i b(i) \cdot e_i\), both sides of the claimed equality reduce (using \(\operatorname {TensorProduct.sum_tmul}\) and \(\operatorname {map_sum}\)) to \(\sum _i b(i) \cdot (\text{basis term at }i)\). For each basis term, Lemma 202 gives \(\widetilde{d_h^1}(e_i \otimes f) = d_B(e_i) \otimes f\), and pulling out the scalar \(b(i)\) via linearity completes the proof.

Define the forward map \(\langle x, h_x\rangle \mapsto \langle e_1(x), \cdot \rangle \) where membership in \(\ker (g)\) follows from \(g(e_1(x)) = e_2(f(x)) = e_2(0) = 0\). The inverse sends \(\langle y, h_y\rangle \mapsto \langle e_1^{-1}(y), \cdot \rangle \), with membership verified by applying \(e_2\) (which is injective) and using the commutative diagram together with \(h_y\). Left and right inverses hold by \(\operatorname {simp}\) (using \(e_1\)’s equivalence properties). Linearity of the map follows from linearity of \(e_1\).

First, we show \(e_2(\operatorname {im}(f)) = \operatorname {im}(g)\). For the forward inclusion: given \(e_2(f(x)) \in e_2(\operatorname {im}(f))\), the commutativity \(e_2(f(x)) = g(e_1(x))\) places this in \(\operatorname {im}(g)\). For the reverse: given \(g(w) \in \operatorname {im}(g)\), we have \(g(w) = e_2(f(e_1^{-1}(w)))\) by commutativity, so it lies in \(e_2(\operatorname {im}(f))\). With \(e_2(\operatorname {im}(f)) = \operatorname {im}(g)\) established, the result follows from \(\operatorname {Submodule.Quotient.equiv}\).

Since \(\operatorname {id} \otimes \iota _{\ker d_F}\) is injective (by flatness of \(\mathbb {F}_2^{m_1}\)), it suffices to show equality after composing with this injection. For any \(\langle x, h_x\rangle \in \ker (\operatorname {id} \otimes d_F)\), the left-hand side gives \((\operatorname {id}\otimes \iota )(e_2(\bar{d}_h^1\langle x, h_x\rangle )) = (\bar{d}_h^1\langle x,h_x\rangle ).\operatorname {val} = d_h^1(x)\) (using \(\operatorname {lTensor_ker_equiv_apply_val}\)). On the right, applying Lemma 203 at \(e_1\langle x, h_x\rangle \) and using \(\operatorname {lTensor_ker_equiv_apply_val}\) again yields the same expression \(d_h^1(x)\).

Expanding by \(\operatorname {twistedDhLin_tmul}\) and distributing the quotient map \(\pi \) through the sum and scalar multiples, only the \(b^1 = i\) summand survives (since \(e_i(b^1) = 0\) for \(b^1 \neq i\)). In the surviving term, for each \(b^0\) with \(d_B(e_i)(b^0) \neq 0\), identity-on-homology at degree 0 gives \(\pi (\alpha _0^\varphi (i, b^0)(f)) = \pi (f)\) (since \(\alpha _0(f) - f \in \operatorname {im}(d_F) = \ker \pi \)). For \(b^0\) with \(d_B(e_i)(b^0) = 0\) the term vanishes. Hence the left side equals \(\sum _{b^0} d_B(e_i)(b^0) \cdot (e_{b^0} \otimes [f]) = d_B(e_i) \otimes [f]\).

By \(\operatorname {TensorProduct.ext’}\) it suffices to check on pure tensors \(b \otimes f\). Writing \(b = \sum _i b(i) \cdot e_i\), both sides decompose as sums over basis elements. For each \(i\), pulling out the scalar \(b(i)\) via linearity and applying Lemma 207 (using \(\operatorname {map_smul}\) and \(\operatorname {smul_tmul’}\)) gives the equality term by term.

Let \(E = \operatorname {fiberBundleSmallDC}(d_B, d_F, \varphi )\).

Step 1. By the SmallDC homology equivalence at degree 2, \(\operatorname {totH}_2(E) \simeq \operatorname {itH}_2(E) = \ker (\bar{d}_h^1)\).

Step 2. By Lemma 206, \(\bar{d}_h^1\) is conjugate (via the flatness equivalences \(e_1, e_2\) of Definition 197) to \(d_B \otimes _r \operatorname {id}_{\ker (d_F)}\). Applying Definition 204 to this commutative diagram yields \(\ker (\bar{d}_h^1) \simeq \ker (d_B \otimes _r \operatorname {id}_{\ker (d_F)})\).

Step 3. By Definition 199 (flatness of \(\ker (d_F)\) over \(\mathbb {F}_2\)), \(\ker (d_B \otimes _r \operatorname {id}_{\ker (d_F)}) \simeq \ker (d_B) \otimes _{\mathbb {F}_2} \ker (d_F)\).

Composing the three equivalences gives \(H_2(B\otimes _\varphi F) \simeq \ker (d_B) \otimes \ker (d_F)\).

Let \(E = \operatorname {fiberBundleSmallDC}(d_B, d_F, \varphi )\).

Step 1. By the SmallDC homology equivalence at degree 0, \(\operatorname {totH}_0(E) \simeq \operatorname {itH}_0(E) = A_{0,0}/\operatorname {im}(\bar{d}_h^0)\).

Step 2. By Lemma 209, \(\bar{d}_h^0\) is conjugate (via the flatness quotient equivalences \(q_1, q_2\) of Definition 198) to \(d_B \otimes _r \operatorname {id}_{\operatorname {coker}(d_F)}\). Applying Definition 205 gives \(\operatorname {coker}(\bar{d}_h^0) \simeq \operatorname {coker}(d_B \otimes _r \operatorname {id}_{\operatorname {coker}(d_F)})\).

Step 3. By Definition 200, \(\operatorname {coker}(d_B \otimes _r \operatorname {id}_{\operatorname {coker}(d_F)}) \simeq \operatorname {coker}(d_B) \otimes _{\mathbb {F}_2} \operatorname {coker}(d_F)\).

Composing yields \(H_0(B \otimes _\varphi F) \simeq \operatorname {coker}(d_B) \otimes \operatorname {coker}(d_F)\).

Let \(E = \operatorname {fiberBundleSmallDC}(d_B, d_F, \varphi )\).

Step 1. By the SmallDC homology equivalence at degree 1, \(\operatorname {totH}_1(E) \simeq \operatorname {itH}_1^{\mathrm{fst}}(E) \times \operatorname {itH}_1^{\mathrm{snd}}(E)\), where \(\operatorname {itH}_1^{\mathrm{fst}} = \ker (\bar{d}_h^0)\) and \(\operatorname {itH}_1^{\mathrm{snd}} = \operatorname {vH}_{0,1}/\operatorname {im}(\bar{d}_h^1)\).

Step 2a (first factor). By Lemma 209, \(\bar{d}_h^0\) is conjugate (via the quotient flatness equivalences \(q_k\)) to \(d_B \otimes _r \operatorname {id}_{\operatorname {coker}(d_F)}\). Applying Definition 204 gives \(\ker (\bar{d}_h^0) \simeq \ker (d_B \otimes _r \operatorname {id}_{\operatorname {coker}(d_F)})\). Then Definition 199 gives \(\ker (d_B \otimes _r \operatorname {id}_{\operatorname {coker}(d_F)}) \simeq \ker (d_B) \otimes \operatorname {coker}(d_F)\).

Step 2b (second factor). By Lemma 206, \(\bar{d}_h^1\) is conjugate (via the kernel flatness equivalences \(e_k\)) to \(d_B \otimes _r \operatorname {id}_{\ker (d_F)}\). Applying Definition 205 gives \(\operatorname {coker}(\bar{d}_h^1) \simeq \operatorname {coker}(d_B \otimes _r \operatorname {id}_{\ker (d_F)})\). Then Definition 200 gives \(\operatorname {coker}(d_B \otimes _r \operatorname {id}_{\ker (d_F)}) \simeq \operatorname {coker}(d_B) \otimes \ker (d_F)\).

Combining both factors via the product of equivalences (\(\operatorname {prodCongr}\)) with Step 1 yields: