-
Notifications
You must be signed in to change notification settings - Fork 259
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/VectorBundle/Tangent): tangentCoordChange #8672
Conversation
Minor comment (here and elsewhere): a new rule in the style guide asks for a space after a left arrow. |
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.
The added lemmas look plausible and straightforward; their uses in the dependent PR make this compelling to me. (Please address the style comment.)
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.
Thanks!
bors d+
✌️ winstonyin can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
We define `tangentCoordChange` as a convenient abbreviation for coordinate changes on the tangent bundle. We also restate the axioms of `VectorBundleCore` as lemmas involving `extChartAt`. Currently, we need to write `(tangentBundleCore I M).coordChange (achart H x) (achart H y)`, referring explicitly to the atlas of `M`. Since `tangentBundleCore` uses the same base sets as the preferred charts of the base manifold, we wish to work directly with points `x y : M` and the preferred extended charts at those points (`extChartAt`). We find this definition and related lemmas useful in #8483 in shortening proofs.
Build failed: |
bors r+ |
We define `tangentCoordChange` as a convenient abbreviation for coordinate changes on the tangent bundle. We also restate the axioms of `VectorBundleCore` as lemmas involving `extChartAt`. Currently, we need to write `(tangentBundleCore I M).coordChange (achart H x) (achart H y)`, referring explicitly to the atlas of `M`. Since `tangentBundleCore` uses the same base sets as the preferred charts of the base manifold, we wish to work directly with points `x y : M` and the preferred extended charts at those points (`extChartAt`). We find this definition and related lemmas useful in #8483 in shortening proofs.
Pull request successfully merged into master. Build succeeded: |
We define
tangentCoordChange
as a convenient abbreviation for coordinate changes on the tangent bundle. We also restate the axioms ofVectorBundleCore
as lemmas involvingextChartAt
.Currently, we need to write
(tangentBundleCore I M).coordChange (achart H x) (achart H y)
, referring explicitly to the atlas ofM
. SincetangentBundleCore
uses the same base sets as the preferred charts of the base manifold, we wish to work directly with pointsx y : M
and the preferred extended charts at those points (extChartAt
).We find this definition and related lemmas useful in #8483 in shortening proofs.