## Stream: Is there code for X?

### Topic: tangent bundle is a topological_vector_bundle

#### 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.

#### 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?

#### 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!)

#### Yury G. Kudryashov (Apr 09 2021 at 08:48):

It is not registered yet.

#### Yury G. Kudryashov (Apr 09 2021 at 08:49):

@Nicolò Cavalleri For vector bundle morphisms.

#### Nicolò Cavalleri (Apr 09 2021 at 08:52):

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

#### Yury G. Kudryashov (Apr 09 2021 at 08:54):

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

#### Yury G. Kudryashov (Apr 09 2021 at 08:55):

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

#### 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.

#### 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