tangent bundle is a topological_vector_bundle

Stream: Is there code for X?

[Yury G. Kudryashov]

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]

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]

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]

It is not registered yet.

[Yury G. Kudryashov]

@Nicolò Cavalleri For vector bundle morphisms.

[Nicolò Cavalleri]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Nicolò Cavalleri]

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