mathlib documentation

topology.vector_bundle.basic

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 additionally have the following data:

If all these conditions are satisfied, and if moreover for any two trivializations e, e' in the atlas the transition function considered as a map from B into F →L[R] F is continuous on e.base_set ∩ e'.base_set with respect to the operator norm topology on F →L[R] F, we register the typeclass topological_vector_bundle R F E.

We define constructions on vector bundles like pullbacks and direct sums in other files. Only the trivial bundle is defined in this file.

Tags #

Vector bundle

theorem topological_vector_bundle.pretrivialization.ext {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} {_inst_1 : semiring R} {_inst_2 : Π (x : B), add_comm_monoid (E x)} {_inst_3 : Π (x : B), module R (E x)} {_inst_4 : topological_space F} {_inst_5 : add_comm_monoid F} {_inst_6 : module R F} {_inst_7 : topological_space B} (x y : topological_vector_bundle.pretrivialization R F E) (h : x.to_fiber_bundle_pretrivialization = y.to_fiber_bundle_pretrivialization) :
x = y
theorem topological_vector_bundle.pretrivialization.ext_iff {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} {_inst_1 : semiring R} {_inst_2 : Π (x : B), add_comm_monoid (E x)} {_inst_3 : Π (x : B), module R (E x)} {_inst_4 : topological_space F} {_inst_5 : add_comm_monoid F} {_inst_6 : module R F} {_inst_7 : topological_space B} (x y : topological_vector_bundle.pretrivialization R F E) :
@[nolint, ext]
structure topological_vector_bundle.pretrivialization (R : Type u_1) {B : Type u_3} (F : Type u_4) (E : B → Type u_5) [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 B] :
Type (max u_3 u_4 u_5)

A pretrivialization for a (yet to be defined) topological vector bundle total_space E is a local equiv between sets of the form proj ⁻¹' base_set and base_set × F which respects the first coordinate, and is linear in each fiber.

