Homotopically projective periodic complexes

A cyclic cochain complex K is homotopically projective when every morphism from K to an acyclic cyclic complex is null-homotopic; equivalently, its class in the periodic homotopy category is left orthogonal to the acyclic objects. This is the periodic analogue of Mathlib's CochainComplex.IsKProjective. At period zero, when ZMod 0 is integer indexing, the two notions have the same definition.

Homotopically projective complexes are the ones on which passage from the periodic homotopy category to the periodic derived category loses no information: morphisms out of them into any object are the same in both categories, so the full subcategory of homotopically projective objects of the homotopy category embeds fully faithfully into the derived category, and a quasi-isomorphism between homotopically projective complexes is a homotopy equivalence.

The notion must be kept apart from acyclicity, contractibility, and projectivity of the terms. A complex is contractible exactly when it is both acyclic and homotopically projective (isHomotopicallyProjective_and_acyclic_iff). Projectivity of every term does not suffice: the differential module given by multiplication by ε on the dual numbers is acyclic, has a free underlying module, and is not contractible, so it is not homotopically projective (TauCeti.not_isHomotopicallyProjective_dualNumberPeriodicComplex).

Main definitions

• TauCeti.PeriodicComplex.IsHomotopicallyProjective: every morphism to an acyclic periodic complex is null-homotopic.

Main results

• TauCeti.PeriodicComplex.isHomotopicallyProjective_iff_leftOrthogonal: the definition as left orthogonality to the acyclic objects of the periodic homotopy category.
• TauCeti.PeriodicComplex.isHomotopicallyProjective_and_acyclic_iff: a periodic complex is contractible exactly when it is acyclic and homotopically projective.
• TauCeti.PeriodicComplex.IsHomotopicallyProjective.Qh_map_bijective: the periodic Verdier localization is bijective on morphisms out of a homotopically projective complex.
• TauCeti.PeriodicComplex.IsHomotopicallyProjective.quasiIso_iff: between homotopically projective complexes, quasi-isomorphisms are exactly the homotopy equivalences.
• TauCeti.PeriodicComplex.isHomotopicallyProjective_of_d_eq_zero: a complex with projective terms and zero differential is homotopically projective.
• TauCeti.PeriodicComplex.IsHomotopicallyProjective.of_splitting: homotopically projective complexes are closed under extensions that split in every degree.
• TauCeti.PeriodicComplex.nonempty_homotopy_zero_of_epi: a morphism from a complex of projectives to L is null-homotopic when L is covered by a contractible complex Q and every morphism from the shift of the source to the kernel of Q ⟶ L is null-homotopic.

The proofs follow Joël Riou's treatment of K-projective complexes in Mathlib.Algebra.Homology.HomotopyCategory.KProjective and Mathlib.Algebra.Homology.DerivedCategory.KProjective.

References

• T. Stai, The triangulated hull of periodic complexes, Mathematical Research Letters 25 (2018), 199–236, Section 3.
• N. Spaltenstein, Resolutions of unbounded complexes, Compositio Mathematica 65 (1988), 121–154.

class TauCeti.PeriodicComplex.IsHomotopicallyProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {n : ℕ} (K : CochainComplex C (ZMod n)) : Prop

A cyclic cochain complex K is homotopically projective if every morphism from K to an acyclic cyclic complex is null-homotopic. This is the periodic analogue of Mathlib's CochainComplex.IsKProjective.

• nonempty_homotopy_zero {L : CochainComplex C (ZMod n)} (f : K ⟶ L) : HomologicalComplex.Acyclic L → Nonempty (Homotopy f 0)

theorem TauCeti.PeriodicComplex.isHomotopicallyProjective_iff_leftOrthogonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {n : ℕ} (K : CochainComplex C (ZMod n)) : IsHomotopicallyProjective K ↔ (subcategoryAcyclic C n).leftOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up (ZMod n))).obj K)

A complex is homotopically projective exactly when its class in the periodic homotopy category admits no nonzero morphism to an acyclic object.

theorem TauCeti.PeriodicComplex.IsHomotopicallyProjective.leftOrthogonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {n : ℕ} (K : CochainComplex C (ZMod n)) [IsHomotopicallyProjective K] : (subcategoryAcyclic C n).leftOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up (ZMod n))).obj K)

The class of a homotopically projective complex is left orthogonal to the acyclic objects.

theorem HomotopyEquiv.isHomotopicallyProjective_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {n : ℕ} {K L : CochainComplex C (ZMod n)} (e : HomotopyEquiv K L) : TauCeti.PeriodicComplex.IsHomotopicallyProjective K ↔ TauCeti.PeriodicComplex.IsHomotopicallyProjective L

Homotopically projective complexes are invariant under homotopy equivalence.

