Grothendieck-group action of a functorial dg cone #
A closed degree-zero dg natural transformation α : F ⟶ G with chosen
objectwise cones gives a functorial distinguished triangle
H⁰ F X ⟶ H⁰ G X ⟶ H⁰(Cone α) X ⟶ H⁰ F X⟦1⟧.
Consequently its cone functor has class [G X] - [F X]. Automatic
dg-functor exactness upgrades the formula to an equality of homomorphisms on
K₀.
This generic leaf is the owner of the subtraction formula. Adjunction cones, object twists, and any later kernel-cone construction should specialize it rather than repeat the triangle calculation.
theorem
CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.functorK₀Of
{C : Type u}
{D : Type u'}
[DGCategory C]
[DGCategory D]
[IsPretriangulated D]
{F G : DGFunctor C D}
{α : ↥(F.HomogeneousNatTrans G 0)}
(K : ConeData α)
(hα : IsClosed α)
(X : H0 C)
:
Triangulated.K₀.of (H0 D) (K.functor.h0.obj X) = Triangulated.K₀.of (H0 D) (G.h0.obj X) - Triangulated.K₀.of (H0 D) (F.h0.obj X)
The functorial cone triangle gives
[Cone(α) X] = [G X] - [F X] in K₀(H⁰ D).
theorem
CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.functorK₀Map
{C : Type u}
{D : Type u'}
[DGCategory C]
[DGCategory D]
[IsPretriangulated D]
{F G : DGFunctor C D}
{α : ↥(F.HomogeneousNatTrans G 0)}
(K : ConeData α)
[IsPretriangulated C]
(hα : IsClosed α)
:
The functorial cone acts on K₀ by target endpoint minus source endpoint.