Skip to content

[Merged by Bors] - feat: Sum.inl and friends between smooth manifolds are smooth#20664

Closed
grunweg wants to merge 18 commits intomasterfrom
MR-disjUnion-manifolds-3
Closed

[Merged by Bors] - feat: Sum.inl and friends between smooth manifolds are smooth#20664
grunweg wants to merge 18 commits intomasterfrom
MR-disjUnion-manifolds-3

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Jan 11, 2025 •
edited
Loading

We prove that the following maps between manifolds are smooth:

  • Sum.inl, Sum.inr, as well as Sum.map_elim and Sum.swap
  • Furthermore, Sum.map_elim is C^n iff both components are.

Since the file we're editing now contains material both about products and disjoint unions, we rename the file to Constructions.

From my bordism theory project.

Open in Gitpod

@grunweg grunweg added the WIP Work in progress label Jan 11, 2025
@mergify
Copy link
Copy Markdown

mergify bot commented Jan 11, 2025

⚠️ The sha of the head commit of this PR conflicts with #20659. Mergify cannot evaluate rules on this PR. ⚠️

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 11, 2025 •
edited
Loading

PR summary eed79c65ec

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Geometry.Manifold.ContMDiff.Product -1800
Mathlib.Geometry.Manifold.ContMDiff.Constructions 1800

Declarations diff

+ ContMDiff.inl
+ ContMDiff.inr
+ ContMDiff.sum_elim
+ ContMDiff.sum_map
+ ContMDiff.swap
+ contMDiff_of_contMDiff_inl
+ contMDiff_of_contMDiff_inr
+ contMDiff_sum_map
+ extChartAt_inl_apply
+ extChartAt_inr_apply
+ extend_image_target_mem_nhds

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 changed the title feat: Sum.inl between manifolds is smooth feat: Sum.inl and Sum.inr between smooth manifolds is smooth Jan 11, 2025
@grunweg grunweg added t-differential-geometry Manifolds etc please-adopt Inactive PR (would be valuable to adopt) labels Jan 12, 2025
@leanprover-community-bot-assistant leanprover-community-bot-assistant 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) labels Jan 21, 2025
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 29, 2025
@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 Jan 29, 2025
@grunweg grunweg added awaiting-author A reviewer has asked the author a question or requested changes. and removed WIP Work in progress please-adopt Inactive PR (would be valuable to adopt) labels Feb 2, 2025
@grunweg grunweg changed the title feat: Sum.inl and Sum.inr between smooth manifolds is smooth feat: Sum.inl and friends between smooth manifolds are smooth Feb 2, 2025
grunweg
grunweg commented Feb 2, 2025
View reviewed changes
Mathlib/Geometry/Manifold/ContMDiff/Product.lean Outdated
(hf : ContMDiff I J n f) (hg : ContMDiff I J n g) : ContMDiff I J n (Sum.map f g) :=
ContMDiff.sum_elim (ContMDiff.inl.comp hf) (ContMDiff.inr.comp hg)

-- Better names welcome!
Copy link
Copy Markdown
Contributor Author

@grunweg grunweg Feb 2, 2025

Choose a reason for hiding this comment

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

The continuous analogue is called continuous_sum_dom and proves both the inl and inr statement. I'm not convinced that's better here.

grunweg
grunweg commented Feb 2, 2025
View reviewed changes
@grunweg grunweg removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 2, 2025
@grunweg grunweg mentioned this pull request Feb 2, 2025
Closed
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Feb 2, 2025

There linter errors are from the simpNF linter: i.e., one should really look at the tagging to determine which option is best.

@grunweg grunweg mentioned this pull request Feb 2, 2025
Closed
1 task
@grunweg grunweg force-pushed the MR-disjUnion-manifolds-3 branch from 5b518cc to ff934e6 Compare February 4, 2025 13:00
@grunweg grunweg force-pushed the MR-disjUnion-manifolds-3 branch from ff934e6 to b9019b4 Compare February 4, 2025 13:01
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Feb 4, 2025

I have reverted the simp changes for now, to make CI pass and this PR show up in the queue. I'd still welcome opinions on them.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 4, 2025
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Feb 5, 2025

(And thanks for the tiny nits, of course.)

@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Feb 5, 2025

I pushed a commit starting to use your definition, so you can also look at what breaks (once CI comes back).

@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Feb 5, 2025

It's certainly never useful in applications to allow H to be empty. It's more that having useless assumptions around is not nice, because it propagates to all the other statements that use it, so if one can remove it from the start it makes for a cleaner theory.

@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Feb 6, 2025

I've done the cleanup, and I think it looks nice. What do you think?

@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Feb 6, 2025

I like your clean-ups, thanks a lot for the help! I think they would make an excellent PR (this PR could depend on). I'm at a conference until end of this week, but could cherry-pick or maintainer merge one such PR on Monday.

@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Feb 6, 2025

Done in #21500

sgouezel
sgouezel reviewed Feb 15, 2025
View reviewed changes
@sgouezel sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 15, 2025
@grunweg grunweg removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 15, 2025
sgouezel
sgouezel reviewed Feb 17, 2025
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 17, 2025

✌️ 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 the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 17, 2025
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Feb 17, 2025

Thanks for the review!
bors merge

@grunweg grunweg mentioned this pull request Feb 17, 2025
Closed
mathlib-bors bot pushed a commit that referenced this pull request Feb 17, 2025
@grunweg @sgouezel
feat: Sum.inl and friends between smooth manifolds are smooth (#20664)
f7c4a81 
We prove that the following maps between manifolds are smooth:
- Sum.inl, Sum.inr, as well as Sum.map_elim and Sum.swap
- Furthermore, Sum.map_elim is C^n iff both components are.

Since the file we're editing now contains material both about products and disjoint unions, we rename the file to `Constructions`.

From my bordism theory project.



Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 17, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Sum.inl and friends between smooth manifolds are smooth [Merged by Bors] - feat: Sum.inl and friends between smooth manifolds are smooth Feb 17, 2025
@mathlib-bors mathlib-bors bot closed this Feb 17, 2025
@mathlib-bors mathlib-bors bot deleted the MR-disjUnion-manifolds-3 branch February 17, 2025 22:25
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

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.

3 participants

@grunweg @sgouezel @leanprover-community-bot-assistant