-
Notifications
You must be signed in to change notification settings - Fork 297
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] - refactor(geometry/manifold): use a sigma type for the total space of the tangent bundle #3966
Conversation
Co-authored-by: Nicolò Cavalleri <nico@cavalleri.net>
…ty/mathlib into sigma_tangent
Somehow this is causing a timeout in |
Fixed. |
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 all seems reasonable to me. The proposed new definition seems more mathematically attractive, but I am not really equipped to judge whether it will make future constructions easier or harder.
end | ||
/-- The canonical identification between the tangent bundle to the model space and the product, | ||
as a homeomorphim -/ | ||
def tangent_bundle_model_space_homeomorph : tangent_bundle I H ≃ₜ model_prod H E := |
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.
Presumably this could be a structomorphism? Would there be any benefit to registering that fact?
@hrmacbeth thanks for taking a look! As I understand it, this is blocking the update of the LFTCM tutorials, so there's slight urgency here. (Let's not let those bitrot again.) If @PatrickMassot wants us to wait for a review, or if @sgouezel wants to wait for Patrick, that's fine. Otherwise let's get this in. bors d+ |
✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with |
Let's get this in, then. It can still be refactored/improved later if needed. bors r+ |
…the tangent bundle (#3966) Redefine the total space of the tangent bundle to be a sigma type instead of a product type. Before ``` have p : tangent_bundle I M := sorry, rcases p with ⟨x, v⟩, -- x: M -- v: E ``` After ``` have p : tangent_bundle I M := sorry, rcases p with ⟨x, v⟩, -- x: M -- v: tangent_space I x ``` This seems more natural, and is probably needed to do Riemannian manifolds right. The drawback is that we can not abuse identifications any more between the tangent bundle to a vector space and a product space (but we can still identify the tangent space with the vector space itself, which is the most important thing). Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
Canceled. |
@sgouezel I'm at least going to commit Heather's typo fix first! bors r+ |
…the tangent bundle (#3966) Redefine the total space of the tangent bundle to be a sigma type instead of a product type. Before ``` have p : tangent_bundle I M := sorry, rcases p with ⟨x, v⟩, -- x: M -- v: E ``` After ``` have p : tangent_bundle I M := sorry, rcases p with ⟨x, v⟩, -- x: M -- v: tangent_space I x ``` This seems more natural, and is probably needed to do Riemannian manifolds right. The drawback is that we can not abuse identifications any more between the tangent bundle to a vector space and a product space (but we can still identify the tangent space with the vector space itself, which is the most important thing). Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Oops, sorry! (and thanks, of course) |
Pull request successfully merged into master. Build succeeded: |
…the tangent bundle (#3966) Redefine the total space of the tangent bundle to be a sigma type instead of a product type. Before ``` have p : tangent_bundle I M := sorry, rcases p with ⟨x, v⟩, -- x: M -- v: E ``` After ``` have p : tangent_bundle I M := sorry, rcases p with ⟨x, v⟩, -- x: M -- v: tangent_space I x ``` This seems more natural, and is probably needed to do Riemannian manifolds right. The drawback is that we can not abuse identifications any more between the tangent bundle to a vector space and a product space (but we can still identify the tangent space with the vector space itself, which is the most important thing). Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
…the tangent bundle (#3966) Redefine the total space of the tangent bundle to be a sigma type instead of a product type. Before ``` have p : tangent_bundle I M := sorry, rcases p with ⟨x, v⟩, -- x: M -- v: E ``` After ``` have p : tangent_bundle I M := sorry, rcases p with ⟨x, v⟩, -- x: M -- v: tangent_space I x ``` This seems more natural, and is probably needed to do Riemannian manifolds right. The drawback is that we can not abuse identifications any more between the tangent bundle to a vector space and a product space (but we can still identify the tangent space with the vector space itself, which is the most important thing). Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Redefine the total space of the tangent bundle to be a sigma type instead of a product type. Before
After
This seems more natural, and is probably needed to do Riemannian manifolds right. The drawback is that we can not abuse identifications any more between the tangent bundle to a vector space and a product space (but we can still identify the tangent space with the vector space itself, which is the most important thing).