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.

Tags #

Vector bundle

@[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.

@[simp]
theorem topological_vector_bundle.trivialization.coe_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), module R (E x)] [topological_space F] [add_comm_monoid F] [module R F] [topological_space (bundle.total_space E)] [topological_space B] (e : topological_vector_bundle.trivialization R F E) :
@[simp]
@[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_fiber_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_fiber_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] :

Constructing topological vector bundles #

@[nolint]
structure topological_vector_bundle_core (R : Type u_1) (B : Type u_2) (F : Type u_3) [semiring R] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] (ι : Type u_5) :
Type (max u_2 u_3 u_5)

Analogous construction of topological_fiber_bundle_core for vector bundles. This construction gives a way to construct vector bundles from a structure registering how trivialization changes act on fibers.

theorem topological_vector_bundle_core.coord_change_linear_comp {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] {ι : Type u_5} (Z : topological_vector_bundle_core R B F ι) (i j k : ι) (x : B) (H : x Z.base_set i Z.base_set j Z.base_set k) :
(Z.coord_change j k x).comp (Z.coord_change i j x) = Z.coord_change i k x
@[nolint]
def topological_vector_bundle_core.index {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] {ι : Type u_5} (Z : topological_vector_bundle_core R B F ι) :
Type u_5

The index set of a topological vector bundle core, as a convenience function for dot notation

Equations
@[nolint]
def topological_vector_bundle_core.base {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] {ι : Type u_5} (Z : topological_vector_bundle_core R B F ι) :
Type u_2

The base space of a topological vector bundle core, as a convenience function for dot notation

Equations
@[nolint]
def topological_vector_bundle_core.fiber {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] {ι : Type u_5} (Z : topological_vector_bundle_core R B F ι) (x : B) :
Type u_3

The fiber of a topological vector bundle core, as a convenience function for dot notation and typeclass inference

Equations
@[instance]
def topological_vector_bundle_core.topological_space_fiber {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] {ι : Type u_5} (Z : topological_vector_bundle_core R B F ι) (x : B) :
Equations
@[instance]
def topological_vector_bundle_core.add_comm_monoid_fiber {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] {ι : Type u_5} (Z : topological_vector_bundle_core R B F ι) (x : B) :
Equations
@[instance]
def topological_vector_bundle_core.module_fiber {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] {ι : Type u_5} (Z : topological_vector_bundle_core R B F ι) (x : B) :
module R (Z.fiber x)
Equations
@[simp]
def topological_vector_bundle_core.proj {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] {ι : Type u_5} (Z : topological_vector_bundle_core R B F ι) :

The projection from the total space of a topological fiber bundle core, on its base.

Equations
def topological_vector_bundle_core.triv_change {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] {ι : Type u_5} (Z : topological_vector_bundle_core R B F ι) (i j : ι) :
local_homeomorph (B × F) (B × F)

Local homeomorphism version of the trivialization change.

Equations
@[simp]
theorem topological_vector_bundle_core.mem_triv_change_source {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] {ι : Type u_5} (Z : topological_vector_bundle_core R B F ι) (i j : ι) (p : B × F) :
@[instance]

Topological structure on the total space of a topological bundle created from core, designed so that all the local trivialization are continuous.

Equations
@[simp]
theorem topological_vector_bundle_core.coe_cord_change {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] {ι : Type u_5} (Z : topological_vector_bundle_core R B F ι) (b : B) (i j : ι) :
def topological_vector_bundle_core.local_triv {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] {ι : Type u_5} (Z : topological_vector_bundle_core R B F ι) (i : ι) :

Extended version of the local trivialization of a fiber bundle constructed from core, registering additionally in its type that it is a local bundle trivialization.

Equations
def topological_vector_bundle_core.local_triv_at {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] {ι : Type u_5} (Z : topological_vector_bundle_core R B F ι) (b : B) :

Preferred local trivialization of a vector bundle constructed from core, at a given point, as a bundle trivialization

Equations
theorem topological_vector_bundle_core.mem_source_at {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] {ι : Type u_5} (Z : topological_vector_bundle_core R B F ι) (b : B) (a : F) :
@[simp]
theorem topological_vector_bundle_core.local_triv_at_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] {ι : Type u_5} (Z : topological_vector_bundle_core R B F ι) (b : B) (a : F) :
(Z.local_triv_at b) b, a⟩ = (b, a)
@[instance]
theorem topological_vector_bundle_core.continuous_proj {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] {ι : Type u_5} (Z : topological_vector_bundle_core R B F ι) :

The projection on the base of a topological vector bundle created from core is continuous

theorem topological_vector_bundle_core.is_open_map_proj {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] {ι : Type u_5} (Z : topological_vector_bundle_core R B F ι) :

The projection on the base of a topological vector bundle created from core is an open map