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 $\alpha: \pi_{n+k}(S^n)$, or an element in $[S^{n+k}, S^n]$ does it induce $[\alpha]: a =_n a \to a =_{n+k} a$, and do so universally?
$a =_n a$ for $a:A$ stands for the iterated loop space of $A$, $\Omega^n(A)$.
So is he asking whether $\alpha$ induces a map $[[S^n, A], [S^{n+k}, A]]$ (which it surely does), and so a map from $\Omega^n(A)$ to $\Omega^{n+k}(A)$?
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 “$\pi_{n+k}(S^n)$” 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 $\pi_{n+k}(S^n) \to \Omega^n X \to \Omega^{n+k} X$, 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 $\alpha \in \pi_{n+k}(S^n)$, which in turn induces a map $\Omega^n X \to \Omega^{n+k} X$, and equivalent representatives of $\alpha$ 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