The Euler characteristic of a bounded complex in split K₀

For a cochain complex K over an additive category C and a biproduct-additive invariant v, the alternating sum

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

over a finite set s of degrees is the Euler characteristic of K relative to v. When v is the class map of split K₀, this is TauCeti.SplitK0.eulerChar K s. As in the abelian case (TauCeti.AbelianK0.eulerChar), the summation range is data: no finsum is used, and what boundedness buys is that every range containing the support of K gives the same value.

The main theorem is homotopy invariance: the Euler characteristic of a bounded complex depends only on its homotopy type. Its heart is the vanishing on contractible complexes, which is the statement that the even and the odd parts of a contractible bounded complex are isomorphic (Homotopy.biproductEvenIsoBiproductOdd). Homotopy invariance follows from it through the mapping cone: the cone of a homotopy equivalence is contractible, and its terms are the biproducts Kⁿ⁺¹ ⊞ Lⁿ, so its Euler characteristic is χ(L) - χ(K).

These are the ingredients of the standard comparison between split K₀ of an additive category and the triangulated K₀ of its bounded homotopy category, which sends a bounded complex to the alternating sum of the classes of its terms: homotopy invariance makes that assignment well defined on the objects of the homotopy category, and the mapping-cone formula makes it additive on distinguished triangles. The comparison itself is proved in TauCeti.CategoryTheory.GrothendieckGroup.BoundedHomotopy.

Main definitions

• TauCeti.SplitK0.eulerChar: the alternating class ∑ n ∈ s, (-1)ⁿ [Kⁿ] in split K₀ of the terms of a cochain complex over a finite set of degrees.

Main results

• TauCeti.SplitK0.AdditiveInvariant.sum_negOnePow_obj_X_eq_zero_of_homotopy_id_zero and TauCeti.SplitK0.eulerChar_eq_zero_of_homotopy_id_zero: a contractible complex supported on s has vanishing Euler characteristic over s.
• TauCeti.SplitK0.AdditiveInvariant.sum_negOnePow_obj_X_eq_of_homotopyEquiv and TauCeti.SplitK0.eulerChar_eq_of_homotopyEquiv: homotopy invariance of the Euler characteristic of bounded complexes.
• TauCeti.SplitK0.eulerChar_mappingCone and TauCeti.SplitK0.eulerChar_shift: the Euler characteristic of a mapping cone is χ(L) - χ(K), and that of the shift K⟦1⟧ is -χ(K).
• TauCeti.SplitK0.eulerChar_eq_eulerChar: independence of the summation range for a bounded complex.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Exercise 9.15, for the comparison of K₀ of an additive category with K₀ of its bounded homotopy category through the alternating sum of the terms.

theorem TauCeti.SplitK0.AdditiveInvariant.sum_negOnePow_obj_X_eq_of_isZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {G : Type u_1} [AddCommGroup G] (v : AdditiveInvariant C G) (K : CochainComplex C ℤ) {s t : Finset ℤ} (hs : ∀ n ∉ s, CategoryTheory.Limits.IsZero (K.X n)) (ht : ∀ n ∉ t, CategoryTheory.Limits.IsZero (K.X n)) : ∑ n ∈ s, ↑n.negOnePow • v.obj (K.X n) = ∑ n ∈ t, ↑n.negOnePow • v.obj (K.X n)

Two finite sets of degrees both containing the support of a complex give the same alternating sum of the values of an additive invariant on its terms.

theorem TauCeti.SplitK0.AdditiveInvariant.sum_negOnePow_obj_X_shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {G : Type u_1} [AddCommGroup G] (v : AdditiveInvariant C G) (K : CochainComplex C ℤ) (s : Finset ℤ) : ∑ n ∈ s, ↑n.negOnePow • v.obj (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj K).X n) = -∑ n ∈ Finset.map (Equiv.toEmbedding (Equiv.addRight 1)) s, ↑n.negOnePow • v.obj (K.X n)

The Euler characteristic of the shift K⟦1⟧ over s is minus the Euler characteristic of K over the translate s + 1.

