## Idea The homotopy groups of spheres are a fundemental concept in algebraic topology. They tell you about homotopy classes of maps from spheres to other spheres which can be rephrased as the collection of different ways to attach a sphere to another sphere. The homotopy type of a 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) | ## 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.