mathlib documentation

topology.vector_bundle.basic

Vector bundles #

In this file we define (topological) vector bundles.

Let B be the base space, let F be a normed space over a normed field R, and let E : B → Type* be a fiber_bundle with fiber F, in which, for each x, the fiber E x is a topological vector space over R.

To have a vector bundle structure on bundle.total_space E, one should additionally have the following properties:

If these conditions are satisfied, we register the typeclass vector_bundle R F E.

We define constructions on vector bundles like pullbacks and direct sums in other files.

Implementation notes #

The implementation choices in the vector bundle definition are discussed in the "Implementation notes" section of topology.fiber_bundle.basic.

Tags #

Vector bundle

@[class]
structure pretrivialization.is_linear (R : Type u_1) {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) :
Prop

A mixin class for pretrivialization, stating that a pretrivialization is fiberwise linear with respect to given module structures on its fibers and the model fiber.

Instances of this typeclass
theorem pretrivialization.linear (R : Type u_1) {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] (e : pretrivialization F bundle.total_space.proj) [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [pretrivialization.is_linear R e] {b : B} (hb : b e.base_set) :
is_linear_map R (λ (x : E b), (e (bundle.total_space_mk b x)).snd)
@[protected]
noncomputable def pretrivialization.symmₗ (R : Type u_1) {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] (b : B) :
F →ₗ[R] E b

A fiberwise linear inverse to e.

Equations
@[simp]
theorem pretrivialization.symmₗ_apply (R : Type u_1) {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] (b : B) (y : F) :
@[simp]
theorem pretrivialization.linear_equiv_at_symm_apply (R : Type u_1) {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] (b : B) (hb : b e.base_set) :
@[simp]
theorem pretrivialization.linear_equiv_at_apply (R : Type u_1) {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] (b : B) (hb : b e.base_set) :
noncomputable def pretrivialization.linear_equiv_at (R : Type u_1) {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] (b : B) (hb : b e.base_set) :
E b ≃ₗ[R] F

A pretrivialization for a vector bundle defines linear equivalences between the fibers and the model space.

Equations
@[protected]
noncomputable def pretrivialization.linear_map_at (R : Type u_1) {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] (b : B) :
E b →ₗ[R] F

A fiberwise linear map equal to e on e.base_set.

Equations
theorem pretrivialization.coe_linear_map_at {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] (b : B) :
theorem pretrivialization.coe_linear_map_at_of_mem {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] {b : B} (hb : b e.base_set) :
theorem pretrivialization.linear_map_at_apply {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] {b : B} (y : E b) :
theorem pretrivialization.linear_map_at_eq_zero {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] {b : B} (hb : b e.base_set) :
theorem pretrivialization.symmₗ_linear_map_at {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] {b : B} (hb : b e.base_set) (y : E b) :
theorem pretrivialization.linear_map_at_symmₗ {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] {b : B} (hb : b e.base_set) (y : F) :
@[class]
structure trivialization.is_linear (R : Type u_1) {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : trivialization F bundle.total_space.proj) :
Prop

A mixin class for trivialization, stating that a trivialization is fiberwise linear with respect to given module structures on its fibers and the model fiber.

Instances of this typeclass
@[protected]
theorem trivialization.linear (R : Type u_1) {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space E)] (e : trivialization F bundle.total_space.proj) [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [trivialization.is_linear R e] {b : B} (hb : b e.base_set) :
is_linear_map R (λ (y : E b), (e (bundle.total_space_mk b y)).snd)
noncomputable def trivialization.linear_equiv_at (R : Type u_1) {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] (b : B) (hb : b e.base_set) :
E b ≃ₗ[R] F

A trivialization for a vector bundle defines linear equivalences between the fibers and the model space.

Equations
@[simp]
theorem trivialization.linear_equiv_at_apply {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] (b : B) (hb : b e.base_set) (v : E b) :
@[simp]
theorem trivialization.linear_equiv_at_symm_apply {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] (b : B) (hb : b e.base_set) (v : F) :
@[protected]
noncomputable def trivialization.symmₗ (R : Type u_1) {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] (b : B) :
F →ₗ[R] E b

A fiberwise linear inverse to e.

Equations
@[protected]
noncomputable def trivialization.linear_map_at (R : Type u_1) {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] (b : B) :
E b →ₗ[R] F

A fiberwise linear map equal to e on e.base_set.

Equations
theorem trivialization.symmₗ_linear_map_at {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] {b : B} (hb : b e.base_set) (y : E b) :
noncomputable def trivialization.coord_changeL (R : Type u_1) {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e e' : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] [trivialization.is_linear R e'] (b : B) :
F ≃L[R] F

A coordinate change function between two trivializations, as a continuous linear equivalence. Defined to be the identity when b does not lie in the base set of both trivializations.

Equations
theorem trivialization.mk_coord_changeL {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e e' : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] [trivialization.is_linear R e'] {b : B} (hb : b e.base_set e'.base_set) (y : F) :
theorem trivialization.coord_changeL_apply' {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e e' : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] [trivialization.is_linear R e'] {b : B} (hb : b e.base_set e'.base_set) (y : F) :

A version of coord_change_apply that fully unfolds coord_change. The right-hand side is ugly, but has good definitional properties for specifically defined trivializations.

def bundle.zero_section {B : Type u_3} (E : B Type u_5) [Π (x : B), has_zero (E x)] :

The zero section of a vector bundle

Equations
@[simp]
theorem bundle.zero_section_proj {B : Type u_3} (E : B Type u_5) [Π (x : B), has_zero (E x)] (x : B) :
@[simp]
theorem bundle.zero_section_snd {B : Type u_3} (E : B Type u_5) [Π (x : B), has_zero (E x)] (x : B) :
@[class]
structure vector_bundle (R : Type u_1) {B : Type u_3} (F : Type u_4) (E : B Type u_5) [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [topological_space (bundle.total_space E)] [Π (x : B), topological_space (E x)] [fiber_bundle F E] :
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 vector_bundle R F E) if around every point there is a fiber bundle trivialization which is linear in the fibers.

Instances of this typeclass
noncomputable def trivialization.continuous_linear_map_at (R : Type u_1) {B : Type u_3} {F : Type u_4} {E : B Type u_5} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [topological_space (bundle.total_space E)] [Π (x : B), topological_space (E x)] [fiber_bundle F E] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] (b : B) :
E b →L[R] F

