[Merged by Bors] - feat: local diffeomorphisms#8736
Conversation
|
To comment on your naming remark: I want to rename |
| /-- `f : M → N` is called a **`C^n` local diffeomorphism at *x*** iff there exist | ||
| open sets `U ∋ x` and `V ∋ f x` and a diffeomorphism `Φ : U → V` such that `f = Φ` on `U`. -/ | ||
| def IsLocalDiffeomorphAt (f : M → N) (x : M) : Prop := | ||
| ∃ Φ : LocalDiffeomorphAux I J M N n, x ∈ Φ.source ∧ EqOn f Φ Φ.source |
There was a problem hiding this comment.
This doesn't seem like the most convenient definition of IsLocalDiffeomorphAt. For vector spaces we don't really give a definition, but in the statement of the inverse function theorem HasStrictFDerivAt.to_localInverse we use HasStrictFDerivAt. Would it make sense to lift that definition to manifolds?
There was a problem hiding this comment.
Good point! Over R or C, both definitions are indeed equivalent (one direction follows from the inverse function theorem, the other is PR #8738) --- so it's merely a matter of taste or convenience. In several cases, I find the current definition nicer to use (e.g., a local diffeomorphism has open range, I just added that a bijective local diffeomorphism is a diffeomorphism); for showing a particular map is a local diffeomorphism, the other definition can be more useful. Eventually, we should have both --- and I am indeed working on the inverse function theorem also.
I had chosen my definition to match local structomorphisms and local homeomorphisms (in the sense of textbook mathematics, not PartialHomeomorphs). To me, this definition feels more conceptually correct; I regard the coincidence with isomorphic differential is a special fact for C^n maps.
That said: I don't know if these definitions are still equivalent over p-adic numbers, and which definition is correct on that setting.
@sgouezel Do you know more? What's your opinion here?
Move Diffeomorph.toPartialDiffeomorph further down.
Touch up the docs; introduce PartialDiffeomorph.toLocalHomeomorph.
By the way, should |
|
Yes, they should be. |
…ields to continuousOn_{to,inv}Fun (#8848)
They have type ContinuousOn ..., hence should be named accordingly. Suggested by @fpvandoorn in #8736.
…ields to continuousOn_{to,inv}Fun (#8848)
They have type ContinuousOn ..., hence should be named accordingly. Suggested by @fpvandoorn in #8736.
sgouezel
left a comment
There was a problem hiding this comment.
Can you merge master and fix the build (LocalEquiv has been renamed to PartialEquiv)? Thanks!
|
Updated again, and made a few related golfs. |
Audit all defs and lemmas/theorems for variables that should be implicit; change order so dot notation hypothesis always comes first.
|
awaiting-review |
|
Makes sense; I keep learning more best practices for mathlib. Thanks for explaining all these to me. (I wonder if these rules, e.g. "make arguments implicit if they can be inferred from the others" or "a hypothesis which is used in dot notation should be the first explicit argument" could be linted automatically. Put perhaps there are too many exceptions for this to be worthwhile.) |
|
It's pretty hard to lint those since there are a lot of exceptions. It's rules that one shoud keep in mind, and break sometimes but only in a deliberate way. |
|
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Thanks for the review. |
Define local diffeomorphisms between smooth manifolds. As an auxiliary definition, we add `PartialDiffeomorph`, the analogue of `PartialHomeomorph` for diffeomorphisms. In future PRs, we will - show that local diffeomorphisms have invertible differential - show the converse, using the inverse function theorem: if the differential of $f$ at $x$ is invertible, $f$ is a local diffeomorphism at $x$
|
Pull request successfully merged into master. Build succeeded: |
Following a [comment](#8736 (comment)) by @sgouezel, the hypothesis `IsOpen s` should be the first explicit argument.
Define local diffeomorphisms between smooth manifolds. As an auxiliary definition, we add
PartialDiffeomorph, the analogue ofPartialHomeomorphfor diffeomorphisms.In future PRs, we will
Alternative designs considered
A. a local diffeomorphism$M\to N$ is a diffeomorphism between open sets $U\subset M$ and $V\subset N$ containing $x$ and $f(x)$ , respectively.
mathlib already has diffeomorphisms; this definition would be cumbersome to use, as proving e.g. openness of the image or "a diffeomorphism is a local diffeomorphism" required dealing with subtypes U, V instead of M and N.
B. use the junk value pattern, but bundle a choice of inverse (i.e., replace IsLocalDiffeomorphAt with the current LocalDiffeomorphAux together with a proof that$x\in source$ $f$ is a local diffeomorphism at every point $x$ , it's a local diffeomorphism" at least tedious to state and prove. With the current design, that's by definition.
This makes the implication "if