[Merged by Bors] - feat: smooth immersions

[grunweg]

Define smooth immersions between manifolds. We use a definition which allows for corners, infinite dimension and arbitrary fields. This matches the mathematical literature for e.g. real Banach manifolds with corners (even though there is no textbook treating manifolds as general as mathlib's).

This PR provides four central definitions: being an immersion at a point, and being an immersion everywhere,
plus a variant of these with a fixed complement. (Being an immersion at a point is a property with respect to some choice of complement in the model normed space of the codomain. In most applications, there is no need to control this complement. Such control will be helpful, however, when considering the local characterisation of submanifolds: locally, a submanifold is described either as the image of an immersion, or the preimage of a submersion --- w.r.t. the same complement. Having access to a definition version with complements allows stating this equivalence cleanly.

This PR only provides the basic API to keep its size (relatively) small. Future PRs will add more substance, and

• prove that immersions are C^n ([Merged by Bors] - feat: immersions are smooth #28796),
• prove another characterisation of immersions: f is immersed at x iff the differential df_x splits,
  i.e. is injective, has closed range and its image has a closed complement,
  and in particular that a map between finite-dimensional manifolds over a complete field is an
  immersion iff its differential is injective,
• use this to prove that the product ([Merged by Bors] - feat: product of immersions is an immersion #28853) and composition of immersions is an immersion,
• use this theory to give more conceptual proofs of half of Manifold/Instances/Icc.lean ([Merged by Bors] - feat(Manifold/Instances/Icc): golf smoothness proof using immersions #29077)
• define smooth embeddings and immersed and embedded smooth submanifolds.

---

• depends on: [Merged by Bors] - feat: the maximal atlas is closed under restriction #28701
• depends on: [Merged by Bors] - chore(OpenPartialHomeomorph): tag three lemmas with grind #31123
• depends on: [Merged by Bors] - feat: transfer normed spaces and continuous linear equiv's across equ… #31896
• depends on: [Merged by Bors] - feat: Shrink instances for NormedSpace and ContinuousLinearEquiv #31897
• depends on: [Merged by Bors] - feat: ContinuousLinearEquiv.submoduleMap and friends #31899

Most of the above has been done at https://github.com/grunweg/mathlib4/tree/MR-define-immersions.

[github-actions]

PR summary 1159dce834

Import changes for modified files

No significant changes to the import graph
M scripts/count-trans-deps.py
M scripts/count-trans-deps.py
M scripts/count-trans-deps.py

Import changes for all files

Files	Import difference
Mathlib.Geometry.Manifold.LocalSourceTargetProperty (new file)	1566
Mathlib.Geometry.Manifold.Immersion (new file)	1945

---

Declarations diff

+ ImmersionAtProp
+ IsImmersion
+ IsImmersionOfComplement
+ IsLocalSourceTargetProperty
+ LiftSourceTargetPropertyAt
+ LocalPresentationAt
+ instance (h : IsImmersion I J n f) : NormedAddCommGroup h.complement
+ instance (h : IsImmersion I J n f) : NormedSpace 𝕜 h.complement
+ instance (h : IsImmersionAt I J n f x) : NormedAddCommGroup h.complement := by
+ instance (h : IsImmersionAt I J n f x) : NormedSpace 𝕜 h.complement := by
+ instance (hf : IsImmersionAtOfComplement F I J n f x) : NormedAddCommGroup hf.smallComplement := by
+ instance (hf : IsImmersionAtOfComplement F I J n f x) : NormedSpace 𝕜 hf.smallComplement := by
+ isImmersion
+ isImmersionAtOfComplement_complement
+ isImmersionOfComplement_complement
+ isLocalSourceTargetProperty_immersionAtProp
+ localPresentationAt
+ small
+ smallComplement
+ smallEquiv
++ complement
++ congr
++ congr_F
++ congr_iff
++ congr_iff_of_eventuallyEq
++ equiv
++ map_target_subset_target
++ mk_of_charts
++ target_subset_preimage_target
++ trans_F
++ writtenInCharts
+++ codChart
+++ codChart_mem_maximalAtlas
+++ congr_of_eventuallyEq
+++ domChart
+++ domChart_mem_maximalAtlas
+++ isImmersionAt
+++ mem_codChart_source
+++ mem_domChart_source
+++ mk_of_continuousAt
+++ property
+++ source_subset_preimage_source

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[sgouezel]

Nice, thanks!

[grunweg]

@chrisflav I just pushed a first version using local properties to abstract some of the proofs. (They do indeed become a bit clearer.) What do you think?

[grunweg]

(Obviously, this needs to be added to the module doc-string: I'll do that after lunch.)

[grunweg]

Thanks for your comments; all addressed!

Feel free to list missing API lemmas and I'll be happy to add them in a future PR!

[sgouezel]

Have you included the lemma saying that IsImmersionAtOfComplement implies IsImmersionAt? I thought it was the goal of all the small business, but I can't find it.

[grunweg]

The initial motivation for all the Small stuff was to make the constructions mk_of_charts and mk_of_continuousAt for immersions truly usable (by allowing a complement in any universe). I agree that the lemma you pointed out was sorely missing, though, and added it now.

[grunweg]

Should there be an "implementation notes" section describing the universe issues in some detail? (Is there anything else missing for this to get merged?)

[grunweg]

And this PR is definitely also missing IsImmersionOfComplement.isImmersion; I'll add that in a moment.

[grunweg]

Added that: this exposed some more missing API which I also just added.

The proof for the case "M is empty" is a bit awkward because we need to provide a dummy type in the existential. It's not obvious, however, to provide API similar to smallEquiv and smallComplement for IsImmersionOfComplement --- the definitions at a point use the equivalence we have there, which we cannot do as we only have a equivalence at some point. For the empty type the immersion property is vacuously true, but finding a complement in the right universe is a bit annoying.

Update: the empty case proved fine after all, we already have a NormedSpace instance on PUnit.

[grunweg]

I just add two paragraphs of implementation notes and augmented the PR description.

[sgouezel]

Great. Let's get this in. Thanks a lot for all the time you spent on this, and bearing with all our comments!
bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Post-Build Step
• Build
• Lint style

[grunweg]

Thanks a lot, @sgouezel and @chrisflav for the very detailed and meticulous reviews! While this process took a while, I feel the process was clearly worth it --- I learned a lot from your comments and the final result is much better because of it. Thanks in particular for doing the final review rounds this quickly, this is much appreciated.

This PR is (of course) only the first step towards submanifolds in mathlib. I hope the subsequent PRs can be split among more reviewers. (Of course, you're welcome to review as many of them as you like.)