This holds by applying the identity \(\operatorname {fst} \circ (\partial ^v_1 \times \partial ^h_1) = \partial ^v_1\), which follows from the definition of the product map and the projection axiom \(\operatorname {fst}(\partial ^v_1(x), \partial ^h_1(x)) = \partial ^v_1(x)\). Verified by simplification using the component projections of the product linear map.

This holds by applying the identity \(\operatorname {snd} \circ (\partial ^v_1 \times \partial ^h_1) = \partial ^h_1\), verified by simplification using the second projection of the product linear map.

By extensionality, let \(x \in A_{1,1}\). We compute:

Rewriting using the component lemmas \((\partial _2(x))_1 = \partial ^v_1(x)\) and \((\partial _2(x))_2 = \partial ^h_1(x)\), we get

By the commutativity condition \(\partial ^v_0 \circ \partial ^h_1 = \partial ^h_0 \circ \partial ^v_1\), this equals

Since we are over \(\mathbb {F}_2\), any element added to itself is zero, so this sum is \(0\).

Let \(x \in B_1\). We must show \(x \in Z_1 = \ker (\partial _1)\). Since \(x \in \operatorname {im}(\partial _2)\), obtain \(y \in A_{1,1}\) such that \(x = \partial _2(y)\). By the identity \(\partial _1 \circ \partial _2 = 0\) (Lemma 140), we have \(\partial _1(x) = \partial _1(\partial _2(y)) = 0\), so \(x \in \ker (\partial _1) = Z_1\).

Let \(x \in \operatorname {im}(\partial ^v_1)\), so \(x = \partial ^v_1(z)\) for some \(z \in A_{1,1}\). By the commutativity condition \(\partial ^v_0 \circ \partial ^h_1 = \partial ^h_0 \circ \partial ^v_1\), we have

Let \(x \in \ker (\partial ^v_1)\), so \(\partial ^v_1(x) = 0\). We must show \(\partial ^v_0(\partial ^h_1(x)) = 0\). By the commutativity condition \(\partial ^v_0 \circ \partial ^h_1 = \partial ^h_0 \circ \partial ^v_1\):

Rewriting using the membership \(x \in \ker (\partial ^v_1)\) and applying linearity, we conclude \(\partial ^h_1(x) \in \ker (\partial ^v_0)\).

This follows directly from the standard identity \(\ker (f \times g) = \ker (f) \cap \ker (g)\) for product linear maps, applied to \(\partial _2 = \partial ^v_1 \times \partial ^h_1\): an element \(x\) satisfies \(\partial _2(x) = 0\) if and only if \((\partial ^v_1(x), \partial ^h_1(x)) = (0, 0)\), which holds if and only if \(x \in \ker (\partial ^v_1) \cap \ker (\partial ^h_1)\).

This holds by reflexivity from the definition of \(\bar{\partial }^h_1\) as a codomain restriction: \(\bar{\partial }^h_1\langle x, hx \rangle = \langle \partial ^h_1(x), \ldots \rangle \), so its underlying value is \(\partial ^h_1(x)\).

We use the kernel membership criterion \(x \in \ker (\bar{\partial }^h_1) \Leftrightarrow \bar{\partial }^h_1(x) = 0\). Since \(H^v_{0,1}\) is a subtype, \(\bar{\partial }^h_1(x) = 0\) holds in the subtype if and only if its underlying value equals 0 in \(A_{0,1}\). \((\Rightarrow )\): Suppose \(\bar{\partial }^h_1(x) = 0\). Taking the underlying value of both sides: \((\bar{\partial }^h_1(x))_{\text{val}} = 0_{\text{val}} = 0\). By Lemma 158, \(\partial ^h_1(x_{\text{val}}) = 0\), so \(x_{\text{val}} \in \ker (\partial ^h_1)\). \((\Leftarrow )\): Suppose \(x_{\text{val}} \in \ker (\partial ^h_1)\), i.e., \(\partial ^h_1(x_{\text{val}}) = 0\). By subtype injectivity and Lemma 158, the underlying value of \(\bar{\partial }^h_1(x)\) is 0, so \(\bar{\partial }^h_1(x) = 0\).

We construct an explicit \(\mathbb {F}_2\)-linear equivalence. By Lemma 157, \(\ker (\partial _2) = \ker (\partial ^v_1) \cap \ker (\partial ^h_1)\).

