A strengthening of Freudenthal's theorem for H-spaces #1814
Conversation
jdchristensen
left a comment
There was a problem hiding this comment.
Thanks for this! I've got to run now, but I'll continue looking at it later.
| Proposition freudenthal_hspace `{Univalence} | ||
| {n : nat} {X : pType} `{IsConnected n X} | ||
| `{IsHSpace X} `{forall a, IsEquiv (a *.)} | ||
| : IsEquiv (fmap (pPi (n + n).+1) (loop_susp_unit X)). |
There was a problem hiding this comment.
Another way to state this is that loop_susp_unit is a (2n+1)-equivalence, i.e., it is sent to an equivalence by Tr (n+n).+1. There's lots of material in ReflectiveSubuniverse about such maps --- search for O_inverts. Maybe it's worth having this statement in this more abstract form? I'm not sure if the connection between being inverted by Tr k and inducing an iso on Pi n for n <= k is in the library.
jdchristensen
left a comment
There was a problem hiding this comment.
Thanks for this! LGTM, once the minor changes are done.
|
I would also like to take a look a bit later. |
|
@Alizter I forget if I mentioned this earlier, but with this PR, we have basically reproved the The extension to any truncation level implies, for example, that the loop_susp map π_5(S^3 ) → π_6(S^4) is an equivalence (once you have the H-space structure on S^3). |
|
@jdchristensen I think its fine to replace. We always have git history if we want to see it again. The isomorphisms that you get are pretty cool, hopefully once we get a spectral sequence started we can start to use them in computations. |
|
@jarlg Do you want me to push a commit with my suggested changes? |
|
Yes, they all look fine to me, so you can go ahead. Thanks!
… On 16 Jan 2024, at 14:52, Dan Christensen ***@***.***> wrote:
@jarlg Do you want me to push a commit with my suggested changes?
—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you were mentioned.Message ID: ***@***.***>
|
|
@Alizter Let me know if you still want to look at this before merging. |
|
@jdchristensen I didn't get to read it in full just yet, but I think it is fine to merge. I'll leave comments afterwards if I find anything. |
We prove Proposition 2.19 of BCFR and use it to strengthen Freudenthal's theorem for H-spaces. To do this, we define the Hopf construction (but don't prove much about it) and add some minor things that we needed.