Forward map of continuous_linear_equiv_at (only propositionally equal), defined everywhere (0 outside domain).

Equations
@[simp]
noncomputable def trivialization.symmL (R : Type u_1) {B : Type u_3} {F : Type u_4} {E : B Type u_5} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [topological_space (bundle.total_space E)] [Π (x : B), topological_space (E x)] [fiber_bundle F E] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] (b : B) :
F →L[R] E b

Backwards map of continuous_linear_equiv_at, defined everywhere.

Equations
noncomputable def trivialization.continuous_linear_equiv_at (R : Type u_1) {B : Type u_3} {F : Type u_4} {E : B Type u_5} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [topological_space (bundle.total_space E)] [Π (x : B), topological_space (E x)] [fiber_bundle F E] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] (b : B) (hb : b e.base_set) :
E b ≃L[R] F

In a 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
@[protected]
theorem trivialization.zero_section (R : Type u_1) {B : Type u_3} {F : Type u_4} {E : B Type u_5} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [topological_space (bundle.total_space E)] [Π (x : B), topological_space (E x)] [fiber_bundle F E] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] {x : B} (hx : x e.base_set) :
e (bundle.zero_section E x) = (x, 0)

Constructing vector bundles #

structure vector_bundle_core (R : Type u_1) (B : Type u_3) (F : Type u_4) [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] (ι : Type u_6) :
Type (max u_3 u_4 u_6)

Analogous construction of 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.

Instances for vector_bundle_core

The trivial vector bundle core, in which all the changes of coordinates are the identity.

