Project status update

Stream: sphere eversion

[Patrick Massot]

People who closely follow the project may have noticed that we somehow interrupted our global theory sprint one week ago. The paper submission deadline for CPP is September 21th and we decided one week ago that we wouldn't have time to finish the project and write a nice paper before that deadline. It also bugged us to write a single 12 pages long paper on this rather large project. So we decided to write a first paper on Chapter 1 and 2 only. Recall Chapter 1 is about geometric constructions of families of loops in vector spaces, Chapter 2 is the theory of convex integration for maps between vector spaces, while Chapter 3 is the theory of convex integration for maps between manifolds. In order to still get a meaningful milestone to report, we put some extra work to derive the existence of sphere eversions from Chapter 2 alone. Indeed the sphere eversion theorem itself isn't far from being about vector spaces since the 2-sphere naturally sits inside a vector space. This required some extra work to put into Chapter 2 because the original plan involved handling some things only in the manifold case, notably the theorem giving parametricity for free. So we had a short week sprint adding about 1400 lines in a different branch that was merged to master this morning (this involved some nasty git history rewriting, so don't believe git when it tells you we wrote 1400 lines yesterday). We will now work on writing a paper and will resume our work on Chapter 3 in two weeks.

[Patrick Massot]

Of course Heather's work on rotations is used in both ways of deriving the existence of sphere eversions (from Chapter 2 or from the more general Chapter 3).

[Patrick Massot]

In case the above paragraph is too long, here is a summary. We're are not completely done with proving the very general theorem that is the ultimate goal of the project, but the special case of sphere eversion itself is now fully formalized: you can indeed turn a sphere inside-out!

[Oliver Nash]

For emphasis: this is sorry-free.

[Kevin Buzzard]

Congratulations!

[Johan Commelin]

Really cool! Thanks for the update!

[Eric Rodriguez]

What is the more general theorem that is the ultimate goal? Many congratulations!

[Oliver Nash]

Eric Rodriguez said:

What is the more general theorem that is the ultimate goal?

It is the relative, parametric, $C^0$-dense h-principle for open ample differential relations. The sphere eversion result is an application of this to the differential relation of immersions which is open and ample (in positive codimension).

[Oliver Nash]

The theorem (due to Gromov) concerns solutions to a differential relation. Such a solution is a smooth map that satisfies a condition defined by the data that is the differential relation (e.g., being an immersion if the relation is the relation of immersions). Given a smooth map $f : M \to N$ one has its derivative which is a family of linear maps $f_* : T_mM \to T_{f(m)}N$ for each $m \in M$. A key insight is that there can be a topological obstruction to the existence of such a family of linear maps, regardless of whether or not they are actually the derivative of a smooth map.

So one can break down the problem of finding a solution to the differential relation into the topological problem of finding such a family of linear maps (a formal solution) and then finding a way to deform a formal solution into a true solution. The h-principle says that if the differential relation is open and ample then such a deformation can always be done. Furthermore one can also demand that such deformations satisfy various extra conditions (being constant relative to a closed subset, being parametric, being $C^0$-close).

So Gromov's theorem reduces this question of differential topology (existence of a solution of a differential relation) to one of topology (existence of a formal solution).

[Oliver Nash]

The technique for doing the deformation is very clever and is called convex integration.

[Floris van Doorn]

For people working on this project: we force-pushed master to correctly attribute Oliver's commits to him (Github thought he only had 4 commits, but now he has 160).
To update to the latest version, run git reset origin/master --hard on all machines you use (and if you have uncommited local changes you want to keep, you can first commit them, and after the reset you can cherry-pick them).

[Oliver Nash]

Quite a productive day for me: 156 commits.

[Oliver Nash]

(I actually deprecate all this stuff but I was requested to make this change)