Instances for topological_vector_bundle.pretrivialization
@[protected]
theorem topological_vector_bundle.pretrivialization.linear {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {b : B} (hb : b e.to_fiber_bundle_pretrivialization.base_set) :
is_linear_map R (λ (y : E b), (e (bundle.total_space_mk b y)).snd)
@[simp]
theorem topological_vector_bundle.pretrivialization.coe_coe {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) :
@[simp]
theorem topological_vector_bundle.pretrivialization.coe_fst {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {x : bundle.total_space E} (ex : x e.to_fiber_bundle_pretrivialization.to_local_equiv.source) :
(e x).fst = x.proj
theorem topological_vector_bundle.pretrivialization.coe_mem_source {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {b : B} {y : E b} :
theorem topological_vector_bundle.pretrivialization.coe_fst' {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {x : bundle.total_space E} (ex : x.proj e.to_fiber_bundle_pretrivialization.base_set) :
(e x).fst = x.proj
@[protected]
theorem topological_vector_bundle.pretrivialization.mk_proj_snd {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {x : bundle.total_space E} (ex : x e.to_fiber_bundle_pretrivialization.to_local_equiv.source) :
(x.proj, (e x).snd) = e x
@[simp]
theorem topological_vector_bundle.pretrivialization.coe_coe_fst {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {b : B} {y : E b} (hb : b e.to_fiber_bundle_pretrivialization.base_set) :
(e y).fst = b
theorem topological_vector_bundle.pretrivialization.mk_proj_snd' {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {x : bundle.total_space E} (ex : x.proj e.to_fiber_bundle_pretrivialization.base_set) :
(x.proj, (e x).snd) = e x
theorem topological_vector_bundle.pretrivialization.mk_mem_target {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {x : B} {y : F} :
theorem topological_vector_bundle.pretrivialization.proj_symm_apply' {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {b : B} {x : F} (hx : b e.to_fiber_bundle_pretrivialization.base_set) :
theorem topological_vector_bundle.pretrivialization.apply_symm_apply {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {x : B × F} (hx : x e.to_fiber_bundle_pretrivialization.to_local_equiv.target) :
theorem topological_vector_bundle.pretrivialization.apply_symm_apply' {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {b : B} {x : F} (hx : b e.to_fiber_bundle_pretrivialization.base_set) :
theorem topological_vector_bundle.pretrivialization.symm_coe_proj {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] {x : B} {y : F} (e : topological_vector_bundle.pretrivialization R F E) (h : x e.to_fiber_bundle_pretrivialization.base_set) :
@[protected]
noncomputable def topological_vector_bundle.pretrivialization.symm {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) (b : B) (y : F) :
E b

A fiberwise inverse to e. This is the function F → E b that induces a local inverse B × F → total_space E of e on e.base_set. It is defined to be 0 outside e.base_set.

Equations
theorem topological_vector_bundle.pretrivialization.symm_apply {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {b : B} (hb : b e.to_fiber_bundle_pretrivialization.base_set) (y : F) :
theorem topological_vector_bundle.pretrivialization.symm_apply_of_not_mem {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {b : B} (hb : b e.to_fiber_bundle_pretrivialization.base_set) (y : F) :
e.symm b y = 0
theorem topological_vector_bundle.pretrivialization.coe_symm_of_not_mem {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {b : B} (hb : b e.to_fiber_bundle_pretrivialization.base_set) :
e.symm b = 0
theorem topological_vector_bundle.pretrivialization.mk_symm {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {b : B} (hb : b e.to_fiber_bundle_pretrivialization.base_set) (y : F) :
theorem topological_vector_bundle.pretrivialization.symm_proj_apply {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) (z : bundle.total_space E) (hz : z.proj e.to_fiber_bundle_pretrivialization.base_set) :
e.symm z.proj (e z).snd = z.snd
theorem topological_vector_bundle.pretrivialization.symm_apply_apply_mk {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {b : B} (hb : b e.to_fiber_bundle_pretrivialization.base_set) (y : E b) :
theorem topological_vector_bundle.pretrivialization.apply_mk_symm {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {b : B} (hb : b e.to_fiber_bundle_pretrivialization.base_set) (y : F) :
e (bundle.total_space_mk b (e.symm b y)) = (b, y)
@[simp]
theorem topological_vector_bundle.pretrivialization.symmₗ_apply {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) (b : B) (y : F) :
(e.symmₗ b) y = e.symm b y
@[protected]
noncomputable def topological_vector_bundle.pretrivialization.symmₗ {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) (b : B) :
F →ₗ[R] E b

A fiberwise linear inverse to e.

Equations
noncomputable def topological_vector_bundle.pretrivialization.linear_equiv_at {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) (b : B) (hb : b e.to_fiber_bundle_pretrivialization.base_set) :
E b ≃ₗ[R] F

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

Equations
@[simp]
theorem topological_vector_bundle.pretrivialization.linear_equiv_at_apply {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) (b : B) (hb : b e.to_fiber_bundle_pretrivialization.base_set) :
(e.linear_equiv_at b hb) = λ (y : E b), (e (bundle.total_space_mk b y)).snd
@[simp]
theorem topological_vector_bundle.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] [Π (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 B] (e : topological_vector_bundle.pretrivialization R F E) (b : B) (hb : b e.to_fiber_bundle_pretrivialization.base_set) :
((e.linear_equiv_at b hb).symm) = e.symm b
@[protected]
noncomputable def topological_vector_bundle.pretrivialization.linear_map_at {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) (b : B) :
E b →ₗ[R] F

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

Equations
theorem topological_vector_bundle.pretrivialization.coe_linear_map_at {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) (b : B) :
theorem topological_vector_bundle.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] [Π (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 B] (e : topological_vector_bundle.pretrivialization R F E) {b : B} (hb : b e.to_fiber_bundle_pretrivialization.base_set) :
(e.linear_map_at b) = λ (y : E b), (e (bundle.total_space_mk b y)).snd
theorem topological_vector_bundle.pretrivialization.linear_map_at_apply {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {b : B} (y : E b) :
theorem topological_vector_bundle.pretrivialization.linear_map_at_def_of_mem {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {b : B} (hb : b e.to_fiber_bundle_pretrivialization.base_set) :
theorem topological_vector_bundle.pretrivialization.linear_map_at_def_of_not_mem {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {b : B} (hb : b e.to_fiber_bundle_pretrivialization.base_set) :
theorem topological_vector_bundle.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] [Π (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 B] (e : topological_vector_bundle.pretrivialization R F E) {b : B} (hb : b e.to_fiber_bundle_pretrivialization.base_set) :
theorem topological_vector_bundle.pretrivialization.symmₗ_linear_map_at {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {b : B} (hb : b e.to_fiber_bundle_pretrivialization.base_set) (y : E b) :
(e.symmₗ b) ((e.linear_map_at b) y) = y
theorem topological_vector_bundle.pretrivialization.linear_map_at_symmₗ {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] (e : topological_vector_bundle.pretrivialization R F E) {b : B} (hb : b e.to_fiber_bundle_pretrivialization.base_set) (y : F) :
(e.linear_map_at b) ((e.symmₗ b) y) = y
theorem topological_vector_bundle.trivialization.ext {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} {_inst_1 : semiring R} {_inst_2 : Π (x : B), add_comm_monoid (E x)} {_inst_3 : Π (x : B), module R (E x)} {_inst_4 : topological_space F} {_inst_5 : add_comm_monoid F} {_inst_6 : module R F} {_inst_7 : topological_space B} {_inst_8 : topological_space (bundle.total_space E)} (x y : topological_vector_bundle.trivialization R F E) (h : x.to_fiber_bundle_trivialization = y.to_fiber_bundle_trivialization) :
x = y
theorem topological_vector_bundle.trivialization.ext_iff {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} {_inst_1 : semiring R} {_inst_2 : Π (x : B), add_comm_monoid (E x)} {_inst_3 : Π (x : B), module R (E x)} {_inst_4 : topological_space F} {_inst_5 : add_comm_monoid F} {_inst_6 : module R F} {_inst_7 : topological_space B} {_inst_8 : topological_space (bundle.total_space E)} (x y : topological_vector_bundle.trivialization R F E) :
@[nolint, ext]
structure topological_vector_bundle.trivialization (R : Type u_1) {B : Type u_3} (F : Type u_4) (E : B → Type u_5) [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 B] [topological_space (bundle.total_space E)] :
Type (max u_3 u_4 u_5)

A structure extending local homeomorphisms, defining a local trivialization of the projection proj : total_space E → B with fiber F, as a local homeomorphism between total_space E and B × F defined between two sets of the form proj ⁻¹' base_set and base_set × F, acting trivially on the first coordinate and linear in the fibers.

Instances for topological_vector_bundle.trivialization
@[protected]
theorem topological_vector_bundle.trivialization.linear {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) {b : B} (hb : b e.to_fiber_bundle_trivialization.base_set) :
is_linear_map R (λ (y : E b), (e (bundle.total_space_mk b y)).snd)
@[simp]
theorem topological_vector_bundle.trivialization.coe_coe {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) :
@[simp]
theorem topological_vector_bundle.trivialization.coe_fst {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (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 = x.proj
theorem topological_vector_bundle.trivialization.coe_fst' {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) {x : bundle.total_space E} (ex : x.proj e.to_fiber_bundle_trivialization.base_set) :
(e x).fst = x.proj
theorem topological_vector_bundle.trivialization.mk_proj_snd {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (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) :
(x.proj, (e x).snd) = e x
theorem topological_vector_bundle.trivialization.mk_proj_snd' {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) {x : bundle.total_space E} (ex : x.proj e.to_fiber_bundle_trivialization.base_set) :
(x.proj, (e x).snd) = e x
@[simp]
theorem topological_vector_bundle.trivialization.coe_coe_fst {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) {b : B} {y : E b} (hb : b e.to_fiber_bundle_trivialization.base_set) :
(e y).fst = b
theorem topological_vector_bundle.trivialization.proj_symm_apply' {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) {b : B} {x : F} (hx : b e.to_fiber_bundle_trivialization.base_set) :
theorem topological_vector_bundle.trivialization.apply_symm_apply' {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) {b : B} {x : F} (hx : b e.to_fiber_bundle_trivialization.base_set) :
@[simp]
theorem topological_vector_bundle.trivialization.symm_coe_proj {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] {x : B} {y : F} (e : topological_vector_bundle.trivialization R F E) (h : x e.to_fiber_bundle_trivialization.base_set) :
@[protected]
noncomputable def topological_vector_bundle.trivialization.symm {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) (b : B) (y : F) :
E b

A fiberwise inverse to e. The function F → E x that induces a local inverse B × F → total_space E of e on e.base_set. It is defined to be 0 outside e.base_set.

Equations
theorem topological_vector_bundle.trivialization.symm_apply {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) {b : B} (hb : b e.to_fiber_bundle_trivialization.base_set) (y : F) :
theorem topological_vector_bundle.trivialization.symm_apply_of_not_mem {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) {b : B} (hb : b e.to_fiber_bundle_trivialization.base_set) (y : F) :
e.symm b y = 0
theorem topological_vector_bundle.trivialization.mk_symm {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) {b : B} (hb : b e.to_fiber_bundle_trivialization.base_set) (y : F) :
theorem topological_vector_bundle.trivialization.symm_proj_apply {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) (z : bundle.total_space E) (hz : z.proj e.to_fiber_bundle_trivialization.base_set) :
e.symm z.proj (e z).snd = z.snd
theorem topological_vector_bundle.trivialization.symm_apply_apply_mk {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) {b : B} (hb : b e.to_fiber_bundle_trivialization.base_set) (y : E b) :
theorem topological_vector_bundle.trivialization.apply_mk_symm {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) {b : B} (hb : b e.to_fiber_bundle_trivialization.base_set) (y : F) :
e (bundle.total_space_mk b (e.symm b y)) = (b, y)
noncomputable def topological_vector_bundle.trivialization.linear_equiv_at {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) (b : B) (hb : b e.to_fiber_bundle_trivialization.base_set) :
E b ≃ₗ[R] F

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

Equations
@[simp]
theorem topological_vector_bundle.trivialization.linear_equiv_at_apply {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) (b : B) (hb : b e.to_fiber_bundle_trivialization.base_set) (v : E b) :
@[simp]
theorem topological_vector_bundle.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] [Π (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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) (b : B) (hb : b e.to_fiber_bundle_trivialization.base_set) (v : F) :
((e.linear_equiv_at b hb).symm) v = e.symm b v
@[protected]
noncomputable def topological_vector_bundle.trivialization.symmₗ {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) (b : B) :
F →ₗ[R] E b

A fiberwise linear inverse to e.

Equations
theorem topological_vector_bundle.trivialization.coe_symmₗ {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) (b : B) :
(e.symmₗ b) = e.symm b
@[protected]
noncomputable def topological_vector_bundle.trivialization.linear_map_at {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) (b : B) :
E b →ₗ[R] F

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

Equations
theorem topological_vector_bundle.trivialization.coe_linear_map_at {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) (b : B) :
theorem topological_vector_bundle.trivialization.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] [Π (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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) {b : B} (hb : b e.to_fiber_bundle_trivialization.base_set) :
(e.linear_map_at b) = λ (y : E b), (e (bundle.total_space_mk b y)).snd
theorem topological_vector_bundle.trivialization.linear_map_at_apply {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) {b : B} (y : E b) :
theorem topological_vector_bundle.trivialization.linear_map_at_def_of_mem {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) {b : B} (hb : b e.to_fiber_bundle_trivialization.base_set) :
theorem topological_vector_bundle.trivialization.linear_map_at_def_of_not_mem {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) {b : B} (hb : b e.to_fiber_bundle_trivialization.base_set) :
theorem topological_vector_bundle.trivialization.symmₗ_linear_map_at {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) {b : B} (hb : b e.to_fiber_bundle_trivialization.base_set) (y : E b) :
(e.symmₗ b) ((e.linear_map_at b) y) = y
theorem topological_vector_bundle.trivialization.linear_map_at_symmₗ {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e : topological_vector_bundle.trivialization R F E) {b : B} (hb : b e.to_fiber_bundle_trivialization.base_set) (y : F) :
(e.linear_map_at b) ((e.symmₗ b) y) = y
noncomputable def topological_vector_bundle.trivialization.coord_change {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e e' : topological_vector_bundle.trivialization R F 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 topological_vector_bundle.trivialization.coord_change_apply {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e e' : topological_vector_bundle.trivialization R F E) {b : B} (hb : b e.to_fiber_bundle_trivialization.base_set e'.to_fiber_bundle_trivialization.base_set) (y : F) :
(e.coord_change e' b) y = (e' (bundle.total_space_mk b (e.symm b y))).snd
theorem topological_vector_bundle.trivialization.mk_coord_change {R : Type u_1} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} [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 B] [topological_space (bundle.total_space E)] (e e' : topological_vector_bundle.trivialization R F E) {b : B} (hb : b e.to_fiber_bundle_trivialization.base_set e'.to_fiber_bundle_trivialization.base_set) (y : F) :
(b, (e.coord_change e' b) y) = e' (bundle.total_space_mk b (e.symm b y))

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 continuous_transitions (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] (e : local_equiv (B × F) (B × F)) :
Prop

The valid transition functions for a topological vector bundle over B modelled on a normed space F: a transition function must be a local homeomorphism of B × F with source and target both s ×ˢ univ, which on this set is of the form λ (b, v), (b, ε b v) for some continuous map ε from s to F ≃L[R] F. Here continuity is with respect to the operator norm on F →L[R] F.

Equations
@[class]
structure topological_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)] :
Type (max u_3 u_4 u_5)

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 of this typeclass
Instances of other typeclasses for topological_vector_bundle
  • topological_vector_bundle.has_sizeof_inst
noncomputable def topological_vector_bundle.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)] [topological_vector_bundle R F E] (e : topological_vector_bundle.trivialization R F 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]
theorem topological_vector_bundle.trivialization.continuous_linear_map_at_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] [topological_space (bundle.total_space E)] [Π (x : B), topological_space (E x)] [topological_vector_bundle R F E] (e : topological_vector_bundle.trivialization R F E) (b : B) :
noncomputable def topological_vector_bundle.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)] [topological_vector_bundle R F E] (e : topological_vector_bundle.trivialization R F E) (b : B) :
F →L[R] E b

Backwards map of continuous_linear_equiv_at, defined everywhere.

Equations
@[simp]
theorem topological_vector_bundle.trivialization.symmL_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] [topological_space (bundle.total_space E)] [Π (x : B), topological_space (E x)] [topological_vector_bundle R F E] (e : topological_vector_bundle.trivialization R F E) (b : B) :
(e.symmL b) = e.symm b
theorem topological_vector_bundle.trivialization.symmL_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)] [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) :
theorem topological_vector_bundle.trivialization.continuous_linear_map_at_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)] [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 : F) :
noncomputable def topological_vector_bundle.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)] [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]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def topological_vector_bundle.bundle.trivial.module {R : Type u_1} [nontrivially_normed_field R] {B : Type u_2} {F : Type u_3} [add_comm_monoid F] [module R F] (b : B) :
Equations
theorem topological_vector_bundle.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] [topological_space (bundle.total_space E)] [Π (x : B), topological_space (E x)] [topological_vector_bundle R F E] (x : B) :
@[continuity]
theorem topological_vector_bundle.continuous_proj (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)] [topological_vector_bundle R F E] :

Constructing topological vector bundles #

structure topological_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 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.

Instances for topological_vector_bundle_core
def trivial_topological_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_2) [inhabited ι] :

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

Equations
@[protected, instance]
def topological_vector_bundle_core.inhabited (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_2) [inhabited ι] :
Equations
theorem topological_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 : 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_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 : topological_vector_bundle_core R B F ι) :
Type u_6

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

Equations
@[nolint, reducible]
def topological_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 : topological_vector_bundle_core R B F ι) :
Type u_3

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_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 : topological_vector_bundle_core R B F ι) (x : B) :
Type u_4

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

Equations
Instances for topological_vector_bundle_core.fiber
@[protected, instance]
def topological_vector_bundle_core.topological_space_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 : topological_vector_bundle_core R B F ι) (x : B) :
Equations
@[protected, instance]
def topological_vector_bundle_core.add_comm_monoid_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 : topological_vector_bundle_core R B F ι) (x : B) :
Equations
@[protected, instance]
def topological_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 : topological_vector_bundle_core R B F ι) (x : B) :
module R (Z.fiber x)
Equations
@[protected, instance]
def topological_vector_bundle_core.add_comm_group_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 : topological_vector_bundle_core R B F ι) [add_comm_group F] (x : B) :
Equations
@[simp, reducible]
def topological_vector_bundle_core.proj {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 : topological_vector_bundle_core R B F ι) :

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

