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(geometry/manifold/tangent_bundle): the tangent_bundle is a topological_vector_bundle #8295

Closed
wants to merge 23 commits into from
Closed

[Merged by Bors] - feat(geometry/manifold/tangent_bundle): the tangent_bundle is a topological_vector_bundle #8295

wants to merge 23 commits into from

Conversation

Nicknamen
Copy link
Collaborator

@Nicknamen Nicknamen commented Jul 13, 2021 •
edited

Open in Gitpod

This PR changes the underlying structure of the tangent bundle from a fiber bundle to a vector bundle.

@Nicknamen Nicknamen added the WIP Work in progress label Jul 13, 2021
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jul 13, 2021
@Nicknamen Nicknamen removed the WIP Work in progress label Jul 13, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jul 13, 2021
@Nicknamen Nicknamen added the awaiting-review The author would like community review of the PR label Jul 13, 2021
@Nicknamen Nicknamen requested a review from sgouezel July 13, 2021 14:25
sgouezel
sgouezel reviewed Aug 14, 2021
View reviewed changes
src/topology/vector_bundle.lean Outdated Show resolved Hide resolved
src/geometry/manifold/tangent_bundle.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 Aug 14, 2021
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 8, 2021
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Feb 8, 2022
ocfnash
ocfnash reviewed Feb 16, 2022
View reviewed changes
src/geometry/manifold/tangent_bundle.lean
coord_change_self := λ i x hx v, rfl,
coord_change_comp := λ i j k x hx v, rfl,
coord_change_smooth := λ i j, times_cont_diff_snd.times_cont_diff_on }

namespace basic_smooth_bundle_core
namespace basic_smooth_vector_bundle_core
Copy link
Collaborator

Choose a reason for hiding this comment

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

It looks like this change of name, together with the renaming of to_topological_fiber_bundle_core to to_topological_vector_bundle_core contribute substantially to the diff in this PR.

Would it be possible to split this PR so that the proposed name changes happen first and then we can review the proposed new material second?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

The name changes reflect the changes in the content of the code. What is implemented now is a fiber bundle and what is implemented in the PR is a vector bundle. If I do as you say after the first PR a fiber bundle will be called a vector bundle. If for some reason the later changes are not approved or it takes a long time to approve them, is it fine to have this name discrepancy in Mathlib for a while?

Does it help if I point out with comments where the code actually changes apart from renamings and adding lemmas to simps? I believe there are very few points where the code properly changes

Copy link
Collaborator

Choose a reason for hiding this comment

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

I see, sorry I should have looked more closely.

Does this not mean that we are losing basic_smooth_bundle_core then?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

It does but I guess @sgouezel is ok with it? The idea is that this construction should be useful precisely to build the tangent bundle whereas a more general smooth_fiber_bundle_core and smooth_vector_bundle_core should be used in other situations. If smooth_fiber_bundle_core will be needed again it will be easy to bring it back in by all means!

@ocfnash ocfnash 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 Feb 16, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Feb 23, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Feb 23, 2022
@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 labels Feb 23, 2022
sgouezel
sgouezel reviewed Feb 24, 2022
View reviewed changes
src/geometry/manifold/tangent_bundle.lean Outdated Show resolved Hide resolved
src/geometry/manifold/tangent_bundle.lean Outdated Show resolved Hide resolved
src/geometry/manifold/tangent_bundle.lean Outdated Show resolved Hide resolved
src/geometry/manifold/tangent_bundle.lean Show resolved Hide resolved
src/topology/vector_bundle.lean 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 Feb 24, 2022
@sgouezel
Copy link
Collaborator

Could you also update the PR message?

@PatrickMassot PatrickMassot 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 labels Mar 4, 2022
@Nicknamen
Copy link
Collaborator Author

Sorry, I was planning to do the changes myself today, but I understand not much time should pass between the reviews/merges and the changes

@sgouezel
Copy link
Collaborator

sgouezel commented Mar 7, 2022

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 Mar 7, 2022
bors bot pushed a commit that referenced this pull request Mar 7, 2022
@Nicknamen @PatrickMassot
feat(geometry/manifold/tangent_bundle): the tangent_bundle is a `to…
f063d0c 
…pological_vector_bundle` (#8295)

Co-authored-by: Patrick Massot <patrickmassot@free.fr>
@bors
Copy link

bors bot commented Mar 7, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(geometry/manifold/tangent_bundle): the tangent_bundle is a topological_vector_bundle [Merged by Bors] - feat(geometry/manifold/tangent_bundle): the tangent_bundle is a topological_vector_bundle Mar 7, 2022
@bors bors bot closed this Mar 7, 2022
@bors bors bot deleted the vector_tangent_bundle branch March 7, 2022 12:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ocfnash ocfnash ocfnash left review comments

@sgouezel sgouezel sgouezel left review comments

Assignees
No one assigned
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
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@Nicknamen @sgouezel @ocfnash @PatrickMassot @leanprover-community-bot-assistant