local diffeomorphism

Stream: maths

[Nicolò Cavalleri]

@Sebastien Gouezel you did not accept local diffeos when I tried to PR them but now I went beck to the idea that we should have them: what if I want a chart to be recognized as a bundled smooth map? Should I use the constructor at each time?

[Sebastien Gouezel]

I have absolutely no problem with charts as bundled maps. My main comment, though, is that in topological areas of mathlib unbundled maps have proved to be more flexible and easy to use than bundled ones because there are just too many ways to bundle the map (for instance using different smoothness classes for the maps) and building a gluing API between all these points of view would just be a nightmare which is completely avoided by the unbundled point of view. If you have a use case in which bundled charts are really helpful, I'd say go for it, but can you tell us more about this use case?