# Homotopy Type Theory homotopy groups of spheres (Rev #12, changes)

Showing changes from revision #11 to #12: Added | Removed | Changed

## 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$01234
0$\pi_0(S^0)$$\pi_0(S^1)$$\pi_0(S^2)$$\pi_0(S^3)$$\pi_0(S^4)$
1$\pi_1(S^0)$$\pi_1(S^1)$$\pi_1(S^2)$$\pi_1(S^3)$$\pi_1(S^4)$
2$\pi_2(S^0)$$\pi_2(S^1)$$\pi_2(S^2)$$\pi_2(S^3)$$\pi_2(S^4)$
3$\pi_3(S^0)$$\pi_3(S^1)$$\pi_3(S^2)$$\pi_3(S^3)$$\pi_3(S^4)$
4$\pi_4(S^0)$$\pi_4(S^1)$$\pi_4(S^2)$$\pi_4(S^3)$$\pi_4(S^4)$
<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>
$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)$

• Guillaume has proved that there exists an Guillaume Brunerie$n$ has proved that there exists an such that $n$$\pi_4(S^3)$ such that is $\pi_4(S^3)$$\mathbb{Z}_n$ is . Given a computational interpretation, we could run this proof and check that $\mathbb{Z}_n$$n$. Given a computational interpretation, we could run this proof and check that is 2. Added June 2016: Brunerie now has a proof that $n$$n=2$ 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)$

• 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 Peter LeFanu Lumsdaine 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 with it in it.
• Guillaume’s proof that the total space of the Hopf fibration is Guillaume Brunerie$S^3$’s proof that the total space of the Hopf fibration is , together with $S^3$$\pi_n(S^n)$, together with $\pi_n(S^n)$, imply this by a long-exact-sequence argument.
• This was formalized in Lean in 2016.

### $\pi_n(S^2)=\pi_n(S^3)$ for $n\geq 3$

• This follows from the Hopf fibration and long exact sequence of homotopy groups.
• It was formalized in Lean in 2016.

### Freudenthal Suspension Theorem

Implies $\pi_k(S^n) = \pi_{k+1}(S^{n+1})$ whenever $k \le 2n - 2$

• Peter’s encode/decode-style proof, Peter LeFanu Lumsdaine’s encode/decode-style proof, formalized by Dan, using a clever lemma about maps out of two n-connected types.Dan Licata, using a clever lemma about maps out of two n-connected types.

### $\pi_2(S^2)$

• Guillaume’s proof using the total space the Hopf fibration.Guillaume Brunerie’s proof using the total space the Hopf fibration.
• Dan’s encode/decode-style Dan Licata’s encode/decode-style proof.

### $\pi_1(S^1)$

• Mike’s proof by contractibility of total space of universal cover (Mike Shulman’s proof by contractibility of total space of universal cover (HoTT blog).
• Dan’s encode/decode-style proof (Dan Licata’s encode/decode-style proof (HoTT blog). A paper mostly about the encode/decode-style proof, but also describing the relationship between the two.
• Guillaume’s proof using the flattening lemma.Guillaume Brunerie’s proof using the flattening lemma.

category: homotopy theory

Revision on October 17, 2018 at 10:47:52 by Ali Caglayan. See the history of this page for a list of all contributions to it.