chainHomotopyEquiv
plain-language theorem explainer
A continuous homotopy equivalence of topological spaces lifts to a chain-homotopy equivalence of their singular chain complexes with integer coefficients. Algebraic topologists cite this when passing from space-level equivalences to homology isomorphisms. The construction sends each leg of the equivalence to the induced singular chain map and fills the two composition identities with prism-operator chain homotopies.
Claim. If $h\colon X\simeq Y$ is a continuous homotopy equivalence of spaces, then the induced singular chain maps give a homotopy equivalence of chain complexes $SC(X)\simeq SC(Y)$ in $\mathrm{Ch}(\mathbf{Mod}_{\mathbb{Z}})$, where $SC(-)$ denotes the singular chain complex with $\mathbb{Z}$ coefficients.
background
The module works in the Mathlib singular-homology setting: for a space $X$ in $\mathbf{Top}$, $SC(X)$ is the singular chain complex with coefficients in $\mathbb{Z}$, obtained by applying the singular chain complex functor. A continuous map $f\colon X\to Y$ induces a chain map $SC(X)\to SC(Y)$ by functoriality of that construction.
A continuous homotopy between two maps $F_0,F_1\colon X\to Y$ produces, via the classical prism operator on singular simplices, a chain homotopy between the induced chain maps. That prism construction is packaged here as the upstream prismHomotopy result: "A homotopy of continuous maps induces a chain homotopy of the induced maps of singular chain complexes, via the prism operator."
A homotopy equivalence of spaces supplies continuous maps both ways together with homotopies witnessing that the two composites are homotopic to the respective identities. The present definition assembles those data into a homotopy equivalence of chain complexes.
proof idea
Definitional construction, not a tactic proof. The forward chain map is the singular chain map of the forward continuous map of $h$; the inverse chain map is the singular chain map of the continuous inverse.
For the composite-to-identity homotopies: each side starts from functoriality of the singular chain functor (composition of continuous maps becomes composition of chain maps, and the identity map becomes the identity chain map), then inserts prismHomotopy applied to the continuous homotopy that $h$ supplies for the left (resp. right) inverse law, and finishes by transporting across the identity-map equation. The two directions are symmetric.
why it matters
This is the chain-level bridge from space homotopy equivalences to singular homology isomorphisms. Downstream, homotopyEquiv_homology_iso builds the degree-$n$ homology isomorphism from this chain homotopy equivalence, and isIso_homology_map_of_homotopyEquiv records that the forward map on homology is an isomorphism in the categorical sense.
In the Recognition Science foundation stack, singular homology is part of the topological toolkit used to control discrete recognition structure (octave/tick combinatorics and dimensional forcing sit nearby in the forcing chain). The declaration itself is classical AT infrastructure: it does not invoke the $J$-cost, $\varphi$-ladder, or T5–T8 uniqueness statements, but it closes the standard path from continuous homotopy type to integer homology type inside the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.