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:

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), 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)

to_fiber_bundle_trivialization : topological_fiber_bundle.trivialization F (bundle.proj E)
linear : ∀ (x : B), x ∈ self.to_fiber_bundle_trivialization.base_set → is_linear_map R (λ (y : E x), (self.to_fiber_bundle_trivialization.to_local_homeomorph.to_local_equiv.to_fun ↑y).snd)

Local trivialization for vector bundles.

@[protected, 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), module R (E x)] [topological_space F] [add_comm_monoid F] [module R F] [topological_space (bundle.total_space E)] [topological_space B] :

has_coe_to_fun (topological_vector_bundle.trivialization R F E) (λ (_x : topological_vector_bundle.trivialization R F E), bundle.total_space E → B × F)

Equations

topological_vector_bundle.trivialization.has_coe_to_fun R F E = {coe := λ (e : topological_vector_bundle.trivialization R F E), e.to_fiber_bundle_trivialization.to_local_homeomorph.to_local_equiv.to_fun}

@[protected, 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), module R (E x)] [topological_space F] [add_comm_monoid F] [module R F] [topological_space (bundle.total_space E)] [topological_space B] :

has_coe (topological_vector_bundle.trivialization R F E) (topological_fiber_bundle.trivialization F (bundle.proj E))

Equations

topological_fiber_bundle.trivialization.has_coe R F E = {coe := topological_vector_bundle.trivialization.to_fiber_bundle_trivialization _inst_8}

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), 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) {x : bundle.total_space E} :

x ∈ e.to_fiber_bundle_trivialization.to_local_homeomorph.to_local_equiv.source ↔ bundle.proj E x ∈ e.to_fiber_bundle_trivialization.base_set

@[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) :

⇑(e.to_fiber_bundle_trivialization.to_local_homeomorph) = ⇑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), 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) {x : bundle.total_space E} (ex : x ∈ e.to_fiber_bundle_trivialization.to_local_homeomorph.to_local_equiv.source) :

(⇑e x).fst = bundle.proj E 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), 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

inducing : ∀ (b : B), inducing (λ (x : E b), id ⟨b, x⟩)
locally_trivial : ∀ (b : B), ∃ (e : topological_vector_bundle.trivialization R F E), b ∈ e.to_fiber_bundle_trivialization.base_set

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

noncomputable 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) :

topological_vector_bundle.trivialization R F E

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

Equations

topological_vector_bundle.trivialization_at R F E = λ (b : B), classical.some _

@[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) :

b ∈ (topological_vector_bundle.trivialization_at R F E b).to_fiber_bundle_trivialization.base_set

@[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), 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] (z : bundle.total_space E) :

z ∈ (topological_vector_bundle.trivialization_at R F E z.fst).to_fiber_bundle_trivialization.to_local_homeomorph.to_local_equiv.source

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

e.continuous_linear_equiv_at b hb = {to_linear_equiv := {to_fun := λ (y : E b), (⇑e ⟨b, y⟩).snd, map_add' := _, map_smul' := _, inv_fun := λ (z : F), cast _ (⇑(e.to_fiber_bundle_trivialization.to_local_homeomorph.symm) (b, z)).snd, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}

@[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) :

⇑(e.continuous_linear_equiv_at 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), 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) (x : bundle.total_space E) (hx : x ∈ e.to_fiber_bundle_trivialization.to_local_homeomorph.to_local_equiv.source) :

⇑(e.continuous_linear_equiv_at (bundle.proj E x) _) x.snd = (⇑e x).snd

@[protected, instance]

def topological_vector_bundle.bundle.trivial.add_comm_monoid {B : Type u_1} {F : Type u_2} [add_comm_monoid F] (b : B) :

add_comm_monoid (bundle.trivial B F b)

Equations

topological_vector_bundle.bundle.trivial.add_comm_monoid b = _inst_11

@[protected, instance]

def topological_vector_bundle.bundle.trivial.add_comm_group {B : Type u_1} {F : Type u_2} [add_comm_group F] (b : B) :

add_comm_group (bundle.trivial B F b)

Equations

topological_vector_bundle.bundle.trivial.add_comm_group b = _inst_11

@[protected, 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) :

module R (bundle.trivial B F b)

Equations

topological_vector_bundle.bundle.trivial.module b = _inst_12

def topological_vector_bundle.trivial_topological_vector_bundle.trivialization (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] :

topological_vector_bundle.trivialization R F (bundle.trivial B F)

Local trivialization for trivial bundle.

Equations