theorem TauCeti.SplitK0.AdditiveInvariant.sum_negOnePow_obj_X_mappingCone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {G : Type u_1} [AddCommGroup G] (v : AdditiveInvariant C G) {K L : CochainComplex C ℤ} (f : K ⟶ L) (s : Finset ℤ) : ∑ n ∈ s, ↑n.negOnePow • v.obj ((CochainComplex.mappingCone f).X n) = ∑ n ∈ s, ↑n.negOnePow • v.obj (L.X n) - ∑ n ∈ Finset.map (Equiv.toEmbedding (Equiv.addRight 1)) s, ↑n.negOnePow • v.obj (K.X n)

The Euler characteristic of a mapping cone: over any finite set s of degrees, it is the Euler characteristic of the target over s minus that of the source over the translate s + 1, the terms of the cone being the biproducts Kⁿ⁺¹ ⊞ Lⁿ.

theorem TauCeti.SplitK0.AdditiveInvariant.sum_negOnePow_obj_X_eq_zero_of_homotopy_id_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {G : Type u_1} [AddCommGroup G] (v : AdditiveInvariant C G) {K : CochainComplex C ℤ} [CategoryTheory.Limits.HasZeroObject C] (h : Homotopy (CategoryTheory.CategoryStruct.id K) 0) {s : Finset ℤ} (hs : ∀ n ∉ s, CategoryTheory.Limits.IsZero (K.X n)) : ∑ n ∈ s, ↑n.negOnePow • v.obj (K.X n) = 0

A contractible complex has vanishing Euler characteristic. If the identity of K is null-homotopic and the terms of K vanish outside the finite set s of degrees, then the alternating sum over s of the values of a biproduct-additive invariant on the terms of K is zero.

theorem TauCeti.SplitK0.AdditiveInvariant.sum_negOnePow_obj_X_eq_of_homotopyEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {G : Type u_1} [AddCommGroup G] (v : AdditiveInvariant C G) {K L : CochainComplex C ℤ} [CategoryTheory.Limits.HasZeroObject C] (e : HomotopyEquiv K L) {s t : Finset ℤ} (hs : ∀ n ∉ s, CategoryTheory.Limits.IsZero (K.X n)) (ht : ∀ n ∉ t, CategoryTheory.Limits.IsZero (L.X n)) : ∑ n ∈ s, ↑n.negOnePow • v.obj (K.X n) = ∑ n ∈ t, ↑n.negOnePow • v.obj (L.X n)

Homotopy invariance of the Euler characteristic. Homotopy equivalent complexes supported on finite sets of degrees have the same Euler characteristic relative to every biproduct-additive invariant.

