Definition 1: Chain Complex

A chain complex of vector spaces over 𝔽₂ is a sequence C = (C_•, ∂) consisting of 𝔽₂-vector spaces C_i for i ∈ ℤ equipped with 𝔽₂-linear maps ∂_i : C_i → C_{i-1} (called differentials) satisfying ∂_{i-1} ∘ ∂_i = 0 for all i.

We define:

• Cycles: Z_i(C) = ker ∂_i ⊂ C_i
• Boundaries: B_i(C) = im ∂_{i+1} ⊂ C_i
• Homology: H_i(C) = Z_i(C) / B_i(C)

The chain complex type itself is ChainComplex𝔽₂ from Rem_2_NotationConventions. Here we provide concrete Submodule-level definitions of cycles, boundaries, and homology, and prove B_i(C) ⊆ Z_i(C).

Main Definitions

• ChainComplex𝔽₂.differential — the differential ∂_i : C_i → C_{i-1} as a linear map
• ChainComplex𝔽₂.cycles — cycles Z_i(C) = ker ∂_i as a submodule of C_i
• ChainComplex𝔽₂.boundaries — boundaries B_i(C) = im ∂_{i+1} as a submodule of C_i
• ChainComplex𝔽₂.boundariesSubCycles — B_i(C) as a submodule of Z_i(C)
• ChainComplex𝔽₂.homology' — homology H_i(C) = Z_i(C) / B_i(C) as a quotient module
• ChainComplex𝔽₂.boundaries_le_cycles — B_i(C) ⊆ Z_i(C)

The differential as a linear map

noncomputable def ChainComplex𝔽₂.differential (C : ChainComplex𝔽₂) (i : ℤ) : ↑(C.X i) →ₗ[𝔽₂] ↑(C.X (i - 1))

The differential ∂_i : C_i → C_{i-1} extracted as an 𝔽₂-linear map. We use C.d i (i - 1) which is the Mathlib differential for ComplexShape.down ℤ.

Equations

• C.differential i = ModuleCat.Hom.hom (C.d i (i - 1))

noncomputable def ChainComplex𝔽₂.incomingDifferential (C : ChainComplex𝔽₂) (i : ℤ) : ↑(C.X (i + 1)) →ₗ[𝔽₂] ↑(C.X i)

The incoming differential ∂_{i+1} : C_{i+1} → C_i, extracted as a linear map. This uses C.d (i + 1) i, which avoids issues with (i + 1) - 1 vs i.

Equations

• C.incomingDifferential i = ModuleCat.Hom.hom (C.d (i + 1) i)

Cycles

noncomputable def ChainComplex𝔽₂.cycles (C : ChainComplex𝔽₂) (i : ℤ) : Submodule 𝔽₂ ↑(C.X i)

The cycles Z_i(C) = ker ∂_i, i.e., the kernel of the differential ∂_i : C_i → C_{i-1}, as a submodule of C_i.

Equations

• C.cycles i = (C.differential i).ker

Boundaries

noncomputable def ChainComplex𝔽₂.boundaries (C : ChainComplex𝔽₂) (i : ℤ) : Submodule 𝔽₂ ↑(C.X i)

The boundaries B_i(C) = im ∂_{i+1}, i.e., the image of ∂_{i+1} : C_{i+1} → C_i, as a submodule of C_i.

Equations

• C.boundaries i = (C.incomingDifferential i).range

Boundaries ⊆ Cycles

theorem ChainComplex𝔽₂.differential_comp_incomingDifferential (C : ChainComplex𝔽₂) (i : ℤ) : C.differential i ∘ₗ C.incomingDifferential i = 0

The chain complex condition ∂_i ∘ ∂_{i+1} = 0 as a composition of linear maps.

theorem ChainComplex𝔽₂.boundaries_le_cycles (C : ChainComplex𝔽₂) (i : ℤ) : C.boundaries i ≤ C.cycles i

B_i(C) ⊆ Z_i(C): every boundary is a cycle, since ∂_i ∘ ∂_{i+1} = 0.

Boundaries as a submodule of cycles, and homology

noncomputable def ChainComplex𝔽₂.boundariesSubCycles (C : ChainComplex𝔽₂) (i : ℤ) : Submodule 𝔽₂ ↥(C.cycles i)

B_i(C) viewed as a submodule of Z_i(C), using the inclusion B_i ⊆ Z_i. This is the preimage of B_i(C) under the subtype embedding Z_i(C) ↪ C_i.

Equations

• C.boundariesSubCycles i = Submodule.comap (C.cycles i).subtype (C.boundaries i)

noncomputable def ChainComplex𝔽₂.homology' (C : ChainComplex𝔽₂) (i : ℤ) : Type u_1

The i-th homology H_i(C) = Z_i(C) / B_i(C). Since B_i(C) ⊆ Z_i(C), the boundaries form a submodule of the cycles, and the homology is the quotient module.

Equations

• C.homology' i = (↥(C.cycles i) ⧸ C.boundariesSubCycles i)