The Künneth theorem for singular homology over a field and with projective homology #

For topological spaces X and Y and coefficient objects R and S, the homology cross products Hₚ(X; R) ⊗ H_q(Y; S) ⟶ Hₙ(X × Y; R ⊗ S) with p + q = n (TopCat.singularHomologyCross) assemble into the Künneth map

⨁_{p + q = n} Hₚ(X; R) ⊗ H_q(Y; S) ⟶ Hₙ(X × Y; R ⊗ S),

whose source is the degree n part of the tensor product of the graded objects H(X; R) and H(Y; S). It is the algebraic Künneth map HomologicalComplex.homologyKunneth of the singular chain complexes followed by the map induced by the shuffle map, and it is natural in both spaces and in both coefficient objects. Since the shuffle map is a chain homotopy equivalence (Eilenberg–Zilber), the Künneth map is an isomorphism exactly when the algebraic Künneth map of the singular chain complexes is.

For modules M and N over a commutative ring k, the algebraic Künneth map is an isomorphism when the cycles of the singular chain complexes C(X; M) and C(Y; N) split off their terms and their homology splits off their cycles (HomologicalComplex.isIso_homologyKunneth_of_isSplitMono_of_isSplitEpi). This gives the Künneth theorem: the cross product induces an isomorphism

⨁_{p + q = n} Hₚ(X; M) ⊗ H_q(Y; N) ≅ Hₙ(X × Y; M ⊗ N).

The splitting hypotheses hold in two standard situations.

For semisimple modules M and N, the singular chain modules Cₙ(X; M) = ⨁ M and Cₙ(Y; N) = ⨁ N are semisimple, so every submodule splits off. Over a commutative semisimple ring k, for instance a field, every module is semisimple, and with M = N = k, along the unitor k ⊗ k ≅ k, this is the classical form ⨁_{p + q = n} Hₚ(X; k) ⊗ H_q(Y; k) ≅ Hₙ(X × Y; k).
When the cycles split off and the homology modules Hₚ(X; M) and H_q(Y; N) are projective, the projection of the cycles onto the homology splits (TopCat.isIso_singularHomologyKunneth_of_projective). With projective M and N, for instance M = N = k, the singular chain modules are projective (SSet.projective_chainComplex_X), and the cycles split off in two cases. Over a principal ideal domain the boundaries are submodules of the projective chain modules (HomologicalComplex.isSplitMono_iCycles_of_isPrincipalIdealRing). Over any commutative ring they split off once the homology is projective, by induction on the degree (ChainComplex.isSplitMono_iCycles_of_projective_homology). So over any commutative ring the Künneth map is an isomorphism when the homology of X and Y is projective (TopCat.isIso_singularHomologyKunneth_of_projective_homology), for instance free, as for products of spheres.

Over any commutative ring, with projective coefficients, it follows that Hₙ(X × Y; M ⊗ N) is free whenever the homology modules of X and Y are, of finite rank ∑_{p + q = n} rank Hₚ(X; M) · rank H_q(Y; N) when the factors have finite rank.

Main definitions and results #

TopCat.singularHomologyKunneth: the Künneth map, characterized on summands by TopCat.ι_singularHomologyKunneth.
TopCat.singularHomologyKunneth_naturality and TopCat.singularHomologyKunneth_coefficient_naturality: naturality in the spaces and in the coefficients.
TopCat.isIso_singularHomologyKunneth_iff: the Künneth map is an isomorphism exactly when the algebraic Künneth map of the singular chain complexes is.
TopCat.singularHomologyKunnethIso: the Künneth isomorphism when the cycles and the homology of the singular chain complexes split off, for instance for all coefficient modules over a field.
TopCat.isIso_singularHomologyKunneth_of_projective: the Künneth theorem when the cycles split off and the homology is projective.
TopCat.isIso_singularHomologyKunneth_of_projective_homology: the Künneth theorem over any commutative ring, for projective coefficients and projective homology.
TopCat.isSplitMono_singularHomologyKunneth: the Künneth map is a split monomorphism when the cycles split off, for instance over a principal ideal domain.
TopCat.singularHomologyKunnethUnitIso: its form ⨁ Hₚ(X; k) ⊗ H_q(Y; k) ≅ Hₙ(X × Y; k) with coefficients in the ring itself.
TopCat.isZero_singularHomology_tensor: over a commutative semisimple ring, a product of spaces with vanishing positive-degree homology has vanishing positive-degree homology.
TopCat.free_singularHomology_tensor and TopCat.finrank_singularHomology_tensor: the homology of a product of spaces with free homology, over any commutative ring.

References #

A. Hatcher, Algebraic Topology, Section 3.B, the Künneth formula.
C. Weibel, An Introduction to Homological Algebra, Section 3.6, the Künneth formula.