Numerical Grothendieck-group action of an object twist

The generic functorial-cone K₀ interface computes the class of an object twist as

[T_E X] = [X] - [RHom(E,X) ⊗ E].

To identify this categorical formula with the numerical endomorphism twistK₀, one further input is genuinely needed: the chosen copower must have class χ(E,X) • [E]. EvaluationData.IsEulerCopower specializes the shared objectwise rank-one K₀ capability, using the fixed-source descended character chiRight so that the generic statement retains Hom-finiteness and finite Ext-amplitude without requiring every shift functor to be linear. It is invariant under the canonical comparison between evaluation-data choices. The full shift-linearity needed by the two-variable numerical endomorphism remains local to this spherical-twist consumer.

The capability and the categorical subtraction formula live in the generic DG-enhancement layer. This spherical-twist consumer contains only their two comparisons with the pre-existing numerical formula. It does not manufacture the capability from additive IsCopowerOf. The scalar-linear realization now proves the parallel predicate from explicitly supplied finite cohomology presentations, but no adapter identifies its evaluation data with this additive package; any such passage remains explicit.

theorem CategoryTheory.EvaluationData.TwistConeData.twistK₀Of_eq_twistK₀ {C : Type u} [DGCategory C] [IsPretriangulated C] {E : C} (k : Type w) [DivisionRing k] [Linear k (H0 C)] [Triangulated.HomFiniteBounded k (H0 C)] [∀ (n : ℤ), Functor.Linear k (shiftFunctor (H0 C) n)] {V : EvaluationData E} (K : V.TwistConeData) (hV : IsEulerCopower k V) (X : H0 C) : Triangulated.K₀.of (H0 C) (K.twist.h0.obj X) = (Triangulated.SphericalTwist.twistK₀ k (H0 C) (have this := E; this)) (Triangulated.K₀.of (H0 C) X)

Under the Euler copower formula, the class computed by the evaluation triangle is the existing numerical twistK₀ formula on object classes.

theorem CategoryTheory.EvaluationData.TwistConeData.twistK₀Map_eq_twistK₀ {C : Type u} [DGCategory C] [IsPretriangulated C] {E : C} (k : Type w) [DivisionRing k] [Linear k (H0 C)] [Triangulated.HomFiniteBounded k (H0 C)] [∀ (n : ℤ), Functor.Linear k (shiftFunctor (H0 C) n)] {V : EvaluationData E} (K : V.TwistConeData) (hV : IsEulerCopower k V) : Triangulated.K₀.map K.twist.h0 = Triangulated.SphericalTwist.twistK₀ k (H0 C) (have this := E; this)

If evaluation realizes the Euler copower formula, the induced object-twist map is the existing numerical endomorphism twistK₀.