12 Def 9: Double Complex

Definition 112 Double Complex over \(\mathbb {F}_2\)

✓

A double complex of \(\mathbb {F}_2\)-vector spaces is an array of \(\mathbb {F}_2\)-vector spaces \(E_{p,q}\) indexed by \((p,q) \in \mathbb {Z} \times \mathbb {Z}\), equipped with:

a vertical differential \(\partial ^v_{p,q} : E_{p,q} \to E_{p,q-1}\) (decreasing \(q\)),
a horizontal differential \(\partial ^h_{p,q} : E_{p,q} \to E_{p-1,q}\) (decreasing \(p\)),

satisfying:

\(\partial ^v_{p,q-1} \circ \partial ^v_{p,q} = 0\) for all \(p, q\),
\(\partial ^h_{p-1,q} \circ \partial ^h_{p,q} = 0\) for all \(p, q\),
\(\partial ^v_{p-1,q} \circ \partial ^h_{p,q} = \partial ^h_{p,q-1} \circ \partial ^v_{p,q}\) for all \(p, q\) (commutativity).

Over \(\mathbb {F}_2\), commutativity and anticommutativity coincide since \(-1 = 1\) in characteristic \(2\).

Formally, \(\operatorname {DoubleComplex}_{\mathbb {F}_2}\) is defined as \(\operatorname {HomologicalComplex}_2(\operatorname {ModuleCat}\ \mathbb {F}_2,\ \operatorname {ComplexShape.down}\ \mathbb {Z},\ \operatorname {ComplexShape.down}\ \mathbb {Z})\), where the first \(\operatorname {ComplexShape.down}\ \mathbb {Z}\) is the horizontal direction and the second is the vertical direction.

Definition 113 Component Vector Space

✓

Let \(E : \operatorname {DoubleComplex}_{\mathbb {F}_2}\). The \(\mathbb {F}_2\)-vector space at position \((p, q) \in \mathbb {Z} \times \mathbb {Z}\) is defined by

\[ E_{p,q} := (E_p)_q, \]

where \(E_p\) denotes the \(p\)-th column complex and \((E_p)_q\) its \(q\)-th component.

Definition 114 Vertical Differential

✓

Let \(E : \operatorname {DoubleComplex}_{\mathbb {F}_2}\). The vertical differential at position \((p,q)\) is the \(\mathbb {F}_2\)-linear map

\[ \partial ^v_{p,q} : E_{p,q} \to E_{p,q-1} \]

defined as the underlying linear map of the chain complex differential \((E_p).d_{q,q-1}\).

Definition 115 Horizontal Differential

✓

Let \(E : \operatorname {DoubleComplex}_{\mathbb {F}_2}\). The horizontal differential at position \((p,q)\) is the \(\mathbb {F}_2\)-linear map

\[ \partial ^h_{p,q} : E_{p,q} \to E_{p-1,q} \]

defined as the underlying linear map of the \(q\)-th component of the horizontal chain map \(E.d_{p,p-1}\).

Theorem 116 Vertical Differential Squares to Zero

✓

Let \(E : \operatorname {DoubleComplex}_{\mathbb {F}_2}\). For all \(p, q \in \mathbb {Z}\),

\[ \partial ^v_{p,q-1} \circ \partial ^v_{p,q} = 0. \]

Proof ▶

Let \(p, q \in \mathbb {Z}\) be arbitrary. By unfolding the definition of \(\partial ^v\), it suffices to show that for all \(x \in E_{p,q}\),

\[ ((E_p).d_{q-1,q-2} \circ (E_p).d_{q,q-1})(x) = 0. \]

By the chain complex axiom \(d \circ d = 0\) applied to \(E_p\) (i.e., \((E_p).d_{q,q-1} \gg (E_p).d_{q-1,q-2} = 0\)), and simplifying, the composition is the zero map. Rewriting the categorical composition as a composition of module maps via \(\operatorname {ModuleCat.comp_apply}\), we conclude that the value at \(x\) is \(0\).

