## Idea The [[nLab:homotopy groups of spheres]] are a fundemental concept in [[nLab:algebraic topology]]. They tell you about [[nLab:homotopy classes]] of maps from [[nLab:spheres]] to other spheres which can be rephrased as the collection of different ways to attach a sphere to another sphere. The [[nLab:homotopy type]] of a [[nLab:CW complex]] is completely determined by the homotopy types of the attaching maps. Here's a quick reference for the state of the art on homotopy groups of spheres in HoTT. Everything listed here is also discussed on the page on [[Formalized Homotopy Theory]]. ## Table | $n\backslash k$ | 0 | 1 | 2 | 3 | 4 | |--|--|--|--|--|--| | 0 | [$\pi_0(S^0)$](#pinsn) | [$\pi_0(S^1)$](#piksn) | [$\pi_0(S^2)$](#piksn) | [$\pi_0(S^3)$](#piksn) | [$\pi_0(S^4)$](#piksn) | | 1 | $\pi_1(S^0)$ | [$\pi_1(S^1)$](#pinsn) | [$\pi_1(S^2)$](#piksn) | [$\pi_1(S^3)$](#piksn) | [$\pi_1(S^4)$](#piksn) | | 2 | $\pi_2(S^0)$ | $\pi_2(S^1)$ | [$\pi_2(S^2)$](#pinsn) | [$\pi_2(S^3)$](#piksn) | [$\pi_2(S^4)$](#piksn) | | 3 | $\pi_3(S^0)$ | $\pi_3(S^1)$ | [$\pi_3(S^2)$](#pi3s2) | [$\pi_3(S^3)$](#pinsn) | [$\pi_3(S^4)$](#piksn) | | 4 | $\pi_4(S^0)$ | $\pi_4(S^1)$ | [$\pi_4(S^2)$](#hopff) | [$\pi_4(S^3)$](#pi4s3) | [$\pi_4(S^4)$](#pinsn) | <style type="text/css"> .tg {border-collapse:collapse;border-spacing:0;} .tg td{font-family:Arial, sans-serif;font-size:14px;padding:10px 5px;border-style:solid;border-width:1px;overflow:hidden;word-break:normal;border-color:black;} .tg th{font-family:Arial, sans-serif;font-size:14px;font-weight:normal;padding:10px 5px;border-style:solid;border-width:1px;overflow:hidden;word-break:normal;border-color:black;} .tg .tg-1wig{font-weight:bold;text-align:left;vertical-align:top} .tg .tg-mnhx{background-color:#fe0000;text-align:left;vertical-align:top} .tg .tg-hyan{background-color:#34cdf9;text-align:left;vertical-align:top} .tg .tg-0lax{text-align:left;vertical-align:top} .tg .tg-s7ni{background-color:#f8ff00;text-align:left;vertical-align:top} .tg .tg-fd62{background-color:#32cb00;text-align:left;vertical-align:top} </style> <table class="tg"> <tr> <th class="tg-0lax">$n\backslash k$</th> <th class="tg-1wig">0</th> <th class="tg-1wig">1</th> <th class="tg-1wig">2</th> <th class="tg-1wig">3</th> <th class="tg-1wig">4</th> </tr> <tr> <td class="tg-1wig">0</td> <td class="tg-hyan">[$\pi_0(S^0)$](#pinsn)</td> <td class="tg-s7ni">[$\pi_0(S^1)$](#piksn)</td> <td class="tg-0lax">[$\pi_0(S^2)$](#piksn)</td> <td class="tg-0lax">[$\pi_0(S^3)$](#piksn)</td> <td class="tg-0lax">[$\pi_0(S^4)$](#piksn)</td> </tr> <tr> <td class="tg-1wig">1</td> <td class="tg-mnhx">$\pi_1(S^0)$</td> <td class="tg-hyan">[$\pi_1(S^1)$](#pinsn)</td> <td class="tg-0lax">[$\pi_1(S^2)$](#piksn)</td> <td class="tg-0lax">[$\pi_1(S^3)$](#piksn)</td> <td class="tg-0lax">[$\pi_1(S^4)$](#piksn)</td> </tr> <tr> <td class="tg-1wig">2</td> <td class="tg-fd62">$\pi_2(S^0)$</td> <td class="tg-mnhx">$\pi_2(S^1)$</td> <td class="tg-hyan">[$\pi_2(S^2)$](#pinsn)</td> <td class="tg-0lax">[$\pi_2(S^3)$](#piksn)</td> <td class="tg-0lax">[$\pi_2(S^4)$](#piksn)</td> </tr> <tr> <td class="tg-1wig">3</td> <td class="tg-hyan">$\pi_3(S^0)$</td> <td class="tg-fd62">$\pi_3(S^1)$</td> <td class="tg-mnhx">[$\pi_3(S^2)$](#pi3s2)</td> <td class="tg-hyan">[$\pi_3(S^3)$](#pinsn)</td> <td class="tg-0lax">[$\pi_3(S^4)$](#piksn)</td> </tr> <tr> <td class="tg-1wig">4</td> <td class="tg-mnhx">$\pi_4(S^0)$</td> <td class="tg-hyan">$\pi_4(S^1)$</td> <td class="tg-fd62">[$\pi_4(S^2)$](#hopff)</td> <td class="tg-mnhx">[$\pi_4(S^3)$](#pi4s3)</td> <td class="tg-hyan">[$\pi_4(S^4)$](#pinsn)</td> </tr> </table> ## In progress ### $\pi_4(S^3)$ {#pi4s3} * Guillaume has proved that there exists an $n$ such that $\pi_4(S^3)$ is $\mathbb{Z}_n$. Given a computational interpretation, we could run this proof and check that $n$ is 2. Added June 2016: Brunerie now has a proof that $n=2$, using cohomology calculations and a Gysin sequence argument. ## At least one proof has been formalized ### $\pi_3(S^2)$ {#pi3s2} * Peter L. has constructed the Hopf fibration as a dependent type. Lots of people around know the construction, but I don't know anywhere it's written up. Here's some [Agda code](https://github.com/dlicata335/hott-agda/blob/master/homotopy/Hopf.agda) with it in it. * Guillaume's proof that the total space of the Hopf fibration is $S^3$, together with $\pi_n(S^n)$, imply this by a long-exact-sequence argument. * This was [formalized in Lean](https://github.com/leanprover/lean2/blob/master/hott/homotopy/sphere2.hlean) in 2016. ### $\pi_n(S^2)=\pi_n(S^3)$ for $n\geq 3$ {#hopff} * This follows from the Hopf fibration and long exact sequence of homotopy groups. * It was [formalized in Lean](https://github.com/leanprover/lean2/blob/master/hott/homotopy/sphere2.hlean) in 2016. ### Freudenthal Suspension Theorem {#fsusp} Implies $\pi_k(S^n) = \pi_{k+1}(S^{n+1})$ whenever $k \le 2n - 2$ * Peter's encode/decode-style proof, [formalized](https://github.com/dlicata335/hott-agda/blob/master/homotopy/Freudenthal.agda) by Dan, using a clever lemma about maps out of two n-connected types. ### $\pi_n(S^n)$ {#pinsn} * Dan and Guillaume's [encode/decode-style proof using iterated loop spaces](https://github.com/dlicata335/hott-agda/blob/master/homotopy/PiNSN.agda) (for single-loop presentation). * Guillaume's proof (for suspension definition). * Dan's [proof from Freudenthal suspension theorem](https://github.com/dlicata335/hott-agda/blob/master/homotopy/PiSnSusp.agda) (for suspension definition). ### $\pi_k(S^n)$ for $k \lt n$ {#piksn} * Guillaume's proof (see the book). * Dan's encode/decode-style proof [for pi_1(S^2) only](https://github.com/dlicata335/hott-agda/blob/master/homotopy/Pi1S2.agda). * Dan's encode/decode-style proof [for all k < n](https://github.com/dlicata335/hott-agda/blob/master/homotopy/PiKSNLess.agda) (for single-loop presentation). * Dan's [proof from Freudenthal suspension theorem](https://github.com/dlicata335/hott-agda/blob/master/homotopy/PiSnSusp.agda) (for suspension definition). ### $\pi_2(S^2)$ {#pi2s2} * Guillaume's proof using the total space the Hopf fibration. * Dan's encode/decode-style [proof](https://github.com/dlicata335/hott-agda/tree/master/homotopy/pi2s2). ### $\pi_1(S^1)$ {#pi1s1} * Mike's proof by contractibility of total space of universal cover ([HoTT blog](http://uf-ias-2012.wikispaces.com/ofpost)). * Dan's encode/decode-style proof ([HoTT blog](http://homotopytypetheory.org/2012/06/07/a-simpler-proof-that-%CF%80%E2%82%81s%C2%B9-is-z/)). A [paper](http://arxiv.org/abs/1301.3443) mostly about the encode/decode-style proof, but also describing the relationship between the two. * Guillaume's proof using the flattening lemma. category: homotopy theory