hgrpIso
plain-language theorem explainer
A homotopy equivalence of spaces induces a canonical isomorphism on singular homology with integer coefficients in every degree. Anyone transporting vanishing or freeness statements across sphere complements, suspensions, or two-point punctures cites this. The body is a one-line retyping of the layer-1 singular-homology functoriality lemma.
Claim. Given a homotopy equivalence $h:X\simeq Y$ of topological spaces and any degree $k\in\mathbb{N}$, there is a canonical isomorphism $H_k(X;\mathbb{Z})\cong H_k(Y;\mathbb{Z})$ of $\mathbb{Z}$-modules.
background
In this module, $H_k(X)$ (written Hgrp) is the degree-$k$ singular homology of a space $X$ with coefficients in $\mathbb{Z}$, obtained from the singular chain complex. The ambient setting is the geometry of singular spheres and their open covers (north/south punctured hemispheres), used to run Mayer-Vietoris and suspension arguments.
Upstream, the layer-1 lemma states that a homotopy equivalence of spaces induces an isomorphism on singular homology with $\mathbb{Z}$ coefficients: the singular-homology functor sends homotopy equivalences to isomorphisms of modules. The present declaration simply retypes that isomorphism into the local Hgrp abbreviation so downstream sphere and linking arguments can apply it without unpacking the functor.
Homotopy invariance is the standard algebraic-topology fact that continuous maps homotopic induce the same map on homology, and invertible-up-to-homotopy maps therefore give isomorphisms.
proof idea
One-line wrapper: apply the upstream definition homotopyEquiv_homology_iso to the given homotopy equivalence $h$ and degree $k$. No extra algebraic work; the result is exactly that isomorphism, viewed as an iso of Hgrp modules.
why it matters
This is the transport lemma for all homology computations on spheres and their complements in the SingularSphereGeometry layer. Downstream, the suspension isomorphism builds $H_{k+2}(S^{n+1})\cong H_{k+1}(S^n)$ by composing a Mayer-Vietoris connecting map with a homotopy equivalence of the equatorial intersection, and needs this iso to identify the intersection homology with that of $S^n$.
In LinkingVanishingHighDim it moves vanishing statements across two-point complements: $H_2(S^n\setminus{p,q})=0$ is obtained by transporting sphere-homology vanishing along the homotopy equivalence of the two-point complement. That feeds the abstract two-arc Mayer-Vietoris argument and the high-dimensional linking non-detection theorem (no embedded circle in $S^D$ for $D\neq 3$ has homologically nontrivial complement, conditional on arc-frontier acyclicity). It also supports the Stage D fact that spheres of different dimension are not homotopy equivalent, via homology rank mismatch.
In the Recognition forcing chain this sits under the geometric side of $D=3$ (T8): homology of sphere complements is how linking and dimension enter the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.