13 Def 10: Total Complex

Definition 120 Total Complex of a Double Complex

✓

Let \(E = (E_{\bullet ,\bullet }, \partial ^v, \partial ^h)\) be a double complex of \(\mathbb {F}_2\)-vector spaces (see Definition 112). The total complex \(\operatorname {Tot}(E)\) is the chain complex over \(\mathbb {F}_2\) indexed by \(\mathbb {Z}\) defined as follows:

The \(n\)-th object is the direct sum

\[ \operatorname {Tot}(E)_n \; =\; \bigoplus _{p+q=n} E_{p,q}, \]

taken over all pairs of integers \((p,q)\) with \(p + q = n\).
The differential \(\partial _n \colon \operatorname {Tot}(E)_n \to \operatorname {Tot}(E)_{n-1}\) restricts to each summand \(E_{p,q}\) as

\[ \partial _n\big|_{E_{p,q}} \; =\; \partial ^v_{p,q} + \partial ^h_{p,q}, \]

where \(\partial ^v_{p,q} \colon E_{p,q} \to E_{p,q-1}\) maps into the \((p, q-1)\)-summand and \(\partial ^h_{p,q} \colon E_{p,q} \to E_{p-1,q}\) maps into the \((p-1,q)\)-summand of \(\operatorname {Tot}(E)_{n-1}\).

Since \(\operatorname {ModuleCat}(\mathbb {F}_2)\) has all coproducts, the total complex exists. This construction is realized via Mathlib’s HomologicalComplex₂.total with the descending complex shape on \(\mathbb {Z}\).

Sign convention: Mathlib uses sign maps \(\varepsilon (n) = (-1)^n\) (implemented by Int.negOnePow) for the TensorSigns instance on ComplexShape.down \(\mathbb {Z}\), satisfying: for \(p + q + 1 = n\), the sign condition \(\varepsilon '_{\mathrm{succ}}\) gives \(\varepsilon (p+1) = -\varepsilon (p)\), verified by simplification using Int.negOnePow_succ and \(-(-x)=x\). Over \(\mathbb {F}_2\) these signs are trivial (since \(-1 = 1\)), so Mathlib’s construction agrees with the sign-free definition in the paper.

Definition 121 Inclusion into Total Complex

✓

Let \(E\) be a double complex of \(\mathbb {F}_2\)-vector spaces. For integers \(p, q, n\) with \(p + q = n\), the inclusion map

\[ \iota _{p,q}^n \colon E_{p,q} \; \longrightarrow \; \operatorname {Tot}(E)_n \]

is the canonical injection of the summand \(E_{p,q}\) into the coproduct \(\operatorname {Tot}(E)_n = \bigoplus _{p'+q'=n} E_{p',q'}\).

Theorem 122 Differential of Total Complex Squares to Zero

✓

Let \(E\) be a double complex of \(\mathbb {F}_2\)-vector spaces. For all integers \(n, m, k\), the composition of consecutive differentials of \(\operatorname {Tot}(E)\) vanishes:

\[ \partial _m \circ \partial _n \; =\; 0 \; \colon \; \operatorname {Tot}(E)_n \; \longrightarrow \; \operatorname {Tot}(E)_k. \]

Proof ▶

This follows directly from the general fact that in any homological complex, the composition of two consecutive differentials is zero, applied to \(\operatorname {Tot}(E)\) via d_comp_d.

Conceptually, \(\partial ^2 = (\partial ^v + \partial ^h)^2 = (\partial ^v)^2 + (\partial ^v \partial ^h + \partial ^h \partial ^v) + (\partial ^h)^2\). Each term vanishes: \((\partial ^v)^2 = 0\) and \((\partial ^h)^2 = 0\) by the double complex axioms, and \(\partial ^v \partial ^h + \partial ^h \partial ^v = 0\) over \(\mathbb {F}_2\) because \(\partial ^v \partial ^h = \partial ^h \partial ^v\) (commutativity up to sign, and \(-1 = 1\) in \(\mathbb {F}_2\)).

Theorem 123 Objects of Total Complex as Coproducts

✓

Let \(E\) be a double complex of \(\mathbb {F}_2\)-vector spaces. For each integer \(n\), the \(n\)-th object of the total complex equals the coproduct

\[ \operatorname {Tot}(E)_n \; =\; \bigl(E^{\mathrm{gr}}\bigr)^{\operatorname {map}}_n, \]

where \(E^{\mathrm{gr}}\) denotes the underlying graded object of \(E\) and the superscript denotes the graded-object mapping along the complex-shape projection \(\pi \colon \mathbb {Z} \times \mathbb {Z} \to \mathbb {Z}\), \((p,q) \mapsto p+q\).

Proof ▶

This holds by reflexivity: the definition of totalComplex as E.total (ComplexShape.down \(\mathbb {Z}\)) and the definition of the total complex object in Mathlib make both sides definitionally equal.

Theorem 124 Extensionality for Morphisms from Total Complex

✓

Let \(E\) be a double complex of \(\mathbb {F}_2\)-vector spaces, let \(A\) be an \(\mathbb {F}_2\)-module, and let \(n \in \mathbb {Z}\). Suppose \(f, g \colon \operatorname {Tot}(E)_n \to A\) are two morphisms such that for all integers \(p, q\) with \(p + q = n\),

\[ f \circ \iota _{p,q}^n \; =\; g \circ \iota _{p,q}^n. \]

Then \(f = g\).

Proof ▶

This follows from the universal property of coproducts: since \(\operatorname {Tot}(E)_n = \bigoplus _{p+q=n} E_{p,q}\), a morphism out of it is uniquely determined by its restrictions to each summand. Formally, this is an application of HomologicalComplex₂.total.hom_ext with the descending complex shape on \(\mathbb {Z}\), using the hypothesis \(h\) that \(\iota _{p,q}^n \gg f = \iota _{p,q}^n \gg g\) for all \(p, q\) with \(p + q = n\).