# 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.

## 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), (E x)] [ F]  :
Type (max u_2 u_3 u_4)
• to_fiber_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 topological_fiber_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} :
@[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), (E x)] [ F] (e : E) :
@[simp]
theorem topological_vector_bundle.trivialization.coe_fst {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}  :
(e x).fst = x
@[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_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), (E x)] [ F] [Π (x : B), topological_space (E x)] [ E] (e : E) (b : B) (hb : b e.to_fiber_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_topological_vector_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] :

### Constructing topological vector bundles #

@[nolint]
structure topological_vector_bundle_core (R : Type u_1) (B : Type u_2) (F : Type u_3) [semiring R] [ F] (ι : 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.

def topological_vector_bundle_core.to_topological_vector_bundle_core {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [ F] {ι : Type u_5} (Z : ι) :

Natural identification to a topological_fiber_bundle_core.

Equations
@[instance]
def topological_vector_bundle_core.to_topological_vector_bundle_core_coe {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [ F] {ι : Type u_5} :
has_coe ι)
Equations
theorem topological_vector_bundle_core.coord_change_linear_comp {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [ F] {ι : Type u_5} (Z : ι) (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] [ F] {ι : Type u_5} (Z : ι) :
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] [ F] {ι : Type u_5} (Z : ι) :
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] [ F] {ι : Type u_5} (Z : ι) (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] [ F] {ι : Type u_5} (Z : ι) (x : B) :
Equations
• = _inst_4
@[instance]
def topological_vector_bundle_core.add_comm_monoid_fiber {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [ F] {ι : Type u_5} (Z : ι) (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] [ F] {ι : Type u_5} (Z : ι) (x : B) :
(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] [ F] {ι : Type u_5} (Z : ι) :
→ B

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] [ F] {ι : Type u_5} (Z : ι) (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] [ F] {ι : Type u_5} (Z : ι) (i j : ι) (p : B × F) :
@[instance]
def topological_vector_bundle_core.to_topological_space {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [ F] (ι : Type u_5) (Z : ι) :

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] [ F] {ι : Type u_5} (Z : ι) (b : B) (i j : ι) :
j b = (Z.coord_change i j b)
def topological_vector_bundle_core.local_triv {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [ F] {ι : Type u_5} (Z : ι) (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
@[simp]
theorem topological_vector_bundle_core.mem_local_triv_source {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [ F] {ι : Type u_5} (Z : ι) (i : ι) (p : bundle.total_space Z.fiber) :
def topological_vector_bundle_core.local_triv_at {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [ F] {ι : Type u_5} (Z : ι) (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] [ F] {ι : Type u_5} (Z : ι) (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] [ F] {ι : Type u_5} (Z : ι) (b : B) (a : F) :
(Z.local_triv_at b) b, a⟩ = (b, a)
@[instance]
def topological_vector_bundle_core.fiber.topological_vector_bundle {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [ F] {ι : Type u_5} (Z : ι) :
theorem topological_vector_bundle_core.continuous_proj {R : Type u_1} {B : Type u_2} {F : Type u_3} [semiring R] [ F] {ι : Type u_5} (Z : ι) :

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] [ F] {ι : Type u_5} (Z : ι) :

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