Homotopy invariance of singular homology — unconditional

Combining the backported algebraic prism (CategoryTheory.SimplicialObject.Homotopy.toChainHomotopy, in Backports/SimplicialObjectChainHomotopy.lean) with the library's singular cylinder (PrismOperator.cylinder) assembled into a combinatorial simplicial homotopy (Backports/PrismSimplicialHomotopy.lean, prismHomotopy/singularChainHomotopyOfHomotopy), the prism-operator hypothesis SingularPrismOperator isolated in HomotopyInvariance.lean is a theorem.

Consequently every theorem there that was conditional on SingularPrismOperator is dischargeable, and the singular-homology homotopy-invariance results below are unconditional.

Integer coefficients (ModuleCat.{0} ℤ), the case relevant to the topological degree of sphere maps.

theorem SphereOddDegree.singularPrismOperator : SingularPrismOperator

The singular prism operator, discharged. The hypothesis SingularPrismOperator (isolated in HomotopyInvariance.lean) holds: it is witnessed by singularChainHomotopyOfHomotopy.

theorem SphereOddDegree.map_singularHomologyℤ_eq_of_homotopy {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) (n : ℕ) : (singularHomologyℤ n).map f = (singularHomologyℤ n).map g

Homotopy invariance of singular homology (unconditional, TopCat form). A topological homotopy between f, g : X ⟶ Y induces equal maps on the n-th integral singular homology.

theorem SphereOddDegree.map_singularHomologyℤ_eq_of_homotopic {X Y : TopCat} {f g : X ⟶ Y} (h : (TopCat.Hom.hom f).Homotopic (TopCat.Hom.hom g)) (n : ℕ) : (singularHomologyℤ n).map f = (singularHomologyℤ n).map g

Homotopy invariance of singular homology (unconditional, Homotopic form). Homotopic TopCat maps induce equal maps on integral singular homology.

theorem SphereOddDegree.map_singularHomologyℤ_eq_of_homotopic_continuousMap {X Y : TopCat} {f g : C(↑X, ↑Y)} (h : f.Homotopic g) (n : ℕ) : (singularHomologyℤ n).map (TopCat.ofHom f) = (singularHomologyℤ n).map (TopCat.ofHom g)

Homotopy invariance of singular homology (unconditional, C(X, Y) form). Homotopic continuous maps induce equal maps on integral singular homology.