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(topology/vector_bundle): redefine continuous coordinate change #14462
Conversation
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.
That's a change I've been wanting to do for some time, so I'm really glad you did it. Thanks!
bors d+
def continuous_transitions (e : local_equiv (B × F) (B × F)) : Prop := | ||
∃ s : set B, e.source = s ×ˢ (univ : set F) ∧ e.target = s ×ˢ (univ : set F) |
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.
Can't you remove this definition now?
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.
I can, my impression from @hrmacbeth was that she still wanted to use it. I'll delete it in a later PR if that is false.
✌️ fpvandoorn can now approve this pull request. To approve and merge a pull request, simply reply with |
Also, I don't think the PR description is accurate wrt |
bors merge |
…14462) * For any two trivializations, we define the coordinate change between the two trivializations: continous linear automorphism of `F`, defined by composing one trivialization with the inverse of the other. This is defined for any point in the intersection of their base sets, and we define it to be the identity function outside this set. * Redefine `topological_vector_bundle`: we now require that this coordinate change between any two trivializations is continuous on the intersection of their base sets. * Redefine `topological_vector_prebundle` with the existence of a continuous linear coordinate change function. * Simplify the proofs that the coordinate change function is continuous for constructions on vector bundles.
Pull request successfully merged into master. Build succeeded: |
…14462) * For any two trivializations, we define the coordinate change between the two trivializations: continous linear automorphism of `F`, defined by composing one trivialization with the inverse of the other. This is defined for any point in the intersection of their base sets, and we define it to be the identity function outside this set. * Redefine `topological_vector_bundle`: we now require that this coordinate change between any two trivializations is continuous on the intersection of their base sets. * Redefine `topological_vector_prebundle` with the existence of a continuous linear coordinate change function. * Simplify the proofs that the coordinate change function is continuous for constructions on vector bundles.
F
, defined by composing one trivialization with the inverse of the other. This is defined for any point in the intersection of their base sets, and we define it to be the identity function outside this set.topological_vector_bundle
: we now require that this coordinate change between any two trivializations is continuous on the intersection of their base sets.topological_vector_prebundle
with the existence of a continuous linear coordinate change function.Zulip thread