Natural transformations of stable functors commute with shifts

A natural transformation between exact functors preserving projective-injective objects descends to the stable categories of Frobenius exact categories. Its components commute with the canonical suspension comparisons and hence every integral shift. Thus shift compatibility is natural in the original exact functor, not just in the objects of the stable category. Install stableNatTrans_commShift locally after installing the stable shifts and the two stableFunctorCommShift structures. It supplies Mathlib's NatTrans.CommShift interface, including its natural-isomorphism and composition APIs.

The comparison is induced by morphisms of injective presentations. Naturality of the original transformation supplies such a morphism, and independence of the extension to the middle terms identifies its cokernel map in the stable quotient.

References

• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2.

theorem TauCeti.StableConflationExact.stableNatTrans_suspension {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (hF : StableConflationExact E E' F) (hG : StableConflationExact E E' G) (hE : E.IsFrobenius) (hE' : E'.IsFrobenius) (α : F ⟶ G) : CategoryTheory.CategoryStruct.comp (hF.stableSuspensionCompStableFunctorIso hE hE').hom (CategoryTheory.Functor.whiskerRight (hF.stableNatTrans hG hE α) hE'.stableSuspension) = CategoryTheory.CategoryStruct.comp (hE.stableSuspension.whiskerLeft (hF.stableNatTrans hG hE α)) (hG.stableSuspensionCompStableFunctorIso hE hE').hom

The descended natural transformation commutes with the canonical suspension comparisons of the two stable functors.

theorem TauCeti.StableConflationExact.stableNatTrans_suspension_assoc {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (hF : StableConflationExact E E' F) (hG : StableConflationExact E E' G) (hE : E.IsFrobenius) (hE' : E'.IsFrobenius) (α : F ⟶ G) {Z : CategoryTheory.Functor E.ProjectiveStableCategory E'.ProjectiveStableCategory} (h : (hG.stableFunctor hE).comp hE'.stableSuspension ⟶ Z) : CategoryTheory.CategoryStruct.comp (hF.stableSuspensionCompStableFunctorIso hE hE').hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (hF.stableNatTrans hG hE α) hE'.stableSuspension) h) = CategoryTheory.CategoryStruct.comp (hE.stableSuspension.whiskerLeft (hF.stableNatTrans hG hE α)) (CategoryTheory.CategoryStruct.comp (hG.stableSuspensionCompStableFunctorIso hE hE').hom h)

The descended natural transformation commutes with the canonical suspension comparisons of the two stable functors.

theorem TauCeti.StableConflationExact.stableNatTrans_commShift {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (hF : StableConflationExact E E' F) (hG : StableConflationExact E E' G) (hE : E.IsFrobenius) (hE' : E'.IsFrobenius) (α : F ⟶ G) : CategoryTheory.NatTrans.CommShift (hF.stableNatTrans hG hE α) ℤ

A descended natural transformation is compatible with all integral shifts of the stable categories, for the canonical shift comparisons of the two stable functors.