Forward map: Given \(\langle x, hx \rangle \in \ker (\partial _2)\), we have \(x \in \ker (\partial ^v_1) \cap \ker (\partial ^h_1)\). From the intersection decomposition, extract \(hx_1 : x \in \ker (\partial ^v_1)\) and \(hx_2 : x \in \ker (\partial ^h_1)\). Define the image as \(\langle \langle x, hx_1 \rangle , (\bar{\partial }^h_1\text{-kernel membership obtained from } hx_2 \text{ via Lemma~ \ref{lem:SmallDC.barDh1_ker_iff}}) \rangle \in \ker (\bar{\partial }^h_1)\).

Backward map: Given \(\langle \langle x, hx_v \rangle , hx_h \rangle \) where \(\langle x, hx_v \rangle \in H^v_{1,1}\) and the pair lies in \(\ker (\bar{\partial }^h_1)\), by Lemma 159 we have \(x \in \ker (\partial ^h_1)\). Combined with \(hx_v : x \in \ker (\partial ^v_1)\), Lemma 157 gives \(x \in \ker (\partial _2)\).

Linearity: Both \(\operatorname {map_add’}\) and \(\operatorname {map_smul’}\) hold by subtype extensionality and reflexivity.

Inverse laws: Both left and right inverses hold by subtype extensionality and reflexivity.

By extensionality in \(A_{0,0}\), using the definition \(\partial _1(a,b) = \partial ^h_0(a) + \partial ^v_0(b)\). \((\subseteq )\): If \(y \in \operatorname {im}(\partial _1)\), obtain \((a,b) \in A_{1,0} \times A_{0,1}\) with \(\partial _1(a,b) = y\), i.e., \(y = \partial ^h_0(a) + \partial ^v_0(b)\). Then \(\partial ^h_0(a) \in \operatorname {im}(\partial ^h_0)\) and \(\partial ^v_0(b) \in \operatorname {im}(\partial ^v_0)\), so \(y \in \operatorname {im}(\partial ^h_0) + \operatorname {im}(\partial ^v_0)\). \((\supseteq )\): If \(y = u + v\) with \(u = \partial ^h_0(a) \in \operatorname {im}(\partial ^h_0)\) and \(v = \partial ^v_0(b) \in \operatorname {im}(\partial ^v_0)\), then \(y = \partial _1(a,b) \in \operatorname {im}(\partial _1)\).

By extensionality in \(H^v_{0,0}\). \((\subseteq )\): Given \(y \in \operatorname {im}(\bar{\partial }^h_0)\), obtain \([a] \in H^v_{1,0}\) with \(\bar{\partial }^h_0([a]) = y\). By induction on the quotient representative \(a \in A_{1,0}\), the element \(\partial ^h_0(a) \in \operatorname {im}(\partial ^h_0) \subseteq \operatorname {im}(\partial ^h_0) + \operatorname {im}(\partial ^v_0)\), and its image under \(\pi = \operatorname {mkQ}(\operatorname {im}(\partial ^v_0))\) equals \(y\). \((\supseteq )\): Given \(y = \pi (z)\) with \(z \in \operatorname {im}(\partial ^h_0) + \operatorname {im}(\partial ^v_0)\), write \(z = \partial ^h_0(a) + v\) with \(a \in A_{1,0}\) and \(v \in \operatorname {im}(\partial ^v_0)\). Then \(\pi (v) = 0\) in the quotient, so \(\pi (z) = \pi (\partial ^h_0(a)) + 0 = \bar{\partial }^h_0([a]) \in \operatorname {im}(\bar{\partial }^h_0)\).

The isomorphism is constructed as a composition of three quotient equivalences. By Lemma 161, \(\operatorname {im}(\partial _1) = \operatorname {im}(\partial ^h_0) + \operatorname {im}(\partial ^v_0)\), giving

By the second isomorphism theorem for modules (quotient-quotient equivalence), since \(\operatorname {im}(\partial ^v_0) \leq \operatorname {im}(\partial ^h_0) + \operatorname {im}(\partial ^v_0)\):

By Lemma 162, \((\operatorname {im}(\partial ^h_0) + \operatorname {im}(\partial ^v_0))/\operatorname {im}(\partial ^v_0) = \operatorname {im}(\bar{\partial }^h_0)\), so the result is \(H^v_{0,0}/\operatorname {im}(\bar{\partial }^h_0) = \mathcal{H}_0\).

Let \(z = (a,b) \in Z_1 = \ker (\partial _1)\). We must show \(\bar{\partial }^h_0([a]) = 0\) in \(H^v_{0,0}\). By definition, \(\bar{\partial }^h_0([a]) = [\partial ^h_0(a)]\) in \(H^v_{0,0} = A_{0,0}/\operatorname {im}(\partial ^v_0)\), so we need \(\partial ^h_0(a) \in \operatorname {im}(\partial ^v_0)\). Since \((a,b) \in \ker (\partial _1)\), we have \(\partial ^h_0(a) + \partial ^v_0(b) = 0\), hence \(\partial ^h_0(a) = -\partial ^v_0(b)\). Over \(\mathbb {F}_2\), negation is the identity, so \(\partial ^h_0(a) = \partial ^v_0(b) \in \operatorname {im}(\partial ^v_0)\).

