By simplification using the definitions of piStarSummandLin, augMap_zero, and the \(\mathbb {F}_2\)-module isomorphism \(\operatorname {TensorProduct.rid}\), together with the formula for \(\operatorname {lTensor}\) on pure tensors, the result follows by reflexivity.

By simplification using the definitions of piStarSummandLin and augMap with the conditional dif_neg hq (since \(q \ne 0\)), the augmentation map at degree \(q\) is zero, so the composition \(\operatorname {TensorProduct.rid} \circ (\operatorname {id} \otimes 0)\) reduces to zero by \(\operatorname {LinearMap.comp_zero}\).

We proceed by extensionality: it suffices to show \(\varepsilon (\alpha _0(y)) = \varepsilon (y)\) for an arbitrary \(y\). By the degree-\(0\) condition of \(\operatorname {ActsAsIdOnHomology}\), we have \(\alpha _0(y) - y \in \operatorname {im}(\partial ^F)\); that is, there exists \(z\) such that \(\partial ^F(z) = \alpha _0(y) - y\). Since \(\varepsilon \circ \partial ^F = 0\), we rewrite to obtain

Applying \(\varepsilon \) to the difference and using linearity of \(\varepsilon \):

which gives \(\varepsilon (\alpha _0(y)) = \varepsilon (y)\) by \(\operatorname {sub_eq_zero}\).

This is an immediate consequence of aug_comp_\(\alpha _0\)_eq applied to the chain automorphism \(\varphi \, b_1\, b_0\), using the fact that \(\operatorname {ActsAsIdentityOnHomology}\) implies \((\varphi \, b_1\, b_0).\operatorname {ActsAsIdOnHomology}\) whenever \(\partial ^B(\delta _{b_1})(b_0) \ne 0\).

We apply tensor product extensionality: it suffices to verify the equality on pure tensors \(b \otimes f\). Let \(b : \operatorname {Fin}(\operatorname {baseSize}(n_1,m_1,1)) \to \mathbb {F}_2\) and \(f : \operatorname {Fin}(\operatorname {fiberSize}(n_2,m_2,0)) \to \mathbb {F}_2\) be arbitrary.

By twistedDhLin_tmul, we expand the left-hand side:

Applying \(\operatorname {piStarSummandLin}(\partial ^F, \mathtt{aug}, 0, 0)\) and using piStarSummandLin_tmul_q0, each summand becomes \(\varepsilon (\alpha _{b_1,b_0}(f)) \cdot \partial ^B(\delta _{b_1})(b_0) \cdot \delta _{b_0}\).

We then simplify using \(\operatorname {map_sum}\) and \(\operatorname {map_smul}\), and evaluate pointwise at an arbitrary index \(j \in \operatorname {Fin}(m_1)\). The sum collapses via \(\operatorname {Pi.single_apply}\) and \(\operatorname {Finset.sum_ite_eq}\), yielding:

For each pair \((b_1, j)\), we distinguish two cases:

• If \(\partial ^B(\delta _{b_1})(j) = 0\), the contribution is zero on both sides.

• If \(\partial ^B(\delta _{b_1})(j) \ne 0\), by aug_preserved_by_connection and autAtDeg_zero, we have \(\varepsilon \circ \alpha _{b_1,j} = \varepsilon \), so \(\varepsilon (\alpha _{b_1,j}(f)) = \varepsilon (f)\).

Thus each summand equals \(b(b_1) \cdot \partial ^B(\delta _{b_1})(j) \cdot \varepsilon (f)\), and we can factor out \(\varepsilon (f)\):

By linearity of \(\partial ^B\) and the expansion \(b = \sum _{b_1} b(b_1) \cdot \delta _{b_1}\), we obtain \((\partial ^B(b))(j) \cdot \varepsilon (f)\).

For the right-hand side, \(\operatorname {piStarSummandLin}(\partial ^F, \mathtt{aug}, 1, 0)(b \otimes f) = \varepsilon (f) \cdot b\) by piStarSummandLin_tmul_q0, and then \(\partial ^B(\varepsilon (f) \cdot b) = \varepsilon (f) \cdot \partial ^B(b)\) by linearity. Both sides agree at every index \(j\), completing the proof.

We apply tensor product extensionality on pure tensors \(b \otimes f\). By lTensor_tmul, the left-hand side evaluates to:

Since \(\operatorname {fiberDiff}(n_2, m_2, \partial ^F, 1, 0)(f) = \partial ^F(f)\) by unfolding the definition of fiberDiff and using reflexivity, and by piStarSummandLin_tmul_q0, this equals \(\varepsilon (\partial ^F(f)) \cdot b\). Since \(\varepsilon \circ \partial ^F = 0\) (the chain map condition of the augmented complex), we have \(\varepsilon (\partial ^F(f)) = 0\), and therefore \(0 \cdot b = 0\).