noncomputable def EilenbergZilber.singularChainComplex {R : Type u} [CommRing R] (M : ModuleCat R) (X : TopCat) : ChainComplex (ModuleCat R) ℕ

The singular chain complex of a topological space $X$ with coefficients in an $R$-module $M$, viewed as a chain complex of $R$-modules.

noncomputable def EilenbergZilber.eilenbergZilber_homotopyEquiv {R : Type u} [CommRing R] (M : ModuleCat R) (X Y : TopCat) : HomotopyEquiv (HomologicalComplex.tensorObj (singularChainComplex M X) (singularChainComplex M Y)) (singularChainComplex M (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))

Theorem 25.13 (Eilenberg–Zilber theorem). There is a natural chain homotopy equivalence $$S_*(X; M) \otimes S_*(Y; M) \simeq S_*(X \times Y; M)$$ covering the canonical isomorphism in degree $0$. This packaged form provides both the forward (shuffle) map and a chain homotopy inverse (Alexander–Whitney), unique up to chain homotopy.

theorem EilenbergZilber.eilenbergZilber_unique {R : Type u} [CommRing R] (M : ModuleCat R) (X Y : TopCat) (φ fwd : HomologicalComplex.tensorObj (singularChainComplex M X) (singularChainComplex M Y) ⟶ singularChainComplex M (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) (hfwd : fwd = (eilenbergZilber_homotopyEquiv M X Y).hom) (hφ : HomologicalComplex.homologyMap φ 0 = HomologicalComplex.homologyMap fwd 0) : Nonempty (Homotopy φ fwd)

Uniqueness part of Theorem 25.13: any chain map $S_*(X; M) \otimes S_*(Y; M) \to S_*(X \times Y; M)$ that agrees with the Eilenberg–Zilber map on $H_0$ is chain homotopic to it. A direct consequence of the acyclic models theorem.

theorem EilenbergZilber.alexanderWhitney_unique {R : Type u} [CommRing R] (M : ModuleCat R) (X Y : TopCat) (ψ bwd : singularChainComplex M (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ⟶ HomologicalComplex.tensorObj (singularChainComplex M X) (singularChainComplex M Y)) (hbwd : bwd = (eilenbergZilber_homotopyEquiv M X Y).inv) (hψ : HomologicalComplex.homologyMap ψ 0 = HomologicalComplex.homologyMap bwd 0) : Nonempty (Homotopy ψ bwd)

Dual uniqueness statement to eilenbergZilber_unique: any chain map $S_*(X \times Y; M) \to S_*(X; M) \otimes S_*(Y; M)$ that agrees with the Alexander–Whitney map on $H_0$ is chain homotopic to it. Together with eilenbergZilber_unique this gives the uniqueness clause of Theorem 25.13.

theorem EilenbergZilber.eilenbergZilber_natural {R : Type u} [CommRing R] (M : ModuleCat R) {X X' Y Y' : TopCat} (f : X ⟶ X') (g : Y ⟶ Y') : CategoryTheory.CategoryStruct.comp (HomologicalComplex.tensorHom (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj M).map f) (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj M).map g)) (eilenbergZilber_homotopyEquiv M X' Y').hom = CategoryTheory.CategoryStruct.comp (eilenbergZilber_homotopyEquiv M X Y).hom (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj M).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))

Naturality of the Eilenberg–Zilber map: the forward map $S_*(X) \otimes S_*(Y) \to S_*(X \times Y)$ commutes with maps $f : X \to X'$ and $g : Y \to Y'$ on each side of the square.

noncomputable def EilenbergZilber.eilenbergZilberHomologyIso {R : Type u} [CommRing R] (M : ModuleCat R) (X Y : TopCat) (n : ℕ) : (HomologicalComplex.tensorObj (singularChainComplex M X) (singularChainComplex M Y)).homology n ≅ HomologicalComplex.homology (singularChainComplex M (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) n

Corollary 25.14. The induced isomorphism on homology from the Eilenberg–Zilber chain homotopy equivalence: $$H_n\bigl(S_*(X; M) \otimes S_*(Y; M)\bigr) \;\cong\; H_n(X \times Y; M).$$