Equations
@[protected, instance]
Equations
@[simp]
theorem vector_bundle_core.coord_change_linear_comp {R : Type u_1} {B : Type u_3} {F : Type u_4} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_6} (Z : 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 vector_bundle_core.index {R : Type u_1} {B : Type u_3} {F : Type u_4} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_6} (Z : vector_bundle_core R B F ι) :
Type u_6

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

Equations
@[nolint, reducible]
def vector_bundle_core.base {R : Type u_1} {B : Type u_3} {F : Type u_4} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_6} (Z : vector_bundle_core R B F ι) :
Type u_3

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

Equations
@[protected, instance]
Equations
@[protected, instance]
def vector_bundle_core.module_fiber {R : Type u_1} {B : Type u_3} {F : Type u_4} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_6} (Z : vector_bundle_core R B F ι) (x : B) :
module R (Z.fiber x)
Equations
@[protected, instance]
Equations
@[simp, reducible]

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

Equations
@[nolint, reducible]
def vector_bundle_core.total_space {R : Type u_1} {B : Type u_3} {F : Type u_4} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_6} (Z : vector_bundle_core R B F ι) :
Type (max u_3 u_4)

The total space of the vector bundle, as a convenience function for dot notation. It is by definition equal to bundle.total_space Z.fiber, a.k.a. Σ x, Z.fiber x but with a different name for typeclass inference.

Equations
def vector_bundle_core.triv_change {R : Type u_1} {B : Type u_3} {F : Type u_4} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_6} (Z : vector_bundle_core R B F ι) (i j : ι) :
local_homeomorph (B × F) (B × F)

Local homeomorphism version of the trivialization change.

Equations
@[simp]
theorem vector_bundle_core.mem_triv_change_source {R : Type u_1} {B : Type u_3} {F : Type u_4} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_6} (Z : vector_bundle_core R B F ι) (i j : ι) (p : B × F) :
@[protected, instance]

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

Equations
@[simp]
theorem vector_bundle_core.coe_coord_change {R : Type u_1} {B : Type u_3} {F : Type u_4} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_6} (Z : vector_bundle_core R B F ι) (b : B) (i j : ι) :

One of the standard local trivializations of a vector bundle constructed from core, taken by considering this in particular as a fiber bundle constructed from core.

Equations
Instances for vector_bundle_core.local_triv
@[protected, instance]

The standard local trivializations of a vector bundle constructed from core are linear.

@[simp]
theorem vector_bundle_core.base_set_at {R : Type u_1} {B : Type u_3} {F : Type u_4} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_6} (Z : vector_bundle_core R B F ι) (i : ι) :
@[simp]
theorem vector_bundle_core.local_triv_apply {R : Type u_1} {B : Type u_3} {F : Type u_4} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_6} (Z : vector_bundle_core R B F ι) (i : ι) (p : Z.total_space) :
(Z.local_triv i) p = (p.fst, (Z.coord_change (Z.index_at p.fst) i p.fst) p.snd)
@[simp]
theorem vector_bundle_core.local_triv_symm_fst {R : Type u_1} {B : Type u_3} {F : Type u_4} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_6} (Z : vector_bundle_core R B F ι) (i : ι) (p : B × F) :
@[simp]
theorem vector_bundle_core.local_triv_symm_apply {R : Type u_1} {B : Type u_3} {F : Type u_4} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_6} (Z : vector_bundle_core R B F ι) (i : ι) {b : B} (hb : b Z.base_set i) (v : F) :
(Z.local_triv i).symm b v = (Z.coord_change i (Z.index_at b) b) v
@[simp]
theorem vector_bundle_core.local_triv_coord_change_eq {R : Type u_1} {B : Type u_3} {F : Type u_4} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_6} (Z : vector_bundle_core R B F ι) (i j : ι) {b : B} (hb : b Z.base_set i Z.base_set j) (v : F) :

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

