Finite-presentation realization for scalar-linear evaluation

A finite cohomology presentation for every dg Hom-complex proves the shared rank-one K₀ formula for scalar-linear evaluation when all scalar-linear copowers exist. Such presentations may be supplied explicitly, or constructed automatically from HomFiniteBounded using coefficient-side formality.

The result makes no exactness claim for the evaluation functor and supplies no comparison with additive evaluation data. The scalar-universe restriction belongs to the finite-free copower realization consumed here, not to the generic numerical predicate.

theorem CategoryTheory.LinearEvaluationData.IsEulerCopower.ofFiniteCohomologyPresentations (k : Type v) [Field k] {C : Type u} [DGCategory C] [IsPretriangulated C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [Triangulated.HomFiniteBounded k (H0 C)] {E : C} [HasLinearCopowers k C] (V : LinearEvaluationData k E) (P : (X : C) → (DGLinear.homComplex k E X).FiniteCohomologyPresentation) : IsEulerCopower k V

Supplied finite cohomology presentations compute every scalar-linear evaluation class by the Euler pairing.

theorem CategoryTheory.LinearEvaluationData.IsEulerCopower.ofHomFiniteBounded (k : Type v) [Field k] {C : Type u} [DGCategory C] [IsPretriangulated C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [Triangulated.HomFiniteBounded k (H0 C)] {E : C} [HasLinearCopowers k C] (V : LinearEvaluationData k E) : IsEulerCopower k V

Over a field, HomFiniteBounded and coefficient-side formality construct the finite presentation family needed for the scalar-linear Euler copower formula.