Grothendieck-group action of a scalar-linear object twist #
The generic functorial-cone formula specializes to scalar-linear evaluation:
[T_E X] = [X] - [DGLinear.homComplex k E X ⊗ₖ E].
Automatic dg-functor exactness upgrades the same identity to induced
endomorphisms of K₀. No Euler-characteristic identification is
used here; that numerical specialization belongs to SphericalTwist.
theorem
CategoryTheory.LinearEvaluationData.TwistConeData.twistK₀Of
{k : Type w}
[CommRing k]
{C : Type u}
[DGCategory C]
[IsPretriangulated C]
[(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)]
[DGLinear k C]
{E : C}
{V : LinearEvaluationData k E}
(K : TwistConeData k V)
(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 scalar-linear object-twist triangle gives the identity-minus-evaluation formula on object classes.
theorem
CategoryTheory.LinearEvaluationData.TwistConeData.twistK₀Map
{k : Type w}
[CommRing k]
{C : Type u}
[DGCategory C]
[IsPretriangulated C]
[(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)]
[DGLinear k C]
{E : C}
{V : LinearEvaluationData k E}
(K : TwistConeData k V)
:
The scalar-linear object twist acts on K₀ by identity minus evaluation.