Unfolding periodic complexes

Unfolding repeats a cyclically indexed complex along the integers. In degree i, the unfolded complex has the term indexed by the residue of i, and its differential is the corresponding cyclic differential. Differentials between nonconsecutive integers are zero, even if their residues are consecutive.

The unfolding functor preserves homotopies and compares ordinary homology in degree i with cyclic homology in degree i mod n. It preserves and reflects acyclicity and quasi-isomorphisms. This allows an exact periodic tail to be used as an ordinary complex. The construction also works for n = 0, when ZMod 0 is integer indexing; only positive n describes a finite period.

References

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

The complex constructor and short-complex homology comparisons are Mathlib's CochainComplex.of and HomologicalComplex.homologyFunctorIso'.

@[implicit_reducible]

def TauCeti.PeriodicComplex.unfoldFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Functor (HomologicalComplex C (ComplexShape.up (ZMod n))) (CochainComplex C ℤ)

Repeat a ZMod n-indexed complex along the integers, retaining only consecutive integer differentials.

@[simp]

theorem TauCeti.PeriodicComplex.unfoldFunctor_obj_X (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C (ComplexShape.up (ZMod n))) (i : ℤ) : ((unfoldFunctor C n).obj K).X i = K.X ↑i

Unfolding reads the term at the residue of the integer degree.

@[simp]

theorem TauCeti.PeriodicComplex.unfoldFunctor_obj_d (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C (ComplexShape.up (ZMod n))) (i : ℤ) : ((unfoldFunctor C n).obj K).d i (i + 1) = K.d ↑i ↑(i + 1)

The consecutive differential of the unfolding is the cyclic differential.

theorem TauCeti.PeriodicComplex.unfoldFunctor_obj_d_of_add_one_eq (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C (ComplexShape.up (ZMod n))) {i i' : ℤ} (h : i + 1 = i') : ((unfoldFunctor C n).obj K).d i i' = K.d ↑i ↑i'

A consecutive differential of the unfolding is the cyclic differential, with the target degree given by any integer equal to the successor of the source degree.

@[simp]

theorem TauCeti.PeriodicComplex.unfoldFunctor_map_f (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C (ComplexShape.up (ZMod n))} (f : K ⟶ L) (i : ℤ) : ((unfoldFunctor C n).map f).f i = f.f ↑i

Unfolding reads a morphism at the residue of the integer degree.

instance TauCeti.PeriodicComplex.instFaithfulHomologicalComplexZModUpCochainComplexIntUnfoldFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Limits.HasZeroMorphisms C] : (unfoldFunctor C n).Faithful

instance TauCeti.PeriodicComplex.instHasHomologyIntObjHomologicalComplexZModUpCochainComplexUnfoldFunctorOfCast (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C (ComplexShape.up (ZMod n))) (i : ℤ) [K.HasHomology ↑i] : HomologicalComplex.HasHomology ((unfoldFunctor C n).obj K) i

Homology at a cyclic degree supplies homology at each integer degree lying over it.

noncomputable def TauCeti.PeriodicComplex.unfoldHomologyIso (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] (i : ℤ) : (unfoldFunctor C n).comp (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) i) ≅ HomologicalComplex.homologyFunctor C (ComplexShape.up (ZMod n)) ↑i

Ordinary homology of the unfolding is cyclic homology at the residue of the degree.

@[simp]

theorem TauCeti.PeriodicComplex.unfoldFunctor_exactAt_iff (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C (ComplexShape.up (ZMod n))) (i : ℤ) : HomologicalComplex.ExactAt ((unfoldFunctor C n).obj K) i ↔ K.ExactAt ↑i

Unfolding preserves and reflects exactness at the corresponding residue.

@[simp]

theorem TauCeti.PeriodicComplex.unfoldFunctor_acyclic_iff (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C (ComplexShape.up (ZMod n))) : HomologicalComplex.Acyclic ((unfoldFunctor C n).obj K) ↔ K.Acyclic

The unfolding is acyclic exactly when the cyclic complex is acyclic.

@[simp]

