mathlib documentation

topology.vector_bundle

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:

If all these conditions are satisfied, we register the typeclass topological_vector_bundle R 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 R 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[R] E₂ x) (and with the topology inherited from the norm-topology on F₁ →L[R] F₂, without the need to define the strong topology on continuous linear maps between general topological vector spaces). Let vector_bundle_continuous_linear_map R F₁ E₁ F₂ E₂ (x : B) be a type synonym for E₁ x →L[R] E₂ x. Then one can endow bundle.total_space (vector_bundle_continuous_linear_map R 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.

@[nolint]
structure topological_vector_bundle.trivialization (R : Type u_1) {B : Type u_2} (F : Type u_3) (E : B → Type u_4) [semiring R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [topological_space F] [add_comm_monoid F] [module R F] [topological_space (bundle.total_space E)] [topological_space B] :
Type (max u_2 u_3 u_4)

Local trivialization for vector bundles.

@[class]
structure topological_vector_bundle (R : Type u_1) {B : Type u_2} (F : Type u_3) (E : B → Type u_4) [semiring R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [topological_space F] [add_comm_monoid F] [module R F] [topological_space (bundle.total_space E)] [topological_space B] [Π (x : B), topological_space (E x)] :
Prop

The space total_space E (for E : B → Type* such that each E x is a topological vector space) has a topological vector space structure with fiber F (denoted with topological_vector_bundle R F E) if around every point there is a fiber bundle trivialization which is linear in the fibers.

Instances
def topological_vector_bundle.trivialization_at (R : Type u_1) {B : Type u_2} (F : Type u_3) (E : B → Type u_4) [semiring R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [topological_space F] [add_comm_monoid F] [module R F] [topological_space (bundle.total_space E)] [topological_space B] [Π (x : B), topological_space (E x)] [topological_vector_bundle R F E] (b : B) :

trivialization_at R F E b is some choice of trivialization of a vector bundle whose base set contains a given point b.

Equations
@[simp]
theorem topological_vector_bundle.mem_base_set_trivialization_at (R : Type u_1) {B : Type u_2} (F : Type u_3) (E : B → Type u_4) [semiring R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [topological_space F] [add_comm_monoid F] [module R F] [topological_space (bundle.total_space E)] [topological_space B] [Π (x : B), topological_space (E x)] [topological_vector_bundle R F E] (b : B) :
def topological_vector_bundle.trivialization.continuous_linear_equiv_at {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [semiring R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [topological_space F] [add_comm_monoid F] [module R F] [topological_space (bundle.total_space E)] [topological_space B] [Π (x : B), topological_space (E x)] [topological_vector_bundle R F E] (e : topological_vector_bundle.trivialization R F E) (b : B) (hb : b e.to_bundle_trivialization.base_set) :
E b ≃L[R] F

In a topological vector bundle, a trivialization in the fiber (which is a priori only linear) is in fact a continuous linear equiv between the fibers and the model fiber.

Equations
@[simp]
theorem topological_vector_bundle.trivialization.continuous_linear_equiv_at_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [semiring R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [topological_space F] [add_comm_monoid F] [module R F] [topological_space (bundle.total_space E)] [topological_space B] [Π (x : B), topological_space (E x)] [topological_vector_bundle R F E] (e : topological_vector_bundle.trivialization R F E) (b : B) (hb : b e.to_bundle_trivialization.base_set) (y : E b) :
@[instance]
def topological_vector_bundle.bundle.trivial.module {R : Type u_1} [semiring R] {B : Type u_2} {F : Type u_3} [add_comm_monoid F] [module R F] (b : B) :
Equations
theorem topological_vector_bundle.is_topological_vector_bundle_is_topological_fiber_bundle {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [semiring R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [topological_space F] [add_comm_monoid F] [module R F] [topological_space (bundle.total_space E)] [topological_space B] [Π (x : B), topological_space (E x)] [topological_vector_bundle R F E] :