Documentation

DerivedAlgGeo.CategoryTheory.Triangulated.GrothendieckGroup.Biproduct

Finite biproducts in the triangulated Grothendieck group #

The class of a finite biproduct is the sum of the classes of its summands. The binary statement comes directly from the distinguished split triangle; the finite statement only packages the resulting induction over a finite indexing type.

source
@[simp]
theorem CategoryTheory.Triangulated.K₀.of_biprod (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X Y : C) :
of C (X ⊞ Y) = of C X + of C Y

The Grothendieck class of a binary biproduct is the sum of the two classes.

source
theorem CategoryTheory.Triangulated.K₀.of_biproduct (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type w} [Fintype ι] (X : ι → C) :
of C (⨁ X) = ∑ i : ι, of C (X i)

The Grothendieck class of a finite biproduct is the sum of the classes of its summands.

source
theorem CategoryTheory.Triangulated.K₀.of_biproduct_const (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type w} [Fintype ι] (X : C) :
of C (⨁ fun (x : ι) => X) = Fintype.card ι • of C X

A finite biproduct of copies of one object represents the corresponding natural multiple of its Grothendieck class.