LikeLike

]]>LikeLike

]]>Now that I looked at this again, two years later, I have double checked my argument works using only the stated hypothesis (differentiable and not assuming ), using precise forms of the fundamental theorem of calculus and integration by substitution. I was slightly worried I might have conceivably ended up with some weird counterexample that isn’t Riemann integrable or something.

LikeLike

]]>Yes. More precisely, one can form S^0 by taking the disjoint union of the terminal object with itself, and then one can form S^3 by suspending S^0 three times, where the suspension of an object X in an ∞-topos is defined as the pushout of X along two copies of the map to the terminal object. Also in any ∞-topos, one can form the loop space of a pointed object Y as the pullback of Y along two copies of the map from the terminal object that defines the pointing. Finally, in any ∞-topos one can define the 0-truncation as the left adjoint to the inclusion of the 0-truncated objects; this corresponds to π_0, which forms the “set” of components of an object. Combining all of this, one can define π_4(S^3) as the 0-truncation of the fourth loop space of S^3. A proof in HoTT that π_4(S^3) is Z/2 proves that in any ∞-topos π_4(S^3) is equivalent to the (internal) Z/2.

Here’s an example that might be more interesting to you. At first, it might seem disappointing that we can’t prove in HoTT that Ext^n(A,B) = 0 when n > 1 for abelian group objects A and B. But in sheaf models, A and B correspond to sheaves of abelian groups and these Ext groups turn out to correspond to sheaf Ext, which is something that algebraic geometers already study. So the things we can prove about Ext in HoTT turn out to imply things about sheaf Ext. The extra generality here isn’t just abstract nonsense, but helps in concrete situations. So while one could add axioms to make HoTT behave more like classical mathematics, one would then rule out these models that are important examples that arise in applications.

Another point to make is that knowing about these models is important for realizing what things you can’t expect to be able to prove in HoTT.

LikeLike

]]>I see. You’re stressing the point that this S^3 is not an “analytic” S^3 (i.e. some subset of points in R^4) but a “synthetic” S^3 (an abstract “space” (i.e. some higher inductive type) satisfying some rules) and so the argument works in any situation where those rules are obeyed and can thus be said to be a proof of a more general theorem.

LikeLike

]]>For example, there are ∞-toposes (models of HoTT) in which the universal coefficient short exact sequence is instead a universal coefficient spectral sequence. And in which Ext^n(A, B) can be non-zero for abelian groups A and B and n > 1. (Work in progress with Jarl Flaten.) And in which a set can have non-trivial higher cohomology. (https://homotopytypetheory.org/2013/07/24/cohomology/)

When we prove something in HoTT, we are not just proving it for spaces, but for all ∞-toposes, so one expects there to be such twists. This makes it a lot of fun!

LikeLike

]]>I see! Are there other higher homotopy groups of spheres which one can prove are cyclic using this method? And the point is that if you never assume the law of the excluded middle or the axiom of choice in your proof, every number which shows up in your proof is in theory computable so you can attempt to stare at the proof and evaluate the number.

I guess one way of interpreting the current state of things is that it demonstrates that this is a lousy way of actually computing pi_4(S^3), in the sense that we could instead formalise the usual proof given in a graduate topology course and it wouldn’t have this problem (although of course it would be some hard work to do this! But it would not run into issues of the inability to do a gigantic calculation). Similarly let’s say we wait until computers are 1000000 times better and then it turns out that we can compute that pi_4(S^3)=Z/2Z with this method. We’re then immediately faced with the problem that we can’t do pi_5(S^3), whereas the classical approach https://en.wikipedia.org/wiki/Homotopy_groups_of_spheres#Table has given us dozens of nontrivial examples of homotopy groups of spheres. I guess the traditional approach is almost certainly not constructive in the sense that it will use the law of the excluded middle somewhere, but I am unclear about whether this constructive approach actually buys you anything from the point of view of, say, a working topologist.

My take home from this story (hopefully I’ve got my facts straight) is that it (n=2) is a very interesting example of something which can be proved classically, but there is a much longer constructive proof and the challenge is to formalise this constructive proof. And it is a nice “sweet spot” because it’s out of reach right now but one could envisage that with some more good ideas, and as more powerful computers become more accessible, it might become within reach, thus making it a good problem to work on. There is a computational side to the question and also a constructive mathematical side to it, because there could be speed-ups coming from both domains.

LikeLike

]]>It’s more like they formalise not this theorem, but merely \exists n:N pi_4(S^3)=Z/nZ. Classically this would be like proving that pi_4(S^3) is a finite group with one generator. And then the code runs the algorithm that proves such a number exists, by actually constructing it as a numeral, namely SS0.

One could in principle formalise Brunerie’s paper proof of n=2 in a proof assistant that allows univalence, and that is a more prosaic proof more analogous to the usual proof. But the computational challenge is not to formalise this with computational output, but the pure existence statement.

LikeLike

]]>LikeLike

]]>I was going to suggest that as an even more achievable goal 🙂

LikeLike

]]>