feat: immersions are smooth#28796
feat: immersions are smooth#28796grunweg wants to merge 47 commits intoleanprover-community:masterfrom
Conversation
PR summary 0401a17286
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Geometry.Manifold.Immersion | 2230 | 2239 | +9 (+0.40%) |
| Mathlib.Geometry.Manifold.SmoothEmbedding | 2234 | 2241 | +7 (+0.31%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Geometry.Manifold.SmoothEmbedding |
7 |
Mathlib.Geometry.Manifold.Immersion |
9 |
Declarations diff
++ contMDiffAt
++ contMDiffOn
++ continuousAt
++ continuousOn
++ mapsto_domChart_source_codChart_source
+++ contMDiff
You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/reporting/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).
abc479f to
b35944e
Compare
|
This pull request has conflicts, please merge |
0e73fee to
f10845e
Compare
|
This pull request has conflicts, please merge |
Use I and J consistently. Also add further variables for use when adding products.
There are a bunch of CI warnings, which are all false positives.
|
Note that you have to merge master for the linting stage. |
| theorem continuousAt (h : IsImmersionAtOfComplement F I J n f x) : ContinuousAt f x := | ||
| h.continuousOn.continuousAt (h.domChart.open_source.mem_nhds (mem_domChart_source h)) | ||
|
|
||
| variable [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] |
There was a problem hiding this comment.
Is that really needed? If a map is an immersion, then in some charts in the C^n maximal atlas it is well behaved. By definition, the changes of coordinates wrt these charts are C^n, so no need to add more assumptions, right?
Same thing elsewhere in the PR.
There was a problem hiding this comment.
In my book, IsManifold says exactly "the changes of coordinates are well-behaved". The hypothesis on I' is not necessary; let me remove it.
There was a problem hiding this comment.
Sure. What I'm saying is that here it's not needed because what you need is already implied by the assumption IsImmersionAt.
There was a problem hiding this comment.
I'm not convinced. I presume you're thinking of the following argument.
IsImmersionAtimplies thatfread in some charts (h.domChart.extend Iandh.codChart.extend J) is smooth --- let's call itf'- if both extended charts are smooth, thus also
g := (h.codChart.extend J).symm ∘ f' ∘ (h.domChart.extend I)is smooth - locally,
f = g, so we are done
Steps 1 and 3 work (and Lean agrees). The issue is in the second step: why would e.g. h.domChart.extend I be smooth? The key lemmas ("at atlas member is C^n" contMDiffOn_of_mem_maximalAtlas resp. the inverse version contMDiffOn_symm_of_mem_maximalAtlas) use the manifold structure...
do you see something I don't see, which is how to get around this?
There was a problem hiding this comment.
ContMDiffOn/ContMDiffAt are defined w.r.t. the extended charts at that point --- but being an immersion only gives you some chart in the maximal atlas. To me, requiring some compatibility condition makes sense.
There was a problem hiding this comment.
In the definition of IsImmersionAt (or, unfolding everything, in LocalPresentationAt), there is the condition that the chart you get is in IsManifold.maximalAtlas I n M. This tells you that the composition of this chart with (the inverse of) any of the reference charts gives a C^n map (at least locally around the point you're looking at). By composition, you get that the composition of any two of the reference charts is also C^n there. I don't see what more you could need.
|
-awaiting-author |
|
-awaiting-author |
|
This pull request has conflicts, please merge |
Cherry-picked from leanprover-community#28796
Cherry-picked form leanprover-community#28796, and used to prove immersions are smooth.
|
Status update: I have started to work on the generalisation mentioned above. I'm certain it will work, but there is a bunch of missing API I'll have to fill in first. In the mean-time, the preliminary lemmas have incurred a merge conflict --- I have split out #36816 with just them. |
…er-community#36816) Cherry-picked from leanprover-community#28796: it might not get used in the eventual PR there, but this lemma seems useful independently. (In any case, I would like to use these lemmas now, and there is no reason to wait until I have filled in the missing API for leanprover-community#28796.)
The conventional textbook definition demands that an immersion be smooth.
When asking for the immersion to have local slice charts (as we do), this implies smoothness automatically.