Equations
@[simp]
theorem vector_bundle_core.local_triv_at_def {R : Type u_1} {B : Type u_3} {F : Type u_4} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_6} (Z : vector_bundle_core R B F ι) (b : B) :
@[simp]
@[simp]
theorem vector_bundle_core.local_triv_at_apply {R : Type u_1} {B : Type u_3} {F : Type u_4} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_6} (Z : vector_bundle_core R B F ι) (p : Z.total_space) :
(Z.local_triv_at p.fst) p = (p.fst, p.snd)
@[simp]
theorem vector_bundle_core.local_triv_at_apply_mk {R : Type u_1} {B : Type u_3} {F : Type u_4} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_6} (Z : vector_bundle_core R B F ι) (b : B) (a : F) :
(Z.local_triv_at b) b, a⟩ = (b, a)
@[simp]
@[protected, instance]
Equations
@[protected, instance]
@[continuity]

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

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

Vector prebundle #

@[nolint]
structure vector_prebundle (R : Type u_1) {B : Type u_3} (F : Type u_4) (E : B Type u_5) [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] :
Type (max u_3 u_4 u_5)

This structure permits to define a vector bundle when trivializations are given as local equivalences but there is not yet a topology on the total space or the fibers. The total space is hence given a topology in such a way that there is a fiber bundle structure for which the local equivalences are also local homeomorphisms and hence vector bundle trivializations. The topology on the fibers is induced from the one on the total space.

The field exists_coord_change is stated as an existential statement (instead of 3 separate fields), since it depends on propositional information (namely e e' ∈ pretrivialization_atlas). This makes it inconvenient to explicitly define a coord_change function when constructing a vector_prebundle.

Instances for vector_prebundle
  • vector_prebundle.has_sizeof_inst
noncomputable def vector_prebundle.coord_change {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] (a : vector_prebundle R F E) {e e' : pretrivialization F bundle.total_space.proj} (he : e a.pretrivialization_atlas) (he' : e' a.pretrivialization_atlas) (b : B) :
F →L[R] F

A randomly chosen coordinate change on a vector_prebundle, given by the field exists_coord_change.

Equations
theorem vector_prebundle.coord_change_apply {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] (a : vector_prebundle R F E) {e e' : pretrivialization F bundle.total_space.proj} (he : e a.pretrivialization_atlas) (he' : e' a.pretrivialization_atlas) {b : B} (hb : b e.base_set e'.base_set) (v : F) :
(a.coord_change he he' b) v = (e' (bundle.total_space_mk b (e.symm b v))).snd
theorem vector_prebundle.mk_coord_change {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] (a : vector_prebundle R F E) {e e' : pretrivialization F bundle.total_space.proj} (he : e a.pretrivialization_atlas) (he' : e' a.pretrivialization_atlas) {b : B} (hb : b e.base_set e'.base_set) (v : F) :
(b, (a.coord_change he he' b) v) = e' (bundle.total_space_mk b (e.symm b v))

Topology on the total space that will make the prebundle into a bundle.

Equations
theorem vector_prebundle.mem_trivialization_at_source {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] (a : vector_prebundle R F E) (b : B) (x : E b) :
def vector_prebundle.fiber_topology {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] (a : vector_prebundle R F E) (b : B) :

Topology on the fibers E b induced by the map E b → E.total_space.

Equations
@[continuity]
theorem vector_prebundle.inducing_total_space_mk {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] (a : vector_prebundle R F E) (b : B) :
@[continuity]
theorem vector_prebundle.continuous_total_space_mk {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] (a : vector_prebundle R F E) (b : B) :
def vector_prebundle.to_fiber_bundle {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] (a : vector_prebundle R F E) :

Make a fiber_bundle from a vector_prebundle; auxiliary construction for vector_prebundle.vector_bundle.

Equations
theorem vector_prebundle.to_vector_bundle {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B Type u_5} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] (a : vector_prebundle R F E) :

Make a vector_bundle from a vector_prebundle. Concretely this means that, given a vector_prebundle structure for a sigma-type E -- which consists of a number of "pretrivializations" identifying parts of E with product spaces U × F -- one establishes that for the topology constructed on the sigma-type using vector_prebundle.total_space_topology, these "pretrivializations" are actually "trivializations" (i.e., homeomorphisms with respect to the constructed topology).