Immersions and smooth embeddings

Stream: PR reviews

[Michael Rothgang]

I think I have found a good way to formalise immersions and smooth embeddings, in a manner encompassing infinite-dimensional manifolds. As my overall PR #23040 is growing large (around 1000 lines already), let me open this topic to track the overall progress.
Proving everything nice one would like about immersions and embeddings is still a moment away (as this requires the inverse function theorem), but quite a few things can already be said.

Already reviewable are

• #23175 (an injective bounded linear operator has closed range iff it is anti-Lipschitz) and
• #23219 (preliminaries about local diffeomorphisms)

The latter will also unblock #8738, which has been sitting idle for about a year now.

[Michael Rothgang]

Thanks for the two reviews already! The next PR in this series is #8738 (local diffeomorphisms have isomorphic differential).

[Michael Rothgang]

I have resumed my work on this, to get things over the line. There are a few PRs which are reviewable already.

[Michael Rothgang]

#28701 (+92/-2) feat: the maximal atlas is closed under restriction
An auxiliary lemma, which seems useful to have anyways, and is used to provide a more intuitive constructor for immersions (in the next PR).

[Michael Rothgang]

#28793 (+276/--4) defines smooth immersions and provides two basic constructors.
I intentionally kept this small to ease reviewing, future PRs will prove more interesting properties.

[Michael Rothgang]

#28840 (+35/-0) feat: add ContinuousLinearEquiv.prodProdProdComm
just got bors-ed already (thanks)

[Michael Rothgang]

#28796 (building on 28793, 100 additional lines) proves that immersions are automatically smooth

[Michael Rothgang]

#28853 (building on 28796, 150 additional lines) proves that products of immersions are immersions

[Michael Rothgang]

As you see, the current bottle-neck is the first PR #28701. @Heather Macbeth As you brought structure groupoids into mathlib, if I understand correctly, is that something you'd like to take a look at?

[Michael Rothgang]

#28793 is now ready for review

[Michael Rothgang]

At long last, mathlib just gained the definition of smooth immersions :tada:. Thanks to Christian Merten and Sébastien Gouezel for the patient and meticuluous reviews, which have helped refine the design a lot.

[Michael Rothgang]

#30356 is the next PR in that series: just 31 lines, for a little API lemma.

[Michael Rothgang]

After that, it will be #28853: the product of immersions is an immersion (+172/-30)

[Michael Rothgang]

(Note that #30356 is in fact ready for review again.)

[Michael Rothgang]

Michael Rothgang said:

After that, it will be #28853: the product of immersions is an immersion (+172/-30)

This PR is ready for review now. (CI fails, but that's a false positive. I can report this on zulip soon. Actually, I had copy-pasted some typeclass hypotheses twice, so the error was legitimate. It's fixed now.)

[Michael Rothgang]

Products of immersions just got merged! Next PRs up for review are
#28796 (+156/-3): immersions are smooth (automatically)

[Michael Rothgang]

#32589 (+97) defines smooth embeddings
It mentions two statements which cannot be proven yet (because they require the corresponding immersion result); I'm happy to remove their statements if preferred.

[Michael Rothgang]

#32760 (+49/-6) proves that the inclusion of an open subset is an immersion

[Michael Rothgang]

Proving it is an open embedding will be easy, once that PR is merged. (Edit: eine and merged)

[Michael Rothgang]

#28796 is ready for review again (the emojibot is lagging behind a bit)

[Michael Rothgang]

The next PR in the sequence will be #28905 (proving the immersions are locally embeddings).