Definition 2: Cochains and Cohomology

Given a chain complex C = (C_•, ∂) (Def_1) where each C_i is finite-dimensional, we identify C^i = C_i using the 𝔽₂-scalar product. We define:

• Coboundary maps: δ^i = (∂_{i+1})^tr : C^i → C^{i+1}, where the transpose is LinearMap.dualMap (= Module.Dual.transpose).
• Cocycles: Z^i(C) = ker δ^i ⊂ Dual C_i
• Coboundaries: B^i(C) = im δ^{i-1} ⊂ Dual C_i
• Cohomology: H^i(C) = Z^i(C) / B^i(C)

The key relation B^i(C) = (Z_i(C))^{ann} holds, where the dual annihilator corresponds to the orthogonal complement under the 𝔽₂-scalar product (using im(A^tr) = (ker A)^⊥ for finite-dimensional 𝔽₂-vector spaces).

This induces an isomorphism H_i(C) ≅ H^i(C).

Main Definitions

• ChainComplex𝔽₂.coboundaryMap — the coboundary δ^i = (∂_{i+1})^tr
• ChainComplex𝔽₂.incomingCoboundaryMap — the incoming coboundary δ^{i-1} = (∂_i)^tr
• ChainComplex𝔽₂.cocycles — cocycles Z^i(C) = ker δ^i
• ChainComplex𝔽₂.coboundaries — coboundaries B^i(C) = im δ^{i-1}
• ChainComplex𝔽₂.coboundariesSubCocycles — B^i(C) as a submodule of Z^i(C)
• ChainComplex𝔽₂.cohomology — cohomology H^i(C) = Z^i(C) / B^i(C)

Main Theorems

• ChainComplex𝔽₂.coboundaries_eq_dualAnnihilator_cycles — B^i(C) = Z_i(C)^{ann}
• ChainComplex𝔽₂.cocycles_eq_dualAnnihilator_boundaries — Z^i(C) = B_i(C)^{ann}
• ChainComplex𝔽₂.homologyCohomologyEquiv — H_i(C) ≃ₗ[𝔽₂] H^i(C)

Coboundary maps

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

The coboundary map δ^i = (∂_{i+1})^tr : Dual C_i → Dual C_{i+1}. Here ∂_{i+1} is the incoming differential C.incomingDifferential i, and the transpose is LinearMap.dualMap.

Equations

• C.coboundaryMap i = (C.incomingDifferential i).dualMap

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

The incoming coboundary δ^{i-1} = (∂_i)^tr : Dual C_{i-1} → Dual C_i. This is the coboundary map landing in degree i, defined using C.differential i to avoid index arithmetic issues.

Equations

• C.incomingCoboundaryMap i = (C.differential i).dualMap

Cocycles

noncomputable def ChainComplex𝔽₂.cocycles (C : ChainComplex𝔽₂) (i : ℤ) : Submodule 𝔽₂ (Module.Dual 𝔽₂ ↑(C.X i))

The cocycles Z^i(C) = ker δ^i, i.e., the kernel of the coboundary map δ^i : Dual C_i → Dual C_{i+1}, as a submodule of Dual C_i.

Equations

• C.cocycles i = (C.coboundaryMap i).ker

Coboundaries

noncomputable def ChainComplex𝔽₂.coboundaries (C : ChainComplex𝔽₂) (i : ℤ) : Submodule 𝔽₂ (Module.Dual 𝔽₂ ↑(C.X i))

The coboundaries B^i(C) = im δ^{i-1}, i.e., the image (range) of the incoming coboundary δ^{i-1} : Dual C_{i-1} → Dual C_i, as a submodule of Dual C_i.

Equations

• C.coboundaries i = (C.incomingCoboundaryMap i).range

Coboundary composition δ² = 0

theorem ChainComplex𝔽₂.coboundaryMap_comp_incomingCoboundaryMap (C : ChainComplex𝔽₂) (i : ℤ) : C.coboundaryMap i ∘ₗ C.incomingCoboundaryMap i = 0

The coboundary maps satisfy δ^i ∘ δ^{i-1} = 0, dual to ∂_i ∘ ∂_{i+1} = 0.

Coboundaries ⊆ Cocycles

theorem ChainComplex𝔽₂.coboundaries_le_cocycles (C : ChainComplex𝔽₂) (i : ℤ) : C.coboundaries i ≤ C.cocycles i

B^i(C) ⊆ Z^i(C): every coboundary is a cocycle, since δ^i ∘ δ^{i-1} = 0.

Coboundaries as a submodule of cocycles, and cohomology

noncomputable def ChainComplex𝔽₂.coboundariesSubCocycles (C : ChainComplex𝔽₂) (i : ℤ) : Submodule 𝔽₂ ↥(C.cocycles 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) ↪ Dual C_i.

Equations

• C.coboundariesSubCocycles i = Submodule.comap (C.cocycles i).subtype (C.coboundaries i)

@[reducible, inline]

noncomputable abbrev ChainComplex𝔽₂.cohomology (C : ChainComplex𝔽₂) (i : ℤ) : Type

