The periodic stable comparison commutes with integral shifts

The canonical equivalence from the componentwise split stable category of cyclic cochain complexes to the homotopy category intertwines stable suspension with the signed shift by one. This file extends that comparison coherently to every integer shift. The target keeps its existing signed cyclic shift, including its addition constraints. This supplies the shift compatibility required to transport the stable triangulation to the homotopy category.

The construction uses stableSuspensionCompStableToHomotopyIso and the sequence-model comparison TauCeti.ExactStructure.IsFrobenius.commShiftOfIntertwiningStableSuspensionShift.

References

• B. Keller, Chain complexes and stable categories, Manuscripta Mathematica 67 (1990), 379–417, Section 1.
• T. Stai, The triangulated hull of periodic complexes, Mathematical Research Letters 25 (2018), 199–236, Section 3.

@[instance_reducible]

noncomputable def TauCeti.PeriodicComplex.stableToHomotopyCommShift (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (n : ℕ) : (ExactStructure.homologicalComplexSplitStableToHomotopy C (ComplexShape.up (ZMod n)) ⋯).CommShift ℤ

The stable-to-homotopy equivalence commutes coherently with the stable integral shift and the signed cyclic shift already installed on the homotopy category.

theorem TauCeti.PeriodicComplex.stableToHomotopyCommShift_iso_one (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (n : ℕ) : CategoryTheory.Functor.commShiftIso (ExactStructure.homologicalComplexSplitStableToHomotopy C (ComplexShape.up (ZMod n)) ⋯) 1 = CategoryTheory.Functor.isoWhiskerRight ⋯.stableShiftFunctorOneIso (ExactStructure.homologicalComplexSplitStableToHomotopy C (ComplexShape.up (ZMod n)) ⋯) ≪≫ stableSuspensionCompStableToHomotopyIso C n

In degree one, the stable comparison identifies stable suspension with the signed cyclic shift using the supplied suspension comparison.