Homogeneous components of morphisms between compressions

A morphism g : Δₙ K ⟶ Δₙ L between the n-periodic compressions of two integer-indexed complexes sends the summand Kⁱ of (Δₙ K)^r into the summands L^(i + k) with k divisible by n. For a fixed k, these pieces form a chain map K ⟶ L⟦k⟧ after the sign (-1)^(k * i) on the summand of degree i: this is the component TauCeti.PeriodicComplex.compressionComponent of degree k of g. It factors as the inclusion of K into the unfolding of its compression, the unfolding of g, and a projection from the unfolding of Δₙ L onto L⟦k⟧, so it is additive and carries homotopies to homotopies.

The component of degree k' of Δₙ f followed by the periodicity isomorphism Δₙ (L⟦k⟧) ≅ Δₙ L is f when k' = k and zero otherwise (TauCeti.PeriodicComplex.compressionComponent_compressionMap_comp_compressionPeriodicityIso_hom). Conversely, when only finitely many components can be nonzero, for instance for bounded K and L and positive n, every morphism Δₙ K ⟶ Δₙ L is the sum of its components, transported back along compression and periodicity (TauCeti.PeriodicComplex.sum_compressionMap_compressionComponent_comp). Thus the morphisms Δₙ K ⟶ Δₙ L are the finite sums of compressions of morphisms K ⟶ L⟦n * j⟧, and the same holds up to homotopy. This is the computation behind the full faithfulness of the orbit functor K^b(C)/[n] ⥤ K_n(C).

Main definitions

• TauCeti.PeriodicComplex.toUnfoldCompression: the inclusion K ⟶ unfold (Δₙ K).
• TauCeti.PeriodicComplex.fromUnfoldCompression: the signed projection unfold (Δₙ L) ⟶ L⟦k⟧.
• TauCeti.PeriodicComplex.compressionComponent: the component of degree k of a morphism between compressions.

References

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

noncomputable def TauCeti.PeriodicComplex.toUnfoldCompression {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (K : CochainComplex C ℤ) [HasCompression n K] : K ⟶ (unfoldFunctor C n).obj (compression n K)

The inclusion of a complex into the unfolding of its compression: in degree i, the inclusion of the summand of degree i into the term of residue i of the compression.

@[simp]

theorem TauCeti.PeriodicComplex.toUnfoldCompression_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (K : CochainComplex C ℤ) [HasCompression n K] (i : ℤ) : (toUnfoldCompression n K).f i = ιCompression n K i ↑i ⋯

noncomputable def TauCeti.PeriodicComplex.fromUnfoldCompression {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (L : CochainComplex C ℤ) [HasCompression n L] (k : ℤ) : (unfoldFunctor C n).obj (compression n L) ⟶ L⟦k⟧

The projection of the unfolding of the compression of L onto L⟦k⟧: in degree i, the projection of the term of residue i onto the summand of degree i + k, with the sign (-1)^(k * i). It is zero in every degree when k is not divisible by n.

@[simp]

theorem TauCeti.PeriodicComplex.fromUnfoldCompression_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (L : CochainComplex C ℤ) [HasCompression n L] (k i : ℤ) : (fromUnfoldCompression n L k).f i = (k * i).negOnePow • CategoryTheory.CategoryStruct.comp (πCompression n L (↑i) (i + k)) (L.shiftFunctorObjXIso k i (i + k) ⋯).inv

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

The component of degree k of a morphism g : Δₙ K ⟶ Δₙ L between compressions: the chain map K ⟶ L⟦k⟧ whose component in degree i is the piece Kⁱ ⟶ L^(i + k) of g, with the sign (-1)^(k * i). It is the inclusion of K into the unfolding of its compression, followed by the unfolding of g and the projection onto L⟦k⟧.

theorem TauCeti.PeriodicComplex.compressionComponent_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) {K L : CochainComplex C ℤ} [HasCompression n K] [HasCompression n L] (k : ℤ) (g : compression n K ⟶ compression n L) (i : ℤ) : ((compressionComponent n k) g).f i = (k * i).negOnePow • CategoryTheory.CategoryStruct.comp (ιCompression n K i ↑i ⋯) (CategoryTheory.CategoryStruct.comp (g.f ↑i) (CategoryTheory.CategoryStruct.comp (πCompression n L (↑i) (i + k)) (L.shiftFunctorObjXIso k i (i + k) ⋯).inv))

The component of degree k of g restricts, on the summand of degree i, to the piece of g with values in the summand of degree i + k, with the sign (-1)^(k * i).

noncomputable def TauCeti.PeriodicComplex.compressionComponentHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) {K L : CochainComplex C ℤ} [HasCompression n K] [HasCompression n L] (k : ℤ) {g g' : compression n K ⟶ compression n L} (h : Homotopy g g') : Homotopy ((compressionComponent n k) g) ((compressionComponent n k) g')

A homotopy between morphisms of compressions induces a homotopy between their components of any degree.

@[simp]

theorem TauCeti.PeriodicComplex.compressionComponent_compressionMap_comp_compressionPeriodicityIso_hom_of_ne {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {n : ℕ} {K L : CochainComplex C ℤ} [HasCompression n K] [HasCompression n L] {k k' : ℤ} (hk : ↑k = 0) (f : K ⟶ L⟦k⟧) (hkk' : k' ≠ k) : (compressionComponent n k') (CategoryTheory.CategoryStruct.comp (compressionMap n f) (compressionPeriodicityIso n L k hk).hom) = 0

The component of degree k' of the compression of f : K ⟶ L⟦k⟧, followed by the periodicity isomorphism, vanishes unless k' = k.

@[simp]

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

The component of degree k of the compression of f : K ⟶ L⟦k⟧, followed by the periodicity isomorphism Δₙ (L⟦k⟧) ≅ Δₙ L, is f.

theorem TauCeti.PeriodicComplex.sum_compressionMap_compressionComponent_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) {K L : CochainComplex C ℤ} [HasCompression n K] [HasCompression n L] [NeZero n] (g : compression n K ⟶ compression n L) (J : Finset ℤ) (hJ : ∀ (i j : ℤ), ¬CategoryTheory.Limits.IsZero (K.X i) → ¬CategoryTheory.Limits.IsZero (L.X (i + ↑n * j)) → j ∈ J) : ∑ j ∈ J, CategoryTheory.CategoryStruct.comp (compressionMap n ((compressionComponent n (↑n * j)) g)) (compressionPeriodicityIso n L (↑n * j) ⋯).hom = g

If the pieces Kⁱ ⟶ L^(i + n * j) can only be nonzero for j in a finite set J, a morphism Δₙ K ⟶ Δₙ L between compressions is the sum over J of the compressions of its components of degree n * j, followed by the periodicity isomorphisms.

theorem TauCeti.PeriodicComplex.exists_sum_compressionMap_compressionComponent_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) {K L : CochainComplex C ℤ} [HasCompression n K] [HasCompression n L] [NeZero n] (hK : CochainComplex.bounded C K) (hL : CochainComplex.bounded C L) (g : compression n K ⟶ compression n L) : ∃ (J : Finset ℤ), ∑ j ∈ J, CategoryTheory.CategoryStruct.comp (compressionMap n ((compressionComponent n (↑n * j)) g)) (compressionPeriodicityIso n L (↑n * j) ⋯).hom = g

A morphism Δₙ K ⟶ Δₙ L between the compressions of bounded complexes is a finite sum of the compressions of its components of degrees n * j, followed by the periodicity isomorphisms.