Compression on derived categories

Let C be an abelian category. The n-periodic compression K^b(C) ⥤ K_n(C) from the bounded homotopy category to the n-periodic homotopy category preserves and reflects quasi-isomorphisms (TauCeti.PeriodicComplex.quasiIso_iff_trW_homotopyCompressionFunctor_map): it is a triangle functor, and a bounded complex is acyclic exactly when its compression is. Since K^b(C) ⥤ D^b(C) is a localization at the quasi-isomorphisms, compression descends to a triangle functor TauCeti.PeriodicComplex.derivedCompressionFunctor : D^b(C) ⥤ D_n(C) from the bounded derived category to the n-periodic derived category, compatible with the localization functors up to the natural isomorphism TauCeti.PeriodicComplex.derivedCompressionFunctorFactors.

Compression on derived categories is invariant under the shift by any multiple k of n (TauCeti.PeriodicComplex.derivedCompressionFunctorPeriodicityIso): the periodicity isomorphism of K^b(C) ⥤ K_n(C) descends along K^b(C) ⥤ D^b(C). Taking k = n, Keller's universal property of the orbit category descends compression to the orbit functor D^b(C)/[n] ⥤ D_n(C) (TauCeti.PeriodicComplex.orbitDerivedCompressionFunctor), which restricts to compression along the projection D^b(C) ⥤ D^b(C)/[n]. It is induced by the orbit functor K^b(C)/[n] ⥤ K_n(C): the induced functor K^b(C)/[n] ⥤ D^b(C)/[n] followed by the derived orbit functor is the homotopy orbit functor followed by K_n(C) ⥤ D_n(C) (TauCeti.PeriodicComplex.orbitDerivedCompressionFunctorFactors). No hypothesis on C beyond abelianity is needed for these constructions. In finite global dimension the derived orbit functor is fully faithful (TauCeti.PeriodicComplex.fullyFaithfulOrbitDerivedCompressionFunctor, in TauCeti.Algebra.Homology.Periodic.Compression.GlobalDimension), generalizing Stai's Lemma 3.12.

References

• B. Keller, On triangulated orbit categories, Documenta Mathematica 10 (2005), 551–581, Section 1.
• T. Stai, The triangulated hull of periodic complexes, Mathematical Research Letters 25 (2018), 199–236, Section 3.3.
• derivedCompressionFunctorPeriodicityIso is descended along the localization functor like TauCeti.PeriodicComplex.homotopyCompressionFunctorPeriodicityIso (TauCeti.Algebra.Homology.Periodic.Compression.Periodicity).

theorem TauCeti.PeriodicComplex.homotopyCompressionFunctor_obj_mem_subcategoryAcyclic_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) (K : HomotopyCategory.Bounded C) : subcategoryAcyclic C n ((homotopyCompressionFunctor n).obj K) ↔ HomotopyCategory.Bounded.subcategoryAcyclic C K

An object of the bounded homotopy category is acyclic exactly when its compression is acyclic.

theorem TauCeti.PeriodicComplex.subcategoryAcyclic_inverseImage_homotopyCompressionFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : (subcategoryAcyclic C n).inverseImage (homotopyCompressionFunctor n) = HomotopyCategory.Bounded.subcategoryAcyclic C

The acyclic objects of the bounded homotopy category are the inverse image of the acyclic objects of the n-periodic homotopy category under compression.

theorem TauCeti.PeriodicComplex.quasiIso_iff_trW_homotopyCompressionFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) {K L : HomotopyCategory.Bounded C} (f : K ⟶ L) : HomotopyCategory.Bounded.quasiIso C f ↔ (subcategoryAcyclic C n).trW ((homotopyCompressionFunctor n).map f)

A morphism of the bounded homotopy category is a quasi-isomorphism exactly when its compression has an acyclic cone, and hence becomes an isomorphism in the periodic derived category.

theorem TauCeti.PeriodicComplex.homotopyCompressionFunctor_comp_Qh_inverts_quasiIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : (HomotopyCategory.Bounded.quasiIso C).IsInvertedBy ((homotopyCompressionFunctor n).comp (DerivedCategory.Qh C n))

Compression followed by the localization to the periodic derived category inverts the quasi-isomorphisms of bounded complexes.

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

The n-periodic compression D^b(C) ⥤ D_n(C) from the bounded derived category to the n-periodic derived category, induced by the compression of bounded complexes.

noncomputable def TauCeti.PeriodicComplex.derivedCompressionFunctorFactors {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) [HasDerivedCategory C] : (DerivedCategory.Bounded.Qh C).comp (derivedCompressionFunctor n) ≅ (homotopyCompressionFunctor n).comp (DerivedCategory.Qh C n)

The compression D^b(C) ⥤ D_n(C) is induced by the compression K^b(C) ⥤ K_n(C).

@[instance_reducible]

noncomputable instance TauCeti.PeriodicComplex.instLiftingBoundedBoundedDerivedCategoryQhQuasiIsoCompHomotopyCategoryZModUpHomotopyCompressionFunctorQhDerivedCompressionFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) [HasDerivedCategory C] : CategoryTheory.Localization.Lifting (DerivedCategory.Bounded.Qh C) (HomotopyCategory.Bounded.quasiIso C) ((homotopyCompressionFunctor n).comp (DerivedCategory.Qh C n)) (derivedCompressionFunctor n)

@[instance_reducible]

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

instance TauCeti.PeriodicComplex.instCommShiftBoundedDerivedCategoryHomFunctorDerivedCompressionFunctorFactorsInt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) [HasDerivedCategory C] : CategoryTheory.NatTrans.CommShift (derivedCompressionFunctorFactors n).hom ℤ

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

