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): derivation_bundle
#7708
Conversation
derivation_bundle
48f2b66
to
000c764
Compare
Eric's suggestions Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
000c764
to
90eae14
Compare
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.
Some minor comments.
|
||
/-- Type synonym, introduced to put a different `has_scalar` action on `C^n⟮I, M; 𝕜⟯` | ||
which is defined as `f • r = f(x) * r`. -/ | ||
@[nolint unused_arguments] def pointed_smooth_map (x : M) := C^n⟮I, M; 𝕜⟯ |
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's not clear to me that this case will never be explored. I have a slight preference for the pointed_times
name.
If you fix the things that I flagged in the comments above, then this is ready for merging. |
Co-authored-by: Oliver Nash <github@olivernash.org> Co-authored-by: Johan Commelin <johan@commelin.net>
bors merge |
In this PR we define the `derivation_bundle`. Note that this definition is purely algebraic and that the whole geometry/analysis is contained in the algebra structure of smooth global functions on the manifold. I believe everything runs smoothly and elegantly and that most proofs can be naturally done by `rfl`. To anticipate some discussions that already arose on Zulip about 9 months ago, note that the content of these files is purely algebraic and that there is no intention whatsoever to replace the current tangent bundle. I prefer this definition to the one given through the adjoint representation, because algebra is more easily formalized and simp can solve most proofs with this definition. However, in the future, there will be also the adjoint representation for sure.
Pull request successfully merged into master. Build succeeded: |
derivation_bundle
derivation_bundle
In this PR we define the `derivation_bundle`. Note that this definition is purely algebraic and that the whole geometry/analysis is contained in the algebra structure of smooth global functions on the manifold. I believe everything runs smoothly and elegantly and that most proofs can be naturally done by `rfl`. To anticipate some discussions that already arose on Zulip about 9 months ago, note that the content of these files is purely algebraic and that there is no intention whatsoever to replace the current tangent bundle. I prefer this definition to the one given through the adjoint representation, because algebra is more easily formalized and simp can solve most proofs with this definition. However, in the future, there will be also the adjoint representation for sure.
In this PR we define the
derivation_bundle
. Note that this definition is purely algebraic and that the whole geometry/analysis is contained in the algebra structure of smooth global functions on the manifold.I believe everything runs smoothly and elegantly and that most proofs can be naturally done by
rfl
. To anticipate some discussions that already arose on Zulip about 9 months ago, note that the content of these files is purely algebraic and that there is no intention whatsoever to replace the current tangent bundle. I prefer this definition to the one given through the adjoint representation, because algebra is more easily formalized and simp can solve most proofs with this definition. However, in the future, there will be also the adjoint representation for sure.