[Merged by Bors] - feat(geometry/manifold/vector_bundle): smooth_fiberwise_linear groupoid#17302
[Merged by Bors] - feat(geometry/manifold/vector_bundle): smooth_fiberwise_linear groupoid#17302
smooth_fiberwise_linear groupoid#17302Conversation
|
Should parts of this be generalized right away to be useful for talking about (iso)morphisms between different vector bundles? |
|
Can you explain a bit more what you have in mind? A lot of the work in this file is specific to the local-homeomorph situation, where one is juggling specified "source" and "target" sets for a partially defined function. This wouldn't be the case for morphisms of vector bundles -- I would expect them to be defined everywhere. |
|
I don't know precisely what I mean. I feel that it should be possible to deduplicate some proofs by looking at the corresponding category, not its core. E.g., how do you define a morphism of smooth vector bundles? If you use coordinates, then you need lemmas like "composition of morphisms is a morphism" for morphisms, not isomorphisms. |
|
Maybe we have different definitions for morphisms of vector bundles in mind, so the problem looks different to us? I can see at least two co-ordinate-free options for defining morphisms of vector bundles, from E over B to E' over B':
|
|
I see that other groupoids allow |
|
@urkud You can see this Zulip post for the big picture, and the branch We provide a vector bundle The idea is that this will be used with the "composition" of charted spaces and groupoids introduced in #17305 to make a smooth vector bundle into a smooth manifold. If |
| (h2φ : smooth_on IB 𝓘(𝕜, F →L[𝕜] F) (λ x, ((φ x).symm : F →L[𝕜] F)) u), | ||
| (e.restr (u ×ˢ univ)).eq_on_source | ||
| (fiberwise_linear.local_homeomorph φ hu hφ.continuous_on h2φ.continuous_on)) : | ||
| ∃ (Φ : B → (F ≃L[𝕜] F)) (U : set B) (hU₀ : is_open U) |
There was a problem hiding this comment.
| ∃ (Φ : B → (F ≃L[𝕜] F)) (U : set B) (hU₀ : is_open U) | |
| ∃ (Φ : B → (F ≃L[𝕜] F)) (hU₀ : is_open U) |
???
If you want to keep the strange conclusion with the (U : set B) since it is useful for the formulation of later results, you should add a comment somewhere.
There was a problem hiding this comment.
This is an aux-lemma and the statement is indeed designed to match what's needed in smooth_fiberwise_linear, so I'm keeping it this way
|
✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
…poid (#17302) Let `B` be a smooth manifold and `F` a normed space. We build the groupoid of local homeomorphisms of `B × F` which are "smooth and fibrewise linear": that is, they are of the form `λ x, (x.1, φ x.1 x.2)` for some function `φ` from `B` to the automorphisms of `F`, which is smooth and has smooth inverse on the proposed domain. Membership in this groupoid is the natural property characterizing the transition functions of a smooth vector bundle over `B` modelled on `F`. 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: |
smooth_fiberwise_linear groupoidsmooth_fiberwise_linear groupoid
Let
Bbe a smooth manifold andFa normed space. We build the groupoid of local homeomorphisms ofB × Fwhich are "smooth and fibrewise linear": that is, they are of the formλ x, (x.1, φ x.1 x.2)for some functionφfromBto the automorphisms ofF, which is smooth and has smooth inverse on the proposed domain.Membership in this groupoid is the natural property characterizing the transition functions of a smooth vector bundle over
Bmodelled onF.Co-authored-by: Floris van Doorn fpvdoorn@gmail.com