Definition 9: Double Complex

A double complex E = (E_{•,•}, ∂^v, ∂^h) is an array of 𝔽₂-vector spaces E_{p,q} indexed by (p, q) ∈ ℤ × ℤ, equipped with vertical and horizontal differentials:

• ∂^v_{p,q} : E_{p,q} → E_{p,q-1} (vertical, decreasing q)
• ∂^h_{p,q} : E_{p,q} → E_{p-1,q} (horizontal, decreasing p)

satisfying:

1. ∂^v_{p,q-1} ∘ ∂^v_{p,q} = 0 for all p, q
2. ∂^h_{p-1,q} ∘ ∂^h_{p,q} = 0 for all p, q
3. ∂^v_{p-1,q} ∘ ∂^h_{p,q} = ∂^h_{p,q-1} ∘ ∂^v_{p,q} for all p, q (commutativity)

Over 𝔽₂, commutativity and anticommutativity coincide since -1 = 1.

We use Mathlib's HomologicalComplex₂ as the underlying type, with both complex shapes being ComplexShape.down ℤ (decreasing indices).

Main Definitions

• DoubleComplex𝔽₂ — a double complex of 𝔽₂-vector spaces, as a bicomplex
• DoubleComplex𝔽₂.obj — the vector space E_{p,q} at position (p, q)
• DoubleComplex𝔽₂.dv — the vertical differential ∂^v_{p,q} : E_{p,q} → E_{p,q-1}
• DoubleComplex𝔽₂.dh — the horizontal differential ∂^h_{p,q} : E_{p,q} → E_{p-1,q}

Main Results

• DoubleComplex𝔽₂.dv_comp_dv — ∂^v ∘ ∂^v = 0
• DoubleComplex𝔽₂.dh_comp_dh — ∂^h ∘ ∂^h = 0
• DoubleComplex𝔽₂.comm — commutativity: ∂^v ∘ ∂^h = ∂^h ∘ ∂^v
• DoubleComplex𝔽₂.anticomm_eq_comm — over 𝔽₂, anticommutativity = commutativity

Definition

@[reducible, inline]

abbrev DoubleComplex𝔽₂ : Type (u_1 + 1)

A double complex of 𝔽₂-vector spaces indexed by ℤ × ℤ. This is HomologicalComplex₂ (ModuleCat 𝔽₂) (ComplexShape.down ℤ) (ComplexShape.down ℤ), where the first ComplexShape.down ℤ is the horizontal direction (decreasing p) and the second is the vertical direction (decreasing q).

For E : DoubleComplex𝔽₂:

• (E.X p).X q is the vector space E_{p,q}
• (E.X p).d q q' is the vertical differential ∂^v_{p,q} when q' + 1 = q
• (E.d p p').f q is the horizontal differential ∂^h_{p,q} when p' + 1 = p

Equations

• DoubleComplex𝔽₂ = HomologicalComplex₂ (ModuleCat 𝔽₂) (ComplexShape.down ℤ) (ComplexShape.down ℤ)

Accessor functions

noncomputable def DoubleComplex𝔽₂.obj (E : DoubleComplex𝔽₂) (p q : ℤ) : ModuleCat 𝔽₂

The 𝔽₂-vector space E_{p,q} at position (p, q).

Equations

• E.obj p q = (E.X p).X q

noncomputable def DoubleComplex𝔽₂.dv (E : DoubleComplex𝔽₂) (p q : ℤ) : ↑(E.obj p q) →ₗ[𝔽₂] ↑(E.obj p (q - 1))

The vertical differential ∂^v_{p,q} : E_{p,q} → E_{p,q-1} as a linear map.

Equations

• E.dv p q = ModuleCat.Hom.hom ((E.X p).d q (q - 1))

noncomputable def DoubleComplex𝔽₂.dh (E : DoubleComplex𝔽₂) (p q : ℤ) : ↑(E.obj p q) →ₗ[𝔽₂] ↑(E.obj (p - 1) q)

The horizontal differential ∂^h_{p,q} : E_{p,q} → E_{p-1,q} as a linear map.

Equations

• E.dh p q = ModuleCat.Hom.hom ((E.d p (p - 1)).f q)

theorem DoubleComplex𝔽₂.dv_comp_dv (E : DoubleComplex𝔽₂) (p q : ℤ) : E.dv p (q - 1) ∘ₗ E.dv p q = 0

The vertical differential squares to zero: ∂^v_{p,q-1} ∘ ∂^v_{p,q} = 0.

theorem DoubleComplex𝔽₂.dh_comp_dh (E : DoubleComplex𝔽₂) (p q : ℤ) : E.dh (p - 1) q ∘ₗ E.dh p q = 0

The horizontal differential squares to zero: ∂^h_{p-1,q} ∘ ∂^h_{p,q} = 0.

theorem DoubleComplex𝔽₂.comm (E : DoubleComplex𝔽₂) (p q : ℤ) : E.dv (p - 1) q ∘ₗ E.dh p q = E.dh p (q - 1) ∘ₗ E.dv p q

The differentials commute: ∂^v_{p-1,q} ∘ ∂^h_{p,q} = ∂^h_{p,q-1} ∘ ∂^v_{p,q}. This is the commutativity condition for the double complex.

Commutativity and anticommutativity over 𝔽₂

theorem DoubleComplex𝔽₂.anticomm_eq_comm (E : DoubleComplex𝔽₂) (p q : ℤ) : E.dv (p - 1) q ∘ₗ E.dh p q + E.dh p (q - 1) ∘ₗ E.dv p q = 0

Over 𝔽₂, anticommutativity ∂^v ∘ ∂^h + ∂^h ∘ ∂^v = 0 is equivalent to commutativity ∂^v ∘ ∂^h = ∂^h ∘ ∂^v, since -1 = 1 in characteristic 2.