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/vector_bundle/basic): smooth vector bundles #17611
Conversation
slightly shorter test ci Apply suggestions from code review Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> clean up `cont_mdiff_on_of_mem_cont_diff_groupoid`
lint
merged with master. I'll make changes to incorporate my comment, but feel free to already review |
…t delete some changes to this file, but it's hard to figure out if there are any
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This seems to be working very nicely, congrats!
bors d+
|
||
## Main definitions and constructions | ||
|
||
* `fiber_bundle.charted_space`: A fibre bundle `E` over a base `B` with model fibre `F` is naturally |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It looks strange to me that the Lean name has fiber_bundle
but the docstring talks of fibre bundle
. I would uniformize that (or uniformise that, as you like), maybe in a later PR.
✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with |
… about fiber bundles/vector bundles.
bors merge |
…17611) Definition of smooth vector bundle, and basic constructions (direct sum, pullback, core construction). Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Pull request successfully merged into master. Build succeeded: |
SHA-only updates: * leanprover-community/mathlib#17611 – `CategoryTheory.Sites.Sheaf` already uses `aesop_cat` at this location, nothing to port. * leanprover-community/mathlib#18742 – fiber spelling, which is all of the changes to `Topology.FiberBundle.Trivialization`, is already in mathlib4. * leanprover-community/mathlib#18198 – `FunLike` change to `Data.PEquiv` is already in mathlib4. Substantative forward port: * leanprover-community/mathlib#18520 Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
SHA-only updates: * leanprover-community/mathlib#17611 – `CategoryTheory.Sites.Sheaf` already uses `aesop_cat` at this location, nothing to port. * leanprover-community/mathlib#18742 – fiber spelling, which is all of the changes to `Topology.FiberBundle.Trivialization`, is already in mathlib4. * leanprover-community/mathlib#18198 – `FunLike` change to `Data.PEquiv` is already in mathlib4. Substantative forward port: * leanprover-community/mathlib#18520 Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Definition of smooth vector bundle, and basic constructions (direct sum, pullback, core construction).
Co-authored-by: Floris van Doorn fpvdoorn@gmail.com
cont_diff_groupoid
#17291smooth_fiberwise_linear
groupoid #17302