Projective cycles and contractible complexes

This file collects the facts about cycles of complexes that are needed to show that complexes of projectives are homotopically projective in finite global dimension. The complexes may have any shape, possibly unbounded in both directions or cyclic.

• The cycles of a contractible complex are retracts of its terms; so they are projective when the terms are. This only needs a preadditive category. (A contractible complex is acyclic, Homotopy.acyclic; conversely, an acyclic complex whose cycles are projective is contractible, HomologicalComplex.Acyclic.nonempty_homotopy_id_zero_of_projective_cycles in TauCeti.Algebra.Homology.Split.)
• In an abelian category, a short exact sequence 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 of complexes with X₃ exact at a degree j induces a short exact sequence of cycles in degree j. When the cycles of X₂ in degree j have projective dimension < n, those of X₁ do as soon as those of X₃ have projective dimension < n + 1. In particular, when the cycles of X₂ are projective, those of X₁ are syzygies of those of X₃, and their projective dimension drops by one. Likewise, along an exact range of projectives the projective dimension of the cycles drops by one in each degree.
• With enough projectives, and when every index is both the source and the target of a relation of the shape, every complex receives a degreewise epimorphism from a contractible complex with projective terms, the mapping cone of the identity of a complex with zero differential made of projective presentations of the terms.

Iterating the last two points replaces an acyclic complex by acyclic complexes whose cycles have smaller and smaller projective dimension, until the cycles are projective.

Dually, the cycle sequences 0 ⟶ Zʲ ⟶ Kʲ ⟶ Zʲ⁺¹ ⟶ 0 with projective middle terms show that the cycles of a complex of projectives exact in degrees j + 1, …, j + d are d-th syzygies; in particular they have no higher extensions into objects of injective dimension at most d (CategoryTheory.ObjectProperty.IsSyzygy.ext_eq_zero_of_hasInjectiveDimensionLE).

Main results

• Homotopy.projective_cycles: the cycles of a contractible complex of projectives are projective.
• CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_cycles_X₁: dimension shifting for the cycles of a short exact sequence of complexes.
• HomologicalComplex.exists_projective_contractible_epi_f: when every index is both the source and the target of a relation, every complex is the target of a degreewise epimorphism from a contractible complex with projective terms.
• CochainComplex.hasProjectiveDimensionLT_cycles_of_add: dimension shifting for the projective dimension of the cycles along an exact range of projectives.
• CochainComplex.isSyzygy_cycles: the cycles of an exact range of projectives are syzygies.

References

• C. Weibel, An Introduction to Homological Algebra, Section 4.1 (dimension shifting).

theorem Homotopy.projective_cycles {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Preadditive C] {K : HomologicalComplex C c} (h : Homotopy (CategoryTheory.CategoryStruct.id K) 0) {i j : ι} (hij : c.Rel i j) [K.HasHomology j] [CategoryTheory.Projective (K.X i)] : CategoryTheory.Projective (K.cycles j)

In a contractible complex, the cycles in degree j are a retract of the term in degree i for every relation i → j; in particular they are projective when that term is.

theorem CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_cycles_X₁ {C : Type u_1} [Category.{v_1, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [Abelian C] {S : ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) {j : ι} (h₃ : S.X₃.ExactAt j) (n : ℕ) (h₂ : HasProjectiveDimensionLT (S.X₂.cycles j) n) (hZ : HasProjectiveDimensionLT (S.X₃.cycles j) (n + 1)) : HasProjectiveDimensionLT (S.X₁.cycles j) n

Let 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 be a short exact sequence of complexes where X₃ is exact at the degree j. It gives a short exact sequence 0 ⟶ Z(X₁) ⟶ Z(X₂) ⟶ Z(X₃) ⟶ 0 of cycles in degree j, so the cycles of X₁ have projective dimension < n when those of X₂ have projective dimension < n and those of X₃ have projective dimension < n + 1.

theorem HomologicalComplex.exists_projective_contractible_epi_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] (hc : ∀ (i : ι), ∃ (j : ι), c.Rel i j) (hc' : ∀ (j : ι), ∃ (i : ι), c.Rel i j) (L : HomologicalComplex C c) : ∃ (Q : HomologicalComplex C c) (π : Q ⟶ L), (∀ (i : ι), CategoryTheory.Projective (Q.X i)) ∧ (∀ (i : ι), CategoryTheory.Epi (π.f i)) ∧ Nonempty (Homotopy (CategoryTheory.CategoryStruct.id Q) 0)

In an abelian category with enough projectives, every complex is the target of a morphism which is an epimorphism in every degree, from a contractible complex with projective terms. The source is the mapping cone of the identity of a complex with zero differential, whose term in degree j is a projective presentation of Lᵢ for the relation i → j. Every index must be both the source and the target of a relation of the shape.

theorem CochainComplex.hasProjectiveDimensionLT_cycles_of_add {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K : CochainComplex C ℤ} (j : ℤ) (k : ℕ) (hproj : ∀ l < k, CategoryTheory.Projective (K.X (j + ↑l))) (hexact : ∀ l < k, HomologicalComplex.ExactAt K (j + ↑l + 1)) (p : ℕ) (h : CategoryTheory.HasProjectiveDimensionLT (HomologicalComplex.cycles K (j + ↑k)) (p + 1 + k)) : CategoryTheory.HasProjectiveDimensionLT (HomologicalComplex.cycles K j) (p + 1)

Dimension shifting for the cycles: if K has projective terms in degrees j, …, j + k - 1 and is exact in degrees j + 1, …, j + k, then the cycles of K in degree j have projective dimension < p + 1 whenever those in degree j + k have projective dimension < p + 1 + k, along the short exact sequences 0 ⟶ Zⁱ ⟶ Kⁱ ⟶ Zⁱ⁺¹ ⟶ 0.

theorem CochainComplex.isSyzygy_cycles {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K : CochainComplex C ℤ} (j : ℤ) (d : ℕ) (hproj : ∀ l < d, CategoryTheory.Projective (K.X (j + ↑l))) (hexact : ∀ l < d, HomologicalComplex.ExactAt K (j + ↑l + 1)) : (CategoryTheory.isProjective C).IsSyzygy d (HomologicalComplex.cycles K j)

Cycles of an exact range of projectives are syzygies: if K has projective terms in degrees j, …, j + d - 1 and is exact in degrees j + 1, …, j + d, then Zʲ is a d-th syzygy relative to the projective objects, along the short exact sequences 0 ⟶ Zˡ ⟶ Kˡ ⟶ Zˡ⁺¹ ⟶ 0.