mathlib3

5c856c39 - feat(topology/vector_bundle): definition of topological vector bundle (#4658)

feat(topology/vector_bundle): definition of topological vector bundle (#4658) # Topological vector bundles In this file we define topological vector bundles. Let `B` be the base space. In our formalism, a topological vector bundle is by definition the type `bundle.total_space E` where `E : B → Type*` is a function associating to `x : B` the fiber over `x`. This type `bundle.total_space E` is just a type synonym for `Σ (x : B), E x`, with the interest that one can put another topology than on `Σ (x : B), E x` which has the disjoint union topology. To have a topological vector bundle structure on `bundle.total_space E`, one should addtionally have the following data: * `F` should be a topological vector space over a field `𝕜`; * There should be a topology on `bundle.total_space E`, for which the projection to `E` is a topological fiber bundle with fiber `F` (in particular, each fiber `E x` is homeomorphic to `F`); * For each `x`, the fiber `E x` should be a topological vector space over `𝕜`, and the injection from `E x` to `bundle.total_space F E` should be an embedding; * The most important condition: around each point, there should be a bundle trivialization which is a continuous linear equiv in the fibers. If all these conditions are satisfied, we register the typeclass `topological_vector_bundle 𝕜 F E`. We emphasize that the data is provided by other classes, and that the `topological_vector_bundle` class is `Prop`-valued. The point of this formalism is that it is unbundled in the sense that the total space of the bundle is a type with a topology, with which one can work or put further structure, and still one can perform operations on topological vector bundles (which are yet to be formalized). For instance, assume that `E₁ : B → Type*` and `E₂ : B → Type*` define two topological vector bundles over `𝕜` with fiber models `F₁` and `F₂` which are normed spaces. Then one can construct the vector bundle of continuous linear maps from `E₁ x` to `E₂ x` with fiber `E x := (E₁ x →L[𝕜] E₂ x)` (and with the topology inherited from the norm-topology on `F₁ →L[𝕜] F₂`, without the need to define the strong topology on continuous linear maps between general topological vector spaces). Let `vector_bundle_continuous_linear_map 𝕜 F₁ E₁ F₂ E₂ (x : B)` be a type synonym for `E₁ x →L[𝕜] E₂ x`. Then one can endow `bundle.total_space (vector_bundle_continuous_linear_map 𝕜 F₁ E₁ F₂ E₂)` with a topology and a topological vector bundle structure. Similar constructions can be done for tensor products of topological vector bundles, exterior algebras, and so on, where the topology can be defined using a norm on the fiber model if this helps. Coauthored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>