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