Euler--Poincaré for chain complexes of vector spaces indexed by ℕ

A chain complex K indexed by ℕ, with differentials Kₙ₊₁ ⟶ Kₙ, is the shape of singular and cellular chains. When its terms are finite-dimensional vector spaces, rank--nullity for each differential, applied to the boundaries Bₙ = im (Kₙ₊₁ ⟶ Kₙ), gives

dim Kₙ = dim Hₙ(K) + dim Bₙ + dim Bₙ₋₁,

(ChainComplex.finrank_X_zero, ChainComplex.finrank_X_succ), and the alternating sum of these identities telescopes: up to degree n the alternating sums of the dimensions of the terms and of the homology differ by (-1)ⁿ dim Bₙ (ChainComplex.sum_range_finrank_X_eq_sum_range_finrank_homology_add). If the differential Kₙ₊₁ ⟶ Kₙ vanishes, the last boundary term dim Bₙ vanishes, so the alternating sums of the dimensions of the terms and of the homology agree up to degree n (ChainComplex.sum_range_finrank_X_eq_sum_range_finrank_homology). The terms in degrees above n + 1 play no role.

For a complex of finite-dimensional vector spaces that vanishes in all large degrees this is the equality of Mathlib's term and homology Euler characteristics (ChainComplex.eulerChar_eq_homologyEulerChar). Both sides are finsums, and the vanishing hypothesis is what makes them honest finite sums. The same equality for bounded cochain complexes indexed by ℤ with terms in FGModuleCat k is HomologicalComplex.eulerChar_forgetFG_eq_homologyEulerChar; here the complex stays in ModuleCat k with the homological indexing by ℕ, and finite-dimensionality of its terms is a hypothesis.

The telescoping rests on the description of the homology of one short complex X₁ ⟶ X₂ ⟶ X₃ of modules as the kernel of the second map modulo the range of the first: over a division ring its dimension is dim ker g - dim im f (CategoryTheory.ShortComplex.finrank_homology_add_finrank_range_f). The same description shows that over a noetherian ring the homology is finitely generated when X₂ is (CategoryTheory.ShortComplex.finite_homology).

References

• Charles A. Weibel, An Introduction to Homological Algebra, Sections 1.1 and 1.3.

theorem ChainComplex.finrank_X_zero {k : Type u} [DivisionRing k] (K : ChainComplex (ModuleCat k) ℕ) [Module.Finite k ↑(K.X 0)] : Module.finrank k ↑(K.X 0) = Module.finrank k ↑(HomologicalComplex.homology K 0) + Module.finrank k ↥(ModuleCat.Hom.hom (K.d 1 0)).range

In degree 0, every element is a cycle, so dim K₀ = dim H₀(K) + dim im (K₁ ⟶ K₀).

theorem ChainComplex.finrank_X_succ {k : Type u} [DivisionRing k] (K : ChainComplex (ModuleCat k) ℕ) (n : ℕ) [Module.Finite k ↑(K.X (n + 1))] : Module.finrank k ↑(K.X (n + 1)) = Module.finrank k ↑(HomologicalComplex.homology K (n + 1)) + Module.finrank k ↥(ModuleCat.Hom.hom (K.d (n + 2) (n + 1))).range + Module.finrank k ↥(ModuleCat.Hom.hom (K.d (n + 1) n)).range

In degree n + 1, rank--nullity for Kₙ₊₁ ⟶ Kₙ gives dim Kₙ₊₁ = dim Hₙ₊₁(K) + dim im (Kₙ₊₂ ⟶ Kₙ₊₁) + dim im (Kₙ₊₁ ⟶ Kₙ).

theorem ChainComplex.sum_range_finrank_X_eq_sum_range_finrank_homology_add {k : Type u} [DivisionRing k] (K : ChainComplex (ModuleCat k) ℕ) (n : ℕ) (hfinite : ∀ i ≤ n, Module.Finite k ↑(K.X i)) : ∑ i ∈ Finset.range (n + 1), (-1) ^ i * ↑(Module.finrank k ↑(K.X i)) = ∑ i ∈ Finset.range (n + 1), (-1) ^ i * ↑(Module.finrank k ↑(HomologicalComplex.homology K i)) + (-1) ^ n * ↑(Module.finrank k ↥(ModuleCat.Hom.hom (K.d (n + 1) n)).range)

If the terms of K through degree n are finite-dimensional, the alternating sums up to degree n of the dimensions of the terms and of the homology of K differ by the dimension of the boundaries im (Kₙ₊₁ ⟶ Kₙ) in degree n, with sign (-1)ⁿ.

theorem ChainComplex.sum_range_finrank_X_eq_sum_range_finrank_homology {k : Type u} [DivisionRing k] (K : ChainComplex (ModuleCat k) ℕ) {n : ℕ} (hfinite : ∀ i ≤ n, Module.Finite k ↑(K.X i)) (hn : K.d (n + 1) n = 0) : ∑ i ∈ Finset.range (n + 1), (-1) ^ i * ↑(Module.finrank k ↑(K.X i)) = ∑ i ∈ Finset.range (n + 1), (-1) ^ i * ↑(Module.finrank k ↑(HomologicalComplex.homology K i))

Euler--Poincaré for a chain complex of vector spaces indexed by ℕ. If the terms of K through degree n are finite-dimensional and the differential Kₙ₊₁ ⟶ Kₙ vanishes, then the alternating sums up to degree n of the dimensions of the terms and of the homology of K agree.

theorem ChainComplex.eulerChar_eq_homologyEulerChar {k : Type u} [DivisionRing k] (K : ChainComplex (ModuleCat k) ℕ) [∀ (n : ℕ), Module.Finite k ↑(K.X n)] (hK : ∀ᶠ (n : ℕ) in Filter.atTop, CategoryTheory.Limits.IsZero (K.X n)) : HomologicalComplex.eulerChar K = HomologicalComplex.homologyEulerChar K

Euler--Poincaré for a bounded chain complex of vector spaces. For a chain complex of finite-dimensional vector spaces indexed by ℕ whose terms vanish in all large degrees, Mathlib's Euler characteristic of the terms equals that of the homology.