Commit 2026-03-30 09:56 f71a4059

feat(AlgebraicTopology): homotopy invariance of singular homology (#37091) This PR completes the proof of the homotopy invariance of singular homology. In #32881, Fabian Odermatt added the definition of "combinatorial" homotopies of morphisms between simplicial objects and showed that in the case of preadditive categories, these homotopies induce chain homotopies on the alternating face map complexes. In #33683, it was shown that an "ordinary" homotopy of simplicial sets (defined using a morphism X ⊗ Δ[1] ⟶ Y) induces a combinatorial homotopy of simplicial sets. Here, we show that a homotopy between morphisms in the category of topological spaces induces a homotopy between the corresponding morphisms on the associated singular simplicial sets. The homotopy invariance of singular homology follows from the combination of these facts. This result was first formalized in Lean 3 in 2022 by Brendan Seamus Murphy.