Complexes of projective modules over a principal ideal domain #
Let K be a homological complex of modules over a principal ideal ring k without zero divisors,
of any shape. Every module injecting into a projective k-module is free
(Module.Free.of_injective_of_projective_of_isPrincipalIdealRing). So when the term Kᵢ is
projective, its cycles Zᵢ are free, hence projective. When the term Kⱼ after Kᵢ is
projective, the boundaries Bⱼ ⊆ Kⱼ are projective, so the short exact sequence
0 ⟶ Zᵢ ⟶ Kᵢ ⟶ Bⱼ ⟶ 0 splits and the cycles split off Kᵢ.
These are the hypotheses of the universal coefficient sequence
(TauCeti.ChainComplex.exact_extToHomology_kronecker), so it applies to every complex of free
abelian groups, for instance to singular chains with integer coefficients. The splitting of
complexes (HomologicalComplex.exists_homotopyEquiv_d_eq_zero) additionally needs the homology to
split off the cycles, which holds when the homology is projective
(HomologicalComplex.isSplitEpi_homologyπ_of_projective). Over a field the cycles split off for
the simpler reason that all modules are semisimple (TauCeti.Algebra.Homology.Semisimple).
Main results #
HomologicalComplex.free_cycles_of_isPrincipalIdealRing: the cycles of a projective term are free.HomologicalComplex.isSplitMono_iCycles_of_isPrincipalIdealRing: the cycles split off a term when the next term is projective.HomologicalComplex.free_cokernel_iCycles_of_isPrincipalIdealRing: the quotient of a term by its cycles is free when the next term is projective.
References #
- C. Weibel, An Introduction to Homological Algebra, Section 3.6, where the same splitting gives the Künneth and universal coefficient theorems for complexes of free abelian groups.
Over a principal ideal ring without zero divisors, the cycles of a projective term of a complex of modules are free.
Over a principal ideal ring without zero divisors, the inclusion of the cycles into a term of a complex of modules is a split monomorphism when the next term is projective: the differential maps the term onto the boundaries, which are projective as a submodule of the next term.
Over a principal ideal ring without zero divisors, the quotient of a term of a complex of modules by its cycles is free when the next term is projective: the differential embeds the quotient into the next term.