Compression and shifts

Periodic compression commutes with the cohomological shift. In residue degree r, the comparison reindexes the summand in integer degree i as the summand in degree i + k; the signs on the two differentials then agree. This compatibility is the shift datum needed to compare mapping-cone triangles before compression with periodic mapping-cone triangles.

The comparisons are coherent with the identifications X⟦0⟧ ≅ X and X⟦a + b⟧ ≅ X⟦a⟧⟦b⟧, so compression of bounded complexes commutes with the shift (TauCeti.PeriodicComplex.commShiftCompressionFunctor). Since the quotient functor from bounded complexes to their homotopy category is a localization functor, this compatibility descends to the compression functor K^b(C) ⥤ K_n(C) on homotopy categories (TauCeti.PeriodicComplex.commShiftHomotopyCompressionFunctor), compatibly with the quotient functors.

References

• T. Stai, The triangulated hull of periodic complexes, Mathematical Research Letters 25 (2018), 199–236, Section 3.3.

instance TauCeti.PeriodicComplex.hasCompression_shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (K : CochainComplex C ℤ) (k : ℤ) [HasCompression n K] : HasCompression n (K⟦k⟧)

A shift of a complex with an n-periodic compression again has an n-periodic compression.

noncomputable def TauCeti.PeriodicComplex.compressionShiftXIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (K : CochainComplex C ℤ) (k : ℤ) [HasCompression n K] (r : ZMod n) : (compression n (K⟦k⟧)).X r ≅ compression n K⟦k⟧.X r

The degreewise isomorphism which reindexes the compression of a shifted complex by i ↦ i + k.

@[simp]

theorem TauCeti.PeriodicComplex.ιCompression_compressionShiftXIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (K : CochainComplex C ℤ) (k : ℤ) [HasCompression n K] (i : ℤ) (r : ZMod n) (hi : ↑i = r) : CategoryTheory.CategoryStruct.comp (ιCompression n (K⟦k⟧) i r hi) (compressionShiftXIso n K k r).hom = CategoryTheory.CategoryStruct.comp (K.shiftFunctorObjXIso k i (i + k) ⋯).hom (ιCompression n K (i + k) (r + ↑k) ⋯)

On a summand, the shift comparison is the inclusion whose degree has been translated by the shift.

@[simp]

theorem TauCeti.PeriodicComplex.ιCompression_compressionShiftXIso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (K : CochainComplex C ℤ) (k : ℤ) [HasCompression n K] (i : ℤ) (r : ZMod n) (hi : ↑i = r) {Z : C} (h : compression n K⟦k⟧.X r ⟶ Z) : CategoryTheory.CategoryStruct.comp (ιCompression n (K⟦k⟧) i r hi) (CategoryTheory.CategoryStruct.comp (compressionShiftXIso n K k r).hom h) = CategoryTheory.CategoryStruct.comp (K.shiftFunctorObjXIso k i (i + k) ⋯).hom (CategoryTheory.CategoryStruct.comp (ιCompression n K (i + k) (r + ↑k) ⋯) h)

On a summand, the shift comparison is the inclusion whose degree has been translated by the shift.

@[simp]

theorem TauCeti.PeriodicComplex.ιCompression_compressionShiftXIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (K : CochainComplex C ℤ) (k : ℤ) [HasCompression n K] (j : ℤ) (r : ZMod n) (hj : ↑j = r + ↑k) : CategoryTheory.CategoryStruct.comp (ιCompression n K j (r + ↑k) hj) (compressionShiftXIso n K k r).inv = CategoryTheory.CategoryStruct.comp (K.shiftFunctorObjXIso k (j - k) j ⋯).inv (ιCompression n (K⟦k⟧) (j - k) r ⋯)

On a summand, the inverse shift comparison is the inclusion whose degree has been translated back by the shift.

@[simp]

theorem TauCeti.PeriodicComplex.ιCompression_compressionShiftXIso_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (K : CochainComplex C ℤ) (k : ℤ) [HasCompression n K] (j : ℤ) (r : ZMod n) (hj : ↑j = r + ↑k) {Z : C} (h : (compression n (K⟦k⟧)).X r ⟶ Z) : CategoryTheory.CategoryStruct.comp (ιCompression n K j (r + ↑k) hj) (CategoryTheory.CategoryStruct.comp (compressionShiftXIso n K k r).inv h) = CategoryTheory.CategoryStruct.comp (K.shiftFunctorObjXIso k (j - k) j ⋯).inv (CategoryTheory.CategoryStruct.comp (ιCompression n (K⟦k⟧) (j - k) r ⋯) h)

