Definition 10: Total Complex

Given a double complex E = (E_{•,•}, ∂^v, ∂^h) (Def_9), the total complex Tot(E) is the chain complex (Def_1) defined by:

• Tot(E)_n = ⊕_{p+q=n} E_{p,q} (direct sum over all pairs with p + q = n)
• ∂_n|_{E_{p,q}} = ∂^v_{p,q} + ∂^h_{p,q} (the differential on summand E_{p,q})

where ∂^v_{p,q} : E_{p,q} → E_{p,q-1} maps into the (p, q-1)-summand and ∂^h_{p,q} : E_{p,q} → E_{p-1,q} maps into the (p-1, q)-summand of Tot(E)_{n-1}.

This is indeed a differential since ∂² = (∂^v + ∂^h)² = (∂^v)² + (∂^v∂^h + ∂^h∂^v) + (∂^h)² = 0 + 0 + 0 = 0, using that E is a double complex and we work over 𝔽₂ where ∂^v∂^h + ∂^h∂^v = 2∂^v∂^h = 0.

We use Mathlib's HomologicalComplex₂.total construction, which builds the total complex with sign conventions. Over 𝔽₂, the signs are trivial (-1 = 1), so Mathlib's total complex agrees with the paper's sign-free definition.

Main Definitions

• tensorSigns_down_int — TensorSigns instance for ComplexShape.down ℤ
• DoubleComplex𝔽₂.totalComplex — the total complex Tot(E) as a chain complex over 𝔽₂
• DoubleComplex𝔽₂.ιTotal — the inclusion E_{p,q} ↪ Tot(E)_n when p + q = n

Main Results

• DoubleComplex𝔽₂.totalComplex_d_sq_zero — the differential squares to zero: ∂² = 0
• DoubleComplex𝔽₂.totalComplex_obj_eq — Tot(E)_n is the coproduct of E_{p,q} with p+q=n

TensorSigns instance for ComplexShape.down ℤ

instance tensorSigns_down_int : (ComplexShape.down ℤ).TensorSigns

TensorSigns instance for the descending complex shape on ℤ. The sign map is ε(n) = (-1)^n, implemented via Int.negOnePow. For ComplexShape.down ℤ, Rel i j ↔ j + 1 = i.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ε_down_int (n : ℤ) : (ComplexShape.down ℤ).ε n = n.negOnePow

HasTotal instance

instance DoubleComplex𝔽₂.hasTotal (E : DoubleComplex𝔽₂) : HomologicalComplex₂.HasTotal E (ComplexShape.down ℤ)

A double complex of 𝔽₂-vector spaces has a total complex, since ModuleCat 𝔽₂ has all coproducts.

The total complex

noncomputable def DoubleComplex𝔽₂.totalComplex (E : DoubleComplex𝔽₂) : ChainComplex𝔽₂

The total complex Tot(E) of a double complex E. This is a chain complex over 𝔽₂ indexed by ℤ, where Tot(E)_n = ⊕_{p+q=n} E_{p,q} and the differential is ∂_n|_{E_{p,q}} = ∂^v_{p,q} + ∂^h_{p,q}.

Equations

• E.totalComplex = HomologicalComplex₂.total E (ComplexShape.down ℤ)

Inclusion maps

noncomputable def DoubleComplex𝔽₂.ιTotalComplex (E : DoubleComplex𝔽₂) (p q n : ℤ) (h : p + q = n) : E.obj p q ⟶ E.totalComplex.X n

The inclusion of summand E_{p,q} into Tot(E)_n when p + q = n.

Equations

• E.ιTotalComplex p q n h = HomologicalComplex₂.ιTotal E (ComplexShape.down ℤ) p q n h

The total complex is a chain complex (∂² = 0)

theorem DoubleComplex𝔽₂.totalComplex_d_sq_zero (E : DoubleComplex𝔽₂) (n m k : ℤ) : CategoryTheory.CategoryStruct.comp (E.totalComplex.d n m) (E.totalComplex.d m k) = 0

The differential of the total complex squares to zero: ∂_{n-1} ∘ ∂_n = 0. This follows from (∂^v + ∂^h)² = (∂^v)² + (∂^v∂^h + ∂^h∂^v) + (∂^h)² = 0, using the double complex and the fact that over 𝔽₂, ∂^v∂^h + ∂^h∂^v = 0.

theorem DoubleComplex𝔽₂.totalComplex_obj_eq (E : DoubleComplex𝔽₂) (n : ℤ) : E.totalComplex.X n = (HomologicalComplex₂.toGradedObject E).mapObj ((ComplexShape.down ℤ).π (ComplexShape.down ℤ) (ComplexShape.down ℤ)) n

The n-th object of the total complex is the coproduct ⊕_{p+q=n} E_{p,q}.

Extensionality for morphisms from the total complex

theorem DoubleComplex𝔽₂.totalComplex_hom_ext (E : DoubleComplex𝔽₂) {A : ModuleCat 𝔽₂} {n : ℤ} {f g : E.totalComplex.X n ⟶ A} (h : ∀ (p q : ℤ) (hpq : p + q = n), CategoryTheory.CategoryStruct.comp (E.ιTotalComplex p q n hpq) f = CategoryTheory.CategoryStruct.comp (E.ιTotalComplex p q n hpq) g) : f = g

To show two morphisms from Tot(E)_n are equal, it suffices to check on each summand.