The Euler characteristic of a bounded complex in abelian and exact K₀

For a cochain complex K over an abelian category A and an invariant v additive on short exact sequences, the alternating sum

∑ n ∈ s, (-1)ⁿ v(Kⁿ)

over a finite set s of degrees is the Euler characteristic of K relative to v. This file proves the Euler–Poincaré theorem: as soon as K is bounded and s contains every degree where K lives, this alternating sum equals the alternating sum formed from the cohomology objects of K. The argument is carried out for an arbitrary additive invariant, so it needs no smallness hypothesis on A; specializing it to the tautological invariant X ↦ [X] gives the statement in TauCeti.AbelianK0 A, which is the form the rest of the theory consumes.

The finiteness is carried by data, not inferred: the summation range is an explicit Finset ℤ. Nothing here is a finsum, so every value is a truncation to an explicitly given finite range of degrees, and what boundedness buys is that all large enough ranges give the same answer.

Which boundedness is needed depends on what is being summed. The alternating class of the terms, and with it Euler–Poincaré, needs the terms to vanish outside a finite range, which is Mathlib's CochainComplex.IsStrictlyGE/CochainComplex.IsStrictlyLE. The alternating class of the cohomology needs only the cohomology to vanish there, which is IsGE/IsLE; so a complex whose terms are nonzero in every degree, such as an unbounded resolution, still has a range-independent homologyEulerChar, while having no canonical eulerChar. A complex outside both regimes is assigned no canonical value rather than a junk one. The comparison with the totalized HomologicalComplex.eulerChar of Mathlib is left to the finite-dimensionality layer that gives it a ℤ-valued additive invariant.

The same comparison holds in the exact K₀ of an extension-closed full subcategory P of A, with its induced exact structure, under explicit closure hypotheses on the complex: the boundaries im dⁿ and the cohomology objects of K must lie in P. The cocycles are then extensions of the cohomology by the boundaries, and the terms extensions of the boundaries by the cocycles, so both lie in P too, and every short exact sequence used by the argument is a conflation of the subcategory. The statement is at the level of the complex: no derived category of the subcategory is formed. Both theorems run on one telescoping engine, HomologicalComplex.sum_negOnePow_X_eq_sum_negOnePow_homology, which needs of a function on objects only that it vanishes on zero objects and satisfies the degreewise homology relation.

Main definitions

• TauCeti.AbelianK0.eulerChar: the alternating class ∑ n ∈ s, (-1)ⁿ [Kⁿ] of the terms of a cochain complex over a finite set of degrees.
• TauCeti.AbelianK0.homologyEulerChar: the same alternating class formed from the cohomology objects.

Main results

• HomologicalComplex.sum_negOnePow_X_eq_sum_negOnePow_homology: the telescoping argument for any function on objects satisfying the degreewise homology relation.
• TauCeti.AbelianK0.AdditiveInvariant.obj_kernel_add_obj_kernel: for a short complex S in an abelian category, v(ker S.g) + v(ker S.f) = v(S.homology) + v(S.X₁). This is the single relation from which the telescoping argument runs.
• TauCeti.AbelianK0.AdditiveInvariant.sum_negOnePow_obj_X_eq_sum_negOnePow_obj_homology: Euler–Poincaré. A bounded complex has the same Euler characteristic computed from its terms and from its cohomology, for every invariant additive on short exact sequences.
• TauCeti.AbelianK0.of_kernel_add_of_kernel and TauCeti.AbelianK0.eulerChar_eq_homologyEulerChar: the two statements above in abelian K₀.
• TauCeti.AbelianK0.homologyEulerChar_eq_homologyEulerChar: the alternating class of the cohomology does not depend on the summation range as soon as the cohomology is bounded; the terms of the complex need not be.
• TauCeti.AbelianK0.eulerChar_eq_of_quasiIso: the Euler characteristic of a bounded complex depends only on its image in the derived category.
• TauCeti.ExactStructure.IsExtensionClosed.prop_kernel_d and TauCeti.ExactStructure.IsExtensionClosed.prop_X: if the boundaries and the cohomology of a complex lie in an extension-closed property, then so do its cocycles and its terms.
• TauCeti.ExactK0.AdditiveInvariant.sum_negOnePow_obj_X_eq_sum_negOnePow_obj_homology and TauCeti.ExactK0.sum_negOnePow_of_X_eq_sum_negOnePow_of_homology: Euler–Poincaré in an extension-closed subcategory, for an additive invariant of the subcategory and in its exact K₀.