On a summand, the inverse shift comparison is the inclusion whose degree has been translated back by the shift.

noncomputable def TauCeti.PeriodicComplex.compressionShiftIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (K : CochainComplex C ℤ) (k : ℤ) [HasCompression n K] : compression n (K⟦k⟧) ≅ compression n K⟦k⟧

Compression of a shifted complex is canonically isomorphic to the shift of its compression. The comparison reindexes the summands by translation and introduces no additional sign.

@[simp]

theorem TauCeti.PeriodicComplex.compressionShiftIso_hom_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (K : CochainComplex C ℤ) (k : ℤ) [HasCompression n K] (r : ZMod n) : (compressionShiftIso n K k).hom.f r = (compressionShiftXIso n K k r).hom

The component in residue degree r of the shift comparison is the reindexing isomorphism.

@[simp]

theorem TauCeti.PeriodicComplex.compressionShiftIso_inv_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (K : CochainComplex C ℤ) (k : ℤ) [HasCompression n K] (r : ZMod n) : (compressionShiftIso n K k).inv.f r = (compressionShiftXIso n K k r).inv

The inverse component in residue degree r is the inverse reindexing map.

theorem TauCeti.PeriodicComplex.compressionShiftIso_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (K : CochainComplex C ℤ) (k : ℤ) [HasCompression n K] {L : CochainComplex C ℤ} [HasCompression n L] (f : K ⟶ L) : CategoryTheory.CategoryStruct.comp (compressionMap n (f⟦k⟧')) (compressionShiftIso n L k).hom = CategoryTheory.CategoryStruct.comp (compressionShiftIso n K k).hom (compressionMap n f⟦k⟧')

The shift comparison is natural in the complex.

theorem TauCeti.PeriodicComplex.compressionShiftIso_hom_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (K : CochainComplex C ℤ) (k : ℤ) [HasCompression n K] {L : CochainComplex C ℤ} [HasCompression n L] (f : K ⟶ L) {Z : HomologicalComplex C (ComplexShape.up (ZMod n))} (h : compression n L⟦k⟧ ⟶ Z) : CategoryTheory.CategoryStruct.comp (compressionMap n (f⟦k⟧')) (CategoryTheory.CategoryStruct.comp (compressionShiftIso n L k).hom h) = CategoryTheory.CategoryStruct.comp (compressionShiftIso n K k).hom (CategoryTheory.CategoryStruct.comp (compressionMap n f⟦k⟧') h)

The shift comparison is natural in the complex.

theorem TauCeti.PeriodicComplex.compressionShiftIso_zero_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (K : CochainComplex C ℤ) [HasCompression n K] : (compressionShiftIso n K 0).hom = CategoryTheory.CategoryStruct.comp (compressionMap n ((CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K)) ((CategoryTheory.shiftFunctorZero (HomologicalComplex C (ComplexShape.up (ZMod n))) ℤ).inv.app (compression n K))

The shift comparison for the shift by zero is induced by the identifications X⟦0⟧ ≅ X.

theorem TauCeti.PeriodicComplex.compressionShiftIso_add_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (K : CochainComplex C ℤ) [HasCompression n K] (a b : ℤ) : (compressionShiftIso n K (a + b)).hom = CategoryTheory.CategoryStruct.comp (compressionMap n ((CategoryTheory.shiftFunctorAdd (CochainComplex C ℤ) a b).hom.app K)) (CategoryTheory.CategoryStruct.comp (compressionShiftIso n (K⟦a⟧) b).hom (CategoryTheory.CategoryStruct.comp ((compressionShiftIso n K a).hom⟦b⟧') ((CategoryTheory.shiftFunctorAdd (HomologicalComplex C (ComplexShape.up (ZMod n))) a b).inv.app (compression n K))))

The shift comparison for the shift by a + b is the composite of the comparisons for the shifts by a and by b, through the identifications X⟦a + b⟧ ≅ X⟦a⟧⟦b⟧.

noncomputable def TauCeti.PeriodicComplex.shiftCompressionFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) [CategoryTheory.Limits.HasFiniteCoproducts C] : CategoryTheory.Functor (CochainComplex.Bounded C) (HomologicalComplex C (ComplexShape.up (ZMod n)))

The compression of the shift by k of the underlying complex, as a functor on bounded complexes.

@[simp]

theorem TauCeti.PeriodicComplex.shiftCompressionFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) [CategoryTheory.Limits.HasFiniteCoproducts C] (K : CochainComplex.Bounded C) : (shiftCompressionFunctor n k).obj K = compression n (K.obj⟦k⟧)

The functor shiftCompressionFunctor sends a bounded complex to the compression of the shift of its underlying complex.

@[simp]

theorem TauCeti.PeriodicComplex.shiftCompressionFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) [CategoryTheory.Limits.HasFiniteCoproducts C] {K L : CochainComplex.Bounded C} (f : K ⟶ L) : (shiftCompressionFunctor n k).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (compressionMap n (f.hom⟦k⟧')) (CategoryTheory.eqToHom ⋯))

The functor shiftCompressionFunctor acts on a morphism by compressing the shift of the underlying chain map, after transporting along the object equations.

noncomputable def TauCeti.PeriodicComplex.shiftCompCompressionFunctorIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) [CategoryTheory.Limits.HasFiniteCoproducts C] : (CategoryTheory.shiftFunctor (CochainComplex.Bounded C) k).comp (compressionFunctor n) ≅ shiftCompressionFunctor n k

Compressing the shift of a bounded complex agrees, naturally in the complex, with compressing the shift of its underlying complex.

@[simp]

theorem TauCeti.PeriodicComplex.shiftCompCompressionFunctorIso_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) [CategoryTheory.Limits.HasFiniteCoproducts C] (K : CochainComplex.Bounded C) : (shiftCompCompressionFunctorIso n k).hom.app K = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (compressionMap n ((CategoryTheory.Functor.commShiftIso (CochainComplex.Bounded.ι C) k).hom.app K)) (CategoryTheory.eqToHom ⋯))

The forward component of shiftCompCompressionFunctorIso compresses the comparison between the underlying complex of the shift and the shift of the underlying complex.

@[simp]

theorem TauCeti.PeriodicComplex.shiftCompCompressionFunctorIso_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) [CategoryTheory.Limits.HasFiniteCoproducts C] (K : CochainComplex.Bounded C) : (shiftCompCompressionFunctorIso n k).inv.app K = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (compressionMap n ((CategoryTheory.Functor.commShiftIso (CochainComplex.Bounded.ι C) k).inv.app K)) (CategoryTheory.eqToHom ⋯))

