suspensionIso
plain-language theorem explainer
Canonical isomorphism identifying integer singular homology of the (n+1)-sphere in degree k+2 with that of the n-sphere in degree k+1. Algebraic topologists computing sphere homology by induction on dimension cite it. The construction composes the Mayer-Vietoris connecting map for the two-punctured cover (an iso by contractibility of the open hemispheres) with the homology iso induced by the intersection-to-equator homotopy equivalence.
Claim. For all natural numbers $n$ and $k$, there is a canonical isomorphism $H_{k+2}(S^{n+1};\mathbb{Z})\cong H_{k+1}(S^n;\mathbb{Z})$ of singular homology modules with integer coefficients, obtained from the two-punctured open cover of $S^{n+1}$.
background
The ambient space is the unit sphere $S^n$ realized as the topological space of unit vectors in Euclidean space of dimension $n+1$. Integer singular homology $H_\bullet(-;\mathbb{Z})$ is taken from the singular chain complex of that space.
The module works with the standard two-set open cover of $S^{n+1}$: the complement of the south pole and the complement of the north pole. Both sets are open, their union is the whole sphere, and each is contractible. Their intersection is homotopy equivalent to the equatorial $S^n$ (via a polar/homeomorphism chain recorded as the intersection homotopy equivalence).
Upstream, the Mayer-Vietoris connecting homomorphism for this cover is already known to be an isomorphism once the two open sets are contractible; separately, any continuous homotopy equivalence induces an isomorphism on singular homology.
proof idea
Instantiate the Mayer-Vietoris connecting map of the two-punctured cover of $S^{n+1}$ in degree $k+1$. The contractibility lemma supplies the IsIso instance for that map, so asIso turns it into an isomorphism of homology modules. Compose (via ≪≫) with the homology isomorphism induced by the intersection-to-equator homotopy equivalence, shifted to degree $k+1$. The composite is the desired suspension isomorphism.
why it matters
This is the inductive step that lets sphere homology be computed from the base case $S^0$. Downstream, the vanishing theorem (Stage D: $H_k(S^n)=0$ for $1\le k\ne n$) and the non-vanishing of top homology ($H_n(S^n)\ne 0$ for $n\ge 1$) both induct on dimension by transporting isomorphisms and zero/non-zero statements across this map.
In the Recognition Science foundation layer the result is pure algebraic topology scaffolding: it underwrites the singular-homology computation of spheres that later geometry and forcing arguments may quote, without itself invoking the J-cost, the phi ladder, or the T0-T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.