UF IAS 2012 Archive HomotopyGroupsOfSpheres

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.

In progress

π4(S3)

• Guillaume has proved that there exists an n such that π4(S3) is Z_n, and given a computational interpretation, we could run this proof and check that n is 2.

π3(S2)

• 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 with it in it.
• Guillaume’s proof that the total space of the Hopf fibration is S3, together with π_n(Sn), imply this by a long-exact-sequence argument, but this hasn’t been formalized.

At least one proof has been formalized

Freudenthal Suspension Theorem

Implies π_k(Sn) = π_k+1(Sn+1) whenever k <= 2n - 2

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

π_n(Sn)

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

π_k(Sn) for k < n

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

π2(S2)

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

π1(S1)

• Mike’s proof by contractibility of total space of universal cover (HoTT blog).
• Dan’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.