Grothendieck classes from bounded derived cohomology

For an abelian category A, the alternating sum of the cohomology classes of an object of Dᵇ(A) is additive on distinguished triangles. It therefore descends to a canonical homomorphism

K₀(Dᵇ(A)) →+ K₀Ab(A).

This file constructs that direction only. Its identification as the inverse of the standard-heart comparison is proved separately, by dévissage, in GrothendieckGroup.Comparison.

@[reducible, inline]

noncomputable abbrev DerivedCategory.boundedHomologyFunctor (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (n : ℤ) : CategoryTheory.Functor (Bounded A) A

Degree-n cohomology of a bounded-derived object.

Equations

• DerivedCategory.boundedHomologyFunctor A n = DerivedCategory.Bounded.ι.comp (DerivedCategory.homologyFunctor A n)

theorem DerivedCategory.boundedHomology_hasFiniteNonzeroSupport (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (X : Bounded A) : CategoryTheory.K₀Ab.HasFiniteNonzeroSupport fun (n : ℤ) => (boundedHomologyFunctor A n).obj X

A bounded-derived object has only finitely many nonzero cohomology objects.

noncomputable def DerivedCategory.boundedEulerClass (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (X : Bounded A) : CategoryTheory.K₀Ab A

The alternating sum of the cohomology classes of a bounded-derived object.

Equations

• DerivedCategory.boundedEulerClass A X = CategoryTheory.K₀Ab.eulerClass fun (n : ℤ) => (DerivedCategory.boundedHomologyFunctor A n).obj X

theorem DerivedCategory.boundedEulerClass_additive (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (T : CategoryTheory.Pretriangulated.Triangle (Bounded A)) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : boundedEulerClass A T.obj₂ = boundedEulerClass A T.obj₁ + boundedEulerClass A T.obj₃

The bounded cohomology Euler class is additive on distinguished triangles.

instance DerivedCategory.boundedEulerClass_isTriangleAdditive (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] : CategoryTheory.Triangulated.IsTriangleAdditive (boundedEulerClass A)

Triangle additivity packaged for the universal property of K₀.

noncomputable def DerivedCategory.boundedEulerClassHom (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] : CategoryTheory.Triangulated.K₀ (Bounded A) →+ CategoryTheory.K₀Ab A

The canonical cohomological Euler map K₀(Dᵇ(A)) →+ K₀Ab(A).

Equations

• DerivedCategory.boundedEulerClassHom A = CategoryTheory.Triangulated.K₀.lift (DerivedCategory.Bounded A) (DerivedCategory.boundedEulerClass A)

@[simp]

theorem DerivedCategory.boundedEulerClassHom_of (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (X : Bounded A) : (boundedEulerClassHom A) (CategoryTheory.Triangulated.K₀.of (Bounded A) X) = boundedEulerClass A X