Grothendieck-group actions of enhanced adjunction cones

The four distinguished adjunction triangles determine the K₀ class of each conventional twist or cotwist value. Automatic dg-functor exactness upgrades those generator formulas to equalities of homomorphisms on K₀.

These formulas stop at the adjunction composites. Identifying an object-twist evaluation composite with chiHom k C E X • K₀.of C E is the separate copower/Euler-characteristic seam needed to recover the numerical reflection twistK₀.

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.twistFunctorK₀Of {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] (X : H0 B) : K₀.of (H0 B) (P.twistFunctor.h0.obj X) = K₀.of (H0 B) X - K₀.of (H0 B) ((R.comp S).h0.obj X)

The twist triangle gives [T X] = [X] - [S R X] in K₀(H⁰ B).

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.twistFunctorK₀Map {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] : K₀.map P.twistFunctor.h0 = AddMonoidHom.id (K₀ (H0 B)) - K₀.map (R.comp S).h0

The twist acts on K₀ by identity minus the adjunction composite. The exact structures used here are canonical for dg functors.

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualTwistFunctorK₀Of {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] (X : H0 B) : K₀.of (H0 B) (P.dualTwistFunctor.h0.obj X) = K₀.of (H0 B) X - K₀.of (H0 B) ((L.comp S).h0.obj X)

The dual-twist triangle gives [T' X] = [X] - [S L X] in K₀(H⁰ B).

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualTwistFunctorK₀Map {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] : K₀.map P.dualTwistFunctor.h0 = AddMonoidHom.id (K₀ (H0 B)) - K₀.map (L.comp S).h0

The dual twist acts on K₀ by identity minus the left-adjunction composite. The exact structures used here are canonical for dg functors.

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistFunctorK₀Of {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] (X : H0 A) : K₀.of (H0 A) (P.cotwistFunctor.h0.obj X) = K₀.of (H0 A) X - K₀.of (H0 A) ((S.comp R).h0.obj X)

The cotwist triangle gives [C X] = [X] - [R S X] in K₀(H⁰ A).

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistFunctorK₀Map {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] : K₀.map P.cotwistFunctor.h0 = AddMonoidHom.id (K₀ (H0 A)) - K₀.map (S.comp R).h0

The cotwist acts on K₀ by identity minus the right-adjunction composite. The exact structures used here are canonical for dg functors.

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualCotwistFunctorK₀Of {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] (X : H0 A) : K₀.of (H0 A) (P.dualCotwistFunctor.h0.obj X) = K₀.of (H0 A) X - K₀.of (H0 A) ((S.comp L).h0.obj X)

The dual-cotwist triangle gives [C' X] = [X] - [L S X] in K₀(H⁰ A).

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualCotwistFunctorK₀Map {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] : K₀.map P.dualCotwistFunctor.h0 = AddMonoidHom.id (K₀ (H0 A)) - K₀.map (S.comp L).h0

The dual cotwist acts on K₀ by identity minus the left-adjunction composite. The exact structures used here are canonical for dg functors.