Let \(n_2, m_2 \in \mathbb {N}\) and let \(\partial ^F : \mathbb {F}_2^{n_2} \to \mathbb {F}_2^{m_2}\) be a linear map (the differential of a 1-complex \(F\) over \(\mathbb {F}_2\)). A chain automorphism of \(F\) is a structure consisting of:

• an invertible linear map \(\alpha _1 : \mathbb {F}_2^{n_2} \xrightarrow {\sim } \mathbb {F}_2^{n_2}\) (automorphism on \(F_1\)),

• an invertible linear map \(\alpha _0 : \mathbb {F}_2^{m_2} \xrightarrow {\sim } \mathbb {F}_2^{m_2}\) (automorphism on \(F_0\)),

• the chain map condition: \(\partial ^F \circ \alpha _1 = \alpha _0 \circ \partial ^F\).

Given a differential \(\partial ^F : \mathbb {F}_2^{n_2} \to \mathbb {F}_2^{m_2}\), the identity chain automorphism \(\operatorname {id}_F\) is the chain automorphism with \(\alpha _1 = \operatorname {id}_{\mathbb {F}_2^{n_2}}\) and \(\alpha _0 = \operatorname {id}_{\mathbb {F}_2^{m_2}}\).

A connection for a fiber bundle with base dimensions \(n_1, m_1\) and fiber differential \(\partial ^F : \mathbb {F}_2^{n_2} \to \mathbb {F}_2^{m_2}\) is a function

That is, to each pair \((b^1, b^0) \in \operatorname {Fin}(n_1) \times \operatorname {Fin}(m_1)\), the connection assigns a chain automorphism of \(F\). Values outside the support of \(\partial ^B(e_{b^1})\) are irrelevant.

The trivial connection assigns to every pair \((b^1, b^0)\) the identity chain automorphism:

Let \(V\) be an \(\mathbb {F}_2\)-module, let \(\partial ^B : \mathbb {F}_2^{n_1} \to \mathbb {F}_2^{m_1}\) be a linear map, and let \(\operatorname {autComp} : \operatorname {Fin}(n_1) \to \operatorname {Fin}(m_1) \to (V \to _{\mathbb {F}_2} V)\) be a family of linear endomorphisms. The twisted horizontal differential

is the linear map defined via the universal property of the tensor product (via \(\operatorname {TensorProduct.lift}\)): on a pure tensor \(b \otimes f\) (with \(b : \mathbb {F}_2^{n_1}\), \(f : V\)), it acts as

where \(e_{b_1}\) and \(e_{b_0}\) denote the standard basis vectors. This is well-defined as a bilinear map and extends to a linear map on the tensor product.

The base size function assigns dimensions to degrees:

This encodes the graded structure of the base 1-complex \(B = (\mathbb {F}_2^{n_1} \xrightarrow {\partial ^B} \mathbb {F}_2^{m_1})\).

The fiber size function assigns dimensions to degrees:

This encodes the graded structure of the fiber 1-complex \(F = (\mathbb {F}_2^{n_2} \xrightarrow {\partial ^F} \mathbb {F}_2^{m_2})\).

The graded object underlying the fiber bundle double complex is the functor

Given \(\partial ^F : \mathbb {F}_2^{n_2} \to \mathbb {F}_2^{m_2}\), the fiber differential at degrees \((q, q')\) is the linear map

The vertical differential \(\partial ^v = \operatorname {id}_B \otimes \partial ^F\) is the morphism in \(\operatorname {Mod}_{\mathbb {F}_2}\):

defined via \(\operatorname {LinearMap.lTensor}\).

Given a connection \(\varphi \) and a fiber degree \(q \in \mathbb {Z}\), the automorphism component at degree \(q\) is the family of linear endomorphisms

The twisted horizontal differential is the morphism in \(\operatorname {Mod}_{\mathbb {F}_2}\):

where \(\partial ^h_\varphi = \operatorname {twistedDhLin}(\partial ^B, (b_1, b_0) \mapsto \operatorname {autAtDeg}(\partial ^F, \varphi , q, b_1, b_0))\) is the connection-twisted horizontal differential.

Let \(\partial ^B : \mathbb {F}_2^{n_1} \to \mathbb {F}_2^{m_1}\), \(\partial ^F : \mathbb {F}_2^{n_2} \to \mathbb {F}_2^{m_2}\), and \(\varphi \) a connection. The fiber bundle double complex \(B \boxtimes _\varphi F\) is the double complex over \(\mathbb {F}_2\) with:

• Objects: \((p, q) \mapsto \mathbb {F}_2^{\operatorname {baseSize}(p)} \otimes _{\mathbb {F}_2} \mathbb {F}_2^{\operatorname {fiberSize}(q)}\),

• Horizontal differential: \(\partial ^h_\varphi = \operatorname {fbDh}(p, p', q)\) (the connection-twisted map),

• Vertical differential: \(\partial ^v = \operatorname {fbDv}(p, q, q') = \operatorname {id}_B \otimes \partial ^F\).

This is constructed using \(\operatorname {HomologicalComplex}_2.\operatorname {ofGradedObject}\) with the descending complex shape on \(\mathbb {Z}\). The double complex axioms are verified by the following conditions:

1. \((\partial ^h)^2 = 0\): since \(\operatorname {fbDh}(p, p', q) \circ \operatorname {fbDh}(p', p'', q) = 0\) (at most one factor can be nonzero, as \(p = 1, p' = 0\) and \(p' = 1, p'' = 0\) cannot both hold),

2. \((\partial ^v)^2 = 0\): since \(\operatorname {fbDv}(p, q', q'') \circ \operatorname {fbDv}(p, q, q') = 0\) (similarly),

3. Commutativity \(\partial ^h \circ \partial ^v = \partial ^v \circ \partial ^h\): by Lemma 184, since each \(\varphi (b_1, b_0)\) is a chain automorphism.

The fiber bundle complex \(B \otimes _\varphi F = \operatorname {Tot}(B \boxtimes _\varphi F)\) is the total complex of the fiber bundle double complex:

It is the chain complex over \(\mathbb {F}_2\) obtained by taking the direct sum totalization of the double complex \(B \boxtimes _\varphi F\), with differential given by \(\partial ^h_\varphi + \partial ^v\) (summing the horizontal and vertical differentials in each total degree). The existence of the total complex is guaranteed because each graded piece is a finitely-generated \(\mathbb {F}_2\)-module, so all necessary coproducts exist and the \(\operatorname {HasTotal}\) instance holds by type class inference.