The inverse component of shiftCompCompressionFunctorIso compresses the inverse comparison between the underlying complex of the shift and the shift of the underlying complex.

noncomputable def TauCeti.PeriodicComplex.compressionFunctorShiftIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) [CategoryTheory.Limits.HasFiniteCoproducts C] : (CategoryTheory.shiftFunctor (CochainComplex.Bounded C) k).comp (compressionFunctor n) ≅ (compressionFunctor n).comp (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) k)

Compression of bounded complexes commutes naturally with the shift by k.

@[simp]

theorem TauCeti.PeriodicComplex.compressionFunctorShiftIso_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) [CategoryTheory.Limits.HasFiniteCoproducts C] (K : CochainComplex.Bounded C) : (compressionFunctorShiftIso n k).hom.app K = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (compressionMap n ((CategoryTheory.Functor.commShiftIso (CochainComplex.Bounded.ι C) k).hom.app K)) (CategoryTheory.CategoryStruct.comp (compressionShiftIso n K.obj k).hom (CategoryTheory.eqToHom ⋯)))

The forward component of bounded shift compatibility is the composite of the underlying bounded-complex comparison with the shift comparison for compression.

@[simp]

theorem TauCeti.PeriodicComplex.compressionFunctorShiftIso_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) [CategoryTheory.Limits.HasFiniteCoproducts C] (K : CochainComplex.Bounded C) : (compressionFunctorShiftIso n k).inv.app K = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (compressionShiftIso n K.obj k).inv (CategoryTheory.CategoryStruct.comp (compressionMap n ((CategoryTheory.Functor.commShiftIso (CochainComplex.Bounded.ι C) k).inv.app K)) (CategoryTheory.eqToHom ⋯)))

