[Merged by Bors] - feat(geometry/manifold): stab at diffeomorphisms

[Nicknamen]

---

This PR implements diffeomorphisms. Many lemmas are missing but I plan to add them when I need them, not to create unnecessary clutter.

[Nicknamen]

PS Planning to PR the smooth inverse function theorem this weekend -- should be useful for this!

Great! So I guess the regular value theorem will follow?

I wonder if the answer is to frame more things in terms of universal properties?

I am not sure what you exactly mean by this here but in general I strongly agree with stating stuff with universal properties when it is possible. In any case, I believe we can come up with ideas to save structomorphisms, but supposing all ways require a huge refactor of the geometry library, what are the big advantages of saving them? Why would it be a much better description than writing manually isomorphisms each time? I believe the flexibility of manually written isomorphism can also be an advantage! (Especially if we do not want to also generalize normal morphisms)

[Nicknamen]

Suggestions for better notation are welcome (I still would like a notation here but I'd be happy to improve the one I chose)

[sgouezel]

I am completely convinced by the diffeomorphism part. A little bit less by the local diffeos part: I am wondering if there is really added value to have them bundled, or if an unbundled Prop (like local_homeomorph.mdifferentiable) would be more usable. For the differentiable ones, I used unbundled because it allowed me to say conveniently that charts (which are by definition local homeos) are in fact differentiable.

Do you have applications in mind where bundled local diffeos would be more convenient than a Prop like local_homeomorph.mdifferentiable?

[Nicknamen]

@sgouezel thanks for reviewing. Just to say, if you do it because I urged you but you would not really have time to review right now, it is totally not a problem for me if you want to wait some weeks, I am not in a rush!

[Nicknamen]

Do you have applications in mind where bundled local diffeos would be more convenient than a Prop like local_homeomorph.mdifferentiable?

I used them mainly for vector bundles. I see things could probably be done as you suggest, but the con I see is that it would break the symmetry between the topology and the geometry library and hence all statements and proofs should be written in a different way. I agree this is not hugely important but still it is handy this way.

I do totally see your point, but I do not see why in the case of charts for example we do not rename atlas to atlas' and chart_at to chart_at' and then define atlas to be the corresponding set of diffeomorphism by using local_homeomorph.to_local_diffeomorph. In my understanding, on of the reasons to have things bundled in general is that this way Lean finds proofs on its own and you do not need to tell it explicitly which homeomorphs are smooth, plus we would really want to think to charts as diffeos rather than homeos, wouldn't we?

[sgouezel]

The point of the atlas is that it is associated to the manifold once and for all, and then you can discuss its smoothness. If you have an analytic manifold, you can also see it as as C^\infty manifold, a C^n manifold for any n, a PL manifold or a topological manifold. Which would amount to several ways to enhance charts, by bundling different classes of smoothness in them. But this would mean registering a bunch of glue to say how the restriction of one bundled chart to another smoothness degree behaves. The version "one size fits all" with only local homeos as first-class citizens, and props giving additional properties, looks more light-weight.

[Nicknamen]

The point of the atlas is that it is associated to the manifold once and for all, and then you can discuss its smoothness. If you have an analytic manifold, you can also see it as as C^\infty manifold, a C^n manifold for any n, a PL manifold or a topological manifold. Which would amount to several ways to enhance charts, by bundling different classes of smoothness in them. But this would mean registering a bunch of glue to say how the restriction of one bundled chart to another smoothness degree behaves. The version "one size fits all" with only local homeos as first-class citizens, and props giving additional properties, looks more light-weight.

Ok I believe what you say can be attained with coercions and namespaces in an elegant way, but I see your point, let me see what things would look like your way. I might take a while cause I am very busy lately, but in the while I'll take out local diffeos from this PR so that diffeos can be merged.

[sgouezel]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests