Projective cycles over a category of projective dimension at most one

Suppose every object of an abelian category has projective dimension at most one. Then subobjects of projective objects are projective. For a homological complex, this makes the cycles and boundaries of a projective term projective. The quotient of a term by its cycles embeds into the next term, so it too is projective when that next term is projective.

These instances supply the projectivity hypotheses in the Künneth and universal coefficient sequences. The instance HomologicalComplex.isSplitMono_iCycles_of_projective then splits the inclusion of the cycles, supplying the splittings used by these sequences. No projectivity of homology is required, and the complex can have any shape.

The condition is expressed using Mathlib's CategoryTheory.HasProjectiveDimensionLE, without assuming the category has enough projectives. It holds for modules over a principal ideal domain by ModuleCat.hasProjectiveDimensionLE_one_of_isPrincipalIdealRing.

References

• C. Weibel, An Introduction to Homological Algebra, Sections 3.6 and 4.2.

instance HomologicalComplex.projective_cycles_of_hasProjectiveDimensionLE_one {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [∀ (X : C), CategoryTheory.HasProjectiveDimensionLE X 1] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [CategoryTheory.Projective (K.X i)] : CategoryTheory.Projective (K.cycles i)

If every object has projective dimension at most one, the cycles of a projective term are projective.

instance HomologicalComplex.projective_kernel_homologyπ_of_hasProjectiveDimensionLE_one {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [∀ (X : C), CategoryTheory.HasProjectiveDimensionLE X 1] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [CategoryTheory.Projective (K.X i)] : CategoryTheory.Projective (CategoryTheory.Limits.kernel (K.homologyπ i))

If every object has projective dimension at most one, the boundaries in a projective term are projective.

instance HomologicalComplex.projective_cokernel_iCycles_of_hasProjectiveDimensionLE_one {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [∀ (X : C), CategoryTheory.HasProjectiveDimensionLE X 1] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [CategoryTheory.Projective (K.X (c.next i))] : CategoryTheory.Projective (CategoryTheory.Limits.cokernel (K.iCycles i))

If every object has projective dimension at most one, the quotient of a term by its cycles is projective when the next term is projective. Consequently the cycles split off the term.