The inverse component of bounded shift compatibility is the reverse composite of the underlying shift comparison and the inverse compression comparison.

theorem TauCeti.PeriodicComplex.compressionFunctorShiftIso_zero_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) [CategoryTheory.Limits.HasFiniteCoproducts C] (K : CochainComplex.Bounded C) : (compressionFunctorShiftIso n 0).hom.app K = CategoryTheory.CategoryStruct.comp ((compressionFunctor n).map ((CategoryTheory.shiftFunctorZero (CochainComplex.Bounded C) ℤ).hom.app K)) ((CategoryTheory.shiftFunctorZero (HomologicalComplex C (ComplexShape.up (ZMod n))) ℤ).inv.app ((compressionFunctor n).obj K))

The shift compatibility of bounded compression for the shift by zero is induced by the identifications X⟦0⟧ ≅ X.

theorem TauCeti.PeriodicComplex.compressionFunctorShiftIso_add_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) [CategoryTheory.Limits.HasFiniteCoproducts C] (a b : ℤ) (K : CochainComplex.Bounded C) : (compressionFunctorShiftIso n (a + b)).hom.app K = CategoryTheory.CategoryStruct.comp ((compressionFunctor n).map ((CategoryTheory.shiftFunctorAdd (CochainComplex.Bounded C) a b).hom.app K)) (CategoryTheory.CategoryStruct.comp ((compressionFunctorShiftIso n b).hom.app (K⟦a⟧)) (CategoryTheory.CategoryStruct.comp ((compressionFunctorShiftIso n a).hom.app K⟦b⟧') ((CategoryTheory.shiftFunctorAdd (HomologicalComplex C (ComplexShape.up (ZMod n))) a b).inv.app ((compressionFunctor n).obj K))))

The shift compatibility of bounded compression for the shift by a + b is the composite of the compatibilities for the shifts by a and by b, through the identifications X⟦a + b⟧ ≅ X⟦a⟧⟦b⟧.

@[instance_reducible]

noncomputable instance TauCeti.PeriodicComplex.commShiftCompressionFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) [CategoryTheory.Limits.HasFiniteCoproducts C] : (compressionFunctor n).CommShift ℤ

Compression of bounded complexes commutes with the shift: the comparisons compressionFunctorShiftIso are coherent with the identifications X⟦0⟧ ≅ X and X⟦a + b⟧ ≅ X⟦a⟧⟦b⟧.

@[simp]

theorem TauCeti.PeriodicComplex.compressionFunctor_commShiftIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (k : ℤ) [CategoryTheory.Limits.HasFiniteCoproducts C] : CategoryTheory.Functor.commShiftIso (compressionFunctor n) k = compressionFunctorShiftIso n k

The shift compatibility of bounded compression is compressionFunctorShiftIso.

@[instance_reducible]

noncomputable instance TauCeti.PeriodicComplex.instLiftingBoundedBoundedHomotopyCategoryZModUpQuotientInverseImageHomologicalComplexIntHomotopyEquivalencesιCompCompressionFunctorQuotientHomotopyCompressionFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (n : ℕ) : CategoryTheory.Localization.Lifting (HomotopyCategory.Bounded.quotient C) ((HomologicalComplex.homotopyEquivalences C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Bounded.ι C)) ((compressionFunctor n).comp (HomotopyCategory.quotient C (ComplexShape.up (ZMod n)))) (homotopyCompressionFunctor n)

The descended compression is induced, along the localization functor HomotopyCategory.Bounded.quotient C, by compression of bounded complexes.

@[instance_reducible]

noncomputable instance TauCeti.PeriodicComplex.commShiftHomotopyCompressionFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (n : ℕ) : (homotopyCompressionFunctor n).CommShift ℤ

The compression functor K^b(C) ⥤ K_n(C) commutes with the shift. Its shift compatibility is induced by that of compression of bounded complexes, along the localization functor HomotopyCategory.Bounded.quotient C.

instance TauCeti.PeriodicComplex.instCommShiftBoundedHomotopyCategoryZModUpHomFunctorQuotientCompHomotopyCompressionFunctorIsoInt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (n : ℕ) : CategoryTheory.NatTrans.CommShift (quotientCompHomotopyCompressionFunctorIso n).hom ℤ

The identification of the descended compression on the classes of bounded complexes with the classes of their compressions is compatible with the shifts.