Grothendieck classes of scalar-linear copowers

A supplied finite cohomology presentation reduces a scalar-linear copower to a finite biproduct of shifts. Finite-free homology then makes its Grothendieck class the homological Euler characteristic of the coefficient complex times the class of the object.

This result consumes the presentation as explicit data. It does not infer formality or a finite presentation from bounded or finite-dimensional homology.

theorem CochainComplex.FiniteCohomologyPresentation.linearCopowerK₀Of {k : Type v} [CommRing k] [Nontrivial k] [StrongRankCondition k] {C : Type u} [CategoryTheory.DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((CategoryTheory.DGCategoryStruct.dgHom X Y).X p)] [CategoryTheory.DGLinear k C] [CategoryTheory.HasLinearCopowers k C] {K : CochainComplex (ModuleCat k) ℤ} [CategoryTheory.IsPretriangulated C] (P : K.FiniteCohomologyPresentation) [∀ (i : ↥P.degrees), Module.Free k ↑(HomologicalComplex.homology K ↑i)] [∀ (i : ↥P.degrees), Module.Finite k ↑(HomologicalComplex.homology K ↑i)] (X : C) : CategoryTheory.Triangulated.K₀.of (CategoryTheory.H0 C) (have this := CategoryTheory.linearCopowerObj K X; this) = HomologicalComplex.homologyEulerChar K • CategoryTheory.Triangulated.K₀.of (CategoryTheory.H0 C) (have this := X; this)

A supplied finite cohomology presentation with finite-free homology computes the class of the selected scalar-linear copower by Mathlib's homological Euler characteristic.