[Merged by Bors] - feat: smooth immersions#28793
[Merged by Bors] - feat: smooth immersions#28793grunweg wants to merge 140 commits intoleanprover-community:masterfrom
Conversation
PR summary 1159dce834
|
| 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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
f2d6c64 to
2e60e92
Compare
6829f56 to
85f7eb6
Compare
bd543ea to
ae609a6
Compare
ae609a6 to
9c8e4d5
Compare
If `G` is a `StructureGroupoid` that is `ClosedUnderRestriction`, if `e` is a chart in the maximal atlas of `G`, then so is any restriction `e.restr s` to an open set `s`. In #28793, I will use this to give a more natural constructor for "f is an immersion at x". From the path towards smooth immersions, embeddings and embedded submanifolds. Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
If `G` is a `StructureGroupoid` that is `ClosedUnderRestriction`, if `e` is a chart in the maximal atlas of `G`, then so is any restriction `e.restr s` to an open set `s`. In #28793, I will use this to give a more natural constructor for "f is an immersion at x". From the path towards smooth immersions, embeddings and embedded submanifolds. Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
9c8e4d5 to
5eb960a
Compare
…nity#28701) If `G` is a `StructureGroupoid` that is `ClosedUnderRestriction`, if `e` is a chart in the maximal atlas of `G`, then so is any restriction `e.restr s` to an open set `s`. In leanprover-community#28793, I will use this to give a more natural constructor for "f is an immersion at x". From the path towards smooth immersions, embeddings and embedded submanifolds. Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
…nity#28701) If `G` is a `StructureGroupoid` that is `ClosedUnderRestriction`, if `e` is a chart in the maximal atlas of `G`, then so is any restriction `e.restr s` to an open set `s`. In leanprover-community#28793, I will use this to give a more natural constructor for "f is an immersion at x". From the path towards smooth immersions, embeddings and embedded submanifolds. Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
|
Nice, thanks! |
d75f73d to
3999186
Compare
|
@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? |
|
(Obviously, this needs to be added to the module doc-string: I'll do that after lunch.) |
|
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
left a comment
There was a problem hiding this comment.
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.
|
The initial motivation for all the |
|
Should there be an "implementation notes" section describing the universe issues in some detail? (Is there anything else missing for this to get merged?) |
|
And this PR is definitely also missing |
|
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 Update: the empty case proved fine after all, we already have a |
this one is/will be large enough already
|
I just add two paragraphs of implementation notes and augmented the PR description. |
|
Great. Let's get this in. Thanks a lot for all the time you spent on this, and bearing with all our comments! |
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 Co-authored-by: Christian Merten <christian@merten.dev>
|
Pull request successfully merged into master. Build succeeded: |
|
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.) |
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
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,
Manifold/Instances/Icc.lean(feat(Manifold/Instances/Icc): golf smoothness proof using immersions #29077)Shrinkinstances for NormedSpace and ContinuousLinearEquiv #31897Most of the above has been done at https://github.com/grunweg/mathlib4/tree/MR-define-immersions.