The Grothendieck group of a pretriangulated dg category

K₀ is defined once, at GrothendieckPresentation, and instantiated at the distinguished triangles of a pretriangulated category (Triangulated/GrothendieckGroup/Basic.lean). A pretriangulated dg category is not itself pretriangulated — its H⁰ is, by H0.pretriangulated (DGEnhancement/H0/Triangle.lean, dg-enhancements-e6). So the dg Grothendieck group needs no new construction: it is the existing one at H0 C.

That is the whole content of this file, and it is the point. The dg layer has carried H0.pretriangulated since e6 without any downstream declaration using it; K₀dg is the first, and it is three lines because the tower was already built to admit it.

Why not a new presentation

A dg category has no distinguished triangles of its own — a dg cone is functorial, and the triangulated structure appears only after passing to H⁰, where the choice of cone stops mattering up to isomorphism. Writing a separate GrothendieckPresentation on dg objects would either reproduce distinguishedTriangles C (which is what H0's instance already quotients by) or quotient by something finer, which would not be the Grothendieck group of the homotopy category. Neither is wanted.

Main definitions

• K₀dg — the Grothendieck group of a pretriangulated dg category.
• K₀dg.of — the class of a dg object.

@[reducible, inline]

abbrev CategoryTheory.DGCategory.K₀dg (C : Type u) [DGCategory C] [IsPretriangulated C] : Type u

The Grothendieck group of a pretriangulated dg category: the Grothendieck group of its homotopy category H⁰.

This is K₀ at the Pretriangulated (H0 C) instance, not a new construction.

Equations

• CategoryTheory.DGCategory.K₀dg C = CategoryTheory.Triangulated.K₀ (CategoryTheory.H0 C)

noncomputable def CategoryTheory.DGCategory.K₀dg.of {C : Type u} [DGCategory C] [IsPretriangulated C] (X : C) : K₀dg C

The class of a dg object in K₀dg, through its image in H⁰.

Equations

• CategoryTheory.DGCategory.K₀dg.of X = CategoryTheory.Triangulated.K₀.of (CategoryTheory.H0 C) (have this := X; this)

@[simp]

theorem CategoryTheory.DGCategory.K₀dg.of_eq {C : Type u} [DGCategory C] [IsPretriangulated C] (X : C) : of X = Triangulated.K₀.of (H0 C) (have this := X; this)

theorem CategoryTheory.DGCategory.K₀dg.of_triangle {C : Type u} [DGCategory C] [IsPretriangulated C] (T : Pretriangulated.Triangle (H0 C)) (hT : T ∈ Pretriangulated.distinguishedTriangles) : Triangulated.K₀.of (H0 C) T.obj₂ = Triangulated.K₀.of (H0 C) T.obj₁ + Triangulated.K₀.of (H0 C) T.obj₃

A distinguished triangle of H⁰ gives the defining relation, inherited from K₀.