Acyclic periodic complexes

Cyclic homology is a homological functor on the periodic homotopy category. The objects with zero homology in every residue form a triangulated subcategory, closed under retracts. This is the kernel used in the Verdier construction of the periodic derived category.

The shift comparison follows Joël Riou's short-complex construction in Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence. The homological-functor argument follows Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor, using the componentwise split conflations that define the periodic triangulation.

References

• T. Stai, The triangulated hull of periodic complexes, Sections 3.1–3.2.

noncomputable def TauCeti.PeriodicComplex.homologyShiftIso (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (k : ℤ) (i : ZMod n) : (CategoryTheory.shiftFunctor (CochainComplex C (ZMod n)) k).comp (HomologicalComplex.homologyFunctor C (ComplexShape.up (ZMod n)) i) ≅ HomologicalComplex.homologyFunctor C (ComplexShape.up (ZMod n)) (i + ↑k)

Homology of a signed cyclic shift is homology in the shifted residue.

@[simp]

theorem TauCeti.PeriodicComplex.shift_acyclic_iff (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (K : CochainComplex C (ZMod n)) (k : ℤ) : HomologicalComplex.Acyclic (K⟦k⟧) ↔ HomologicalComplex.Acyclic K

Signed cyclic shifts preserve and reflect acyclicity.

instance TauCeti.PeriodicComplex.homologyFunctor_isHomological (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Abelian C] (i : ZMod n) : (HomotopyCategory.homologyFunctor C (ComplexShape.up (ZMod n)) i).IsHomological

Homology in each cyclic degree sends distinguished triangles to exact sequences.

def TauCeti.PeriodicComplex.subcategoryAcyclic (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Abelian C] : CategoryTheory.ObjectProperty (HomotopyCategory C (ComplexShape.up (ZMod n)))

The acyclic objects of the cyclic homotopy category: homology vanishes in every residue.

theorem TauCeti.PeriodicComplex.mem_subcategoryAcyclic_iff (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Abelian C] (K : HomotopyCategory C (ComplexShape.up (ZMod n))) : subcategoryAcyclic C n K ↔ ∀ (i : ZMod n), CategoryTheory.Limits.IsZero ((HomotopyCategory.homologyFunctor C (ComplexShape.up (ZMod n)) i).obj K)

Membership in the acyclic subcategory is vanishing of every cyclic homology object.

@[simp]

theorem TauCeti.PeriodicComplex.quotient_obj_mem_subcategoryAcyclic_iff (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Abelian C] (K : CochainComplex C (ZMod n)) : subcategoryAcyclic C n ((HomotopyCategory.quotient C (ComplexShape.up (ZMod n))).obj K) ↔ HomologicalComplex.Acyclic K

A represented homotopy object is acyclic exactly when the original complex is acyclic.

instance TauCeti.PeriodicComplex.instIsStableUnderRetractsHomotopyCategoryZModUpSubcategoryAcyclic (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Abelian C] : (subcategoryAcyclic C n).IsStableUnderRetracts

instance TauCeti.PeriodicComplex.instIsTriangulatedHomotopyCategoryZModUpSubcategoryAcyclic (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Abelian C] : (subcategoryAcyclic C n).IsTriangulated