Has it gotten easier to prove all homotopy groups of spheres are computable? I don’t care if the computation is inefficient, what’s the easiest proof? Are we still stuck doing Postnikov towers?
$\begingroup$
$\endgroup$
11
-
11$\begingroup$ @JoeShipman Saying that Wikipedia's use of "computation" for things that are not algorithms is "absolutely insulting crap" seems a little excessive to me... $\endgroup$– Carl-Fredrik Nyberg BroddaCommented Feb 11, 2022 at 0:27
-
6$\begingroup$ Homotopy theory has a tendency to call things "computations" when they reduce the computation of something to some relatively standard other object -- but that object itself may be just some mathematically-presented object, i.e. often it is not of a finitary nature. I think the abuse of language, while occasionally frustrating, is understandable, given that specialization has this tendency to put people into bubbles where they are talking with like-minded folks. Whenever you talk to a new person, you have to get used to whatever dialect they are speaking, before your can really converse. $\endgroup$– Ryan BudneyCommented Feb 11, 2022 at 0:36
-
7$\begingroup$ I have never thought that the use of "computation" as a synonym for "calculation" was unique to topologists, but maybe it is, and I never noticed. A web search for "computation of the Chow ring" reveals that some algebraic geometers use the word "computation" this way too, at least. $\endgroup$– user164898Commented Feb 11, 2022 at 0:59
-
5$\begingroup$ @JoeShipman: Complaining about topologists’ use of “computation” is like an American going to Italy and complaining that the “cappucino” isn’t like he’s used to from Starbucks. OK, not quite — that’s an exaggeration — but it’s like complaining that Italian cappucino isn’t like at his nice hipster coffee shop in Brooklyn. The logician’s usage of “computation” is a good and important one — but the topologists’ looser usage is not merely legitimate, but also older than ours, and is essentially what ours was originally derived from. $\endgroup$– Peter LeFanu LumsdaineCommented Feb 11, 2022 at 16:31
-
5$\begingroup$ I had the impression that a computation could be something carried out by a computor, rather than a computer... $\endgroup$– Tyler LawsonCommented Feb 11, 2022 at 17:36
|
Show 6 more comments
1 Answer
$\begingroup$
$\endgroup$
5
It may not be any "easier" than Brown's proof, but the work of people like Francis Sergeraert and others has created a nice conceptual framework for these types of questions. See especially the paper, Effective homotopy of fibrations by Romero and Sergeraert. They have also implemented their algorithms in Kenzo.
See also An algorithm computing homotopy groups by Pedro Real, which uses the ideas of effective homology to sketch an algorithm for the homotopy groups of spheres specifically.
-
$\begingroup$ I have reviewed all the references.My conclusion: the answer to my original question is “no”. $\endgroup$ Commented Feb 11, 2022 at 12:40
-
$\begingroup$ It look like the only proofs that homotopy groups of spheres are effectively computable are still the same proofs that work for ALL simply connected spaces of finite type via Whitehead or Postnikov towers. Sergeraert and others have given us better tools for managing the process, but you must still iteratively and laboriously kill off homotopy groups one dimension at a time by building higher dimensional complexes, an inherently superexponential process (at least 2^(2^n), at most an exponential tower of height n). $\endgroup$ Commented Feb 11, 2022 at 12:49
-
3$\begingroup$ @JoeShipman I don't know anything about the subject (I'm reading this to learn), but in the question you seemed to say that you wanted a simple proof even if it is inefficient, now you seem to be saying that you don't like this approach because it's inherently superexponential. Is this because its description is necessarily complex, or do you care about efficiency after all? $\endgroup$– Gro-TsenCommented Feb 11, 2022 at 14:03
-
1$\begingroup$ @Gro-Tsen I think Joe Shipman is saying that at bottom, these "new" proofs are essentially the same as the original proof. I don't know the subject well, so that may be an accurate assessment. I think the primary value of the modern approach is that it takes a systematic approach to computability questions. So for example, while spectral sequences are definitely a "computational tool" in an informal sense, effective homology insists on computability in a formal sense. I think this is clear conceptual advance, but it may not make specific computability proofs "easier." $\endgroup$ Commented Feb 11, 2022 at 16:37
-
$\begingroup$ Here's another interesting reference I found: Polynomial-Time Computation of Homotopy Groups and Postnikov Systems in Fixed Dimension. But again, I don't think it, or the papers it cites, yields an "easier" proof that homotopy groups of spheres are computable. $\endgroup$ Commented Feb 11, 2022 at 17:41