Zulip Chat Archive

Stream: Is there code for X?

Topic: tangent bundle is a topological_vector_bundle


view this post on Zulip Yury G. Kudryashov (Apr 09 2021 at 04:49):

Hi @Nicolò Cavalleri @Sebastien Gouezel, I see that this is not in master but possibly you already have it in some branch. I want to prove that {x | n ≤ rank (mfderiv f I I' x)} is open, and it seems natural to me to do it for a fiberwise-linear continuous map between topological vector bundles.

view this post on Zulip Nicolò Cavalleri (Apr 09 2021 at 08:34):

You want to prove it for vector bundle morphisms? Or you don't want to assume the map preserves fiber but is only fiberwise linear?

view this post on Zulip Sebastien Gouezel (Apr 09 2021 at 08:45):

I don't have this in a branch, so please go ahead. I agree that the natural setting is for fiber-linear maps between topological vector bundles, although I don't know how much additional work this would be (I am not even sure that the tangent bundle is already registered as a topological vector bundle!)

view this post on Zulip Yury G. Kudryashov (Apr 09 2021 at 08:48):

It is not registered yet.

view this post on Zulip Yury G. Kudryashov (Apr 09 2021 at 08:49):

@Nicolò Cavalleri For vector bundle morphisms.

view this post on Zulip Nicolò Cavalleri (Apr 09 2021 at 08:52):

Yeah actually me neither, I think I wrote something on morphisms but nothing of this kind

view this post on Zulip Yury G. Kudryashov (Apr 09 2021 at 08:54):

@Nicolò Cavalleri Do you have "tangent bundle is a topological vector bundle"?

view this post on Zulip Yury G. Kudryashov (Apr 09 2021 at 08:55):

(or something more general about bundles defined using docs#topological_fiber_bundle_core)

view this post on Zulip Yury G. Kudryashov (Apr 09 2021 at 08:57):

Ideally, we should have topological_vector_bundle_core and an instance of topological_vector_bundle for the fiber bundle created from core.

view this post on Zulip Nicolò Cavalleri (Apr 09 2021 at 09:00):

No I don't but Sebastien registered it as a sigma type precisely for this reason so I hope it's not too much work


Last updated: May 07 2021 at 22:14 UTC