Homotopy Type Theory
homotopy groups of spheres > history (Rev #11, changes)
Showing changes from revision #10 to #11:
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
<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
π 4 ( S 3 ) \pi_4(S^3)
Guillaume has proved that there exists an n n such that π 4 ( S 3 ) \pi_4(S^3) is ℤ n \mathbb{Z}_n . Given a computational interpretation, we could run this proof and check that n n is 2. Added June 2016: Brunerie now has a proof that n = 2 n=2 , using cohomology calculations and a Gysin sequence argument.
π 3 ( S 2 ) \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 Agda code with it in it.
Guillaume’s proof that the total space of the Hopf fibration is S 3 S^3 , together with π n ( S n ) \pi_n(S^n) , imply this by a long-exact-sequence argument.
This was formalized in Lean in 2016.
π n ( S 2 ) = π n ( S 3 ) \pi_n(S^2)=\pi_n(S^3) for n ≥ 3 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 π k ( S n ) = π k + 1 ( S n + 1 ) \pi_k(S^n) = \pi_{k+1}(S^{n+1}) whenever k ≤ 2 n − 2 k \le 2n - 2
Peter’s encode/decode-style proof, formalized by Dan, using a clever lemma about maps out of two n-connected types.
π n ( S n ) \pi_n(S^n)
π k ( S n ) \pi_k(S^n) for k < n k \lt n
π 2 ( S 2 ) \pi_2(S^2)
Guillaume’s proof using the total space the Hopf fibration.
Dan’s encode/decode-style proof .
π 1 ( S 1 ) \pi_1(S^1)
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.
Revision on October 9, 2018 at 14:10:00 by
Anonymous? .
See the history of this page for a list of all contributions to it.