feat: define immersions and smooth embeddings in infinite dimensions#23040
feat: define immersions and smooth embeddings in infinite dimensions#23040
Conversation
Sadly, we cannot prove most nice things about them yet, as we don't have the inverse function theorem yet.
PR summary 93f7c1d0aaImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 922 | 2 | erw |
Current commit 93f7c1d0aa
Reference commit ddb4ebecc0
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).
I'd merely like to ask for equality on the source of the inverse extChart
In finite dimensions, that certainly holds; need to think about inf-dim
The naive proof certainly fails (we get a coordinate change between the two charts in the middle, which can be anything, and need not be linear at all). Can we always "modify" a slice chart to match a modification downstairs? I presume no, but would need to think...
aad2e30 to
bf688fd
Compare
…f composition (coming next, after lunch)
…osition lemmas with diffeos.
…what I need is mostly in mathlib.
|
This pull request has conflicts, please merge |
I wanted this lemma both while working on an early version of leanprover-community#28056 and while working on leanprover-community#23040: time to add it. Besides, it fills a natural API gap.
I wanted this lemma both while working on an early version of leanprover-community#28056 and while working on leanprover-community#23040: time to add it. Besides, it fills a natural API gap.
I wanted this lemma both while working on an early version of leanprover-community#28056 and while working on leanprover-community#23040: time to add it. Besides, it fills a natural API gap.
|
Status: #28793 and friends add the basic definitions (and basic API) - let's land those first and then revisit this PR (for the "composition of immersions") part. |
I wanted this lemma both while working on an early version of leanprover-community#28056 and while working on leanprover-community#23040: time to add it. Besides, it fills a natural API gap.
I wanted this lemma both while working on an early version of leanprover-community#28056 and while working on leanprover-community#23040: time to add it. Besides, it fills a natural API gap.
I wanted this lemma both while working on an early version of leanprover-community#28056 and while working on leanprover-community#23040: time to add it. Besides, it fills a natural API gap.
Sadly, we cannot prove most nice things about them yet, as we don't have
the inverse function theorem yet.
TODO: prove the few things we can already say
depends on: feat: immersions are smooth #28796
depends on: [Merged by Bors] - feat: product of immersions is an immersion #28853
depends on: [Merged by Bors] - chore: an injective bounded linear operator has closed range iff it is anti-Lipschitz #23175 (preliminaries)
depends on: feat: split continuous linear maps #23186
depends on: another PR, about
MSplitAt(to be filed) - and perhaps some prerequisites about products of complemented modules etc.depends on: [Merged by Bors] - feat: local inverse of a diffeomorphism #23219 (preliminaries about local diffeomorphisms)
depends on: [Merged by Bors] - feat: differential of a local diffeomorphism is a continuous linear equivalence #8738
in fact, feat: extended charts are local diffeomorphisms on their source #9273 is not a strict pre-requisite for this. It suffices to know "extended charts have invertible differentials", which isInvertible_mfderiv_extChartAt mostly proves. (There's nothing wrong with completing that PR, for all interior points.)