Split K₀ and the bounded homotopy category

This file proves the standard comparison between split K₀ of an additive category and the triangulated K₀ of its bounded homotopy category. The Euler characteristic of a representing complex (TauCeti.SplitK0.eulerChar) is well defined on the objects of the homotopy category by homotopy invariance, and additive on distinguished triangles by the mapping-cone formula, so it induces a homomorphism out of triangulated K₀. It is inverse to the map placing an object in degree zero: splitting off the top term of a bounded complex is a degreewise split short exact sequence, hence a distinguished triangle, and induction on the length of the complex shows that the class of a bounded complex is the alternating sum of the classes of its terms.

Main definitions

• TauCeti.SplitK0.boundedHomotopyEquiv: the isomorphism between split K₀ of an additive category and triangulated K₀ of its bounded homotopy category.

Main results

• TauCeti.TriangulatedK0.of_bounded_quotient_obj: in triangulated K₀ of the bounded homotopy category, the class of a bounded complex is the alternating sum of the classes of its terms placed in degree zero; TauCeti.TriangulatedK0.of_boundedSingleFunctor_obj computes the class of an object placed in degree n as (-1)ⁿ times its class in degree zero.
• TauCeti.SplitK0.boundedHomotopyEquiv_symm_of_quotient_obj: the inverse comparison is the Euler characteristic.

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.TriangulatedK0.of_boundedSingleFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (n : ℤ) (X : C) : of ((HomotopyCategory.Bounded.singleFunctor C n).obj X) = ↑n.negOnePow • of ((HomotopyCategory.Bounded.singleFunctor C 0).obj X)

In triangulated K₀ of the bounded homotopy category, an object placed in degree n has the class of the same object placed in degree zero, multiplied by the sign (-1)ⁿ.

theorem TauCeti.TriangulatedK0.of_bounded_quotient_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (K : CochainComplex.Bounded C) {s : Finset ℤ} (hs : ∀ n ∉ s, CategoryTheory.Limits.IsZero (K.obj.X n)) : of ((HomotopyCategory.Bounded.quotient C).obj K) = ∑ n ∈ s, ↑n.negOnePow • of ((HomotopyCategory.Bounded.singleFunctor C 0).obj (K.obj.X n))

The class of a bounded complex in triangulated K₀ of the bounded homotopy category is the alternating sum of the classes of its terms, each placed in degree zero. The sum runs over any finite set of degrees outside which the complex vanishes.

noncomputable def TauCeti.SplitK0.boundedHomotopyEquiv (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : SplitK0 C ≃+ TriangulatedK0 (HomotopyCategory.Bounded C)

Split K₀ of an additive category is triangulated K₀ of its bounded homotopy category. The class of an object goes to the class of that object placed in degree zero, and in the inverse direction the class of a bounded complex goes to its Euler characteristic, the alternating sum of the classes of its terms.

Equations

• TauCeti.SplitK0.boundedHomotopyEquiv C = (TauCeti.SplitK0.toBoundedHomotopy✝ C).toAddEquiv (TauCeti.TriangulatedK0.lift (TauCeti.SplitK0.boundedHomotopyEulerChar✝ C)) ⋯ ⋯

@[simp]

theorem TauCeti.SplitK0.boundedHomotopyEquiv_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (X : C) : (boundedHomotopyEquiv C) (of X) = TriangulatedK0.of ((HomotopyCategory.Bounded.singleFunctor C 0).obj X)

TauCeti.SplitK0.boundedHomotopyEquiv sends the class of an object to the class of that object placed in degree zero.

theorem TauCeti.SplitK0.boundedHomotopyEquiv_symm_of_quotient_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (K : CochainComplex.Bounded C) {s : Finset ℤ} (hs : ∀ n ∉ s, CategoryTheory.Limits.IsZero (K.obj.X n)) : (boundedHomotopyEquiv C).symm (TriangulatedK0.of ((HomotopyCategory.Bounded.quotient C).obj K)) = eulerChar K.obj s

The inverse of TauCeti.SplitK0.boundedHomotopyEquiv sends the class of a bounded complex to its Euler characteristic, summed over any finite set of degrees outside which it vanishes.

@[simp]

theorem TauCeti.SplitK0.boundedHomotopyEquiv_symm_of_singleFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (n : ℤ) (X : C) : (boundedHomotopyEquiv C).symm (TriangulatedK0.of ((HomotopyCategory.Bounded.singleFunctor C n).obj X)) = ↑n.negOnePow • of X

The inverse of TauCeti.SplitK0.boundedHomotopyEquiv sends the class of an object placed in degree n to (-1)ⁿ times its class.