instance TauCeti.PeriodicComplex.instIsHomotopicallyProjectiveObjCochainComplexZModShiftFunctorInt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {n : ℕ} (K : CochainComplex C (ZMod n)) [IsHomotopicallyProjective K] (k : ℤ) : IsHomotopicallyProjective (K⟦k⟧)

Homotopically projective complexes are stable under the integral shifts.

theorem TauCeti.PeriodicComplex.isHomotopicallyProjective_shift_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {n : ℕ} (K : CochainComplex C (ZMod n)) (k : ℤ) : IsHomotopicallyProjective (K⟦k⟧) ↔ IsHomotopicallyProjective K

A shift of a complex is homotopically projective exactly when the complex is.

theorem TauCeti.PeriodicComplex.isHomotopicallyProjective_of_homotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {n : ℕ} {K : CochainComplex C (ZMod n)} (h : Homotopy (CategoryTheory.CategoryStruct.id K) 0) : IsHomotopicallyProjective K

A contractible complex is homotopically projective.

theorem TauCeti.PeriodicComplex.isHomotopicallyProjective_and_acyclic_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {n : ℕ} (K : CochainComplex C (ZMod n)) : IsHomotopicallyProjective K ∧ HomologicalComplex.Acyclic K ↔ Nonempty (Homotopy (CategoryTheory.CategoryStruct.id K) 0)

A periodic complex is contractible exactly when it is acyclic and homotopically projective.

theorem TauCeti.PeriodicComplex.isHomotopicallyProjective_of_d_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {n : ℕ} {K : CochainComplex C (ZMod n)} [∀ (i : ZMod n), CategoryTheory.Projective (K.X i)] (hd : ∀ (i j : ZMod n), K.d i j = 0) : IsHomotopicallyProjective K

A periodic complex with projective terms and zero differential is homotopically projective.

theorem TauCeti.PeriodicComplex.IsHomotopicallyProjective.of_splitting {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {n : ℕ} (S : CategoryTheory.ShortComplex (CochainComplex C (ZMod n))) (hS : ∀ (i : ZMod n), Nonempty (S.map (HomologicalComplex.eval C (ComplexShape.up (ZMod n)) i)).Splitting) [IsHomotopicallyProjective S.X₁] [IsHomotopicallyProjective S.X₃] : IsHomotopicallyProjective S.X₂

Homotopically projective periodic complexes are closed under extensions that split in every degree. The splittings need not be compatible with the differentials.

theorem TauCeti.PeriodicComplex.nonempty_homotopy_zero_of_epi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {n : ℕ} {K L Q : CochainComplex C (ZMod n)} [∀ (i : ZMod n), CategoryTheory.Projective (K.X i)] (π : Q ⟶ L) [∀ (i : ZMod n), CategoryTheory.Epi (π.f i)] (hQ : Homotopy (CategoryTheory.CategoryStruct.id Q) 0) (hN : ∀ (u : K⟦-1⟧ ⟶ CategoryTheory.Limits.kernel π), Nonempty (Homotopy u 0)) (f : K ⟶ L) : Nonempty (Homotopy f 0)

A morphism f : K ⟶ L from a periodic complex of projectives is null-homotopic as soon as L is the target of a degreewise epimorphism π : Q ⟶ L from a contractible complex such that every morphism K⟦-1⟧ ⟶ ker π is null-homotopic.

theorem TauCeti.PeriodicComplex.IsHomotopicallyProjective.Qh_map_bijective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {n : ℕ} (K : CochainComplex C (ZMod n)) (L : HomotopyCategory C (ComplexShape.up (ZMod n))) [IsHomotopicallyProjective K] : Function.Bijective (DerivedCategory.Qh C n).map

Passage to the periodic derived category is bijective on morphisms out of a homotopically projective complex.

theorem TauCeti.PeriodicComplex.IsHomotopicallyProjective.quasiIso_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {n : ℕ} {K L : CochainComplex C (ZMod n)} [IsHomotopicallyProjective K] [IsHomotopicallyProjective L] (f : K ⟶ L) : QuasiIso f ↔ HomologicalComplex.homotopyEquivalences C (ComplexShape.up (ZMod n)) f

A morphism between homotopically projective complexes is a quasi-isomorphism exactly when it is a homotopy equivalence.

instance TauCeti.PeriodicComplex.DerivedCategory.instFullFullSubcategoryHomotopyCategoryZModUpLeftOrthogonalSubcategoryAcyclicCompιQh (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : ((subcategoryAcyclic C n).leftOrthogonal.ι.comp (Qh C n)).Full

The periodic Verdier localization is full on homotopically projective objects.

instance TauCeti.PeriodicComplex.DerivedCategory.instFaithfulFullSubcategoryHomotopyCategoryZModUpLeftOrthogonalSubcategoryAcyclicCompιQh (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ) : ((subcategoryAcyclic C n).leftOrthogonal.ι.comp (Qh C n)).Faithful

The periodic Verdier localization is faithful on homotopically projective objects.