From the Grothendieck group of a heart to the ambient one

K₀Ab.toAmbient sends the class of a heart object to the class of the underlying ambient object, K₀Ab 𝒜 →+ K₀ C for 𝒜 the heart of a t-structure on C.

Why only one direction, and why that is enough

Weak/Basic/Definitions.lean records that the comparison K(𝒜) ≅ K(D) for a bounded t-structure is not available at this Mathlib pin and is not assumed. That is the isomorphism. This file constructs only the map, which needs no boundedness and no inverse: a short exact sequence in the heart extends to a distinguished triangle on the same three objects (heartFullSubcategory_shortExact_triangle), so the abelian relations are carried into the triangulated ones and GrothendieckPresentation.map applies.

Every conversion between a charge on a heart and a charge on K₀ C uses the map in this direction only, so nothing here depends on the unavailable iso.

What this replaces

Charges written on heart objects and charges written on K₀ C were previously two unrelated families, and the conversion between them existed once, hand-rolled and inlined, inside a mass-subadditivity file. With this map the conversion is AddMonoidHom.comp.

noncomputable def CategoryTheory.Triangulated.TStructure.shortExactToTriangle {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) (r : { S : ShortComplex t.heart.FullSubcategory // S.ShortExact }) : { T : Pretriangulated.Triangle C // T ∈ Pretriangulated.distinguishedTriangles }

A short exact sequence in the heart, as a distinguished triangle on the same three ambient objects. The delta is chosen; the map below only needs the objects, which are determined.

Equations

• t.shortExactToTriangle r = ⟨CategoryTheory.Pretriangulated.Triangle.mk (↑r).f.hom (↑r).g.hom ⋯.choose, ⋯⟩

theorem CategoryTheory.Triangulated.TStructure.toAmbient_isAdditive {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) : (abelianPresentation t.heart.FullSubcategory).IsAdditive ((triangulatedPresentation C).of ∘ fun (X : t.heart.FullSubcategory) => X.obj)

The underlying-object function carries abelian relations of the heart into triangulated relations of C.

noncomputable def CategoryTheory.K₀Ab.toAmbient {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : Triangulated.TStructure C) : K₀Ab t.heart.FullSubcategory →+ Triangulated.K₀ C

The comparison map K₀Ab 𝒜 →+ K₀ C.

Built from GrothendieckPresentation.map: the underlying-object function carries the abelian relations of the heart into the triangulated relations of C, which is exactly heartFullSubcategory_shortExact_triangle.

Equations

• CategoryTheory.K₀Ab.toAmbient t = (CategoryTheory.abelianPresentation t.heart.FullSubcategory).map (fun (X : t.heart.FullSubcategory) => X.obj) ⋯

@[simp]

theorem CategoryTheory.K₀Ab.toAmbient_of {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : Triangulated.TStructure C) (E : t.heart.FullSubcategory) : (toAmbient t) (of E) = Triangulated.K₀.of C E.obj