Compression is a triangle functor on derived categories.

noncomputable def TauCeti.PeriodicComplex.derivedCompressionFunctorPeriodicityIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) [HasDerivedCategory C] (k : ℤ) (hk : ↑k = 0) : (CategoryTheory.shiftFunctor (DerivedCategory.Bounded C) k).comp (derivedCompressionFunctor n) ≅ derivedCompressionFunctor n

The compression functor D^b(C) ⥤ D_n(C) is invariant under the shift by a multiple k of n. It is induced, along the localization functor K^b(C) ⥤ D^b(C), by the periodicity isomorphism of the compression functor K^b(C) ⥤ K_n(C).

@[simp]

theorem TauCeti.PeriodicComplex.derivedCompressionFunctorPeriodicityIso_hom_app_Qh_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) [HasDerivedCategory C] (k : ℤ) (hk : ↑k = 0) (K : HomotopyCategory.Bounded C) : (derivedCompressionFunctorPeriodicityIso n k hk).hom.app ((DerivedCategory.Bounded.Qh C).obj K) = CategoryTheory.CategoryStruct.comp ((derivedCompressionFunctor n).map ((CategoryTheory.Functor.commShiftIso (DerivedCategory.Bounded.Qh C) k).inv.app K)) (CategoryTheory.CategoryStruct.comp ((derivedCompressionFunctorFactors n).hom.app (K⟦k⟧)) (CategoryTheory.CategoryStruct.comp ((DerivedCategory.Qh C n).map ((homotopyCompressionFunctorPeriodicityIso n k hk).hom.app K)) ((derivedCompressionFunctorFactors n).inv.app K)))

On the image of a bounded homotopy class, the periodicity isomorphism of D^b(C) ⥤ D_n(C) is the image of the periodicity isomorphism of K^b(C) ⥤ K_n(C), conjugated by the identifications derivedCompressionFunctorFactors of the two compressions.

@[simp]

theorem TauCeti.PeriodicComplex.derivedCompressionFunctorPeriodicityIso_inv_app_Qh_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) [HasDerivedCategory C] (k : ℤ) (hk : ↑k = 0) (K : HomotopyCategory.Bounded C) : (derivedCompressionFunctorPeriodicityIso n k hk).inv.app ((DerivedCategory.Bounded.Qh C).obj K) = CategoryTheory.CategoryStruct.comp ((derivedCompressionFunctorFactors n).hom.app K) (CategoryTheory.CategoryStruct.comp ((DerivedCategory.Qh C n).map ((homotopyCompressionFunctorPeriodicityIso n k hk).inv.app K)) (CategoryTheory.CategoryStruct.comp ((derivedCompressionFunctorFactors n).inv.app (K⟦k⟧)) ((derivedCompressionFunctor n).map ((CategoryTheory.Functor.commShiftIso (DerivedCategory.Bounded.Qh C) k).hom.app K))))

On the image of a bounded homotopy class, the inverse of the periodicity isomorphism of D^b(C) ⥤ D_n(C) is the image of the inverse periodicity isomorphism of K^b(C) ⥤ K_n(C), conjugated by the identifications derivedCompressionFunctorFactors of the two compressions.

@[reducible, inline]

noncomputable abbrev TauCeti.PeriodicComplex.orbitDerivedCompressionFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) [HasDerivedCategory C] : CategoryTheory.Functor (OrbitCategory (DerivedCategory.Bounded C) ↑n) (DerivedCategory C n)

The orbit functor D^b(C)/[n] ⥤ D_n(C): the descent of the compression functor D^b(C) ⥤ D_n(C) to the orbit category, along its periodicity isomorphism for the shift by n. It restricts to compression along the projection D^b(C) ⥤ D^b(C)/[n] (TauCeti.OrbitCategory.projectionCompLift).

noncomputable def TauCeti.PeriodicComplex.orbitDerivedCompressionFunctorFactors {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) [HasDerivedCategory C] : (OrbitCategory.map (DerivedCategory.Bounded.Qh C)).comp (orbitDerivedCompressionFunctor n) ≅ (orbitCompressionFunctor n).comp (DerivedCategory.Qh C n)

The orbit functor D^b(C)/[n] ⥤ D_n(C) is induced by the orbit functor K^b(C)/[n] ⥤ K_n(C): the functor K^b(C)/[n] ⥤ D^b(C)/[n] induced by the localization K^b(C) ⥤ D^b(C), followed by the derived orbit functor, is the homotopy orbit functor followed by the localization K_n(C) ⥤ D_n(C). On components it is derivedCompressionFunctorFactors.

@[simp]

theorem TauCeti.PeriodicComplex.orbitDerivedCompressionFunctorFactors_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) [HasDerivedCategory C] (K : HomotopyCategory.Bounded C) : (orbitDerivedCompressionFunctorFactors n).hom.app { obj := K } = (derivedCompressionFunctorFactors n).hom.app K

The component of orbitDerivedCompressionFunctorFactors at a bounded homotopy class is the component of derivedCompressionFunctorFactors.

@[simp]

theorem TauCeti.PeriodicComplex.orbitDerivedCompressionFunctorFactors_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) [HasDerivedCategory C] (K : HomotopyCategory.Bounded C) : (orbitDerivedCompressionFunctorFactors n).inv.app { obj := K } = (derivedCompressionFunctorFactors n).inv.app K

The inverse component of orbitDerivedCompressionFunctorFactors at a bounded homotopy class is the inverse component of derivedCompressionFunctorFactors.