Gysin sequence/Hopf invariant/Homotopy groups #617
Conversation
|
I think π₄S³≅ℤ/2ℤ not ℤ. |
|
Very nice! Let's go through it all together soon. At some point I think we should make a summary file relating the formalization to Brunerie's thesis |
Good catch, I updated the description of the PR |
| is structure preserving | ||
|
|
||
| 2. Using the above, the complete group structure on (Sⁿ →∙ A), | ||
| the alternative definition of homotopy groups |
There was a problem hiding this comment.
Couldn't this be done using the SIP? Seems like you're doing it manually now?
There was a problem hiding this comment.
These types are not sets, but in principle it should still be possible to transport higher group structures.
There was a problem hiding this comment.
Indeed, I'm not sure if we can do this with the current SIP setup... Can @ecavallo help us investigate this? Maybe we can take a look in person on Monday afternoon?
There was a problem hiding this comment.
Sure. Just from looking I'm not clear on what exactly you want to sip.
There was a problem hiding this comment.
Axel and I discussed the code today over Zoom and it seems maybe possible to SIP some parts, but it's not obvious how... Anyway let's just look at it together on Monday after lunch
There was a problem hiding this comment.
https://github.com/ecavallo/cubical/blob/GysinCleanup/Cubical/Homotopy/Group/Properties.agda
Left a hole for a proof of inverse preservation.
There was a problem hiding this comment.
Nice! But couldn't one transfer all of the laws in one go? So you define isWildGroup as a structure on RawGroup and subst it.
It then doesn't seem necessary to extract the fields as they're only used to define https://github.com/ecavallo/cubical/blob/GysinCleanup/Cubical/Homotopy/Group/Properties.agda#L264 ... Or?
Haha wups, thanks:-) |
Cubical/Foundations/Prelude.agda
Outdated
| @@ -517,3 +514,13 @@ compPathR→PathP∙∙ {p = p} {q = q} {r = r} {s = s} P j i = | |||
| ; (j = i0) → r i | |||
| ; (j = i1) → doubleCompPath-filler p s (sym q) (~ k) i}) | |||
| (P j i) | |||
|
|
|||
| doubleCompPath≡compPath : | |||
There was a problem hiding this comment.
No levels needed
| is structure preserving | ||
|
|
||
| 2. Using the above, the complete group structure on (Sⁿ →∙ A), | ||
| the alternative definition of homotopy groups |
There was a problem hiding this comment.
These types are not sets, but in principle it should still be possible to transport higher group structures.
aljungstrom
force-pushed
the
GysinCleanup
branch
from
964e6e5
to
a945d87
Compare
|
Ok, changed Homotopy.Group a bit I moved I also generalised Concerning the SIP/Wild groups etc. I'd suggest we do that in a separate future PR. I've fixed all the previous comments now, so unless there's something I've messed up in these new changes, I think we can merge. |
|
Great! I'll merge this mega PR now I think it sounds reasonable to integrate the SIP stuff in a future PR. @ecavallo Can you please make a PR with your incomplete code when I've merged this? I can take a look at it and maybe finish it |
Big PR again... I think @mortberg and I can go through it together next week. It contains: