(Extended) chart is a local diffeomorphism

Stream: Is there code for X?

[Michael Rothgang]

Say: When M is a smooth manifold without boundary, modelled on the pair (E,H) and e is a chart of M, the extended chart I \circ e : M \to E is a local diffeomorphism on e.source. (I have not thought about the case of boundary.)

Mathlib seems to have the an open subset of M is a smooth manifold again, but not much more material about diffeomorphisms. (I only see Diffeomorph.lean; WhitneyEmbedding.lean is apparently the only file importing this.)

[Michael Rothgang]

Building on this: we're also missing the fact that the differential of a diffeomorphism (at each point) is a linear isomorphism, right?

[Heather Macbeth]

@Michael Rothgang There is also some material about diffeomorphisms phrased in the greater generality of docs#Structomorph, for example this condition for well-behaved groupoid composition: docs#StructureGroupoid.HasGroupoid.comp. I think I would advocate for working with that concept rather than docs#Diffeomorph, where possible.

[Michael Rothgang]

@Heather Macbeth Thank you for the pointer, indeed I hadn't seen Structomorph yet. I agree that this looks right the right conceptual framework for the charts statement.

[Michael Rothgang]

A short update: I have formalised most of both points above; I'm not refactoring it to make it mathlib-ready.
For instance, the second item holds generally for local diffeomorphisms at a point - so I'm also formalising local diffeomorphisms.

[Michael Rothgang]

Trying to actually prove this ("charts are structomorphisms"), I realised an obvious complication. A chart on a manifold M modelled on (E,H) is not a structomorphism, as charts are only local homeomorphisms. Does mathlib have that open subsets of manifolds are manifolds? Then, I could regard charts as honest homeomorphisms between these subsets.

I'm not sure if that's the best approach, or one should rather define a notion of "local structomorphisms": a function that's a structomorphisms on an open set and has junk values everywhere else. I do have local diffeomorphisms on a branch, so showing "a local structomorphism of $C^m$ manifolds is a local $C^m$ diffeo"doesn't seem too bad.

[Michael Rothgang]

As I understand it, we have some of the way to "open subsets of manifolds are manifolds", but not everything

• we don't have yet that an open subset of a charted space (whose structure groupoid is ClosedUnderRestriction) is a charted space,
• but we do have docs#TopologicalSpace.Opens.instHasGroupoid and this instance which show the structure groupoid part of this.
• (We also have that continuous, C^m and analytic groupoids are ClosedUnderRestriction.)

[Heather Macbeth]

Michael Rothgang said:

Does mathlib have that open subsets of manifolds are manifolds? Then, I could regard charts as honest homeomorphisms between these subsets.

As I understand it, we have some of the way to "open subsets of manifolds are manifolds", but not everything

• we don't have yet that an open subset of a charted space (whose structure groupoid is ClosedUnderRestriction) is a charted space,

@Michael Rothgang I think we do, see
docs#TopologicalSpace.Opens.instChartedSpace
(or do I misunderstand)? in addition to the instances you mentioned for the structure groupoid compatibility
docs#TopologicalSpace.Opens.instHasGroupoid
docs#TopologicalSpace.Opens.instSmoothManifoldWithCornersSubtypeMemOpensInstMembershipInstSetLikeOpensInstTopologicalSpaceSubtypeInstChartedSpace

[Michael Rothgang]

Oh, nice. Thanks for pointing this out! (My searching strategy using apply? had failed (I didn't search with Opens in the context, only with a set and a separate hypothesis of its openness). I've learned to use loogle now :-)

[Michael Rothgang]

My proof that charts are structomorphisms is complete now (draft PR at #8160) --- except for one mathematically trivial detail I'm stuck at: the case of the chart source being empty. In this case the target is also empty, but establishing the structomorphism between the empty set (in two different spaces) doesn't work easily.

I need to go now; can write more about the precise error later.Update: asked here; the other sorry is pushed on the branch.

[Michael Rothgang]

Thanks to help on the other thread, this PR is now ready for review.

[Michael Rothgang]

Splitting ContMDiff.lean, I realised that the desired result is in fact already (essentially) in mathlib:
docs#contMDiffAt_extend shows smoothness of each extended chart, docs#contMDiffAt_extend_symm for its inverse. If M is boundaryless, source and target are open and we get an actual diffeomorphism.
PR #8160 may still be useful (e.g., it adds some basic API for structomorphisms), but not for any specific application I have in mind.