π₄(S³) ≅ π₃(S²×S² ← S²∨S² → S²) #684
Conversation
|
It's so cool that this proof worked out! It seems like a very big simplification if we can avoid the James construction. Please ping me when you fixed the comments and I'll merge |
| This file has been split in two due to slow type checking | ||
| combined with insufficient reductions when the | ||
| experimental-lossy-unification flag is included. | ||
| Part 2: Cubical.Homotopy.Group.Pi4S3.S3PushoutIso2 |
There was a problem hiding this comment.
@Saizan This is a bit weird... Some parts need experimental-lossy-unification to terminate, but some other parts don't typecheck if we have it... Any clue what we can do?
Is it somehow possible to have flags at the level of modules instead of files?
|
Only one last step! That's really cool! |
Yeah! Or sort of one and a half -- turns out getting the long exact sequence on the appropriate form is a bit harder than I thought (when I did it following the HoTT book it turned out to be quite tricky to trace the maps in the sequence, since some of of them get defined in a somewhat roundabout way). The proof is finished though, and I'll make a PR soon. After that it should be relatively straightforward to put everything together (I hope...) |
Finally got to it. I think it should be ready now. |
This module contains a proof of the iso
π₄(S³) ≅ π₃(S²×S² ← S²∨S² → S²)which is used in Brunere's proof ofπ₄(S³)≅ℤ/2ℤ. Instead of using the James construction, it is proved directly here. As far as I can tell, this means that we no longer need James for a full formalisation ofπ₄(S³)≅ℤ/2ℤ. My hope is that the remainder of Brunerie's proof should now be relatively straightforward formalise.I created a new directory for π₄(S³) at
Cubical.Homotopy.Group.Pi4S3and moved the summary file there.The main result of this PR can be found in
Cubical.Homotopy.Group.Pi4S3.S3PushoutIso2. The proof had to be split up due to a minor problem with the lossy-unifcation flag.