Euler--Poincaré for finite-dimensional cochain complexes

Mathlib defines the Euler characteristic of a homological complex using finsum. That definition is intentionally total: it returns zero when the summand has infinite support, and finrank itself returns zero for modules that are not finite free. This file identifies those totalized definitions with honest finite sums for bounded cochain complexes of finite-dimensional vector spaces, and proves that the term and homology Euler characteristics agree.

Finite-dimensionality is encoded by taking the original complex in FGModuleCat k. The characteristics are evaluated after applying the forgetful functor to ModuleCat k, as required by Mathlib's definitions. Boundedness is retained as explicit lower and upper bounds. Thus neither possible junk value is used in the Euler--Poincaré identity.

Main results

• HomologicalComplex.eulerChar_forgetFG_eq_sum_finrank: Mathlib's term Euler characteristic is the finite sum over any finite set containing the bounding interval.
• HomologicalComplex.homologyEulerChar_forgetFG_eq_sum_finrank: Mathlib's homology Euler characteristic is the corresponding finite sum of the homology dimensions in FGModuleCat k.
• HomologicalComplex.eulerChar_forgetFG_eq_homologyEulerChar: the finite-dimensional Euler--Poincaré identity in Mathlib's Euler-characteristic API.

References

• Charles A. Weibel, An Introduction to Homological Algebra, Sections 1.3 and 1.6.
• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Proposition 6.6.

theorem HomologicalComplex.finrankSupport_X_subset_Icc {R : Type u} [Ring R] [Nontrivial R] (K : CochainComplex (ModuleCat R) ℤ) (a b : ℤ) [K.IsStrictlyGE a] [K.IsStrictlyLE b] : GradedObject.finrankSupport K.X ⊆ ↑(Finset.Icc a b)

The finrank support of a strictly bounded complex of modules lies in any interval supplied by its bounds.

theorem HomologicalComplex.finrankSupport_homology_subset_Icc {R : Type u} [Ring R] [Nontrivial R] (K : CochainComplex (ModuleCat R) ℤ) (a b : ℤ) [K.IsGE a] [K.IsLE b] : (GradedObject.finrankSupport fun (n : ℤ) => homology K n) ⊆ ↑(Finset.Icc a b)

The finrank support of the homology of a cohomologically bounded complex of modules lies in any interval supplied by its bounds.

theorem HomologicalComplex.eulerChar_forgetFG_eq_sum_finrank {k : Type u} [DivisionRing k] (K : CochainComplex (FGModuleCat k) ℤ) (a b : ℤ) [K.IsStrictlyGE a] [K.IsStrictlyLE b] {s : Finset ℤ} (hs : Finset.Icc a b ⊆ s) : (((CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k)).mapHomologicalComplex (ComplexShape.up ℤ)).obj K).eulerChar = ∑ n ∈ s, ↑n.negOnePow * ↑(Module.finrank k ↑(K.X n))

Mathlib's finsum Euler characteristic of a bounded complex of finite-dimensional vector spaces is the honest finite sum of its term dimensions over any finite set containing the bounding interval Finset.Icc a b.

@[simp]

theorem HomologicalComplex.finrank_homology_forget {k : Type u} [DivisionRing k] (K : CochainComplex (FGModuleCat k) ℤ) (n : ℤ) : Module.finrank k ↑((((CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k)).mapHomologicalComplex (ComplexShape.up ℤ)).obj K).homology n) = Module.finrank k ↑(homology K n)

Forgetting an FGModuleCat complex before taking homology does not change homology finrank.

theorem HomologicalComplex.homologyEulerChar_forgetFG_eq_sum_finrank {k : Type u} [DivisionRing k] (K : CochainComplex (FGModuleCat k) ℤ) (a b : ℤ) [K.IsGE a] [K.IsLE b] {s : Finset ℤ} (hs : Finset.Icc a b ⊆ s) : (((CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k)).mapHomologicalComplex (ComplexShape.up ℤ)).obj K).homologyEulerChar = ∑ n ∈ s, ↑n.negOnePow * ↑(Module.finrank k ↑(homology K n))

Mathlib's finsum homology Euler characteristic of a bounded complex of finite-dimensional vector spaces is the honest finite sum of the dimensions of its homology objects. The homology on the right is computed in FGModuleCat k; exactness of the forgetful functor identifies it with the homology used on the left.

theorem HomologicalComplex.eulerChar_forgetFG_eq_homologyEulerChar {k : Type u} [DivisionRing k] (K : CochainComplex (FGModuleCat k) ℤ) (a b : ℤ) [K.IsStrictlyGE a] [K.IsStrictlyLE b] : (((CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k)).mapHomologicalComplex (ComplexShape.up ℤ)).obj K).eulerChar = (((CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k)).mapHomologicalComplex (ComplexShape.up ℤ)).obj K).homologyEulerChar

Euler--Poincaré for a bounded finite-dimensional cochain complex. Mathlib's Euler characteristic of the terms agrees with its homology Euler characteristic after forgetting a bounded complex from FGModuleCat k to ModuleCat k.

The source category makes every term finite-dimensional, while the explicit bounds make both finsums finite. Consequently this equality does not rely on either totalized junk value.