[Merged by Bors] - feat: extend smoothness category of manifolds with corners to include analytic manifolds#19696
[Merged by Bors] - feat: extend smoothness category of manifolds with corners to include analytic manifolds#19696
Conversation
PR summary 6d9ca2fe6aImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 4878 | -4 | exceptions for the docPrime linter |
Current commit 6d9ca2fe6a
Reference commit dd2e6e36fc
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).
|
About naming: how about |
grunweg
left a comment
There was a problem hiding this comment.
This change means the following paragraph is also obsolete --- right? Can you take a pass over the module doc-string to ensure the implementation notes are up to date?
We concentrate on C^∞ manifolds: all the definitions work equally well for C^n manifolds, but later on it is a pain to carry all over the smoothness parameter, especially when one wants to deal with C^k functions as there would be additional conditions k ≤ n everywhere. Since one deals almost all the time with C^∞ (or analytic) manifolds, this seems to be a reasonable choice that one could revisit later if needed. C^k manifolds are still available, but they should be called using [HasGroupoid](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Geometry/Manifold/ChartedSpace.html#HasGroupoid) M (contDiffGroupoid k I) where I is the model with corners.
|
Yes, I will need to pass over all docs to adjust it to the new setting. I'll do that once people agree on what they want in the Zulip discussion. |
grunweg
left a comment
There was a problem hiding this comment.
Three small comments; I have to turn to other things now.
Can you add deprecations for the old names, please? Thanks for doing this refactor!
|
I'll add the deprecations once everything has been sorted out in the Zulip discussion: no need to do the same work two or three times... |
There was a problem hiding this comment.
I've reviewed everything once, except for
- Geometry/Manifold/Algebra/Monoid.lean
- Geometry/Manifold/Algebra/SmoothFunctions.lean
- Geometry/Manifold/AnalyticManifold.lean
- Geometry/Manifold/ContMDiff/Defs.lean
- Geometry/Manifold/SmoothManifoldWithCorners.lean
Mostly very minor comments. This PR is so cross-cutting that also doc-strings and lemma names can go stale: because you generalise things to C^n where appropriate, I think some more things should be called "contDiffThing" and not "smoothThing".
I didn't read the file changing it yet, but "smoothMaximalAtlas" is another such example.
I'm repeating myself, but let me say it again anyway: thanks for attempting this monumental feat. It's only natural that there are lots of little details that can go stale.
I've reviewed this diff "from the bottom", so if something is confusing, you may want to read the comments in opposite order.
| (hf : ContMDiffWithinAt (J.prod I) I' n (Function.uncurry f) (t ×ˢ u) (x₀, g x₀)) | ||
| (hg : ContMDiffWithinAt J I m g t x₀) (hx₀ : x₀ ∈ t) | ||
| (hu : MapsTo g t u) (hmn : m + 1 ≤ n) (h'u : UniqueMDiffOn I u) : | ||
| haveI : IsManifold I 1 M := .of_le (le_trans le_add_self hmn) |
There was a problem hiding this comment.
These are annoying, but perhaps that's the price of such a major refactoring. It need not block in this, in any case.
457a78f to
c07cf67
Compare
c07cf67 to
e6fa967
Compare
As a preparation for #19696
|
This PR/issue depends on: |
|
As I also wrote on zulip: I can review the rest of the PR/re-review it on (probably) Tuesday or Wednesday. Review help is very welcome, though. |
|
Remaining steps
This PR is a huge one, but I think this is close to landing! |
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
…munity/mathlib4 into SG_smoothmanifold
|
Thanks for fixing directly some files, and for the thorough review! I think I have taken into account all your comments. I wouldn't rename the files I have switched to |
|
Thanks for the last changes. I think this has waited for long enough and is ready to go. If we find non-ideal uses of the word "smooth", these can be fixed in future PRs. I'll try to merge master, then maintainer merge this. Thanks for your sustained patience! |
|
Mathlib builds; I just pushed a last commit updating the deprecation dates to today. I think this is good to go. |
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
|
This looks really good! Maybe the file Thanks! bors merge |
… analytic manifolds (#19696) Now that `ContDiff` includes smoothness exponents up to analytic functions, we can do the same for manifolds. The PR renames `SmoothManifoldWithCorners` to `IsManifold`, and includes an additional smoothness exponent (ranging from 0 to infinity and omega). The docstring of `IsManifold` emphasizes that this allows (but does not mandate) corners or boundaries. The file `SmoothManifoldWithCorners` itself is not renamed, to avoid confusing git, and will be renamed in a follow-up PR. The current version of the PR also allows an additional smoothness exponent in the algebraic classes like `ContMDiffMul` or `LieGroup`. For all of these, we add a bunch of instances to deduce low smoothness from high smoothness versions (for example, `LieGroup I 2 G` is found by typeclass inference from `LieGroup I ∞ G`). This change makes it possible to do things with the correct assumptions. For instance, the tangent bundle is a fiber bundle assuming only that the manifold is `C^1` (but we have instances saying that it is `C^∞` if the manifold is `C^∞`, analytic if the manifold is analytic). Normally, I should have properly deprecated everything but instances. TODO in follow-up PRs: * rename `SmoothManifoldWithCorners.lean` to `IsManifold.lean` * deprecate the whole file `Manifold.Analytic.lean` Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
|
(I see that this rename has been discussed before, I don't feel strongly, but I think it might be nice for discoverability if you already know the Mathlib name of the concept it's about.) |
|
Pull request successfully merged into master. Build succeeded: |
Now that
ContDiffincludes smoothness exponents up to analytic functions, we can do the same for manifolds. The PR renamesSmoothManifoldWithCornerstoIsManifold, and includes an additional smoothness exponent (ranging from 0 to infinity and omega). The docstring ofIsManifoldemphasizes that this allows (but does not mandate) corners or boundaries.The file
SmoothManifoldWithCornersitself is not renamed, to avoid confusing git, and will be renamed in a follow-up PR.The current version of the PR also allows an additional smoothness exponent in the algebraic classes like
ContMDiffMulorLieGroup. For all of these, we add a bunch of instances to deduce low smoothness from high smoothness versions (for example,LieGroup I 2 Gis found by typeclass inference fromLieGroup I ∞ G).This change makes it possible to do things with the correct assumptions. For instance, the tangent bundle is a fiber bundle assuming only that the manifold is
C^1(but we have instances saying that it isC^∞if the manifold isC^∞, analytic if the manifold is analytic).Normally, I should have properly deprecated everything but instances.
TODO in follow-up PRs:
SmoothManifoldWithCorners.leantoIsManifold.leanManifold.Analytic.lean