Inverse function theorem for manifolds status

Stream: mathlib4

[Matthew Spillman]

Hi everyone,

I'm somewhat new to Lean and recently had a crack at proving the inverse function theorem for manifolds as a learning project. It was mentioned in this thread that there's a PR proving this already (which was almost done at the time), so after running into some issues with my approach I'm curious about how that PR proves the theorem.

My general approach was as follows, for $f : M \to M'$:

1. Define composition of partial diffeomorphisms
2. Show that if $p$ lies in the interior of $M$, then the extended chart at $p$ can be restricted to a partial diffeomorphism $M \to E$, where $E$ is the model vector space (with the trivial manifold structure). Similarly, if $f(p)$ lies in the interior of $M'$, then the chart around $f(p)$ can also be restricted to a partial diffeomorphism $M' \to E'$.
3. Writing $f$ in local coordinates, apply the inverse function theorem for normed vector spaces to obtain a partial diffeomorphism $E \to E'$.
4. Compose this with the chart diffeomorphisms to obtain a partial diffeomorphism $M \to M'$ which will show that $f$ is a local diffeomorphism at $p$.

Steps 1 and 2 went fine, but I got stuck at step 3 since Mathlib's inverse function theorem only provides ContDiff at p and f(p), not on neighborhoods of those points, so we can't actually construct a partial diffeomorphism $E \to E'$. It seems to me that the current formulation of the inverse function theorem isn't quite strong enough for the desired statement for manifolds. I may be missing something here though, as I'm still getting familiar with the ContDiff and related APIs.

Could someone point me to the current PR proving the inverse function theorem? I'd also appreciate comments on whether my points above are valid or if I'm missing something obvious. Although I did this as a learning project, I also may be interested in helping with that PR if there's any work left to do that a relative beginner could help with.

[Yury G. Kudryashov]

See docs#ContDiffAt.eventually

[Yury G. Kudryashov]

Also, if you want to include $C^{\infty}$, then you can use docs#OpenPartialHomeomorph.contDiffAt_symm directly.

[Yury G. Kudryashov]

What's your plan for manifolds with boundary?

[Matthew Spillman]

Ah, docs#ContDiffAt.eventually does seem to be exactly what I was missing, thanks!

[Matthew Spillman]

As for manifolds with boundary, in my understanding the theorem doesn't hold in the usual sense (df invertible -> local diffeomorphism) when p is on the boundary of M, so we must assume that p is in the interior of M. In Lee's book (Problem 4.2) he claims that we can infer $f(p) \in \text{Int}(M')$ from the other hypotheses, so performing this reduction would be a separate task (I'm not sure in what generality that argument applies, since Lee only deals with manifolds modeled on R^n). For now I am not placing any restrictions on $M$ or $M'$ (both can have boundary) but am requiring $p$ and $f(p)$ to be interior points.

As for the case when $p$ is on the boundary of $M$, I suppose we could obtain a weaker statement where we no longer require the sets containing $p$ and $f(p)$ to be open. Or, if $p$ and $f(p)$ were both boundary points, then maybe we could obtain the standard statement, but I think we would need the partial diffeomorphism $E \to E'$ to restrict to a partial diffeomorphism $H \to H'$, and I'm not sure exactly what would be needed to show that. I haven't considered these cases for now as I don't know what would actually be needed. I'm curious how/whether the existing PR handles these cases or if there's another boundary version that I'm not thinking of.

[Yury G. Kudryashov]

ContDiffAt.eventually fails for $C^\infty$, so you may have better luck with the other theorem I've mentioned. I'm going to add more API about this in a few days.

[Yury G. Kudryashov]

(I'm going to migrate from HasFDerivAt + ContinuousLinearEquiv to (fderiv ..).IsInvertible)

[Matthew Spillman]

I ended up finishing it using OpenPartialHomeomorph.contDiffAt_symm as you suggested. The final statement looks like:

variable {𝕜 : Type*} [RCLike 𝕜]
  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
  {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F]
  {H : Type*} [TopologicalSpace H]
  {G : Type*} [TopologicalSpace G]
  {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
  {N : Type*} [TopologicalSpace N] [ChartedSpace G N]
  {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold J n N]

theorem localDiffeomorph_of_mfderiv_iso (hn : n ≠ 0) {f : M → N} (hf : ContMDiff I J n f) {p : M}
    (hp : IsInteriorPoint I p) (hfp : IsInteriorPoint J (f p))
    (hf' : (mfderiv I J f p).ker = ⊥ ∧ (mfderiv I J f p).range = ⊤) :
    IsLocalDiffeomorphAt I J n f p

I went ahead and made a PR into my own fork of mathlib if anyone wants to take a look (I would love feedback, but don't necessarily expect any because people are busy). It's still a bit rough, but at least accomplishes what I set out to do. Thank you for the help Yury!

[Yury G. Kudryashov]

Why don't you make a PR to the upstream Mathlib?

[Michael Rothgang]

I guess the open question is whether this PR or a dusted off and completed version of #26115 would be preferable. As the author of the latter, I'm biased (but it's also been a long time and I haven't looked at the code much since then). I'll update the PR to current master and a fork tomorrow.

[Yury G. Kudryashov]

@Michael Rothgang When you update your PR, could you please compare your API with @Matthew Spillman 's?

[Michael Rothgang]

Yes, I will! (Since I wrote that PR when I knew much less Lean, having a second reference is definitely helpful.)

[Matthew Spillman]

We decided that we would try to merge my version first before fixing up Michael's more general version. My version is now in #34005.