Euler--Poincaré for complexes of finitely generated modules

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 is the natural-number conversion of Module.rank, so it returns zero for modules of infinite rank. This file identifies those totalized definitions with honest finite sums for bounded cochain complexes of finitely generated modules, and proves that the term and homology Euler characteristics agree.

The coefficient ring R is Noetherian and satisfies the rank-nullity theorem (HasRankNullity). This covers division rings, where finrank is dimension, and Noetherian commutative domains such as ℤ, where finrank is the rank of the free part of a finitely generated abelian group, so that torsion in the terms or in the homology contributes nothing. Noetherianity keeps the homology finitely generated, and rank-nullity makes finrank additive on short exact sequences.

Finite generation is encoded either by taking the original complex in FGModuleCat R, with the characteristics evaluated after applying the forgetful functor to ModuleCat R as required by Mathlib's definitions, or by an explicit hypothesis on the terms of a complex in ModuleCat R. Finite generation ensures that every term and every homology object has finite rank, without requiring freeness, and 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 finranks in FGModuleCat R.
• HomologicalComplex.eulerChar_forgetFG_eq_homologyEulerChar: the Euler--Poincaré identity for a bounded complex in FGModuleCat R, in Mathlib's Euler-characteristic API.
• CochainComplex.eulerChar_eq_homologyEulerChar: the same identity for a bounded complex in ModuleCat R whose terms are finitely generated.

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 {R : Type u} [Ring R] [Nontrivial R] (K : CochainComplex (FGModuleCat R) ℤ) (a b : ℤ) [K.IsStrictlyGE a] [K.IsStrictlyLE b] {s : Finset ℤ} (hs : Finset.Icc a b ⊆ s) : (((CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R)).mapHomologicalComplex (ComplexShape.up ℤ)).obj K).eulerChar = ∑ n ∈ s, ↑n.negOnePow * ↑(Module.finrank R ↑(K.X n))

Mathlib's finsum Euler characteristic of a bounded complex of finitely generated modules is the honest finite sum of its term finranks over any finite set containing the bounding interval Finset.Icc a b.

@[simp]

theorem HomologicalComplex.finrank_homology_forget {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (FGModuleCat R) c) (i : ι) : Module.finrank R ↑((((CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R)).mapHomologicalComplex c).obj K).homology i) = Module.finrank R ↑(K.homology i)

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

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

Mathlib's finsum homology Euler characteristic of a bounded complex of finitely generated modules is the honest finite sum of the finranks of its homology objects. The homology on the right is computed in FGModuleCat R; exactness of the forgetful functor identifies it with the homology used on the left.

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

Euler--Poincaré for a bounded cochain complex of finitely generated modules. Over a Noetherian ring with the rank-nullity property, Mathlib's Euler characteristic of the terms agrees with its homology Euler characteristic after forgetting a bounded complex from FGModuleCat R to ModuleCat R.

The source category makes every term and homology object finitely generated, hence of finite rank, while the explicit bounds make both finsums finite. Consequently this equality does not rely on either totalized junk value.

theorem CochainComplex.eulerChar_eq_homologyEulerChar {R : Type u} [Ring R] [IsNoetherianRing R] [HasRankNullity.{v, u} R] (K : CochainComplex (ModuleCat R) ℤ) (hK : ∀ (n : ℤ), Module.Finite R ↑(K.X n)) (a b : ℤ) [K.IsStrictlyGE a] [K.IsStrictlyLE b] : HomologicalComplex.eulerChar K = HomologicalComplex.homologyEulerChar K

Euler--Poincaré for a bounded cochain complex of finitely generated modules. Over a Noetherian ring with the rank-nullity property, such as ℤ, a strictly bounded cochain complex in ModuleCat R whose terms are finitely generated has the same Euler characteristic as its homology.