Vector bundles #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 F E, one should additionally have the
following properties:
- The bundle trivializations in the trivialization atlas should be continuous linear equivs in the fibers;
- For any two trivializations
e,e'in the atlas the transition function considered as a map fromBintoF →L[R] Fis continuous one.base_set ∩ e'.base_setwith respect to the operator norm topology onF →L[R] F.
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.
Main Definitions #
trivialization.is_linear: a class stating that a trivialization is fiberwise linear on its base set.trivialization.linear_equiv_atandtrivialization.continuous_linear_map_atare the (continuous) linear fiberwise equivalences a trivialization induces.- They have forward maps
trivialization.linear_map_at/trivialization.continuous_linear_map_atand inversestrivialization.symmₗ/trivialization.symmL. Note that these are all defined everywhere, since they are extended using the zero function. trivialization.coord_changeLis the coordinate change induced by two trivializations. It only makes sense on the intersection of their base sets, but is extended outside it using the identity.- Given a continuous (semi)linear map between
E xandE' ywhereEandE'are bundles over possibly different base sets,continuous_linear_map.in_coordinatesturns this into a continuous (semi)linear map between the chosen fibers of those bundles.
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_2}
{F : Type u_3}
{E : B → Type u_4}
[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_2}
{F : Type u_3}
{E : B → Type u_4}
[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) :
@[protected]
noncomputable
def
pretrivialization.symmₗ
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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) :
A fiberwise linear inverse to e.
Equations
- pretrivialization.symmₗ R e b = is_linear_map.mk' (e.symm b) _
@[simp]
theorem
pretrivialization.symmₗ_apply
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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) :
⇑(pretrivialization.symmₗ R e b) y = e.symm b y
@[simp]
theorem
pretrivialization.linear_equiv_at_symm_apply
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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) :
⇑((pretrivialization.linear_equiv_at R e b hb).symm) = e.symm b
@[simp]
theorem
pretrivialization.linear_equiv_at_apply
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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_2}
{F : Type u_3}
{E : B → Type u_4}
[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) :
A pretrivialization for a vector bundle defines linear equivalences between the fibers and the model space.
@[protected]
noncomputable
def
pretrivialization.linear_map_at
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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) :
A fiberwise linear map equal to e on e.base_set.
theorem
pretrivialization.coe_linear_map_at
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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_2}
{F : Type u_3}
{E : B → Type u_4}
[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_2}
{F : Type u_3}
{E : B → Type u_4}
[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_def_of_mem
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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) :
pretrivialization.linear_map_at R e b = ↑(pretrivialization.linear_equiv_at R e b hb)
theorem
pretrivialization.linear_map_at_def_of_not_mem
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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) :
pretrivialization.linear_map_at R e b = 0
theorem
pretrivialization.linear_map_at_eq_zero
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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) :
pretrivialization.linear_map_at R e b = 0
theorem
pretrivialization.symmₗ_linear_map_at
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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) :
⇑(pretrivialization.symmₗ R e b) (⇑(pretrivialization.linear_map_at R e b) y) = y
theorem
pretrivialization.linear_map_at_symmₗ
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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) :
⇑(pretrivialization.linear_map_at R e b) (⇑(pretrivialization.symmₗ R e b) y) = y
@[class]
structure
trivialization.is_linear
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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.
@[protected]
theorem
trivialization.linear
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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) :
@[protected, instance]
def
trivialization.to_pretrivialization.is_linear
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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] :
noncomputable
def
trivialization.linear_equiv_at
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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) :
A trivialization for a vector bundle defines linear equivalences between the fibers and the model space.
Equations
- trivialization.linear_equiv_at R e b hb = pretrivialization.linear_equiv_at R e.to_pretrivialization b hb
@[simp]
theorem
trivialization.linear_equiv_at_apply
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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) :
⇑((trivialization.linear_equiv_at R e b hb).symm) v = e.symm b v
@[protected]
noncomputable
def
trivialization.symmₗ
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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) :
A fiberwise linear inverse to e.
Equations
theorem
trivialization.coe_symmₗ
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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) :
⇑(trivialization.symmₗ R e b) = e.symm b
@[protected]
noncomputable
def
trivialization.linear_map_at
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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) :
A fiberwise linear map equal to e on e.base_set.
Equations
theorem
trivialization.coe_linear_map_at
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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) :
theorem
trivialization.coe_linear_map_at_of_mem
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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) :
theorem
trivialization.linear_map_at_apply
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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}
(y : E b) :
theorem
trivialization.linear_map_at_def_of_mem
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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) :
trivialization.linear_map_at R e b = ↑(trivialization.linear_equiv_at R e b hb)
theorem
trivialization.linear_map_at_def_of_not_mem
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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) :
trivialization.linear_map_at R e b = 0
theorem
trivialization.symmₗ_linear_map_at
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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) :
⇑(trivialization.symmₗ R e b) (⇑(trivialization.linear_map_at R e b) y) = y
theorem
trivialization.linear_map_at_symmₗ
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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 : F) :
⇑(trivialization.linear_map_at R e b) (⇑(trivialization.symmₗ R e b) y) = y
noncomputable
def
trivialization.coord_changeL
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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) :
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
- trivialization.coord_changeL R e e' b = {to_linear_equiv := {to_fun := (dite (b ∈ e.base_set ∩ e'.base_set) (λ (hb : b ∈ e.base_set ∩ e'.base_set), (trivialization.linear_equiv_at R e b _).symm.trans (trivialization.linear_equiv_at R e' b _)) (λ (hb : b ∉ e.base_set ∩ e'.base_set), linear_equiv.refl R F)).to_fun, map_add' := _, map_smul' := _, inv_fun := (dite (b ∈ e.base_set ∩ e'.base_set) (λ (hb : b ∈ e.base_set ∩ e'.base_set), (trivialization.linear_equiv_at R e b _).symm.trans (trivialization.linear_equiv_at R e' b _)) (λ (hb : b ∉ e.base_set ∩ e'.base_set), linear_equiv.refl R F)).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
theorem
trivialization.coe_coord_changeL
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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) :
⇑(trivialization.coord_changeL R e e' b) = ⇑((trivialization.linear_equiv_at R e b _).symm.trans (trivialization.linear_equiv_at R e' b _))
theorem
trivialization.coe_coord_changeL'
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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) :
(trivialization.coord_changeL R e e' b).to_linear_equiv = (trivialization.linear_equiv_at R e b _).symm.trans (trivialization.linear_equiv_at R e' b _)
theorem
trivialization.symm_coord_changeL
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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) :
(trivialization.coord_changeL R e e' b).symm = trivialization.coord_changeL R e' e b
theorem
trivialization.coord_changeL_apply
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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.mk_coord_changeL
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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.apply_symm_apply_eq_coord_changeL
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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)
(v : F) :
⇑e' (⇑(e.to_local_homeomorph.symm) (b, v)) = (b, ⇑(trivialization.coord_changeL R e e' b) v)
theorem
trivialization.coord_changeL_apply'
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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) :
⇑(trivialization.coord_changeL R e e' b) y = (⇑e' (⇑(e.to_local_homeomorph.symm) (b, y))).snd
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.
theorem
trivialization.coord_changeL_symm_apply
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space F 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) :
⇑((trivialization.coord_changeL R e e' b).symm) = ⇑((trivialization.linear_equiv_at R e' b _).symm.trans (trivialization.linear_equiv_at R e b _))
def
bundle.zero_section
{B : Type u_2}
(F : Type u_3)
(E : B → Type u_4)
[Π (x : B), has_zero (E x)] :
B → bundle.total_space F E
The zero section of a vector bundle
Equations
- bundle.zero_section F E = λ (x : B), {proj := x, snd := 0}
@[class]
structure
vector_bundle
(R : Type u_1)
{B : Type u_2}
(F : Type u_3)
(E : B → Type u_4)
[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 F E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E] :
Prop
- trivialization_linear' : ∀ (e : trivialization F bundle.total_space.proj) [_inst_10 : mem_trivialization_atlas e], trivialization.is_linear R e
- continuous_on_coord_change' : ∀ (e e' : trivialization F bundle.total_space.proj) [_inst_10 : mem_trivialization_atlas e] [_inst_11 : mem_trivialization_atlas e'], continuous_on (λ (b : B), ↑(trivialization.coord_changeL R e e' b)) (e.base_set ∩ e'.base_set)
The space total_space F 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.
@[protected, instance]
def
trivialization_linear
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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 F E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
[vector_bundle R F E]
(e : trivialization F bundle.total_space.proj)
[mem_trivialization_atlas e] :
theorem
continuous_on_coord_change
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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 F E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
[vector_bundle R F E]
(e e' : trivialization F bundle.total_space.proj)
[he : mem_trivialization_atlas e]
[he' : mem_trivialization_atlas e'] :
continuous_on (λ (b : B), ↑(trivialization.coord_changeL R e e' b)) (e.base_set ∩ e'.base_set)
@[simp]
theorem
trivialization.continuous_linear_map_at_apply
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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 F 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) :
⇑(trivialization.continuous_linear_map_at R e b) = ⇑(trivialization.linear_map_at R e b)
noncomputable
def
trivialization.continuous_linear_map_at
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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 F 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) :
Forward map of continuous_linear_equiv_at (only propositionally equal),
defined everywhere (0 outside domain).
Equations
- trivialization.continuous_linear_map_at R e b = {to_linear_map := {to_fun := ⇑(trivialization.linear_map_at R e b), map_add' := _, map_smul' := _}, cont := _}
@[simp]
theorem
trivialization.symmL_apply
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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 F 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) :
⇑(trivialization.symmL R e b) = e.symm b
noncomputable
def
trivialization.symmL
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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 F 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) :
Backwards map of continuous_linear_equiv_at, defined everywhere.
Equations
- trivialization.symmL R e b = {to_linear_map := {to_fun := e.symm b, map_add' := _, map_smul' := _}, cont := _}
theorem
trivialization.symmL_continuous_linear_map_at
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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 F 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)
(y : E b) :
⇑(trivialization.symmL R e b) (⇑(trivialization.continuous_linear_map_at R e b) y) = y
theorem
trivialization.continuous_linear_map_at_symmL
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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 F 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)
(y : F) :
⇑(trivialization.continuous_linear_map_at R e b) (⇑(trivialization.symmL R e b) y) = y
@[simp]
theorem
trivialization.continuous_linear_equiv_at_symm_apply
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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 F 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) :
⇑((trivialization.continuous_linear_equiv_at R e b hb).symm) = e.symm b
@[simp]
theorem
trivialization.continuous_linear_equiv_at_apply
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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 F 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) :
noncomputable
def
trivialization.continuous_linear_equiv_at
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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 F 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) :
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
- trivialization.continuous_linear_equiv_at R e b hb = {to_linear_equiv := {to_fun := λ (y : E b), (⇑e {proj := b, snd := y}).snd, map_add' := _, map_smul' := _, inv_fun := e.symm b, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
theorem
trivialization.coe_continuous_linear_equiv_at_eq
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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 F 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) :
⇑(trivialization.continuous_linear_equiv_at R e b hb) = ⇑(trivialization.continuous_linear_map_at R e b)
theorem
trivialization.symm_continuous_linear_equiv_at_eq
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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 F 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) :
⇑((trivialization.continuous_linear_equiv_at R e b hb).symm) = ⇑(trivialization.symmL R e b)
@[simp]
theorem
trivialization.continuous_linear_equiv_at_apply'
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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 F E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
(x : bundle.total_space F E)
(hx : x ∈ e.to_local_homeomorph.to_local_equiv.source) :
theorem
trivialization.apply_eq_prod_continuous_linear_equiv_at
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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 F 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)
(z : E b) :
@[protected]
theorem
trivialization.zero_section
(R : Type u_1)
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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 F 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 F E x) = (x, 0)
theorem
trivialization.symm_apply_eq_mk_continuous_linear_equiv_at_symm
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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 F 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)
(z : F) :
⇑(e.to_local_homeomorph.symm) (b, z) = {proj := b, snd := ⇑((trivialization.continuous_linear_equiv_at R e b hb).symm) z}
theorem
trivialization.comp_continuous_linear_equiv_at_eq_coord_change
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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 F E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
(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) :
(trivialization.continuous_linear_equiv_at R e b _).symm.trans (trivialization.continuous_linear_equiv_at R e' b _) = trivialization.coord_changeL R e e' b
Constructing vector bundles #
structure
vector_bundle_core
(R : Type u_1)
(B : Type u_2)
(F : Type u_3)
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space 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 →L[R] F)
- coord_change_self : ∀ (i : ι) (x : B), x ∈ self.base_set i → ∀ (v : F), ⇑(self.coord_change i i x) v = v
- continuous_on_coord_change : ∀ (i j : ι), continuous_on (self.coord_change i j) (self.base_set i ∩ self.base_set j)
- 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 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
- vector_bundle_core.has_sizeof_inst
- vector_bundle_core.inhabited
- vector_bundle_core.to_fiber_bundle_core_coe
def
trivial_vector_bundle_core
(R : Type u_1)
(B : Type u_2)
(F : Type u_3)
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
(ι : Type u_4)
[inhabited ι] :
vector_bundle_core R B F ι
The trivial vector bundle core, in which all the changes of coordinates are the identity.
Equations
- trivial_vector_bundle_core R B F ι = {base_set := λ (ι : ι), set.univ, is_open_base_set := _, index_at := inhabited.default (pi.inhabited B), mem_base_set_at := _, coord_change := λ (i j : ι) (x : B), continuous_linear_map.id R F, coord_change_self := _, continuous_on_coord_change := _, coord_change_comp := _}
@[protected, instance]
def
vector_bundle_core.inhabited
(R : Type u_1)
(B : Type u_2)
(F : Type u_3)
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
(ι : Type u_4)
[inhabited ι] :
inhabited (vector_bundle_core R B F ι)
Equations
- vector_bundle_core.inhabited R B F ι = {default := trivial_vector_bundle_core R B F ι _inst_10}
def
vector_bundle_core.to_fiber_bundle_core
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι) :
fiber_bundle_core ι B F
Natural identification to a fiber_bundle_core.
Equations
- Z.to_fiber_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 := _, continuous_on_coord_change := _, coord_change_comp := _}
@[simp]
theorem
vector_bundle_core.to_fiber_bundle_core_base_set
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι) :
@[simp]
theorem
vector_bundle_core.to_fiber_bundle_core_coord_change
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι) :
Z.to_fiber_bundle_core.coord_change = λ (i j : ι) (b : B), ⇑(Z.coord_change i j b)
@[simp]
theorem
vector_bundle_core.to_fiber_bundle_core_index_at
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι) :
@[protected, instance]
def
vector_bundle_core.to_fiber_bundle_core_coe
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5} :
has_coe (vector_bundle_core R B F ι) (fiber_bundle_core ι B F)
theorem
vector_bundle_core.coord_change_linear_comp
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(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_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι) :
Type u_5
The index set of a vector bundle core, as a convenience function for dot notation
@[nolint, reducible]
def
vector_bundle_core.base
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι) :
Type u_2
The base space of a vector bundle core, as a convenience function for dot notation
@[nolint]
def
vector_bundle_core.fiber
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι) :
The fiber of a vector bundle core, as a convenience function for dot notation and typeclass inference
Equations
@[protected, instance]
def
vector_bundle_core.topological_space_fiber
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
(x : B) :
topological_space (Z.fiber x)
Equations
@[protected, instance]
def
vector_bundle_core.add_comm_monoid_fiber
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
(x : B) :
add_comm_monoid (Z.fiber x)
Equations
- Z.add_comm_monoid_fiber = id (λ (x : B), add_comm_group.to_add_comm_monoid F)
@[protected, instance]
def
vector_bundle_core.module_fiber
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
(x : B) :
Equations
- Z.module_fiber = id (λ (x : B), normed_space.to_module)
@[protected, instance]
def
vector_bundle_core.add_comm_group_fiber
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
[add_comm_group F]
(x : B) :
add_comm_group (Z.fiber x)
Equations
- Z.add_comm_group_fiber = id (λ (x : B), _inst_10)
@[protected, simp, reducible]
def
vector_bundle_core.proj
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι) :
bundle.total_space F Z.fiber → B
The projection from the total space of a fiber bundle core, on its base.
Equations
@[protected, nolint, reducible]
def
vector_bundle_core.total_space
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι) :
Type (max u_2 u_3)
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.
Equations
- Z.total_space = bundle.total_space F Z.fiber
def
vector_bundle_core.triv_change
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : 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
vector_bundle_core.mem_triv_change_source
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : 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
vector_bundle_core.to_topological_space
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι) :
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_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
(b : B)
(i j : ι) :
Z.to_fiber_bundle_core.coord_change i j b = ⇑(Z.coord_change i j b)
def
vector_bundle_core.local_triv
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
(i : ι) :
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
- Z.local_triv i = id (Z.to_fiber_bundle_core.local_triv i)
Instances for vector_bundle_core.local_triv
@[protected, instance]
def
vector_bundle_core.local_triv.is_linear
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
(i : ι) :
trivialization.is_linear R (Z.local_triv i)
The standard local trivializations of a vector bundle constructed from core are linear.
@[simp]
theorem
vector_bundle_core.mem_local_triv_source
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
(i : ι)
(p : Z.total_space) :
p ∈ (Z.local_triv i).to_local_homeomorph.to_local_equiv.source ↔ p.proj ∈ Z.base_set i
@[simp]
theorem
vector_bundle_core.base_set_at
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
(i : ι) :
Z.base_set i = (Z.local_triv i).base_set
@[simp]
theorem
vector_bundle_core.local_triv_apply
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
(i : ι)
(p : Z.total_space) :
⇑(Z.local_triv i) p = (p.proj, ⇑(Z.coord_change (Z.index_at p.proj) i p.proj) p.snd)
@[simp]
theorem
vector_bundle_core.mem_local_triv_target
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
(i : ι)
(p : B × F) :
p ∈ (Z.local_triv i).to_local_homeomorph.to_local_equiv.target ↔ p.fst ∈ (Z.local_triv i).base_set
@[simp]
theorem
vector_bundle_core.local_triv_symm_fst
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
(i : ι)
(p : B × F) :
⇑((Z.local_triv i).to_local_homeomorph.symm) p = {proj := p.fst, snd := ⇑(Z.coord_change i (Z.index_at p.fst) p.fst) p.snd}
@[simp]
theorem
vector_bundle_core.local_triv_symm_apply
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(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_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
(i j : ι)
{b : B}
(hb : b ∈ Z.base_set i ∩ Z.base_set j)
(v : F) :
⇑(trivialization.coord_changeL R (Z.local_triv i) (Z.local_triv j) b) v = ⇑(Z.coord_change i j b) v
def
vector_bundle_core.local_triv_at
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
(b : B) :
Preferred local trivialization of a vector bundle constructed from core, at a given point, as a bundle trivialization
Equations
- Z.local_triv_at b = Z.local_triv (Z.index_at b)
@[simp]
theorem
vector_bundle_core.local_triv_at_def
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
(b : B) :
Z.local_triv (Z.index_at b) = Z.local_triv_at b
@[simp]
theorem
vector_bundle_core.mem_source_at
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
(b : B)
(a : F) :
{proj := b, snd := a} ∈ (Z.local_triv_at b).to_local_homeomorph.to_local_equiv.source
@[simp]
theorem
vector_bundle_core.local_triv_at_apply
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
(p : Z.total_space) :
@[simp]
theorem
vector_bundle_core.local_triv_at_apply_mk
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
(b : B)
(a : F) :
@[simp]
theorem
vector_bundle_core.mem_local_triv_at_base_set
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
(b : B) :
b ∈ (Z.local_triv_at b).base_set
@[protected, instance]
def
vector_bundle_core.fiber_bundle
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι) :
fiber_bundle F Z.fiber
Equations
@[protected, instance]
def
vector_bundle_core.vector_bundle
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι) :
vector_bundle R F Z.fiber
@[continuity]
theorem
vector_bundle_core.continuous_proj
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι) :
The projection on the base of a vector bundle created from core is continuous
theorem
vector_bundle_core.is_open_map_proj
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι) :
The projection on the base of a vector bundle created from core is an open map
@[simp]
theorem
vector_bundle_core.local_triv_continuous_linear_map_at
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
{i : ι}
{b : B}
(hb : b ∈ Z.base_set i) :
trivialization.continuous_linear_map_at R (Z.local_triv i) b = Z.coord_change (Z.index_at b) i b
@[simp]
theorem
vector_bundle_core.trivialization_at_continuous_linear_map_at
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
{b₀ b : B}
(hb : b ∈ (fiber_bundle.trivialization_at F Z.fiber b₀).base_set) :
trivialization.continuous_linear_map_at R (fiber_bundle.trivialization_at F Z.fiber b₀) b = Z.coord_change (Z.index_at b) (Z.index_at b₀) b
@[simp]
theorem
vector_bundle_core.local_triv_symmL
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
{i : ι}
{b : B}
(hb : b ∈ Z.base_set i) :
trivialization.symmL R (Z.local_triv i) b = Z.coord_change i (Z.index_at b) b
@[simp]
theorem
vector_bundle_core.trivialization_at_symmL
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
{b₀ b : B}
(hb : b ∈ (fiber_bundle.trivialization_at F Z.fiber b₀).base_set) :
trivialization.symmL R (fiber_bundle.trivialization_at F Z.fiber b₀) b = Z.coord_change (Z.index_at b₀) (Z.index_at b) b
@[simp]
theorem
vector_bundle_core.trivialization_at_coord_change_eq
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_5}
(Z : vector_bundle_core R B F ι)
{b₀ b₁ b : B}
(hb : b ∈ (fiber_bundle.trivialization_at F Z.fiber b₀).base_set ∩ (fiber_bundle.trivialization_at F Z.fiber b₁).base_set)
(v : F) :
⇑(trivialization.coord_changeL R (fiber_bundle.trivialization_at F Z.fiber b₀) (fiber_bundle.trivialization_at F Z.fiber b₁) b) v = ⇑(Z.coord_change (Z.index_at b₀) (Z.index_at b₁) b) v
Vector prebundle #
@[nolint]
structure
vector_prebundle
(R : Type u_1)
{B : Type u_2}
(F : Type u_3)
(E : B → Type u_4)
[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]
[Π (x : B), topological_space (E x)] :
Type (max u_2 u_3 u_4)
- pretrivialization_atlas : set (pretrivialization F bundle.total_space.proj)
- pretrivialization_linear' : ∀ (e : pretrivialization F bundle.total_space.proj), e ∈ self.pretrivialization_atlas → pretrivialization.is_linear R e
- pretrivialization_at : B → pretrivialization F bundle.total_space.proj
- mem_base_pretrivialization_at : ∀ (x : B), x ∈ (self.pretrivialization_at x).base_set
- pretrivialization_mem_atlas : ∀ (x : B), self.pretrivialization_at x ∈ self.pretrivialization_atlas
- exists_coord_change : ∀ (e : pretrivialization F bundle.total_space.proj), e ∈ self.pretrivialization_atlas → ∀ (e' : pretrivialization F bundle.total_space.proj), e' ∈ self.pretrivialization_atlas → (∃ (f : B → (F →L[R] F)), continuous_on f (e.base_set ∩ e'.base_set) ∧ ∀ (b : B), b ∈ e.base_set ∩ e'.base_set → ∀ (v : F), ⇑(f b) v = (⇑e' {proj := b, snd := e.symm b v}).snd)
- total_space_mk_inducing : ∀ (b : B), inducing (⇑(self.pretrivialization_at b) ∘ bundle.total_space.mk b)
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_2}
{F : Type u_3}
{E : B → Type u_4}
[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]
[Π (x : B), topological_space (E x)]
(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) :
A randomly chosen coordinate change on a vector_prebundle, given by
the field exists_coord_change.
Equations
- a.coord_change he he' b = classical.some _ b
theorem
vector_prebundle.continuous_on_coord_change
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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]
[Π (x : B), topological_space (E x)]
(a : vector_prebundle R F E)
{e e' : pretrivialization F bundle.total_space.proj}
(he : e ∈ a.pretrivialization_atlas)
(he' : e' ∈ a.pretrivialization_atlas) :
continuous_on (a.coord_change he he') (e.base_set ∩ e'.base_set)
theorem
vector_prebundle.coord_change_apply
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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]
[Π (x : B), topological_space (E x)]
(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) :
theorem
vector_prebundle.mk_coord_change
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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]
[Π (x : B), topological_space (E x)]
(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) :
def
vector_prebundle.to_fiber_prebundle
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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]
[Π (x : B), topological_space (E x)]
(a : vector_prebundle R F E) :
fiber_prebundle F E
Natural identification of vector_prebundle as a fiber_prebundle.
Equations
def
vector_prebundle.total_space_topology
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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]
[Π (x : B), topological_space (E x)]
(a : vector_prebundle R F E) :
Topology on the total space that will make the prebundle into a bundle.
Equations
def
vector_prebundle.trivialization_of_mem_pretrivialization_atlas
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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]
[Π (x : B), topological_space (E x)]
(a : vector_prebundle R F E)
{e : pretrivialization F bundle.total_space.proj}
(he : e ∈ a.pretrivialization_atlas) :
Promotion from a trivialization in the pretrivialization_atlas of a
vector_prebundle to a trivialization.
theorem
vector_prebundle.linear_of_mem_pretrivialization_atlas
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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]
[Π (x : B), topological_space (E x)]
(a : vector_prebundle R F E)
{e : pretrivialization F bundle.total_space.proj}
(he : e ∈ a.pretrivialization_atlas) :
theorem
vector_prebundle.mem_trivialization_at_source
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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]
[Π (x : B), topological_space (E x)]
(a : vector_prebundle R F E)
(b : B)
(x : E b) :
{proj := b, snd := x} ∈ (a.pretrivialization_at b).to_local_equiv.source
@[simp]
theorem
vector_prebundle.total_space_mk_preimage_source
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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]
[Π (x : B), topological_space (E x)]
(a : vector_prebundle R F E)
(b : B) :
@[continuity]
theorem
vector_prebundle.continuous_total_space_mk
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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]
[Π (x : B), topological_space (E x)]
(a : vector_prebundle R F E)
(b : B) :
def
vector_prebundle.to_fiber_bundle
{R : Type u_1}
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[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]
[Π (x : B), topological_space (E x)]
(a : vector_prebundle R F E) :
fiber_bundle 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_2}
{F : Type u_3}
{E : B → Type u_4}
[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]
[Π (x : B), topological_space (E x)]
(a : vector_prebundle R F E) :
vector_bundle 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).
noncomputable
def
continuous_linear_map.in_coordinates
{B : Type u_2}
(F : Type u_3)
(E : B → Type u_4)
[Π (x : B), add_comm_monoid (E x)]
[normed_add_comm_group F]
[topological_space B]
[Π (x : B), topological_space (E x)]
{𝕜₁ : Type u_5}
{𝕜₂ : Type u_6}
[nontrivially_normed_field 𝕜₁]
[nontrivially_normed_field 𝕜₂]
{σ : 𝕜₁ →+* 𝕜₂}
{B' : Type u_7}
[topological_space B']
[normed_space 𝕜₁ F]
[Π (x : B), module 𝕜₁ (E x)]
[topological_space (bundle.total_space F E)]
(F' : Type u_8)
[normed_add_comm_group F']
[normed_space 𝕜₂ F']
(E' : B' → Type u_9)
[Π (x : B'), add_comm_monoid (E' x)]
[Π (x : B'), module 𝕜₂ (E' x)]
[topological_space (bundle.total_space F' E')]
[fiber_bundle F E]
[vector_bundle 𝕜₁ F E]
[Π (x : B'), topological_space (E' x)]
[fiber_bundle F' E']
[vector_bundle 𝕜₂ F' E']
(x₀ x : B)
(y₀ y : B')
(ϕ : E x →SL[σ] E' y) :
When ϕ is a continuous (semi)linear map between the fibers E x and E' y of two vector
bundles E and E', continuous_linear_map.in_coordinates F E F' E' x₀ x y₀ y ϕ is a coordinate
change of this continuous linear map w.r.t. the chart around x₀ and the chart around y₀.
It is defined by composing ϕ with appropriate coordinate changes given by the vector bundles
E and E'.
We use the operations trivialization.continuous_linear_map_at and trivialization.symmL in the
definition, instead of trivialization.continuous_linear_equiv_at, so that
continuous_linear_map.in_coordinates is defined everywhere (but see
continuous_linear_map.in_coordinates_eq).
This is the (second component of the) underlying function of a trivialization of the hom-bundle
(see hom_trivialization_at_apply). However, note that continuous_linear_map.in_coordinates is
defined even when x and y live in different base sets.
Therefore, it is is also convenient when working with the hom-bundle between pulled back bundles.
Equations
- continuous_linear_map.in_coordinates F E F' E' x₀ x y₀ y ϕ = (trivialization.continuous_linear_map_at 𝕜₂ (fiber_bundle.trivialization_at F' E' y₀) y).comp (ϕ.comp (trivialization.symmL 𝕜₁ (fiber_bundle.trivialization_at F E x₀) x))
theorem
continuous_linear_map.in_coordinates_eq
{B : Type u_2}
{F : Type u_3}
(E : B → Type u_4)
[Π (x : B), add_comm_monoid (E x)]
[normed_add_comm_group F]
[topological_space B]
[Π (x : B), topological_space (E x)]
{𝕜₁ : Type u_5}
{𝕜₂ : Type u_6}
[nontrivially_normed_field 𝕜₁]
[nontrivially_normed_field 𝕜₂]
{σ : 𝕜₁ →+* 𝕜₂}
{B' : Type u_7}
[topological_space B']
[normed_space 𝕜₁ F]
[Π (x : B), module 𝕜₁ (E x)]
[topological_space (bundle.total_space F E)]
{F' : Type u_8}
[normed_add_comm_group F']
[normed_space 𝕜₂ F']
(E' : B' → Type u_9)
[Π (x : B'), add_comm_monoid (E' x)]
[Π (x : B'), module 𝕜₂ (E' x)]
[topological_space (bundle.total_space F' E')]
[fiber_bundle F E]
[vector_bundle 𝕜₁ F E]
[Π (x : B'), topological_space (E' x)]
[fiber_bundle F' E']
[vector_bundle 𝕜₂ F' E']
(x₀ x : B)
(y₀ y : B')
(ϕ : E x →SL[σ] E' y)
(hx : x ∈ (fiber_bundle.trivialization_at F E x₀).base_set)
(hy : y ∈ (fiber_bundle.trivialization_at F' E' y₀).base_set) :
continuous_linear_map.in_coordinates F E F' E' x₀ x y₀ y ϕ = ↑(trivialization.continuous_linear_equiv_at 𝕜₂ (fiber_bundle.trivialization_at F' E' y₀) y hy).comp (ϕ.comp ↑((trivialization.continuous_linear_equiv_at 𝕜₁ (fiber_bundle.trivialization_at F E x₀) x hx).symm))
rewrite in_coordinates using continuous linear equivalences.
@[protected]
theorem
continuous_linear_map.vector_bundle_core.in_coordinates_eq
{B : Type u_2}
{F : Type u_3}
[normed_add_comm_group F]
[topological_space B]
{𝕜₁ : Type u_5}
{𝕜₂ : Type u_6}
[nontrivially_normed_field 𝕜₁]
[nontrivially_normed_field 𝕜₂]
{σ : 𝕜₁ →+* 𝕜₂}
{B' : Type u_7}
[topological_space B']
[normed_space 𝕜₁ F]
{F' : Type u_8}
[normed_add_comm_group F']
[normed_space 𝕜₂ F']
{ι : Type u_1}
{ι' : Type u_4}
(Z : vector_bundle_core 𝕜₁ B F ι)
(Z' : vector_bundle_core 𝕜₂ B' F' ι')
{x₀ x : B}
{y₀ y : B'}
(ϕ : F →SL[σ] F')
(hx : x ∈ Z.base_set (Z.index_at x₀))
(hy : y ∈ Z'.base_set (Z'.index_at y₀)) :
continuous_linear_map.in_coordinates F Z.fiber F' Z'.fiber x₀ x y₀ y ϕ = (Z'.coord_change (Z'.index_at y) (Z'.index_at y₀) y).comp (ϕ.comp (Z.coord_change (Z.index_at x₀) (Z.index_at x) x))
rewrite in_coordinates in a vector_bundle_core.