feat: a map is smooth iff its post-composition with an immersion is#28865
feat: a map is smooth iff its post-composition with an immersion is#28865grunweg wants to merge 50 commits intoleanprover-community:masterfrom
Conversation
PR summary cefe7b7756Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 4 | 3 | large files |
Current commit 9b9519edc6
Reference commit cefe7b7756
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).
The old name did not follow the naming convention; when adding restrOpen in the next commit, the distinction starts to matter.
These are analogues to existing lemmas about subtypeRestr, but I want to use .restr (not .subtypeRestr).
if e is in the maximal atlas, so is e.restr s for any open set s.
…maining) Apart from that, everything is sorry-free
94de9ce to
b70360f
Compare
At best, "is locally an embedding" would work... but need to make that precise (and AFAICT, there's no such notion in mathlib yet). For now, .continuousOn is the closest approximation I have..."
doesn't quite work yet
Perhaps half done, ask on zulip about good design ideas!
b70360f to
cda7f72
Compare
Works, but need more focused time
|
This pull request has conflicts, please merge |
| lemma ContMDiffAt.iff_comp_isImmersionAt | ||
| [IsManifold I n M] [IsManifold J n N] [IsManifold J' n N'] | ||
| {f : M → N} {φ : N → N'} (h : IsImmersionAt F J J' n φ (f x)) | ||
| (hf : ContinuousAt f x) : -- TODO: is this hypothesis needed? |
There was a problem hiding this comment.
At least globally, this condition is indeed necessary - when a φ satisfies this even for discontinuous f it means in particular that any function to a fibre of φ is smooth, so φ has to be injective. If you then take f to be the map from the image of φ to the domain of φ that you get from injectivity you can even show that φ has to be an embedding. I haven't thought about the local variant of this much but assume it is similar.
There was a problem hiding this comment.
Actually I'm not sure the last step of what I said works, because the image of an injective immersion is not always a submanifold... either way, without assuming continuity this definitely won't hold for most immersions.
The continuous case is mostly solved --- except for one detail where I'm not even sure if this is true.
Maybe!, I need to require continuity, at least in general. (Perhaps not for interior points... we'll see!)
A future PR will use this to golf the results in
Icc/Instances.lean.