Theorem 117 Horizontal Differential Squares to Zero

✓

Let \(E : \operatorname {DoubleComplex}_{\mathbb {F}_2}\). For all \(p, q \in \mathbb {Z}\),

\[ \partial ^h_{p-1,q} \circ \partial ^h_{p,q} = 0. \]

Proof ▶

Let \(p, q \in \mathbb {Z}\) be arbitrary. By unfolding the definition of \(\partial ^h\), it suffices to show that for all \(x \in E_{p,q}\),

\[ (((E.d_{p-1,p-2}).f_q) \circ ((E.d_{p,p-1}).f_q))(x) = 0. \]

From the chain complex axiom \(d \circ d = 0\) applied to \(E\) (i.e., \(E.d_{p,p-1} \gg E.d_{p-1,p-2} = 0\)), we obtain that \(((E.d_{p,p-1} \gg E.d_{p-1,p-2}).f_q)(x) = 0\) after simplification. Rewriting using \(\operatorname {HomologicalComplex.comp_f}\) and \(\operatorname {ModuleCat.comp_apply}\), the result follows.

Theorem 118 Commutativity of Differentials

✓

Let \(E : \operatorname {DoubleComplex}_{\mathbb {F}_2}\). For all \(p, q \in \mathbb {Z}\), the vertical and horizontal differentials commute:

\[ \partial ^v_{p-1,q} \circ \partial ^h_{p,q} = \partial ^h_{p,q-1} \circ \partial ^v_{p,q}. \]

Proof ▶

Let \(p, q \in \mathbb {Z}\) be arbitrary. By unfolding the definitions of \(\partial ^v\) and \(\partial ^h\), it suffices to show that for all \(x \in E_{p,q}\),

\[ ((E.d_{p,p-1}).f_q \text{ composed vertically then horizontally})(x) = ((E.d_{p,p-1}).f_q \text{ composed horizontally then vertically})(x). \]

We apply the Mathlib lemma \(\operatorname {HomologicalComplex}_2\texttt{.d\_ comm}\) to \(E\) at indices \(p, p-1, q, q-1\), which gives the required commutativity identity as a morphism in \(\operatorname {ModuleCat}\ \mathbb {F}_2\). Taking the underlying linear map via \(\operatorname {ModuleCat.Hom.hom}\) and evaluating at \(x\) (using \(\operatorname {congr_arg}\)), the result follows by naturality of the bicomplex structure.

Theorem 119 Anticommutativity Equals Commutativity over \(\mathbb {F}_2\)

✓

Let \(E : \operatorname {DoubleComplex}_{\mathbb {F}_2}\). For all \(p, q \in \mathbb {Z}\), the anticommutativity condition holds:

\[ \partial ^v_{p-1,q} \circ \partial ^h_{p,q} + \partial ^h_{p,q-1} \circ \partial ^v_{p,q} = 0. \]

That is, over \(\mathbb {F}_2\), anticommutativity and commutativity of the differentials coincide, since \(-1 = 1\) in characteristic \(2\).

Proof ▶

Rewriting the left-hand side using the commutativity result \(\partial ^v_{p-1,q} \circ \partial ^h_{p,q} = \partial ^h_{p,q-1} \circ \partial ^v_{p,q}\) (Theorem 118), it suffices to show that for all \(x \in E_{p,q}\),

\[ (\partial ^h_{p,q-1} \circ \partial ^v_{p,q})(x) + (\partial ^h_{p,q-1} \circ \partial ^v_{p,q})(x) = 0. \]

We use the fact that \(2 = 0\) in \(\mathbb {F}_2\), which is verified by computation (\(\mathtt{decide}\)). Then \(2 \cdot v = 0\) for any \(v \in \mathbb {F}_2\). Expressing the sum as \(2 \cdot (\partial ^h_{p,q-1} \circ \partial ^v_{p,q})(x)\) via \(\mathtt{two\_ smul}\) and substituting \(2 = 0\) with \(\mathtt{zero\_ smul}\), we obtain \(0\), completing the proof.