Chain-homotopy implies equality on singular homology

Specializes Mathlib's Homotopy.homologyMap_eq to the integral singular chain and homology functors. The theorem consumes an explicit chain homotopy; the prism-operator modules construct that chain homotopy from a topological homotopy.

@[reducible, inline]

noncomputable abbrev SphereOddDegree.singularChainℤ : CategoryTheory.Functor TopCat (ChainComplex (ModuleCat ℤ) ℕ)

The integral singular chain complex functor TopCat ⥤ ChainComplex (ModuleCat ℤ) ℕ, i.e. singularChainComplexFunctor specialised to coefficients ℤ.

Equations

• SphereOddDegree.singularChainℤ = (AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj ↧ℤ

@[reducible, inline]

noncomputable abbrev SphereOddDegree.singularHomologyℤ (n : ℕ) : CategoryTheory.Functor TopCat (ModuleCat ℤ)

The n-th integral singular homology functor TopCat ⥤ ModuleCat ℤ, i.e. singularHomologyFunctor specialised to coefficients ℤ.

Equations

• SphereOddDegree.singularHomologyℤ n = (AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj ↧ℤ

theorem SphereOddDegree.singularHomologyMap_eq_of_singularChainHomotopy {X Y : TopCat} {f g : X ⟶ Y} (H : Homotopy (singularChainℤ.map f) (singularChainℤ.map g)) (n : ℕ) : (singularHomologyℤ n).map f = (singularHomologyℤ n).map g

Reduction lemma via the prism operator.

If the singular chain maps induced by two continuous maps f, g : X ⟶ Y are chain-homotopic, then the induced maps on the n-th integral singular homology are equal.

The chain homotopy H is a hypothesis: this is the reusable step that turns the required prism operator (ContinuousMap.Homotopy → Homotopy (chain maps)) into homotopy invariance of singular homology, via Homotopy.homologyMap_eq. It is therefore not a homotopy-invariance theorem on its own.