nLab
Freudenthal suspension theorem

Statement

The Freudenthal suspension theorem (Hans Freudenthal, 1937) is the following theorem about homotopy groups of spheres:

The suspension homomorphism $\sigma :{\pi }_{n+k}(S^n)\to {\pi }_{n+k+l}(S^{n+l})$ is an isomorphism for $n>k+1$.

In this statement, one can replace $S^n$ with any $(n-1)$-connected space $Y$ while replacing $S^{n+l}$ with the corresponding suspension ${\Sigma }^{l}Y$.

This theorem justifies introducing the stable homotopy groups of spheres ${\pi }_k(S):={\pi }_{n+k}(S^n)$, as well as stable homotopy groups ${\pi }_k^S(Y)={\pi }_{n+k}({\Sigma }^{n}Y)$, both independent of $n$ where $n>k+1$.

References

A formalization in homotopy type theory in Agda is in

• Peter Lumsdaine, Dan Licata, Freudenthal.agda