Euler-class realization for scalar-linear evaluation data

LinearEvaluationData.IsEulerCopower specializes the shared objectwise rank-one K₀ interface to RHom(E,-) ⊗ₖ E and is invariant under the canonical comparison between choices.

The predicate makes no exactness claim for the evaluation functor. Although additive and scalar-linear evaluation data use the same numerical interface, this supplies no comparison between their different universal properties. The finite-presentation realization is owned downstream by the homotopy- category DG-enhancement layer.

def CategoryTheory.LinearEvaluationData.IsEulerCopower (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)] {E : C} (V : LinearEvaluationData k E) : Prop

Scalar-linear evaluation realizes the Euler copower formula when its object classes are the rank-one operator χ(E,-) [E].

Equations

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

theorem CategoryTheory.LinearEvaluationData.IsEulerCopower.ofCompare (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)] {E : C} {V W : LinearEvaluationData k E} (hV : IsEulerCopower k V) : IsEulerCopower k W

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