Homotopy Type Theory
homotopy groups of spheres (changes)

Showing changes from revision #17 to #18: 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 onhomotopy groups of spheres in HoTT. Everything listed here is also discussed on the page on Formalized Homotopy Theory.

Table

n/k	0	1	2	3	4
0	π0(S0)	π0(S1)	π0(S2)	π0(S3)	π0(S4)
1	π1(S0)	π1(S1)	π1(S2)	π1(S3)	π1(S4)
2	π2(S0)	π2(S1)	π2(S2)	π2(S3)	π2(S4)
3	π3(S0)	π3(S1)	π3(S2)	π3(S3)	π3(S4)
4	π4(S0)	π4(S1)	π4(S2)	π4(S3)	π4(S4)

At least one proof has been formalized

Calculuation of $\pi_4(S^3)$

• Guillaume Brunerie 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.

Calculuation of $\pi_3(S^2)$

• 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 Brunerie’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 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 LeFanu Lumsdaine’s encode/decode-style proof, formalized by Dan Licata, using a clever lemma about maps out of two n-connected types.

Calculuation of $\pi_n(S^n)$

• Dan Licataand Guillaume Brunerie’s encode/decode-style proof using iterated loop spaces (for single-loop presentation).
• Guillaume Brunerie’s proof (for suspension definition).
• Dan Licata’s proof from Freudenthal suspension theorem (for suspension definition).

Calculuation of $\pi_k(S^n)$ for $k \lt n$

• Guillaume Brunerie’s proof (see the book).
• Dan Licata’s encode/decode-style proof for pi_1(S^2) only.
• Dan Licata’s encode/decode-style proof for all k < n (for single-loop presentation).
• Dan Licata’s proof from Freudenthal suspension theorem (for suspension definition).

Calculuation of $\pi_2(S^2)$

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

Calculuation of $\pi_1(S^1)$

• Mike Shulman’s proof by contractibility of total space of universal cover (HoTT blog).
• 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 Brunerie’s proof using the flattening lemma.