Inverse function theorem on manifolds

Stream: Is there code for X?

[Michael Rothgang]

Mathlib does have the inverse and implicit function theorems, but only on normed spaces.

The manifold version would be useful for formalising local diffeomorphisms, which come up naturally in the context of this thread.

[Geoffrey Irving]

I proved one particular case of that here, but it's not in good shape for general use (and of course not yet upstreamed): https://github.com/girving/ray/blob/1c46b8324e991d6d82bb50fdf93c821599c94314/Ray/AnalyticManifold/Inverse.lean#L305

[Heather Macbeth]

There are several ways to phrase the implicit function theorem. Probably the version for zero set of a section of a vector bundle is the most general?

[Heather Macbeth]

For the inverse function theorem, I'd expect to phrase it in terms of docs#StructureGroupoid.IsLocalStructomorphWithinAt

[Michael Rothgang]

For my setting, I only need the consequence "if $f$ is $C^n$ at $x$ and the differential $df_x$ is a linear isomorphism, then $f$ is a local diffeomorphism at $x$, so any version (in several dimensions, covering real manifolds) would do.

In general, the version for the zero set of a section sounds like a good general statement to aim for.

[Notification Bot]

A message was moved here from #Is there code for X? > docs#StructureGroupoid.IsLocalStructomorphWithinAt by Heather Macbeth.

[Heather Macbeth]

Heather Macbeth said:

For the inverse function theorem, I'd expect to phrase it in terms of docs#StructureGroupoid.IsLocalStructomorphWithinAt

Note that this has the advantage of giving a "category -invariant" phrasing, so preliminary work can be shared between the analytic (of interest to Geoffrey) and smooth categories

[Geoffrey Irving]

It's off topic, but the fun thing about the complex analytic setting is that injective functions have global analytic inverses. :)

https://github.com/girving/ray/blob/main/Ray/AnalyticManifold/GlobalInverse.lean#L129

Edit: Changed "analytic" to "complex analytic".

[Michael Rothgang]

Geoffrey Irving said:

It's off topic, but the fun thing about the analytic setting is that injective functions have global analytic inverses. :)

https://github.com/girving/ray/blob/main/Ray/AnalyticManifold/GlobalInverse.lean#L129

I knew this result, but it never ceases to amaze me anew :-)

[Heather Macbeth]

Really??? Isn't x^3 on R a counterexample?

[Geoffrey Irving]

Complex analytic functions, that is. :)

[Junyan Xu]

It's off topic, but the fun thing about the analytic setting is that injective functions have global analytic inverses. :)

Why is this particularly amazing? I think this also holds for C^1 functions if you assume nonvanishing of Jacobian. The inverse function theorem would give you C^1 local inverses, so the global inverse is C^1.

For complex C^1/analytic functions (in one dimension, not sure about higher dimensions), local injectivity implies nonvanishing of derivatives, so we don't need this extra assumption.

A more nontrivial result is invariance of domain, which applies to an injective continuous map between Euclidean spaces of the same (finite) dimension, without any differentiability hypothesis.

[Junyan Xu]

not sure about higher dimensions

Apparently it's also true in higher dimensions.

[Michael Rothgang]

Heather Macbeth said:

Heather Macbeth said:

For the inverse function theorem, I'd expect to phrase it in terms of docs#StructureGroupoid.IsLocalStructomorphWithinAt

Note that this has the advantage of giving a "category -invariant" phrasing, so preliminary work can be shared between the analytic (of interest to Geoffrey) and smooth categories

I've thought about this for way too long in the past days, but I now have proven a "categorical" version of the inverse function theorem: for Banach spaces for now; Banach manifolds will come next. Its conclusion is phrased in terms of G.isLocalStructomorphWithinAt (thanks for the pointer!), its hypotheses in terms of a condition on the pregroupoid inducing G.

Applying this to the smooth or analytic category entails extracting the underlying pregroupoid.

I've done this for contDiffGroupoid on a branch. This extraction breaks a few proofs; I'm out of my depth fixing them. The issue is that unfolding the definition of the groupoid changed... Probably an easy fix if you know what to do. Help is appreciated.

[Ruben Van de Velde]

@Michael Rothgang I fixed the issues locally; should I push them to the branch directly?

[Ruben Van de Velde]

@Michael Rothgang I noticed you didn't PR your branch yet; any reason?

[Michael Rothgang]

Mostly because my work on the IFT isn't full complete yet. (I have a proof of concept result on a branch, which shows to me that my approach works. It shows a categorical version of the inverse function theorem, and does most of the proof that C^n maps on normed spaces fit this framework. Next up is filling in some sorries and generalising to C^n maps on manifolds. This will happen, but most likely only in the new year.)

That said: there's no reason not to submit this branch; I just did so in #9091. (I borked my original branch, so created a new one.)

[Michael Rothgang]

@Ruben Van de Velde