noncomputable def TauCeti.SplitK0.eulerChar {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (K : CochainComplex C ℤ) (s : Finset ℤ) : SplitK0 C

The alternating class ∑ n ∈ s, (-1)ⁿ [Kⁿ] in split 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.SplitK0.eulerChar_eq_eulerChar shows that it stops depending on s once s contains the support of a bounded complex.

Equations

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

theorem TauCeti.SplitK0.eulerChar_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (K : CochainComplex C ℤ) (s : Finset ℤ) : eulerChar K s = ∑ n ∈ s, ↑n.negOnePow • of (K.X n)

The Euler characteristic is the alternating sum of the classes of the terms.

@[simp]

theorem TauCeti.SplitK0.eulerChar_empty {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (K : CochainComplex C ℤ) : eulerChar K ∅ = 0

@[simp]

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

theorem TauCeti.SplitK0.eulerChar_eq_eulerChar_of_isZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (K : CochainComplex C ℤ) {s t : Finset ℤ} (hs : ∀ n ∉ s, CategoryTheory.Limits.IsZero (K.X n)) (ht : ∀ n ∉ t, CategoryTheory.Limits.IsZero (K.X n)) : eulerChar K s = eulerChar K t

The Euler characteristic of a 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.SplitK0.eulerChar_eq_eulerChar {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (K : CochainComplex C ℤ) (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 bounding interval.

theorem TauCeti.SplitK0.eulerChar_shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (K : CochainComplex C ℤ) (s : Finset ℤ) : eulerChar ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj K) s = -eulerChar K (Finset.map (Equiv.toEmbedding (Equiv.addRight 1)) s)

The Euler characteristic of the shift K⟦1⟧ over s is minus the Euler characteristic of K over the translate s + 1.

theorem TauCeti.SplitK0.eulerChar_mappingCone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (s : Finset ℤ) : eulerChar (CochainComplex.mappingCone f) s = eulerChar L s - eulerChar K (Finset.map (Equiv.toEmbedding (Equiv.addRight 1)) s)

The Euler characteristic of a mapping cone is the Euler characteristic of the target minus that of the source over the translated range: χ(cone f) = χ(L) - χ(K).

theorem TauCeti.SplitK0.eulerChar_mappingCone_of_isZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {K L : CochainComplex C ℤ} (f : K ⟶ L) {s t u : Finset ℤ} (hs : ∀ n ∉ s, CategoryTheory.Limits.IsZero (K.X n)) (ht : ∀ n ∉ t, CategoryTheory.Limits.IsZero (L.X n)) (hu : ∀ n ∉ u, CategoryTheory.Limits.IsZero ((CochainComplex.mappingCone f).X n)) : eulerChar (CochainComplex.mappingCone f) u = eulerChar L t - eulerChar K s

The Euler characteristic of a mapping cone, for complexes supported on finite sets of degrees: χ(cone f) = χ(L) - χ(K), each summed over a finite set of degrees containing its support.

theorem TauCeti.SplitK0.eulerChar_eq_zero_of_homotopy_id_zero_of_isZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {K : CochainComplex C ℤ} [CategoryTheory.Limits.HasZeroObject C] (h : Homotopy (CategoryTheory.CategoryStruct.id K) 0) {s : Finset ℤ} (hs : ∀ n ∉ s, CategoryTheory.Limits.IsZero (K.X n)) : eulerChar K s = 0

A contractible complex has vanishing Euler characteristic, over any finite set of degrees containing its support.

theorem TauCeti.SplitK0.eulerChar_eq_zero_of_homotopy_id_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {K : CochainComplex C ℤ} [CategoryTheory.Limits.HasZeroObject C] (h : Homotopy (CategoryTheory.CategoryStruct.id K) 0) (a b : ℤ) [K.IsStrictlyGE a] [K.IsStrictlyLE b] {s : Finset ℤ} (hs : Finset.Icc a b ⊆ s) : eulerChar K s = 0

A contractible bounded complex has vanishing Euler characteristic.

theorem TauCeti.SplitK0.eulerChar_eq_of_homotopyEquiv_of_isZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {K L : CochainComplex C ℤ} [CategoryTheory.Limits.HasZeroObject C] (e : HomotopyEquiv K L) {s t : Finset ℤ} (hs : ∀ n ∉ s, CategoryTheory.Limits.IsZero (K.X n)) (ht : ∀ n ∉ t, CategoryTheory.Limits.IsZero (L.X n)) : eulerChar K s = eulerChar L t

Homotopy invariance of the Euler characteristic, for complexes supported on finite sets of degrees.

theorem TauCeti.SplitK0.eulerChar_eq_of_homotopyEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {K L : CochainComplex C ℤ} [CategoryTheory.Limits.HasZeroObject C] (e : HomotopyEquiv K L) (a b a' b' : ℤ) [K.IsStrictlyGE a] [K.IsStrictlyLE b] [L.IsStrictlyGE a'] [L.IsStrictlyLE b'] {s t : Finset ℤ} (hs : Finset.Icc a b ⊆ s) (ht : Finset.Icc a' b' ⊆ t) : eulerChar K s = eulerChar L t

Homotopy invariance of the Euler characteristic of bounded complexes. Homotopy equivalent bounded complexes have the same Euler characteristic in split K₀, over any finite ranges of degrees containing their respective bounding intervals.