Skip to content

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

Closed
grunweg wants to merge 8 commits intomasterfrom
MR-charts-diffeos2
Closed

[Merged by Bors] - feat: charts are structomorphisms#8160
grunweg wants to merge 8 commits intomasterfrom
MR-charts-diffeos2

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@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 added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-differential-geometry Manifolds etc labels Nov 3, 2023
@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
@grunweg grunweg added awaiting-review and removed awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Nov 4, 2023
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 <grunweg@posteo.de>
@ghost ghost 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 <grunweg@posteo.de>
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 <grunweg@posteo.de>
@ghost ghost 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
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 23, 2023
@grunweg grunweg mentioned this pull request Dec 25, 2023
Closed
1 task
@ghost ghost 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
@ghost ghost 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 (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
winstonyin reviewed Jan 17, 2024
View reviewed changes
winstonyin
winstonyin reviewed Jan 17, 2024
View reviewed changes
@winstonyin
Copy link
Copy Markdown
Collaborator

winstonyin commented Jan 17, 2024

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
Copy Markdown
Collaborator

winstonyin commented Jan 17, 2024

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
@ghost
Copy link
Copy Markdown

ghost commented Feb 6, 2024

This PR/issue depends on:

mcdoll
mcdoll reviewed Feb 6, 2024
View reviewed changes
@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
Copy Markdown
Contributor 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
Copy Markdown
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
Copy Markdown
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.

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Feb 13, 2024
@grunweg
Copy link
Copy Markdown
Contributor 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 <grunweg@posteo.de>
@mathlib-bors
Copy link
Copy Markdown
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 <grunweg@posteo.de>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 13, 2024

Build failed (retrying...):

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 13, 2024

Canceled.

@grunweg
Copy link
Copy Markdown
Contributor 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 <grunweg@posteo.de>
@mathlib-bors
Copy link
Copy Markdown
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 <grunweg@posteo.de>
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 <grunweg@posteo.de>
@hrmacbeth hrmacbeth mentioned this pull request Aug 15, 2025
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sgouezel sgouezel sgouezel left review comments

@mcdoll mcdoll mcdoll left review comments

+1 more reviewer

@winstonyin winstonyin winstonyin left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-differential-geometry Manifolds etc

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@grunweg @winstonyin @sgouezel @mcdoll