Equations
@[nolint, reducible]
def topological_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 : topological_vector_bundle_core R B F ι) :
Type (max u_3 u_4)

The total space of the topological 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 topological_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 : 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_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 : topological_vector_bundle_core R B F ι) (i j : ι) (p : B × F) :
@[protected, 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_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 : topological_vector_bundle_core R B F ι) (b : B) (i j : ι) :

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.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 : topological_vector_bundle_core R B F ι) (i : ι) :
@[simp]
theorem topological_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 : topological_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 topological_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 : topological_vector_bundle_core R B F ι) (i : ι) (p : B × F) :
@[simp]
theorem topological_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 : topological_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 topological_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 : topological_vector_bundle_core R B F ι) (i j : ι) {b : B} (hb : b Z.base_set i Z.base_set j) (v : F) :
((Z.local_triv i).coord_change (Z.local_triv j) b) v = (Z.coord_change i j b) v

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

Equations
@[simp]
theorem topological_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 : topological_vector_bundle_core R B F ι) (b : B) :
@[simp]
theorem topological_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 : topological_vector_bundle_core R B F ι) (p : Z.total_space) :
(Z.local_triv_at p.fst) p = (p.fst, p.snd)
@[simp]
theorem topological_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 : topological_vector_bundle_core R B F ι) (b : B) (a : F) :
(Z.local_triv_at b) b, a⟩ = (b, a)
@[continuity]
theorem topological_vector_bundle_core.continuous_proj {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 : 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_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 : topological_vector_bundle_core R B F ι) :

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