theorem TauCeti.PeriodicComplex.unfoldFunctor_quasiIsoAt_iff (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C (ComplexShape.up (ZMod n))} (f : K ⟶ L) (i : ℤ) [K.HasHomology ↑i] [L.HasHomology ↑i] : QuasiIsoAt ((unfoldFunctor C n).map f) i ↔ QuasiIsoAt f ↑i

Unfolding preserves and reflects quasi-isomorphisms at the corresponding residue.

@[simp]

theorem TauCeti.PeriodicComplex.unfoldFunctor_quasiIso_iff (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C (ComplexShape.up (ZMod n))} (f : K ⟶ L) [∀ (j : ZMod n), K.HasHomology j] [∀ (j : ZMod n), L.HasHomology j] : QuasiIso ((unfoldFunctor C n).map f) ↔ QuasiIso f

A cyclic map is a quasi-isomorphism exactly when its unfolding is one.

instance TauCeti.PeriodicComplex.instAdditiveHomologicalComplexZModUpCochainComplexIntUnfoldFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Preadditive C] : (unfoldFunctor C n).Additive

instance TauCeti.PeriodicComplex.instLinearHomologicalComplexZModUpCochainComplexIntUnfoldFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) [CategoryTheory.Preadditive C] {R : Type u_1} [Semiring R] [CategoryTheory.Linear R C] : CategoryTheory.Functor.Linear R (unfoldFunctor C n)

noncomputable def Homotopy.unfoldPeriodic {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {n : ℕ} {K L : HomologicalComplex C (ComplexShape.up (ZMod n))} {f g : K ⟶ L} (h : Homotopy f g) : Homotopy ((TauCeti.PeriodicComplex.unfoldFunctor C n).map f) ((TauCeti.PeriodicComplex.unfoldFunctor C n).map g)

Repeat a cyclic homotopy along the integers, with zero components outside degree -1. The resulting homotopy witnesses invariance of unfolding under cyclic chain homotopies.

@[simp]

theorem Homotopy.unfoldPeriodic_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {n : ℕ} {K L : HomologicalComplex C (ComplexShape.up (ZMod n))} {f g : K ⟶ L} (h : Homotopy f g) (i : ℤ) : h.unfoldPeriodic.hom (i + 1) i = h.hom ↑(i + 1) ↑i

The consecutive component of an unfolded homotopy is the original cyclic component.

@[implicit_reducible]

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

Unfolding descends to the cyclic homotopy category because it preserves homotopies.

@[simp]

theorem TauCeti.PeriodicComplex.unfoldHomotopyFunctor_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) (K : HomologicalComplex C (ComplexShape.up (ZMod n))) : (unfoldHomotopyFunctor C n).obj ((HomotopyCategory.quotient C (ComplexShape.up (ZMod n))).obj K) = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj ((unfoldFunctor C n).obj K)

The class of an unfolded object is the unfolding of its cyclic homotopy class.

@[simp]

theorem TauCeti.PeriodicComplex.unfoldHomotopyFunctor_map (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) {K L : HomologicalComplex C (ComplexShape.up (ZMod n))} (f : K ⟶ L) : (unfoldHomotopyFunctor C n).map ((HomotopyCategory.quotient C (ComplexShape.up (ZMod n))).map f) = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map ((unfoldFunctor C n).map f)

On a represented map, homotopy-category unfolding is the class of its unfolding.

theorem TauCeti.PeriodicComplex.quotient_comp_unfoldHomotopyFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) : (HomotopyCategory.quotient C (ComplexShape.up (ZMod n))).comp (unfoldHomotopyFunctor C n) = (unfoldFunctor C n).comp (HomotopyCategory.quotient C (ComplexShape.up ℤ))

Unfolding commutes with passage to homotopy classes.

instance TauCeti.PeriodicComplex.instAdditiveHomotopyCategoryZModUpIntUnfoldHomotopyFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) : (unfoldHomotopyFunctor C n).Additive

instance TauCeti.PeriodicComplex.instLinearHomotopyCategoryZModUpIntUnfoldHomotopyFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) {R : Type u_1} [Semiring R] [CategoryTheory.Linear R C] : CategoryTheory.Functor.Linear R (unfoldHomotopyFunctor C n)