# mathlibdocumentation

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:

• F should be a topological space and a module over a semiring R;
• There should be a topology on bundle.total_space E, for which the projection to B 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 R, 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 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), (E x)] [ F]  :
Type (max u_2 u_3 u_4)
• to_bundle_trivialization :
• linear : ∀ (x : B), (λ (y : E x),

Local trivialization for vector bundles.

@[instance]
def topological_vector_bundle.trivialization.has_coe_to_fun (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), (E x)] [ F]  :
Equations
@[instance]
def bundle_trivialization.has_coe (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), (E x)] [ F]  :
Equations
theorem topological_vector_bundle.trivialization.mem_source {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), (E x)] [ F] (e : E) {x : bundle.total_space E} :
@[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), (E x)] [ F] [Π (x : B), topological_space (E x)] :
Prop
• inducing : ∀ (b : B), inducing (λ (x : E b), id b, x⟩)
• locally_trivial : ∀ (b : B), ∃ (e : ,

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), (E x)] [ F] [Π (x : B), topological_space (E x)] [ 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
• = λ (b : B),
@[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), (E x)] [ F] [Π (x : B), topological_space (E x)] [ E] (b : B) :
@[simp]
theorem topological_vector_bundle.mem_source_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), (E x)] [ F] [Π (x : B), topological_space (E x)] [ E] (z : bundle.total_space E) :
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), (E x)] [ F] [Π (x : B), topological_space (E x)] [ E] (e : 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), (E x)] [ F] [Π (x : B), topological_space (E x)] [ E] (e : E) (b : B) (hb : b e.to_bundle_trivialization.base_set) (y : E b) :
hb) y = (e b, y⟩).snd
@[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), (E x)] [ F] [Π (x : B), topological_space (E x)] [ E] (e : E) (x : bundle.total_space E)  :
_) x.snd = (e x).snd
@[instance]
def topological_vector_bundle.bundle.trivial.add_comm_monoid {B : Type u_1} {F : Type u_2} (b : B) :
Equations
@[instance]
def topological_vector_bundle.bundle.trivial.add_comm_group {B : Type u_1} {F : Type u_2} (b : B) :
Equations
@[instance]
def topological_vector_bundle.bundle.trivial.module {R : Type u_1} [semiring R] {B : Type u_2} {F : Type u_3} [ F] (b : B) :
F b)
Equations
def topological_vector_bundle.trivial_bundle_trivialization (R : Type u_1) (B : Type u_2) (F : Type u_3) [semiring R] [ F]  :

Local trivialization for trivial bundle.

Equations
@[instance]
def topological_vector_bundle.trivial_bundle.topological_vector_bundle (R : Type u_1) (B : Type u_2) (F : Type u_3) [semiring R] [ F]  :
F)
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), (E x)] [ F] [Π (x : B), topological_space (E x)] [ E] :