Topological vector prebundle #

@[nolint]
structure topological_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 topological_vector_prebundle.

Instances for topological_vector_prebundle
  • topological_vector_prebundle.has_sizeof_inst
noncomputable def topological_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 : topological_vector_prebundle R F E) {e e' : topological_vector_bundle.pretrivialization R F E} (he : e a.pretrivialization_atlas) (he' : e' a.pretrivialization_atlas) (b : B) :
F →L[R] F

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

Equations
theorem topological_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 : topological_vector_prebundle R F E) {e e' : topological_vector_bundle.pretrivialization R F E} (he : e a.pretrivialization_atlas) (he' : e' a.pretrivialization_atlas) {b : B} (hb : b e.to_fiber_bundle_pretrivialization.base_set e'.to_fiber_bundle_pretrivialization.base_set) (v : F) :
(a.coord_change he he' b) v = (e' (bundle.total_space_mk b (e.symm b v))).snd
theorem topological_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 : topological_vector_prebundle R F E) {e e' : topological_vector_bundle.pretrivialization R F E} (he : e a.pretrivialization_atlas) (he' : e' a.pretrivialization_atlas) {b : B} (hb : b e.to_fiber_bundle_pretrivialization.base_set e'.to_fiber_bundle_pretrivialization.base_set) (v : F) :
(b, (a.coord_change he he' b) v) = e' (bundle.total_space_mk b (e.symm b v))
def topological_vector_prebundle.total_space_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 : topological_vector_prebundle R F E) :

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

Equations
theorem topological_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 : topological_vector_prebundle R F E) (b : B) (x : E b) :
def topological_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 : topological_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 topological_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 : topological_vector_prebundle R F E) (b : B) :
@[continuity]
theorem topological_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 : topological_vector_prebundle R F E) (b : B) :
def topological_vector_prebundle.to_topological_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 : topological_vector_prebundle R F E) :

Make a topological_vector_bundle from a topological_vector_prebundle. Concretely this means that, given a topological_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 topological_vector_prebundle.total_space_topology, these "pretrivializations" are actually "trivializations" (i.e., homeomorphisms with respect to the constructed topology).

Equations