Skip to content

[Merged by Bors] - feat: product of immersions is an immersion#28853

Closed
grunweg wants to merge 24 commits intoleanprover-community:masterfrom
grunweg:immersions-prodMap
Closed

[Merged by Bors] - feat: product of immersions is an immersion#28853
grunweg wants to merge 24 commits intoleanprover-community:masterfrom
grunweg:immersions-prodMap

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Aug 24, 2025 •
edited
Loading

@grunweg grunweg added the t-differential-geometry Manifolds etc label Aug 24, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 24, 2025 •
edited
Loading

PR summary 790901a8c9

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ EqOn.left_of_eqOn_prodMap
+ EqOn.prodMap
+ EqOn.right_of_eqOn_prodMap
+ eqOn_prodMap_iff
+ eqOn_prod_iff
+ extend_prod
+ mem_maximalAtlas_iff
+ mem_maximalAtlas_prod
+ prod_symm_trans_prod
+++++ prodMap

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@grunweg grunweg force-pushed the immersions-prodMap branch from d8d1bcd to ab38403 Compare August 24, 2025 10:51
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 24, 2025
This was referenced Aug 24, 2025
Open
Open
@grunweg grunweg force-pushed the immersions-prodMap branch from 5a72bcc to 1da595e Compare August 28, 2025 09:38
@grunweg grunweg mentioned this pull request Aug 28, 2025
Closed
5 tasks
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-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 Sep 8, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Sep 8, 2025

This pull request has conflicts, please merge master and resolve them.

@grunweg grunweg force-pushed the immersions-prodMap branch from 1da595e to 7efd1ab Compare October 1, 2025 14:53
@github-actions github-actions 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 Oct 1, 2025
@grunweg grunweg force-pushed the immersions-prodMap branch 2 times, most recently from d373b88 to c061805 Compare October 1, 2025 15:49
@grunweg grunweg mentioned this pull request Oct 2, 2025
Open
7 tasks
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-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 Oct 2, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Oct 2, 2025

This pull request has conflicts, please merge master and resolve them.

@grunweg grunweg force-pushed the immersions-prodMap branch from c061805 to a15b4fa Compare October 11, 2025 21:35
@grunweg grunweg removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 11, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Nov 19, 2025

This pull request has conflicts, please merge master and resolve them.

@mathlib4-merge-conflict-bot mathlib4-merge-conflict-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 Nov 19, 2025
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Nov 28, 2025

The variable linter warnings seem like a bug to me: they cannot actually be removed.

@github-actions github-actions 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 Nov 28, 2025
grunweg
grunweg commented Dec 8, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor Author

@grunweg grunweg left a comment

Choose a reason for hiding this comment

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

Thanks for your review! I have addressed all comments now.

@grunweg grunweg removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 8, 2025
grunweg added a commit to grunweg/mathlib4 that referenced this pull request Dec 8, 2025
@grunweg
feat: smooth embeddings
2238baf 
Define smooth embeddings between smooth manifolds: a map is a smooth embedding iff it is both
a smooth immersion and a topological embedding. We also prove basic properties (such as congruence
or being stable under products); stronger results will come in future PRs.

Note that unlike smooth immersions, we do not add definitions for
- being a smooth embedding on a set (as this doesn't exist in the topological category either),
- being an embedding at a point (being an embedding is a global notion; moreover, every immersion is
  locally an embedding anyway, so "being an immersion at x" is sufficient to state this)
- variants with respect to a fixed complement: the motivation for immersions (considering the
  equivalent local descriptions of smooth submanifolds) do not apply to this global notion.

-----

- [ ] depends on: leanprover-community#28853

TODO: write a proper module doc-string; this is probably only worth landing
once enough immersions API has been merged
@grunweg grunweg mentioned this pull request Dec 8, 2025
Closed
1 task
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-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 9, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Dec 9, 2025

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions 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 9, 2025
chrisflav
chrisflav reviewed Dec 9, 2025
View reviewed changes
@chrisflav chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 9, 2025
grunweg and others added 3 commits December 9, 2025 18:22
@grunweg
Grind
0bb25ec
@grunweg @chrisflav
Apply suggestions from code review
76d9ff4 
Co-authored-by: Christian Merten <christian@merten.dev>
@grunweg
Rename
8a89967
@grunweg grunweg removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 9, 2025
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Dec 9, 2025

Thanks! I addressed your comments again.

chrisflav
chrisflav approved these changes Dec 9, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@chrisflav chrisflav left a comment

Choose a reason for hiding this comment

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

Thanks!
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 9, 2025

🚀 Pull request has been placed on the maintainer queue by chrisflav.

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Dec 9, 2025
jcommelin
jcommelin reviewed Dec 10, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Dec 10, 2025
@grunweg
feat: product of immersions is an immersion (#28853)
64832b9
@ghost ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Dec 10, 2025
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Dec 10, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: product of immersions is an immersion [Merged by Bors] - feat: product of immersions is an immersion Dec 10, 2025
@mathlib-bors mathlib-bors bot closed this Dec 10, 2025
grunweg added a commit to grunweg/mathlib4 that referenced this pull request Dec 10, 2025
@grunweg
feat: smooth embeddings
3e66431 
Define smooth embeddings between smooth manifolds: a map is a smooth embedding iff it is both
a smooth immersion and a topological embedding. We also prove basic properties (such as congruence
or being stable under products); stronger results will come in future PRs.

Note that unlike smooth immersions, we do not add definitions for
- being a smooth embedding on a set (as this doesn't exist in the topological category either),
- being an embedding at a point (being an embedding is a global notion; moreover, every immersion is
  locally an embedding anyway, so "being an immersion at x" is sufficient to state this)
- variants with respect to a fixed complement: the motivation for immersions (considering the
  equivalent local descriptions of smooth submanifolds) do not apply to this global notion.

-----

- [ ] depends on: leanprover-community#28853

TODO: write a proper module doc-string; this is probably only worth landing
once enough immersions API has been merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@chrisflav chrisflav chrisflav approved these changes

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-differential-geometry Manifolds etc

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@grunweg @mathlib4-merge-conflict-bot @mathlib4-dependent-issues-bot @jcommelin @chrisflav