topological_vector_bundle.trivial_topological_vector_bundle.trivialization R B F = {to_fiber_bundle_trivialization := {to_local_homeomorph := {to_local_equiv := {to_fun := λ (x : bundle.total_space (bundle.trivial B F)), (x.fst, x.snd), inv_fun := λ (y : B × F), ⟨y.fst, y.snd⟩, source := set.univ (bundle.total_space (bundle.trivial B F)), target := set.univ (B × F), map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}, base_set := set.univ B, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}, linear := _}

@[protected, instance]

def topological_vector_bundle.trivial_bundle.topological_vector_bundle (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] :

topological_vector_bundle R F (bundle.trivial B 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), 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] :

is_topological_fiber_bundle F (bundle.proj 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)

base_set : ι → set B
is_open_base_set : ∀ (i : ι), is_open (self.base_set i)
index_at : B → ι
mem_base_set_at : ∀ (x : B), x ∈ self.base_set (self.index_at x)
coord_change : ι → ι → B → (F →ₗ[R] F)
coord_change_self : ∀ (i : ι) (x : B), x ∈ self.base_set i → ∀ (v : F), ⇑(self.coord_change i i x) v = v
coord_change_continuous : ∀ (i j : ι), continuous_on (λ (p : B × F), ⇑(self.coord_change i j p.fst) p.snd) ((self.base_set i ∩ self.base_set j) ×ˢ set.univ)
coord_change_comp : ∀ (i j k : ι) (x : B), x ∈ self.base_set i ∩ self.base_set j ∩ self.base_set k → ∀ (v : F), ⇑(self.coord_change j k x) (⇑(self.coord_change i j x) v) = ⇑(self.coord_change i k x) v

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] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] {ι : Type u_5} (Z : topological_vector_bundle_core R B F ι) :

topological_fiber_bundle_core ι B F

Natural identification to a topological_fiber_bundle_core.

Equations

Z.to_topological_vector_bundle_core = {base_set := Z.base_set, is_open_base_set := _, index_at := Z.index_at, mem_base_set_at := _, coord_change := λ (i j : ι) (b : B), ⇑(Z.coord_change i j b), coord_change_self := _, coord_change_continuous := _, coord_change_comp := _}

@[protected, 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] [topological_space F] [add_comm_monoid F] [module R F] [topological_space B] {ι : Type u_5} :

has_coe (topological_vector_bundle_core R B F ι) (topological_fiber_bundle_core ι B F)

Equations

topological_vector_bundle_core.to_topological_vector_bundle_core_coe = {coe := topological_vector_bundle_core.to_topological_vector_bundle_core ι}

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

Z.index = ι

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

Z.base = B

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

Z.fiber x = F

@[protected, 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) :

topological_space (Z.fiber x)

Equations

Z.topological_space_fiber x = _inst_4

@[protected, 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) :

add_comm_monoid (Z.fiber x)

Equations

Z.add_comm_monoid_fiber = λ (x : B), _inst_5

@[protected, 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

Z.module_fiber = λ (x : B), _inst_6

@[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 ι) :

bundle.total_space Z.fiber → B

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

Equations

Z.proj = bundle.proj Z.fiber

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

Z.triv_change i j = ↑Z.triv_change i j

@[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) :

p ∈ (Z.triv_change i j).to_local_equiv.source ↔ p.fst ∈ Z.base_set i ∩ Z.base_set j

@[protected, instance]

def topological_vector_bundle_core.to_topological_space {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 ι) :

topological_space (bundle.total_space Z.fiber)

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

Equations

topological_vector_bundle_core.to_topological_space ι Z = topological_fiber_bundle_core.to_topological_space ι ↑Z

@[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 : ι) :

↑Z.coord_change i 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] [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 : ι) :

topological_vector_bundle.trivialization R F Z.fiber

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

Z.local_triv i = {to_fiber_bundle_trivialization := {to_local_homeomorph := (↑Z.local_triv i).to_local_homeomorph, base_set := (↑Z.local_triv i).base_set, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}, linear := _}

@[simp]

theorem topological_vector_bundle_core.mem_local_triv_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 : ι) (p : bundle.total_space Z.fiber) :

p ∈ (Z.local_triv i).to_fiber_bundle_trivialization.to_local_homeomorph.to_local_equiv.source ↔ p.fst ∈ Z.base_set i

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) :

topological_vector_bundle.trivialization R F Z.fiber

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

Equations

Z.local_triv_at b = Z.local_triv (Z.index_at b)

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) :

⟨b, a⟩ ∈ (Z.local_triv_at b).to_fiber_bundle_trivialization.to_local_homeomorph.to_local_equiv.source

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

@[protected, instance]

def topological_vector_bundle_core.fiber.topological_vector_bundle {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 ι) :

topological_vector_bundle R F Z.fiber

@[continuity]

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 ι) :

continuous Z.proj

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 ι) :

is_open_map Z.proj

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