Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] Formalization of π₄(S³)≅ℤ/2ℤ in Cubical Agda completed
@ 2022-02-08 20:19 Anders Mortberg
  2022-02-08 23:24 ` Joyal, André
  0 siblings, 1 reply; 6+ messages in thread
From: Anders Mortberg @ 2022-02-08 20:19 UTC (permalink / raw)
  To: Homotopy Type Theory

[-- Attachment #1: Type: text/plain, Size: 3618 bytes --]

We are happy to announce that we have finished a formalization of
π₄(S³)≅ℤ/2ℤ  in Cubical Agda. Most of the code has been written by my PhD
student Axel Ljungström and the proof largely follows Guillaume Brunerie's
PhD thesis. For details and a summary see:

https://github.com/agda/cubical/blob/master/Cubical/Homotopy/Group/Pi4S3/Summary.agda

The proof involves a lot of synthetic homotopy theory: LES of homotopy
groups, Hopf fibration, Freudenthal suspension theorem, Blakers-Massey,
Z-cohomology (with graded commutative ring structure), Gysin sequence, the
Hopf invariant, Whitehead product... Most of this was written by Axel under
my supervision, but some results are due to other contributors to the
library, in particular Loïc Pujet (3x3 lemma for pushouts, total space of
Hopf fibration), KANG Rongji (Blakers-Massey), Evan Cavallo (Freudenthal
and lots of clever cubical tricks).

Our proof also deviates from the one in Guillaume's thesis in two major
ways:

1. We found a direct encode-decode proof of a special case of corollary
3.2.3 and proposition 3.2.11 which is needed for π₄(S³). This allows us to
completely avoid the use of the James construction of Section 3 in the
thesis (shortening the pen-and-paper proof by ~15 pages), but the price we
pay is a less general final result.

2. With Guillaume we have developed a new approach to Z-cohomology in HoTT,
in particular to the cup product and cohomology ring (see
https://drops.dagstuhl.de/opus/volltexte/2022/15731/). This allows us to
give fairly direct construction of the graded commutative ring H*(X;Z),
completely avoiding the smash product which has proved very hard to work
with formally (and also informally on pen-and-paper as can be seen by the
remark in Guillaume's thesis on page 90 just above prop. 4.1.2). This
simplification allows us to skip Section 4 of the thesis as well,
shortening the pen-and-paper proof by another ~15 pages. This then leads to
various further simplifications in Section 5 (Cohomology) and 6 (Gysin
sequence).

With these mathematical simplifications the proof got a lot more
formalization friendly, allowing us to establish an equivalence of groups
by a mix of formal proof and computer computations. In particular, Cubical
Agda makes it possible to discharge several small steps in the proof
involving univalence and HITs purely by computation. This even reduces some
gnarly path algebra in the Book HoTT pen-and-paper proof to "refl".
Regardless of this, we have not been able to reduce the whole proof to a
computation as originally conjectured by Guillaume. However, if someone
would be able to do this and compute that the Brunerie number is indeed 2
purely by computer computation there would still be the question what this
has to do with π₄(S³). Establishing this connection formally would then
most likely involve formalizing (large) parts of what we have managed to do
here. Furthermore, having a lot of general theory formalized will enable us
to prove more results quite easily which would not be possible from just
having a very optimized computation of a specific result.

Best regards,
Anders and Axel

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppmb%2BAt_Bwp_2USKH9dAigFGx0GBrcG3XQQaqZmkr-kHog%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 4275 bytes --]

^ permalink raw reply	[flat|nested] 6+ messages in thread

end of thread, other threads:[~2022-02-11 11:30 UTC | newest]

Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-02-08 20:19 [HoTT] Formalization of π₄(S³)≅ℤ/2ℤ in Cubical Agda completed Anders Mortberg
2022-02-08 23:24 ` Joyal, André
2022-02-09  3:09   ` Steve Awodey
2022-02-09  4:16     ` Noah Snyder
2022-02-09  4:44       ` 'Urs Schreiber' via Homotopy Type Theory
2022-02-11 11:29         ` Anders Mortberg

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).