The i-th cohomology H^i(C) = Z^i(C) / B^i(C). Since B^i(C) ⊆ Z^i(C), the coboundaries form a submodule of the cocycles, and the cohomology is the quotient module.

Equations

• C.cohomology i = (↥(C.cocycles i) ⧸ C.coboundariesSubCocycles i)

Key relations: dual annihilator characterizations

Over a field, the dual annihilator satisfies im(f^tr) = (ker f)^{ann} and ker(f^tr) = (im f)^{ann}. These give the fundamental identities B^i = (Z_i)^{ann} and Z^i = (B_i)^{ann}.

theorem ChainComplex𝔽₂.cocycles_eq_dualAnnihilator_boundaries (C : ChainComplex𝔽₂) (i : ℤ) : C.cocycles i = (C.boundaries i).dualAnnihilator

The cocycles are the dual annihilator of the boundaries: Z^i(C) = ker δ^i = (im ∂_{i+1})^{ann} = B_i(C)^{ann}. This follows from ker(f^tr) = (im f)^{ann} (which holds over any commutative ring).

theorem ChainComplex𝔽₂.coboundaries_eq_dualAnnihilator_cycles (C : ChainComplex𝔽₂) (i : ℤ) [FiniteDimensional 𝔽₂ ↑(C.X i)] [FiniteDimensional 𝔽₂ ↑(C.X (i - 1))] : C.coboundaries i = (C.cycles i).dualAnnihilator

The coboundaries are the dual annihilator of the cycles: B^i(C) = im δ^{i-1} = (ker ∂_i)^{ann} = Z_i(C)^{ann}. This follows from im(f^tr) = (ker f)^{ann} for vector spaces over a field.

Homology-cohomology isomorphism

The isomorphism H_i(C) ≅ H^i(C) uses the canonical pairing between a finite-dimensional vector space and its dual. Over 𝔽₂, identifying C^i = C_i via the scalar product, the dual annihilator gives the orthogonal complement, and the quotient Z_i / B_i is canonically isomorphic to Z^i / B^i.

The proof proceeds by showing both quotients have the same finrank, using the dual annihilator dimension formula: dim W + dim W^{ann} = dim V.

theorem ChainComplex𝔽₂.finrank_boundariesSubCycles_eq (C : ChainComplex𝔽₂) (i : ℤ) [FiniteDimensional 𝔽₂ ↑(C.X i)] [FiniteDimensional 𝔽₂ ↑(C.X (i + 1))] : Module.finrank 𝔽₂ ↥(C.boundariesSubCycles i) = Module.finrank 𝔽₂ ↥(C.boundaries i)

The finrank of boundariesSubCycles equals the finrank of boundaries, since the comap of boundaries under the cycles inclusion maps to cycles ⊓ boundaries = boundaries (as B_i ⊆ Z_i).

theorem ChainComplex𝔽₂.finrank_coboundariesSubCocycles_eq (C : ChainComplex𝔽₂) (i : ℤ) [FiniteDimensional 𝔽₂ ↑(C.X i)] [FiniteDimensional 𝔽₂ ↑(C.X (i - 1))] [FiniteDimensional 𝔽₂ ↑(C.X (i + 1))] : Module.finrank 𝔽₂ ↥(C.coboundariesSubCocycles i) = Module.finrank 𝔽₂ ↥(C.coboundaries i)

The finrank of coboundariesSubCocycles equals the finrank of coboundaries, since B^i ⊆ Z^i.

theorem ChainComplex𝔽₂.finrank_homology_eq_finrank_cohomology (C : ChainComplex𝔽₂) (i : ℤ) [FiniteDimensional 𝔽₂ ↑(C.X i)] [FiniteDimensional 𝔽₂ ↑(C.X (i - 1))] [FiniteDimensional 𝔽₂ ↑(C.X (i + 1))] : Module.finrank 𝔽₂ (↥(C.cycles i) ⧸ C.boundariesSubCycles i) = Module.finrank 𝔽₂ (↥(C.cocycles i) ⧸ C.coboundariesSubCocycles i)

noncomputable def ChainComplex𝔽₂.homologyCohomologyEquiv (C : ChainComplex𝔽₂) (i : ℤ) [FiniteDimensional 𝔽₂ ↑(C.X i)] [FiniteDimensional 𝔽₂ ↑(C.X (i - 1))] [FiniteDimensional 𝔽₂ ↑(C.X (i + 1))] : (↥(C.cycles i) ⧸ C.boundariesSubCycles i) ≃ₗ[𝔽₂] ↥(C.cocycles i) ⧸ C.coboundariesSubCocycles i

The isomorphism H_i(C) ≃ₗ[𝔽₂] H^i(C) between homology and cohomology. This follows from the fact that both are finite-dimensional vector spaces of the same dimension over 𝔽₂, using the dual annihilator dimension formula.

Equations

• C.homologyCohomologyEquiv i = LinearEquiv.ofFinrankEq (↥(C.cycles i) ⧸ C.boundariesSubCycles i) (↥(C.cocycles i) ⧸ C.coboundariesSubCocycles i) ⋯