Update on Chapter 2

Stream: sphere eversion

[Patrick Massot]

I just pushed the first commit where Chapter 2 has no "large" sorry. It still has 49 small sorries. But all those sorries are meant to be easy and don't require any understanding of the big picture.

[Patrick Massot]

One thing worth mentioning about the last part of this push is that Floris's idea about how to state smoothness lemmas was again very efficient. Now I need to prove those lemmas...

[Patrick Massot]

Chapter 2 sorry count went down from 49 to 14.

[Patrick Massot]

The situation about Chapter 2 is there is no remaining sorry in the main files, but we still need general work on gluing smooth functions. This is happening in https://github.com/leanprover-community/sphere-eversion/blob/master/src/to_mathlib/smoothness.lean. Floris is working on this. I'm currently cleaning up a bit the main file, and I'll need to update the blueprint to put the statement that are actually needed.

[Patrick Massot]

Chapter 2 itself is now complete (but it still relies on crucial results from Chapter 1 that are not fully proved).

[Johan Commelin]

See https://leanprover-community.github.io/sphere-eversion/blueprint/dep_graph_document.html if you like graphs

[Patrick Massot]

There is still work to do on the blueprint to align the exact statements for intermediate results and the proofs, but the main goal of the chapter, which is the $h$-principle for open and ample relation for maps between vector spaces is unambiguous and fully proved modulo Chapter 1.

[Patrick Massot]

On the graph, the missing results from Chapter 1 are reparametrization and loops.

[Patrick Massot]

The Chapter 2 target is h_principle_open_ample_loc

[Patrick Massot]

Actually technically open_ample_immersion_loc is also in Chapter 2, so we still need to do that, but this should be easy.

[Yaël Dillies]

Is someone working on the reparametrization item? Do you think it is accessible for me? My background is the Geometry course here.

[Patrick Massot]

Oliver is working on the reparametrization lemma. But there are probably many preparatory lemmas to prove.

[Patrick Massot]

But the current state of https://github.com/leanprover-community/sphere-eversion/blob/master/src/loops/reparametrization.lean is that all sorried lemmas are about a definition which is sorried...

[Oliver Nash]

@Yaël Dillies There is still one sorry in the reparametrisation lemma which does not depend on the sorried definition, but only on its API, which is in place. It’s this: https://github.com/leanprover-community/sphere-eversion/blob/e08d14f289daf9660cdea10d00dcec16cd52395e/src/loops/reparametrization.lean#L154

[Oliver Nash]

I’m traveling at the moment but I’ll be resuming work on this lemma on Wednesday and I’d say it will take me a week or two to finish everything for reparametrisation.

[Patrick Massot]

Patrick Massot said:

Actually technically open_ample_immersion_loc is also in Chapter 2, so we still need to do that, but this should be easy.

I proved that lemma, so that's one more green node.