The paper presents a formalization in Cubical Agda of the proof that the fourth homotopy group of the 3-sphere, π4(S3), is isomorphic to Z/2Z. This result was first proved synthetically in Homotopy Type Theory by Brunerie in his 2016 PhD thesis.
The formalization closely follows Brunerie's proof, with some simplifications. The key steps are:
Introducing basic HoTT concepts and their formalization in Cubical Agda, including higher inductive types, loop spaces, and homotopy groups.
Formalizing the first part of Brunerie's proof, which culminates in the definition of the "Brunerie number" β such that π4(S3) ∼= Z/βZ. This involves the James construction and Whitehead products.
Formalizing the second part of Brunerie's proof, which shows that |β| ≡ 2, thereby establishing that π4(S3) ∼= Z/2Z. This part relies on advanced machinery like cohomology, the Hopf invariant, and Gysin sequences.
Presenting a new, simpler proof that β = ±2, which avoids the technical difficulties of Brunerie's original proof. This new proof manually computes the image of the generator η of π3(S2) under a sequence of maps, yielding a new "Brunerie number" that normalizes to -2 in Cubical Agda.
The formalization provides the first computer-assisted proof of the classical result that π4(S3) ∼= Z/2Z, and demonstrates the power of Homotopy Type Theory and Cubical Agda for formalizing advanced results in synthetic homotopy theory.
To Another Language
from source content
arxiv.org
Önemli Bilgiler Şuradan Elde Edildi
by Axel... : arxiv.org 05-01-2024
https://arxiv.org/pdf/2302.00151.pdfDaha Derin Sorular