feat: define SliceModel typeclass for models with corners for embedded submanifolds#24550
feat: define SliceModel typeclass for models with corners for embedded submanifolds#24550
SliceModel typeclass for models with corners for embedded submanifolds#24550Conversation
Sadly, we cannot prove most nice things about them yet, as we don't have the inverse function theorem yet.
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...
…f composition (coming next, after lunch)
…osition lemmas with diffeos.
…what I need is mostly in mathlib.
PR summary c7eef3587dImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 922 | 2 | erw |
Current commit c7eef3587d
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).
|
This PR/issue depends on:
|
These were needed for #24550, which is a step towards defining smooth submanifolds.
|
This pull request has conflicts, please merge |
…nity#26083) which are `LinearEquiv.{prodUnique,uniqueProd}` as a continuous linear equivalence. Discovered when working on slice models for defining submanifolds (leanprover-community#24550), one step towards defining smooth submanifolds. This PR continues the work from leanprover-community#23971.
…nity#26083) which are `LinearEquiv.{prodUnique,uniqueProd}` as a continuous linear equivalence. Discovered when working on slice models for defining submanifolds (leanprover-community#24550), one step towards defining smooth submanifolds. This PR continues the work from leanprover-community#23971.
…nity#26083) which are `LinearEquiv.{prodUnique,uniqueProd}` as a continuous linear equivalence. Discovered when working on slice models for defining submanifolds (leanprover-community#24550), one step towards defining smooth submanifolds. This PR continues the work from leanprover-community#23971.
|
Closing in favour of #26087. |
Still work in progress: TODO write a proper module doc-string and commit message.