Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
At the end (at 42:11) of his Voevodsky Memorial talk Pierre Deligne poses a question (for the HoTT community?).
Given , or an element in does it induce , and do so universally?
for stands for the iterated loop space of , .
So is he asking whether induces a map (which it surely does), and so a map from to ?
What’s the challenge?
The maps of fundamnetal groups are truncated to the set level. I think he is asking if the truncation can be rid of. Can this be extended to a map of untruncated loop spaces.
There was some confusion at the meeting about this too. It’s already an interesting question at the level Ali interpreted it; but it seems that Deligne intended his “” to refer to the homotopy groups of spheres as defined in ZFC. In other words, if we know classically that we have some element of a homotopy group of spheres, can we use that to define in type theory a corresponding map on loop spaces.
And what can we say to the question as posed in #2 and #3? Is there something one can ’reasonably’ ask for, that can’t be delivered?
If it’s “reasonable” to ask for a map , then yes; I don’t think we can deliver that. But even in ZFC such a map doesn’t really exist canonically. You can choose a representative of any , which in turn induces a map , and equivalent representatives of induce homotopic maps, but not uniquely homotopic ones. So the axiom of choice can give you a particular map, but it’s not canonically determined.
1 to 5 of 5