Grothendieck comparison for a bounded derived category

For an abelian category A, the standard-heart map

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

and the cohomological Euler map constructed in DerivedCategory.GrothendieckGroup are inverse. The nontrivial direction is proved by bounded cohomological dévissage. Shifted single objects give the base case, and canonical truncation triangles are lifted into the bounded full subcategory for the induction step.

The final section packages the practical consequence for geometry: any additive class map defined on coherent sheaves extends canonically to the bounded derived category by precomposition with the Euler map. No geometric class map is manufactured here; callers must still supply the sheaf-level map.

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

The standard-heart comparison, expressed directly on the original abelian category.

Equations

• DerivedCategory.boundedHeartToAmbient A = (CategoryTheory.K₀Ab.toAmbient DerivedCategory.TStructure.t.onBounded).comp (CategoryTheory.K₀Ab.congrHom (DerivedCategory.boundedHeartEquivalence A))

@[simp]

theorem DerivedCategory.boundedHeartToAmbient_of (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (X : A) : (boundedHeartToAmbient A) (CategoryTheory.K₀Ab.of X) = CategoryTheory.Triangulated.K₀.of (Bounded A) ((boundedSingleFunctor A).obj X)

theorem DerivedCategory.boundedEulerClass_boundedSingleFunctor (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (X : A) : boundedEulerClass A ((boundedSingleFunctor A).obj X) = CategoryTheory.K₀Ab.of X

The Euler class of a degree-zero single object is its abelian Grothendieck class.

theorem DerivedCategory.boundedEulerClass_singleFunctor (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (n : ℤ) (X : A) (hX : TStructure.t.bounded ((singleFunctor A n).obj X)) : boundedEulerClass A { obj := (singleFunctor A n).obj X, property := hX } = ↑n.negOnePow • CategoryTheory.K₀Ab.of X

The Euler class of a single object in degree n is its abelian class with the usual parity sign. The boundedness proof is explicit so the theorem can be used for any chosen lift into Dᵇ(A).

theorem DerivedCategory.boundedEulerClassHom_comp_boundedHeartToAmbient (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] : (boundedEulerClassHom A).comp (boundedHeartToAmbient A) = AddMonoidHom.id (CategoryTheory.K₀Ab A)

Taking the Euler class is a left inverse to the standard-heart map.

theorem DerivedCategory.boundedEulerClassHom_comp_toAmbient (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] : (boundedEulerClassHom A).comp (CategoryTheory.K₀Ab.toAmbient TStructure.t.onBounded) = (CategoryTheory.K₀Ab.congr (boundedHeartEquivalence A)).symm.toAddMonoidHom

On the full standard heart, the Euler map is the inverse of the equivalence identifying that heart with A.

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

Every bounded-derived class is the image of the alternating sum of its cohomology classes. This is the dévissage half of the comparison theorem.

theorem DerivedCategory.boundedHeartToAmbient_comp_boundedEulerClassHom (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] : (boundedHeartToAmbient A).comp (boundedEulerClassHom A) = AddMonoidHom.id (CategoryTheory.Triangulated.K₀ (Bounded A))

The standard-heart map is also a left inverse to the Euler map.

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

The canonical comparison K₀Ab(A) ≃+ K₀(Dᵇ(A)).

Equations

• One or more equations did not get rendered due to their size.

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

Transport an additive class map on an abelian category to its bounded derived category by taking the cohomological Euler class.

Equations

• DerivedCategory.boundedDerivedClassMap A v = v.comp (DerivedCategory.boundedEulerClassHom A)

theorem DerivedCategory.boundedDerivedClassMap_comp_boundedHeartToAmbient (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] {Λ : Type u_1} [AddCommGroup Λ] (v : CategoryTheory.K₀Ab A →+ Λ) : (boundedDerivedClassMap A v).comp (boundedHeartToAmbient A) = v

The transported class map restricts to the original map along the direct standard-heart comparison.

theorem DerivedCategory.boundedDerivedClassMap_comp_toAmbient (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] {Λ : Type u_1} [AddCommGroup Λ] (v : CategoryTheory.K₀Ab A →+ Λ) : (boundedDerivedClassMap A v).comp (CategoryTheory.K₀Ab.toAmbient TStructure.t.onBounded) = v.comp (CategoryTheory.K₀Ab.congr (boundedHeartEquivalence A)).symm.toAddMonoidHom

On the full standard heart, the transported class map is the original map conjugated by the canonical heart equivalence.