feat(geometry/manifold): The preimage straightening theorem

[Nicknamen]

I am not sure about the title of this PR, but this is just the name we sometimes give to this theorem in Italy.

Theorem:
Let f:M → N be map which is smooth at p, and p be a regular point of f. Consider charts φ : U ⊆ M → E and ψ : V ⊆ N → F about p and f(p) respectively. Let g = ψ ∘ f ∘ φ⁻¹. Let K=ker (d g_{φ (p)}). Then there exists a local homeomorphism ϕ: W → F × K ≅ E where W ⊆ U ⊆ M is an open containing p, such that ψ ∘ f ∘ ϕ⁻¹ : (v,k) : F × K ↦ v : F.

This PR is incomplete but the only two missing lemmas should be straightforward once some API for boundaryless manifolds has been written. In any case, I did not want to write the API yet because I think this theorem holds for manifolds with corners meant to be manifolds locally modeled on a quadrant of the euclidean space but does not hold for the general model with corners we have in Mathlib now. To my knowledge, this could be one of the first times that we try to formalize something which is true for manifolds with corners but that does not extend easily to them, so it should be a good stress test for the current implementation. I might be wrong because I am not familiar with strict differentiability but I am sure that the regular value theorem is true for manifolds with corners in the usual sense but not in this case and this PR is meant to be the first step for that proof, so the above problem holds even if I am wrong.

What should we do? Restrict the current definition of model with corners or give up on this theorem in that case? I believe this is a useful theorem for manifolds with boundary.

---

[sgouezel]

Can you expand in the PR description on what the statement of the theorem should be?

For the manifold with boundary case, it is good to keep the following example in mind. Let M be the upper half plane (with boundary), and let f (x, y) = y - e^{-1/x^2} sin (1/x). Then f is a submersion at (0, 0), but the preimage in M of f (0, 0) = 0 is very nasty.

[Nicknamen]

Done!

Sure but it should still be a manifold with boundary right?

[sgouezel]

No, it wouldn't be a manifold with boundary (any neighborhood of 0 has infinitely many connected components, while a one-dimensional manifold with boundary is locally connected).

[Nicknamen]

Ok sure I understand this example now! But I am confused because this theorem should hold for orbifolds and sometimes you even find a proof directly for manifolds with boundary (like here: http://www.math.toronto.edu/mgualt/courses/MAT1300F-2012/docs/1300-2012-notes-5.pdf)... I do not have the time now to think about what is going wrong but I'll think more about this tonight!

[Nicknamen]

Oh ok I think I see the problem now. The theorem holds if the value is regular both for f and for f restricted to the border, and this is not the case in your counterexample. This makes me realize further: there is not a way to define the border of a manifold with the current formalization, right? If yes this will for sure be a problem when we will want to formalize Stokes theorem, so this makes me wonder again: should we make models with corners more restrictive? Actually to define the border of a manifold and prove that it is as well a manifold with corners they should be way more restrictive...