Let \(v = (a',b') \in B_1^Z \subseteq Z_1\). We must show \(\pi '(v) = 0\), i.e., the image of \(\pi '\) at \(v\) is zero in \(\ker (\bar{\partial }^h_0)\). Since \(v \in B_1^Z\), we have \((a',b') \in \operatorname {im}(\partial _2)\); obtain \(x \in A_{1,1}\) with \(\partial _2(x) = (a',b')\). By Lemma 138, \(a' = (\partial _2(x))_1 = \partial ^v_1(x) \in \operatorname {im}(\partial ^v_1)\). Therefore \([a'] = 0\) in \(H^v_{1,0} = A_{1,0}/\operatorname {im}(\partial ^v_1)\), so \(\pi '(v) = 0\).

Let \(v \in \operatorname {im}(\bar{\partial }^h_1)\), so \(v = \bar{\partial }^h_1(\langle w, hw \rangle )\) for some \(w \in A_{1,1}\) with \(hw : w \in \ker (\partial ^v_1)\). We must show \(q(\iota (v)) = 0\) in \(H_1(\operatorname {Tot}(E))\), i.e., \(\iota (v) \in B_1^Z = \operatorname {im}(\partial _2) \cap Z_1\).

We have \(\iota (v) = \iota (\bar{\partial }^h_1\langle w, hw \rangle ) = (0, \partial ^h_1(w)) \in Z_1\). It suffices to show \((0, \partial ^h_1(w)) \in \operatorname {im}(\partial _2)\). We claim \(\partial _2(w) = (0, \partial ^h_1(w))\):

• First component: \((\partial _2(w))_1 = \partial ^v_1(w) = 0\) by Lemma 138 since \(w \in \ker (\partial ^v_1)\).

• Second component: \((\partial _2(w))_2 = \partial ^h_1(w)\) by Lemma 139.

Thus \((0, \partial ^h_1(w)) = \partial _2(w) \in \operatorname {im}(\partial _2)\).

By induction on representatives, it suffices to show that for each \(\langle b, hb \rangle \in H^v_{0,1}\):

Step 1: By definition of \(\bar{\iota }\), \(\bar{\iota }([\langle b, hb \rangle ]) = q(\iota (\langle b, hb \rangle ))\), where \(q\) is the quotient map \(Z_1 \to H_1(\operatorname {Tot}(E))\).

Step 2: By definition of \(\bar{\pi }\), \(\bar{\pi }(q(\iota (\langle b, hb \rangle ))) = \pi '(\iota (\langle b, hb \rangle ))\).

Step 3: We compute \(\pi (\iota (\langle b, hb \rangle )) = [(\iota \langle b, hb \rangle )_1] = [(0, b)_1] = [0] = 0\) in \(H^v_{1,0}\), since \(\iota \) maps to \((0, b)\) and the first component of \((0,b)\) is \(0 \in \operatorname {im}(\partial ^v_1)\). Therefore \(\pi '(\iota (\langle b, hb \rangle )) = 0\).

Suppose \((0, b) \in \operatorname {im}(\partial _2)\); obtain \(w \in A_{1,1}\) with \(\partial _2(w) = (0, b)\).

By Lemma 138: \(\partial ^v_1(w) = (\partial _2(w))_1 = 0\), so \(w \in \ker (\partial ^v_1) = H^v_{1,1}\).

By Lemma 139: \(\partial ^h_1(w) = (\partial _2(w))_2 = b\).

Therefore \(\langle w, \partial ^v_1(w) = 0 \rangle \in H^v_{1,1}\) and \(\bar{\partial }^h_1(\langle w, \cdot \rangle ) = \langle \partial ^h_1(w), \cdot \rangle = \langle b, hb \rangle \), showing \(\langle b, hb \rangle \in \operatorname {im}(\bar{\partial }^h_1)\).

It suffices to show \(\ker (\bar{\iota }) = \{ 0\} \). Let \(y \in \ker (\bar{\iota })\) and lift to a representative \(\langle b, hb \rangle \in H^v_{0,1}\). We must show \([\langle b, hb \rangle ] = 0\) in \(\mathcal{H}_{1,\text{snd}}\), i.e., \(\langle b, hb \rangle \in \operatorname {im}(\bar{\partial }^h_1)\).

From \(\bar{\iota }([\langle b, hb \rangle ]) = 0\) in \(H_1(\operatorname {Tot}(E))\), we have \(q(\iota (\langle b, hb \rangle )) = 0\), so \(\iota (\langle b, hb \rangle ) \in B_1^Z = \operatorname {im}(\partial _2) \cap Z_1\). Unwinding, the element \((0, b) \in \operatorname {im}(\partial _2)\).

By Lemma 173, \(\langle b, hb \rangle \in \operatorname {im}(\bar{\partial }^h_1)\), as required.

Let \(\langle q, hq \rangle \in \ker (\bar{\partial }^h_0) = \mathcal{H}_{1,\text{fst}}\). Lift \(q \in H^v_{1,0}\) to a representative \(a \in A_{1,0}\). Since \([a] \in \ker (\bar{\partial }^h_0)\), we have \(\bar{\partial }^h_0([a]) = 0\) in \(H^v_{0,0}\), i.e., \([\partial ^h_0(a)] = 0\), so \(\partial ^h_0(a) \in \operatorname {im}(\partial ^v_0)\).

Obtain \(b \in A_{0,1}\) with \(\partial ^h_0(a) = \partial ^v_0(b)\). Over \(\mathbb {F}_2\), \(\partial ^h_0(a) + \partial ^v_0(b) = 2\partial ^v_0(b) = 0\), so \((a,b) \in \ker (\partial _1) = Z_1\).

Consider \([(a,b)] \in H_1(\operatorname {Tot}(E))\). Then \(\bar{\pi }([(a,b)]) = [a] \in H^v_{1,0}\), which as an element of \(\ker (\bar{\partial }^h_0)\) equals \(\langle q, hq \rangle \) since \([a] = q\). Hence \(\bar{\pi }\) is surjective.

By extensionality on representatives in \(H_1(\operatorname {Tot}(E))\).

\((\subseteq )\): Let \(z \in Z_1\) with \(\bar{\pi }([z]) = 0\), i.e., \([z] \in \ker (\bar{\pi })\). The condition \(\bar{\pi }([z]) = 0\) means \(\pi '(z) = 0\) in \(\ker (\bar{\partial }^h_0)\), i.e., \(z_1 \in \operatorname {im}(\partial ^v_1)\). Obtain \(w\) with \(z_1 = \partial ^v_1(w)\).

Set \(b' = z_2 + \partial ^h_1(w) \in A_{0,1}\). Using the commutativity condition, \(\partial ^v_0(b') = \partial ^v_0(z_2) + \partial ^h_0(\partial ^v_1(w)) = 0\) (since \(z \in \ker (\partial _1)\) gives \(\partial ^h_0(z_1) + \partial ^v_0(z_2) = 0\) and \(z_1 = \partial ^v_1(w)\), combined with \(\partial ^v_0 \circ \partial ^h_1 = \partial ^h_0 \circ \partial ^v_1\) over \(\mathbb {F}_2\)). Thus \(\langle b', hb' \rangle \in H^v_{0,1}\).

The difference \(z - \iota \langle b', hb' \rangle = (\partial ^v_1(w), -\partial ^h_1(w)) = \partial _2(w)\) (over \(\mathbb {F}_2\), negation is identity) lies in \(B_1^Z\). Hence \([z] = [\iota \langle b', hb' \rangle ] = \bar{\iota }([\langle b', hb' \rangle ]) \in \operatorname {im}(\bar{\iota })\).

\((\supseteq )\): This follows directly from Lemma 172: for any \(y\), \(\bar{\pi }(\bar{\iota }(y)) = 0\).

We construct a short exact sequence that splits over \(\mathbb {F}_2\). By Lemma 172, Lemma 174, Lemma 175, and Lemma 176, the sequence

is short exact (with \(\bar{\iota }\) injective, \(\bar{\pi }\) surjective, and \(\ker (\bar{\pi }) = \operatorname {im}(\bar{\iota })\)).

Over \(\mathbb {F}_2\) (a field), every short exact sequence of vector spaces splits. Concretely, we apply the Mathlib lemma Submodule.exists_isCompl to \(\operatorname {im}(\bar{\iota }) \subseteq H_1(\operatorname {Tot}(E))\) to obtain a complement \(K\) with \(\operatorname {im}(\bar{\iota }) \oplus K = H_1(\operatorname {Tot}(E))\). The isomorphism is assembled as the composition:

Each step uses a standard linear equivalence: the complement decomposition, the linear equivalence from injectivity of \(\bar{\iota }\), the quotient-kernel equivalence for \(\bar{\pi }\), and the product commutativity isomorphism.