The Verdier quotient of periodic complexes

The periodic derived category is the localization of the cyclic homotopy category at morphisms whose cone has zero cyclic homology. Mathlib's Verdier localization supplies its additive and triangulated structures, integral shifts, and localization universal property. The functor from complexes factors through homotopy classes, and sends acyclic complexes to zero. No finite-global-dimension hypothesis is needed for this construction.

The presentation here is the Verdier quotient. The mapping-cone characterization of periodic quasi-isomorphisms identifies its weak equivalences with the homology-based quasi-isomorphisms. Consequently the functor from periodic complexes is itself a localization at quasi-isomorphisms, and the resulting comparison with Mathlib's constructed localization is an equivalence. A positive period gives a finite cyclic grading; period zero is also supported.

The construction follows Joël Riou's localization instances in Mathlib.Algebra.Homology.DerivedCategory.Basic, retaining the existing periodic shift.

References

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

theorem TauCeti.PeriodicComplex.quasiIso_eq_trW_subcategoryAcyclic (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : HomotopyCategory.quasiIso C (ComplexShape.up (ZMod n)) = (subcategoryAcyclic C n).trW

Quasi-isomorphisms in the periodic homotopy category are exactly the morphisms whose Verdier cone is acyclic.

@[reducible, inline]

abbrev TauCeti.PeriodicComplex.DerivedCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : Type (max u v)

The Verdier quotient of the cyclic homotopy category by the acyclic objects.

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

The Verdier localization functor from cyclic homotopy classes.

instance TauCeti.PeriodicComplex.DerivedCategory.instIsLocalizationHomotopyCategoryZModUpQhTrWSubcategoryAcyclic (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : (Qh C n).IsLocalization (subcategoryAcyclic C n).trW

instance TauCeti.PeriodicComplex.DerivedCategory.instIsLocalizationHomotopyCategoryZModUpQhQuasiIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : (Qh C n).IsLocalization (HomotopyCategory.quasiIso C (ComplexShape.up (ZMod n)))

The periodic Verdier functor is also a localization at the homology-based quasi-isomorphisms of the periodic homotopy category.

@[instance_reducible]

noncomputable instance TauCeti.PeriodicComplex.DerivedCategory.instPreadditive (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : CategoryTheory.Preadditive (DerivedCategory C n)

instance TauCeti.PeriodicComplex.DerivedCategory.instAdditiveHomotopyCategoryZModUpQh (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : (Qh C n).Additive

instance TauCeti.PeriodicComplex.DerivedCategory.instHasZeroObject (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : CategoryTheory.Limits.HasZeroObject (DerivedCategory C n)

@[instance_reducible]

noncomputable instance TauCeti.PeriodicComplex.DerivedCategory.instHasShiftInt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : CategoryTheory.HasShift (DerivedCategory C n) ℤ

@[instance_reducible]

noncomputable instance TauCeti.PeriodicComplex.DerivedCategory.instCommShiftHomotopyCategoryZModUpQhInt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : (Qh C n).CommShift ℤ

instance TauCeti.PeriodicComplex.DerivedCategory.instAdditiveShiftFunctorInt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) (k : ℤ) : (CategoryTheory.shiftFunctor (DerivedCategory C n) k).Additive

@[instance_reducible]

noncomputable instance TauCeti.PeriodicComplex.DerivedCategory.instPretriangulated (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : CategoryTheory.Pretriangulated (DerivedCategory C n)

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

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

noncomputable def TauCeti.PeriodicComplex.DerivedCategory.Q (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : CategoryTheory.Functor (CochainComplex C (ZMod n)) (DerivedCategory C n)

Passage from cyclic complexes to their derived classes, through the homotopy category.

theorem TauCeti.PeriodicComplex.DerivedCategory.quotient_comp_Qh (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : (HomotopyCategory.quotient C (ComplexShape.up (ZMod n))).comp (Qh C n) = Q C n

The functor from complexes factors through homotopy classes.

instance TauCeti.PeriodicComplex.DerivedCategory.instIsLocalizationCochainComplexZModQQuasiIsoUp (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : (Q C n).IsLocalization (HomologicalComplex.quasiIso C (ComplexShape.up (ZMod n)))

Passage to the periodic derived category is a localization of periodic complexes at quasi-isomorphisms.

instance TauCeti.PeriodicComplex.DerivedCategory.instIsIsoMapCochainComplexZModQOfQuasiIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) {X Y : CochainComplex C (ZMod n)} (f : X ⟶ Y) [QuasiIso f] : CategoryTheory.IsIso ((Q C n).map f)

A periodic quasi-isomorphism becomes an isomorphism in the periodic derived category.

noncomputable def TauCeti.PeriodicComplex.DerivedCategory.quasiIsoLocalizationEquivalence (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : (HomologicalComplex.quasiIso C (ComplexShape.up (ZMod n))).Localization ≌ DerivedCategory C n

The equivalence from Mathlib's constructed localization at periodic quasi-isomorphisms to the periodic Verdier quotient.

noncomputable def TauCeti.PeriodicComplex.DerivedCategory.quasiIsoLocalizationCompEquivalenceFunctorIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : (HomologicalComplex.quasiIso C (ComplexShape.up (ZMod n))).Q.comp (quasiIsoLocalizationEquivalence C n).functor ≅ Q C n

The localization through quasiIsoLocalizationEquivalence agrees with the periodic Verdier localization.

instance TauCeti.PeriodicComplex.DerivedCategory.instAdditiveCochainComplexZModQ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : (Q C n).Additive

@[instance_reducible]

noncomputable instance TauCeti.PeriodicComplex.DerivedCategory.instCommShiftCochainComplexZModQInt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : (Q C n).CommShift ℤ

instance TauCeti.PeriodicComplex.DerivedCategory.instCommShiftHomologicalComplexZModUpHomFunctorEqToIsoInt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : CategoryTheory.NatTrans.CommShift (CategoryTheory.eqToIso ⋯).hom ℤ

theorem TauCeti.PeriodicComplex.DerivedCategory.isZero_Qh_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) (K : HomotopyCategory C (ComplexShape.up (ZMod n))) (hK : subcategoryAcyclic C n K) : CategoryTheory.Limits.IsZero ((Qh C n).obj K)

The Verdier localization kills every acyclic homotopy object.

theorem TauCeti.PeriodicComplex.DerivedCategory.isZero_Q_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) (K : CochainComplex C (ZMod n)) (hK : HomologicalComplex.Acyclic K) : CategoryTheory.Limits.IsZero ((Q C n).obj K)

An acyclic cyclic complex becomes zero in the periodic derived category.