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.

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

[Merged by Bors] - feat(geometry/manifold): smooth bundled maps #3641

Closed
wants to merge 100 commits into from

Conversation

Nicknamen
Copy link
Collaborator

@Nicknamen Nicknamen commented Jul 31, 2020


We mainly prove field valued smooth maps are an algebra over the field. We also prove intermediate results and we introduce smooth monoids (examples of which are the interval [0,1], nonnegative real numbers, some closed subgroup of matrices groups...).

Copy link
Collaborator

@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.

This looks mostly good to me, I just have minor comments (but a fair number of them :)

src/geometry/manifold/algebra/lie_group.lean Outdated Show resolved Hide resolved
src/geometry/manifold/algebra/monoid.lean Outdated Show resolved Hide resolved
src/geometry/manifold/algebra/monoid.lean Outdated Show resolved Hide resolved
src/geometry/manifold/algebra/smooth_functions.lean Outdated Show resolved Hide resolved
src/geometry/manifold/algebra/smooth_functions.lean Outdated Show resolved Hide resolved
src/geometry/manifold/instances/real.lean Outdated Show resolved Hide resolved
src/geometry/manifold/smooth_manifold_with_corners.lean Outdated Show resolved Hide resolved
src/topology/algebra/continuous_functions.lean Outdated Show resolved Hide resolved
src/topology/algebra/continuous_functions.lean Outdated Show resolved Hide resolved
src/topology/path_connected.lean Outdated Show resolved Hide resolved
@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 28, 2020
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
@Nicknamen Nicknamen added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes awaiting-review The author would like community review of the PR labels Sep 29, 2020
@Nicknamen Nicknamen added the awaiting-review The author would like community review of the PR label Sep 29, 2020
@sgouezel
Copy link
Collaborator

bors r+
Thanks!

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Sep 30, 2020
@hrmacbeth
Copy link
Member

bors r+
Thanks!

@sgouezel Sorry, I had one requested change that I don't think was resolved, is there any way to pause bors (or perhaps @Nicknamen or I could do a follow-up PR just for that)?

@Nicknamen
Copy link
Collaborator Author

Nicknamen commented Sep 30, 2020

@hrmacbeth yes sorry for this we agreed to do it in a next PR because this was too big, I should have tagged you in the message. In fact I will include it in the PR on GL(n), which is my last PR. Do you need it before for your work?

bors bot pushed a commit that referenced this pull request Sep 30, 2020
@hrmacbeth
Copy link
Member

Thanks, that sounds great! No, I don't need it for anything. Sorry I missed the earlier discussion.

@sgouezel
Copy link
Collaborator

If you want to cancel a merge, you can do bors r-
I think it only takes effect if it is written at the beginning of a line, we'll see right now.

@bors
Copy link

bors bot commented Sep 30, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(geometry/manifold): smooth bundled maps [Merged by Bors] - feat(geometry/manifold): smooth bundled maps Sep 30, 2020
@bors bors bot closed this Sep 30, 2020
@bors bors bot deleted the smooth_map branch September 30, 2020 21:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

5 participants