Numerical action of the scalar-linear object twist

The direct scalar-linear evaluation package now reaches the existing numerical Seidel--Thomas formula without passing through additive EvaluationData. LinearEvaluationData.IsEulerCopower identifies the evaluation term in the generic cone subtraction formula with χ(E,X) • [E].

Exactness is automatic for every dg functor. Nothing here compares the additive and scalar-linear universal properties or asserts that the twist is an autoequivalence.

theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistK₀Of_eq_twistK₀ (k : Type w) [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)] [∀ (n : ℤ), Functor.Linear k (shiftFunctor (H0 C) n)] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) (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 scalar-linear Euler copower formula, the evaluation cone has the existing numerical twistK₀ class on every object.

theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistK₀Map_eq_twistK₀ (k : Type w) [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)] [∀ (n : ℤ), Functor.Linear k (shiftFunctor (H0 C) n)] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) (hV : IsEulerCopower k V) : Triangulated.K₀.map K.twist.h0 = Triangulated.SphericalTwist.twistK₀ k (H0 C) (have this := E; this)

If scalar-linear evaluation realizes the Euler copower formula, its cone induces the numerical twist endomorphism on K₀.