Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: charts are structomorphisms #8160

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat: charts are structomorphisms #8160

wants to merge 8 commits into from

Conversation

grunweg
Copy link
Collaborator

@grunweg grunweg commented Nov 3, 2023 •
edited
Loading

This is the ChartedSpace analogue of contMDiffOn_extChartAt and contMDiffOn_extChartAt_symm; proving this revealed a few gaps in other API. This may be useful for showing open subsets of a manifold are submanifolds.

@grunweg grunweg marked this pull request as draft November 3, 2023 17:00
@grunweg grunweg force-pushed the MR-charts-diffeos2 branch 2 times, most recently from 02656bd to 68231f2 Compare November 4, 2023 12:42
@grunweg grunweg marked this pull request as ready for review November 4, 2023 12:54
This was referenced Dec 15, 2023
Closed
Closed
mathlib-bors bot pushed a commit that referenced this pull request Dec 17, 2023
@grunweg
feat: add Homeomorph.empty (#9092)
b067a6f 
This came up in #8160 and (independently) sphere-eversion.



Co-authored-by: grunweg <[email protected]>
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 17, 2023
awueth pushed a commit that referenced this pull request Dec 19, 2023
@grunweg @awueth
feat: add Homeomorph.empty (#9092)
e8d31b7 
This came up in #8160 and (independently) sphere-eversion.



Co-authored-by: grunweg <[email protected]>
mathlib-bors bot pushed a commit that referenced this pull request Dec 19, 2023
@grunweg
feat(Data/Set/Function): add MapsTo.map_nonempty (#9093)
a369b3d 
Extracted from #8160.



Co-authored-by: grunweg <[email protected]>
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 22, 2023
@grunweg grunweg force-pushed the MR-charts-diffeos2 branch 2 times, most recently from d38b96e to 27d8e5d Compare December 22, 2023 23:08
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Dec 23, 2023
@grunweg grunweg mentioned this pull request Dec 25, 2023
Open
1 task
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 26, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) labels Jan 7, 2024
@grunweg grunweg force-pushed the MR-charts-diffeos2 branch from fd02049 to cccbe5a Compare January 12, 2024 09:28
@winstonyin
Copy link
Collaborator

I only looked at and golfed one lemma so far, but I like the spirit of this PR! It'll likely come in handy when we define open submanifolds.

@winstonyin
Copy link
Collaborator

FYI, I made #9802 which renamed a couple things. Should be very quick to review and will lead to some renames in this PR as well.

@grunweg grunweg force-pushed the MR-charts-diffeos2 branch from f2b09eb to c7417ce Compare January 20, 2024 20:01
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Feb 9, 2024
@grunweg
Copy link
Collaborator Author

grunweg commented Feb 10, 2024

awaiting-review

@github-actions github-actions bot added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Feb 10, 2024
sgouezel
sgouezel reviewed Feb 13, 2024
View reviewed changes
Copy link
Contributor

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+
Thanks!

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Feb 13, 2024

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@grunweg
Copy link
Collaborator Author

grunweg commented Feb 13, 2024

Thank you for the review.
bors r+

mathlib-bors bot pushed a commit that referenced this pull request Feb 13, 2024
@grunweg
feat: charts are structomorphisms (#8160)
fb1edba 
This is the `ChartedSpace` analogue of `contMDiffOn_extChartAt` and `contMDiffOn_extChartAt_symm`; proving this revealed a few gaps in other API. This may be useful for showing open subsets of a manifold are submanifolds.



Co-authored-by: grunweg <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Feb 13, 2024

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Feb 13, 2024
@grunweg
feat: charts are structomorphisms (#8160)
ab226b4 
This is the `ChartedSpace` analogue of `contMDiffOn_extChartAt` and `contMDiffOn_extChartAt_symm`; proving this revealed a few gaps in other API. This may be useful for showing open subsets of a manifold are submanifolds.



Co-authored-by: grunweg <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Feb 13, 2024

Build failed (retrying...):

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Feb 13, 2024

Canceled.

@grunweg
Copy link
Collaborator Author

grunweg commented Feb 13, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Feb 14, 2024
@grunweg
feat: charts are structomorphisms (#8160)
bb8fb4e 
This is the `ChartedSpace` analogue of `contMDiffOn_extChartAt` and `contMDiffOn_extChartAt_symm`; proving this revealed a few gaps in other API. This may be useful for showing open subsets of a manifold are submanifolds.



Co-authored-by: grunweg <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Feb 14, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: charts are structomorphisms [Merged by Bors] - feat: charts are structomorphisms Feb 14, 2024
@mathlib-bors mathlib-bors bot closed this Feb 14, 2024
@mathlib-bors mathlib-bors bot deleted the MR-charts-diffeos2 branch February 14, 2024 02:40
riccardobrasca pushed a commit that referenced this pull request Feb 18, 2024
@grunweg @riccardobrasca
feat: charts are structomorphisms (#8160)
bd6e811 
This is the `ChartedSpace` analogue of `contMDiffOn_extChartAt` and `contMDiffOn_extChartAt_symm`; proving this revealed a few gaps in other API. This may be useful for showing open subsets of a manifold are submanifolds.



Co-authored-by: grunweg <[email protected]>
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@grunweg @dagurtomas
feat: charts are structomorphisms (#8160)
a174284 
This is the `ChartedSpace` analogue of `contMDiffOn_extChartAt` and `contMDiffOn_extChartAt_symm`; proving this revealed a few gaps in other API. This may be useful for showing open subsets of a manifold are submanifolds.



Co-authored-by: grunweg <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@winstonyin winstonyin winstonyin left review comments

@sgouezel sgouezel sgouezel left review comments

@mcdoll mcdoll mcdoll left review comments

Assignees
No one assigned
Labels
delegated t-differential-geometry Manifolds etc
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@grunweg @winstonyin @sgouezel @leanprover-community-mathlib4-bot @mcdoll