References

• Charles A. Weibel, An Introduction to Homological Algebra, Sections 1.3 and 1.6, for the cycles/boundaries bookkeeping behind the Euler–Poincaré formula.
• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Proposition 6.6, for the K₀-valued form of the alternating sum used here, and Proposition 7.5, for the Euler characteristic in an exact subcategory of an abelian category and its closure hypotheses.

theorem HomologicalComplex.sum_negOnePow_X_eq_sum_negOnePow_homology {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {G : Type u_1} [AddCommGroup G] (K : CochainComplex A ℤ) {w : A → G} (hzero : ∀ (X : A), CategoryTheory.Limits.IsZero X → w X = 0) (hrel : ∀ (i j k : ℤ), i + 1 = j → j + 1 = k → w (CategoryTheory.Limits.kernel (K.d j k)) + w (CategoryTheory.Limits.kernel (K.d i j)) = w (homology K j) + w (K.X i)) (a b : ℤ) [K.IsStrictlyGE a] [K.IsStrictlyLE b] {s : Finset ℤ} (hs : Finset.Icc a b ⊆ s) : ∑ n ∈ s, ↑n.negOnePow • w (K.X n) = ∑ n ∈ s, ↑n.negOnePow • w (homology K n)

The Euler–Poincaré telescoping. Let w be a function on the objects of an abelian category which vanishes on zero objects and satisfies, in every degree j of a cochain complex K, the homology relation w(ker dʲ) + w(ker dⁱ) = w(Hʲ K) + w(Kⁱ) for i + 1 = j. If K is strictly supported in degrees a to b, then over any finite range of degrees containing [a, b] the alternating sum of the values of w on the terms equals the alternating sum of its values on the cohomology objects.

This is the common engine of the Euler–Poincaré theorems: the homology relation holds for an invariant additive on all short exact sequences, and also for an invariant of an extension-closed subcategory when the boundaries and cohomology of K lie in that subcategory.

theorem TauCeti.AbelianK0.AdditiveInvariant.obj_kernel_add_obj_kernel {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {G : Type u_1} [AddCommGroup G] (v : AdditiveInvariant A G) (S : CategoryTheory.ShortComplex A) : v.obj (CategoryTheory.Limits.kernel S.g) + v.obj (CategoryTheory.Limits.kernel S.f) = v.obj S.homology + v.obj S.X₁

The homology relation for an additive invariant. For a short complex S = (X₁ ⟶ X₂ ⟶ X₃) in an abelian category and an invariant v additive on short exact sequences, v(ker S.g) + v(ker S.f) = v(S.homology) + v(S.X₁).

Both sides count the boundaries im S.f once: the kernel of S.g is an extension of the homology by them, and X₁ is an extension of them by the kernel of S.f.

theorem TauCeti.AbelianK0.AdditiveInvariant.obj_kernel_d_add_obj_kernel_d {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {G : Type u_1} [AddCommGroup G] (v : AdditiveInvariant A G) (K : CochainComplex A ℤ) (i j k : ℤ) (hij : i + 1 = j) (hjk : j + 1 = k) : v.obj (CategoryTheory.Limits.kernel (K.d j k)) + v.obj (CategoryTheory.Limits.kernel (K.d i j)) = v.obj (HomologicalComplex.homology K j) + v.obj (K.X i)

The degreewise homology relation for a cochain complex. For consecutive degrees i + 1 = j and j + 1 = k, the values of an additive invariant on the two cocycle objects around degree j differ from its value on the cohomology at j by its value on the term in degree i.

theorem TauCeti.AbelianK0.AdditiveInvariant.obj_kernel_d_eq_obj_homology {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {G : Type u_1} [AddCommGroup G] (v : AdditiveInvariant A G) (K : CochainComplex A ℤ) (a : ℤ) [K.IsStrictlyGE a] : v.obj (CategoryTheory.Limits.kernel (K.d a (a + 1))) = v.obj (HomologicalComplex.homology K a)

In the lowest degree where a bounded-below complex lives, the cocycles are the cohomology, because there are no coboundaries.

theorem TauCeti.AbelianK0.AdditiveInvariant.sum_negOnePow_obj_X_eq_sum_negOnePow_obj_homology {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {G : Type u_1} [AddCommGroup G] (v : AdditiveInvariant A G) (K : CochainComplex A ℤ) (a b : ℤ) [K.IsStrictlyGE a] [K.IsStrictlyLE b] {s : Finset ℤ} (hs : Finset.Icc a b ⊆ s) : ∑ n ∈ s, ↑n.negOnePow • v.obj (K.X n) = ∑ n ∈ s, ↑n.negOnePow • v.obj (HomologicalComplex.homology K n)

The Euler–Poincaré theorem for an additive invariant. For a cochain complex that is strictly supported in degrees a to b, any finite range of degrees containing [a, b], and any invariant additive on short exact sequences, the alternating sum of the values on the terms equals the alternating sum of the values on the cohomology objects.

theorem TauCeti.AbelianK0.of_kernel_add_of_kernel {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] (S : CategoryTheory.ShortComplex A) : of (CategoryTheory.Limits.kernel S.g) + of (CategoryTheory.Limits.kernel S.f) = of S.homology + of S.X₁

The homology relation in abelian K₀. For a short complex S = (X₁ ⟶ X₂ ⟶ X₃) in an abelian category, [ker S.g] + [ker S.f] = [S.homology] + [S.X₁].

noncomputable def TauCeti.AbelianK0.eulerChar {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] (K : CochainComplex A ℤ) (s : Finset ℤ) : AbelianK0 A

The alternating class ∑ n ∈ s, (-1)ⁿ [Kⁿ] of the terms of a cochain complex over a finite set s of degrees. The set of degrees is data: the value is the truncation of the alternating sum to s, and TauCeti.AbelianK0.eulerChar_eq_eulerChar shows that it stops depending on s once s contains the support of a bounded complex.

Equations

• TauCeti.AbelianK0.eulerChar K s = ∑ n ∈ s, ↑n.negOnePow • TauCeti.AbelianK0.of (K.X n)

noncomputable def TauCeti.AbelianK0.homologyEulerChar {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] (K : CochainComplex A ℤ) (s : Finset ℤ) : AbelianK0 A

The alternating class ∑ n ∈ s, (-1)ⁿ [Hⁿ K] of the cohomology of a cochain complex over a finite set s of degrees.

Equations

• TauCeti.AbelianK0.homologyEulerChar K s = ∑ n ∈ s, ↑n.negOnePow • TauCeti.AbelianK0.of (HomologicalComplex.homology K n)

@[simp]

theorem TauCeti.AbelianK0.eulerChar_empty {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] (K : CochainComplex A ℤ) : eulerChar K ∅ = 0

@[simp]

theorem TauCeti.AbelianK0.homologyEulerChar_empty {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] (K : CochainComplex A ℤ) : homologyEulerChar K ∅ = 0

@[simp]

theorem TauCeti.AbelianK0.eulerChar_insert {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] (K : CochainComplex A ℤ) {s : Finset ℤ} {n : ℤ} (hn : n ∉ s) : eulerChar K (insert n s) = ↑n.negOnePow • of (K.X n) + eulerChar K s

@[simp]

theorem TauCeti.AbelianK0.homologyEulerChar_insert {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] (K : CochainComplex A ℤ) {s : Finset ℤ} {n : ℤ} (hn : n ∉ s) : homologyEulerChar K (insert n s) = ↑n.negOnePow • of (HomologicalComplex.homology K n) + homologyEulerChar K s

theorem TauCeti.AbelianK0.homologyEulerChar_eq_homologyEulerChar_Icc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] (K : CochainComplex A ℤ) (a b : ℤ) [K.IsGE a] [K.IsLE b] {s : Finset ℤ} (hs : Finset.Icc a b ⊆ s) : homologyEulerChar K s = homologyEulerChar K (Finset.Icc a b)

Enlarging the range of degrees beyond the support of the cohomology does not change the alternating class of that cohomology.

Only the cohomology has to be bounded: K.IsGE a and K.IsLE b say that the cohomology of K vanishes outside [a, b]. The terms K.X n may be nonzero in every degree, as they are for an unbounded resolution.

theorem TauCeti.AbelianK0.homologyEulerChar_eq_homologyEulerChar {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] (K : CochainComplex A ℤ) (a b : ℤ) [K.IsGE a] [K.IsLE b] {s t : Finset ℤ} (hs : Finset.Icc a b ⊆ s) (ht : Finset.Icc a b ⊆ t) : homologyEulerChar K s = homologyEulerChar K t

The alternating class of the cohomology of a complex with bounded cohomology does not depend on the finite range of degrees over which it is summed.

theorem TauCeti.AbelianK0.eulerChar_eq_eulerChar_Icc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] (K : CochainComplex A ℤ) (a b : ℤ) [K.IsStrictlyGE a] [K.IsStrictlyLE b] {s : Finset ℤ} (hs : Finset.Icc a b ⊆ s) : eulerChar K s = eulerChar K (Finset.Icc a b)

Enlarging the range of degrees beyond the support of a bounded complex does not change its Euler characteristic.

theorem TauCeti.AbelianK0.eulerChar_eq_eulerChar {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] (K : CochainComplex A ℤ) (a b : ℤ) [K.IsStrictlyGE a] [K.IsStrictlyLE b] {s t : Finset ℤ} (hs : Finset.Icc a b ⊆ s) (ht : Finset.Icc a b ⊆ t) : eulerChar K s = eulerChar K t

The Euler characteristic of a bounded complex does not depend on the finite range of degrees over which it is summed, as long as that range contains the support.

theorem TauCeti.AbelianK0.eulerChar_eq_homologyEulerChar {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] (K : CochainComplex A ℤ) (a b : ℤ) [K.IsStrictlyGE a] [K.IsStrictlyLE b] {s : Finset ℤ} (hs : Finset.Icc a b ⊆ s) : eulerChar K s = homologyEulerChar K s

The Euler–Poincaré theorem in abelian K₀. For a cochain complex that is strictly supported in degrees a to b, and any finite range of degrees containing [a, b], the alternating sum of the classes of the terms equals the alternating sum of the classes of the cohomology objects.

theorem TauCeti.AbelianK0.eulerChar_eq_zero_of_exactAt {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] (K : CochainComplex A ℤ) (a b : ℤ) [K.IsStrictlyGE a] [K.IsStrictlyLE b] (hK : ∀ (n : ℤ), HomologicalComplex.ExactAt K n) {s : Finset ℤ} (hs : Finset.Icc a b ⊆ s) : eulerChar K s = 0

A bounded exact complex has vanishing Euler characteristic.

theorem TauCeti.AbelianK0.homologyEulerChar_eq_of_quasiIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] {K L : CochainComplex A ℤ} (f : K ⟶ L) [QuasiIso f] (s : Finset ℤ) : homologyEulerChar K s = homologyEulerChar L s

A quasi-isomorphism preserves the alternating class of the cohomology, in any range of degrees.

theorem TauCeti.AbelianK0.eulerChar_eq_of_quasiIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] {K L : CochainComplex A ℤ} (f : K ⟶ L) [QuasiIso f] (aK bK aL bL : ℤ) [K.IsStrictlyGE aK] [K.IsStrictlyLE bK] [L.IsStrictlyGE aL] [L.IsStrictlyLE bL] {s : Finset ℤ} (hK : Finset.Icc aK bK ⊆ s) (hL : Finset.Icc aL bL ⊆ s) : eulerChar K s = eulerChar L s

The Euler characteristic is a quasi-isomorphism invariant. Two bounded complexes joined by a quasi-isomorphism have the same alternating class of terms, over any finite range of degrees containing both supports; this is what makes the Euler characteristic a function of the image of the complex in the derived category.

theorem TauCeti.ExactStructure.IsExtensionClosed.prop_kernel_d {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {P : CategoryTheory.ObjectProperty A} [P.ContainsZero] (hP : (abelian A).IsExtensionClosed P) {K : CochainComplex A ℤ} (hB : ∀ (n : ℤ), P (CategoryTheory.Abelian.image (K.d n (n + 1)))) (hH : ∀ (n : ℤ), P (HomologicalComplex.homology K n)) (n : ℤ) : P (CategoryTheory.Limits.kernel (K.d n (n + 1)))

If the boundaries im dⁿ and the cohomology objects of a cochain complex lie in an extension-closed property, then so do its cocycles ker dⁿ, which are extensions of the cohomology by the boundaries.

theorem TauCeti.ExactStructure.IsExtensionClosed.prop_X {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {P : CategoryTheory.ObjectProperty A} [P.ContainsZero] (hP : (abelian A).IsExtensionClosed P) {K : CochainComplex A ℤ} (hB : ∀ (n : ℤ), P (CategoryTheory.Abelian.image (K.d n (n + 1)))) (hH : ∀ (n : ℤ), P (HomologicalComplex.homology K n)) (n : ℤ) : P (K.X n)

If the boundaries im dⁿ and the cohomology objects of a cochain complex lie in an extension-closed property, then so do its terms: Kⁿ is an extension of the boundaries im dⁿ by the cocycles ker dⁿ.

theorem TauCeti.ExactK0.AdditiveInvariant.sum_negOnePow_obj_X_eq_sum_negOnePow_obj_homology {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {P : CategoryTheory.ObjectProperty A} [P.ContainsZero] [P.IsClosedUnderBinaryProducts] {hP : (ExactStructure.abelian A).IsExtensionClosed P} {G : Type u_1} [AddCommGroup G] (v : AdditiveInvariant (ExactStructure.fullSubcategory P hP) G) {K : CochainComplex A ℤ} (hB : ∀ (n : ℤ), P (CategoryTheory.Abelian.image (K.d n (n + 1)))) (hH : ∀ (n : ℤ), P (HomologicalComplex.homology K n)) (a b : ℤ) [K.IsStrictlyGE a] [K.IsStrictlyLE b] {s : Finset ℤ} (hs : Finset.Icc a b ⊆ s) : ∑ n ∈ s, ↑n.negOnePow • v.obj { obj := K.X n, property := ⋯ } = ∑ n ∈ s, ↑n.negOnePow • v.obj { obj := HomologicalComplex.homology K n, property := ⋯ }

The Euler–Poincaré theorem in an extension-closed subcategory. Let P be an extension-closed full subcategory of an abelian category A with its induced exact structure, and let K be a cochain complex strictly supported in degrees a to b whose boundaries im dⁿ and cohomology objects lie in P; its cocycles and terms then lie in P as well (TauCeti.ExactStructure.IsExtensionClosed.prop_X). For any invariant of the subcategory additive on its conflations and any finite range of degrees containing [a, b], the alternating sum of the values on the terms equals the alternating sum of the values on the cohomology objects.

theorem TauCeti.ExactK0.sum_negOnePow_of_X_eq_sum_negOnePow_of_homology {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {P : CategoryTheory.ObjectProperty A} [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian A).IsExtensionClosed P) [CategoryTheory.EssentiallySmall.{w, v, u} P.FullSubcategory] (K : CochainComplex A ℤ) (hB : ∀ (n : ℤ), P (CategoryTheory.Abelian.image (K.d n (n + 1)))) (hH : ∀ (n : ℤ), P (HomologicalComplex.homology K n)) (a b : ℤ) [K.IsStrictlyGE a] [K.IsStrictlyLE b] {s : Finset ℤ} (hs : Finset.Icc a b ⊆ s) : ∑ n ∈ s, ↑n.negOnePow • of { obj := K.X n, property := ⋯ } = ∑ n ∈ s, ↑n.negOnePow • of { obj := HomologicalComplex.homology K n, property := ⋯ }

The Euler–Poincaré theorem in exact K₀ of an extension-closed subcategory. Let P be an extension-closed full subcategory of an abelian category A, with its induced exact structure, and let K be a cochain complex strictly supported in degrees a to b whose boundaries im dⁿ and cohomology objects lie in P, so that its terms do too. Then over any finite range of degrees containing [a, b],

∑ n, (-1)ⁿ [Kⁿ] = ∑ n, (-1)ⁿ [Hⁿ K]

in the exact K₀ of the subcategory. This is the analogue of TauCeti.AbelianK0.eulerChar_eq_homologyEulerChar for the subcategory; the comparison stays at the level of the complex, and no derived category of the subcategory is involved.