Euler-class realization for object-twist evaluation data

The existing EvaluationData gives additive copowers and the functor RHom(E,-) ⊗ E. Relating its object classes to the k-linear Euler form is extra realization content: the current IsCopowerOf represents additive cochains over ℤ, not k-linear cochains.

EvaluationData.IsEulerCopower specializes the shared rank-one K₀ formula, using the fixed-source descended character chiRight; this retains Hom-finiteness and finite Ext-amplitude without imposing the stronger shift-linearity needed to descend in the first variable as well. The property is independent of the chosen additive evaluation data. The parallel direct linear evaluation consumer uses the same numerical interface, but that common formula supplies no map between additive and scalar-linear evaluation data.

theorem CategoryTheory.EvaluationData.TwistConeData.twistK₀Of {C : Type u} [DGCategory C] [IsPretriangulated C] {E : C} {V : EvaluationData E} (K : V.TwistConeData) (X : H0 C) : Triangulated.K₀.of (H0 C) (K.twist.h0.obj X) = Triangulated.K₀.of (H0 C) X - Triangulated.K₀.of (H0 C) (V.functor.h0.obj X)

The object-twist triangle gives [T_E X] = [X] - [RHom(E,X) ⊗ E] in K₀(H⁰ C).

theorem CategoryTheory.EvaluationData.TwistConeData.twistK₀Map {C : Type u} [DGCategory C] [IsPretriangulated C] {E : C} {V : EvaluationData E} (K : V.TwistConeData) : Triangulated.K₀.map K.twist.h0 = AddMonoidHom.id (Triangulated.K₀ (H0 C)) - Triangulated.K₀.map V.functor.h0

The object twist acts on K₀ by identity minus evaluation.

def CategoryTheory.EvaluationData.IsEulerCopower {C : Type u} [DGCategory C] [IsPretriangulated C] {E : C} (k : Type w) [DivisionRing k] [Linear k (H0 C)] [Triangulated.HomFiniteBounded k (H0 C)] (V : EvaluationData E) : Prop

An evaluation choice realizes the Euler copower formula when [RHom(E,X) ⊗ E] = χ(E,X) • [E] for every X.

This is explicit realization input, not a consequence of the present additive IsCopowerOf universal property.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.EvaluationData.IsEulerCopower.ofCompare {C : Type u} [DGCategory C] [IsPretriangulated C] {E : C} (k : Type w) [DivisionRing k] [Linear k (H0 C)] [Triangulated.HomFiniteBounded k (H0 C)] {V W : EvaluationData E} (hV : IsEulerCopower k V) : IsEulerCopower k W

The Euler copower formula is independent of the chosen evaluation data.