Vector bundles #
In this file we define (topological) vector bundles.
Let B be the base space, let F be a normed space over a normed field R, and let
E : B → Type* be a fiber_bundle with fiber F, in which, for each x, the fiber E x is a
topological vector space over R.
To have a vector bundle structure on bundle.total_space E, one should additionally have the
following properties:
- 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.
Implementation notes #
The implementation choices in the vector bundle definition are discussed in the "Implementation
notes" section of topology.fiber_bundle.basic.
Tags #
Vector bundle
@[class]
structure
pretrivialization.is_linear
(R : Type u_1)
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : pretrivialization F bundle.total_space.proj) :
Prop
- linear : ∀ (b : B), b ∈ e.base_set → is_linear_map R (λ (x : E b), (⇑e (bundle.total_space_mk b x)).snd)
A mixin class for pretrivialization, stating that a pretrivialization is fiberwise linear with
respect to given module structures on its fibers and the model fiber.
Instances of this typeclass
theorem
pretrivialization.linear
(R : Type u_1)
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
(e : pretrivialization F bundle.total_space.proj)
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[pretrivialization.is_linear R e]
{b : B}
(hb : b ∈ e.base_set) :
is_linear_map R (λ (x : E b), (⇑e (bundle.total_space_mk b x)).snd)
@[protected]
noncomputable
def
pretrivialization.symmₗ
(R : Type u_1)
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : pretrivialization F bundle.total_space.proj)
[pretrivialization.is_linear R e]
(b : B) :
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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : pretrivialization F bundle.total_space.proj)
[pretrivialization.is_linear R e]
(b : B)
(y : F) :
⇑(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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : pretrivialization F bundle.total_space.proj)
[pretrivialization.is_linear R e]
(b : B)
(hb : b ∈ e.base_set) :
⇑((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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : pretrivialization F bundle.total_space.proj)
[pretrivialization.is_linear R e]
(b : B)
(hb : b ∈ e.base_set) :
⇑(pretrivialization.linear_equiv_at R e b hb) = λ (y : E b), (⇑e (bundle.total_space_mk b y)).snd
noncomputable
def
pretrivialization.linear_equiv_at
(R : Type u_1)
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : pretrivialization F bundle.total_space.proj)
[pretrivialization.is_linear R e]
(b : B)
(hb : b ∈ e.base_set) :
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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : pretrivialization F bundle.total_space.proj)
[pretrivialization.is_linear R e]
(b : B) :
A fiberwise linear map equal to e on e.base_set.
theorem
pretrivialization.coe_linear_map_at
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : pretrivialization F bundle.total_space.proj)
[pretrivialization.is_linear R e]
(b : B) :
⇑(pretrivialization.linear_map_at R e b) = λ (y : E b), ite (b ∈ e.base_set) (⇑e (bundle.total_space_mk b y)).snd 0
theorem
pretrivialization.coe_linear_map_at_of_mem
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : pretrivialization F bundle.total_space.proj)
[pretrivialization.is_linear R e]
{b : B}
(hb : b ∈ e.base_set) :
⇑(pretrivialization.linear_map_at R e b) = λ (y : E b), (⇑e (bundle.total_space_mk b y)).snd
theorem
pretrivialization.linear_map_at_apply
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : pretrivialization F bundle.total_space.proj)
[pretrivialization.is_linear R e]
{b : B}
(y : E b) :
⇑(pretrivialization.linear_map_at R e b) y = ite (b ∈ e.base_set) (⇑e (bundle.total_space_mk b y)).snd 0
theorem
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]
[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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : pretrivialization F bundle.total_space.proj)
[pretrivialization.is_linear R e]
{b : B}
(hb : b ∉ e.base_set) :
pretrivialization.linear_map_at R e b = 0
theorem
pretrivialization.linear_map_at_eq_zero
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : pretrivialization F bundle.total_space.proj)
[pretrivialization.is_linear R e]
{b : B}
(hb : b ∉ e.base_set) :
pretrivialization.linear_map_at R e b = 0
theorem
pretrivialization.symmₗ_linear_map_at
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : pretrivialization F bundle.total_space.proj)
[pretrivialization.is_linear R e]
{b : B}
(hb : b ∈ e.base_set)
(y : E b) :
⇑(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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : pretrivialization F bundle.total_space.proj)
[pretrivialization.is_linear R e]
{b : B}
(hb : b ∈ e.base_set)
(y : F) :
⇑(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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : trivialization F bundle.total_space.proj) :
Prop
- linear : ∀ (b : B), b ∈ e.base_set → is_linear_map R (λ (x : E b), (⇑e (bundle.total_space_mk b x)).snd)
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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
(e : trivialization F bundle.total_space.proj)
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[trivialization.is_linear R e]
{b : B}
(hb : b ∈ e.base_set) :
is_linear_map R (λ (y : E b), (⇑e (bundle.total_space_mk b y)).snd)
@[protected, instance]
def
trivialization.to_pretrivialization.is_linear
(R : Type u_1)
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
(e : trivialization F bundle.total_space.proj)
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[trivialization.is_linear R e] :
noncomputable
def
trivialization.linear_equiv_at
(R : Type u_1)
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
(b : B)
(hb : b ∈ e.base_set) :
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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
(b : B)
(hb : b ∈ e.base_set)
(v : E b) :
⇑(trivialization.linear_equiv_at R e b hb) v = (⇑e (bundle.total_space_mk b v)).snd
@[simp]
theorem
trivialization.linear_equiv_at_symm_apply
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
(b : B)
(hb : b ∈ e.base_set)
(v : F) :
⇑((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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
(b : B) :
A fiberwise linear inverse to e.
Equations
theorem
trivialization.coe_symmₗ
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
(b : B) :
⇑(trivialization.symmₗ R e b) = e.symm b
@[protected]
noncomputable
def
trivialization.linear_map_at
(R : Type u_1)
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
(b : B) :
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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
(b : B) :
⇑(trivialization.linear_map_at R e b) = λ (y : E b), ite (b ∈ e.base_set) (⇑e (bundle.total_space_mk b y)).snd 0
theorem
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]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
{b : B}
(hb : b ∈ e.base_set) :
⇑(trivialization.linear_map_at R e b) = λ (y : E b), (⇑e (bundle.total_space_mk b y)).snd
theorem
trivialization.linear_map_at_apply
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
{b : B}
(y : E b) :
⇑(trivialization.linear_map_at R e b) y = ite (b ∈ e.base_set) (⇑e (bundle.total_space_mk b y)).snd 0
theorem
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]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
{b : B}
(hb : b ∈ e.base_set) :
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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
{b : B}
(hb : b ∉ e.base_set) :
trivialization.linear_map_at R e b = 0
theorem
trivialization.symmₗ_linear_map_at
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
{b : B}
(hb : b ∈ e.base_set)
(y : E b) :
⇑(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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
{b : B}
(hb : b ∈ e.base_set)
(y : 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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e e' : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
[trivialization.is_linear R e']
(b : B) :
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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e e' : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
[trivialization.is_linear R e']
{b : B}
(hb : b ∈ e.base_set ∩ e'.base_set) :
⇑(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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e e' : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
[trivialization.is_linear R e']
{b : B}
(hb : b ∈ e.base_set ∩ e'.base_set) :
(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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e e' : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
[trivialization.is_linear R e']
{b : B}
(hb : b ∈ e'.base_set ∩ e.base_set) :
(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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e e' : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
[trivialization.is_linear R e']
{b : B}
(hb : b ∈ e.base_set ∩ e'.base_set)
(y : F) :
⇑(trivialization.coord_changeL R e e' b) y = (⇑e' (bundle.total_space_mk b (e.symm b y))).snd
theorem
trivialization.mk_coord_changeL
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e e' : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
[trivialization.is_linear R e']
{b : B}
(hb : b ∈ e.base_set ∩ e'.base_set)
(y : F) :
(b, ⇑(trivialization.coord_changeL R e e' b) y) = ⇑e' (bundle.total_space_mk b (e.symm b y))
theorem
trivialization.apply_symm_apply_eq_coord_changeL
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e e' : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
[trivialization.is_linear R e']
{b : B}
(hb : b ∈ e.base_set ∩ e'.base_set)
(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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e e' : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
[trivialization.is_linear R e']
{b : B}
(hb : b ∈ e.base_set ∩ e'.base_set)
(y : F) :
⇑(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_3}
{F : Type u_4}
{E : B → Type u_5}
[semiring R]
[topological_space F]
[topological_space B]
[topological_space (bundle.total_space E)]
[add_comm_monoid F]
[module R F]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(e e' : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
[trivialization.is_linear R e']
{b : B}
(hb : b ∈ e.base_set ∩ e'.base_set) :
⇑((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_3}
(E : B → Type u_5)
[Π (x : B), has_zero (E x)] :
B → bundle.total_space E
The zero section of a vector bundle
Equations
- bundle.zero_section E = λ (x : B), bundle.total_space_mk x 0
@[simp]
theorem
bundle.zero_section_proj
{B : Type u_3}
(E : B → Type u_5)
[Π (x : B), has_zero (E x)]
(x : B) :
(bundle.zero_section E x).proj = x
@[simp]
theorem
bundle.zero_section_snd
{B : Type u_3}
(E : B → Type u_5)
[Π (x : B), has_zero (E x)]
(x : B) :
(bundle.zero_section E x).snd = 0
@[class]
structure
vector_bundle
(R : Type u_1)
{B : Type u_3}
(F : Type u_4)
(E : B → Type u_5)
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
[topological_space (bundle.total_space E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E] :
Prop
- 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 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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
[topological_space (bundle.total_space E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
[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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
[topological_space (bundle.total_space E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
[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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
[topological_space (bundle.total_space E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
(b : B) :
⇑(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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
[topological_space (bundle.total_space E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
(b : B) :
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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
[topological_space (bundle.total_space E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
(b : B) :
⇑(trivialization.symmL R e b) = e.symm b
noncomputable
def
trivialization.symmL
(R : Type u_1)
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
[topological_space (bundle.total_space E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
(b : B) :
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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
[topological_space (bundle.total_space E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
{b : B}
(hb : b ∈ e.base_set)
(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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
[topological_space (bundle.total_space E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
{b : B}
(hb : b ∈ e.base_set)
(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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
[topological_space (bundle.total_space E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
(b : B)
(hb : b ∈ e.base_set) :
⇑((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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
[topological_space (bundle.total_space E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
(b : B)
(hb : b ∈ e.base_set) :
⇑(trivialization.continuous_linear_equiv_at R e b hb) = λ (y : E b), (⇑e (bundle.total_space_mk b y)).snd
noncomputable
def
trivialization.continuous_linear_equiv_at
(R : Type u_1)
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
[topological_space (bundle.total_space E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
(b : B)
(hb : b ∈ e.base_set) :
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 (bundle.total_space_mk b 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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
[topological_space (bundle.total_space E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
{b : B}
(hb : b ∈ e.base_set) :
⇑(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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
[topological_space (bundle.total_space E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
{b : B}
(hb : b ∈ e.base_set) :
⇑((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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
[topological_space (bundle.total_space E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
(x : bundle.total_space 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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
[topological_space (bundle.total_space E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
(b : B)
(hb : b ∈ e.base_set)
(z : E b) :
⇑e ⟨b, z⟩ = (b, ⇑(trivialization.continuous_linear_equiv_at R e b hb) z)
@[protected]
theorem
trivialization.zero_section
(R : Type u_1)
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
[topological_space (bundle.total_space E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
{x : B}
(hx : x ∈ e.base_set) :
⇑e (bundle.zero_section E x) = (x, 0)
theorem
trivialization.symm_apply_eq_mk_continuous_linear_equiv_at_symm
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
[topological_space (bundle.total_space E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear R e]
(b : B)
(hb : b ∈ e.base_set)
(z : F) :
⇑(e.to_local_homeomorph.symm) (b, z) = bundle.total_space_mk b (⇑((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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
[topological_space (bundle.total_space E)]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
(e 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_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)
- 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_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 ι] :
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_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 ι] :
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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι) :
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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι) :
@[simp]
theorem
vector_bundle_core.to_fiber_bundle_core_coord_change
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι) :
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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι) :
@[protected, instance]
def
vector_bundle_core.to_fiber_bundle_core_coe
{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} :
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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(i j k : ι)
(x : B)
(H : x ∈ Z.base_set i ∩ Z.base_set j ∩ Z.base_set k) :
(Z.coord_change j k x).comp (Z.coord_change i j x) = Z.coord_change i k x
@[nolint]
def
vector_bundle_core.index
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι) :
Type u_6
The index set of a vector bundle core, as a convenience function for dot notation
@[nolint, reducible]
def
vector_bundle_core.base
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι) :
Type u_3
The base space of a vector bundle core, as a convenience function for dot notation
@[nolint]
def
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 : 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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(x : B) :
topological_space (Z.fiber x)
Equations
@[protected, instance]
def
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 : 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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(x : B) :
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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
[add_comm_group F]
(x : B) :
add_comm_group (Z.fiber x)
Equations
- Z.add_comm_group_fiber = id (λ (x : B), _inst_10)
@[simp, reducible]
def
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 : vector_bundle_core R B F ι) :
bundle.total_space Z.fiber → B
The projection from the total space of a fiber bundle core, on its base.
Equations
@[nolint, reducible]
def
vector_bundle_core.total_space
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι) :
Type (max u_3 u_4)
The total space of the vector bundle, as a convenience function for dot notation.
It is by definition equal to bundle.total_space Z.fiber, a.k.a. Σ x, Z.fiber x but with a
different name for typeclass inference.
Equations
def
vector_bundle_core.triv_change
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(i j : ι) :
local_homeomorph (B × F) (B × F)
Local homeomorphism version of the trivialization change.
Equations
- 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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(i j : ι)
(p : B × F) :
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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι) :
Topological structure on the total space of a vector bundle created from core, designed so that all the local trivialization are continuous.
Equations
@[simp]
theorem
vector_bundle_core.coe_coord_change
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(b : B)
(i j : ι) :
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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(i : ι) :
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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(i : ι) :
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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(i : ι)
(p : Z.total_space) :
p ∈ (Z.local_triv i).to_local_homeomorph.to_local_equiv.source ↔ p.fst ∈ Z.base_set i
@[simp]
theorem
vector_bundle_core.base_set_at
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(i : ι) :
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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(i : ι)
(p : Z.total_space) :
⇑(Z.local_triv i) p = (p.fst, ⇑(Z.coord_change (Z.index_at p.fst) i p.fst) p.snd)
@[simp]
theorem
vector_bundle_core.mem_local_triv_target
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(i : ι)
(p : B × F) :
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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(i : ι)
(p : B × F) :
⇑((Z.local_triv i).to_local_homeomorph.symm) p = ⟨p.fst, ⇑(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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(i : ι)
{b : B}
(hb : b ∈ Z.base_set i)
(v : F) :
(Z.local_triv i).symm b v = ⇑(Z.coord_change i (Z.index_at b) b) v
@[simp]
theorem
vector_bundle_core.local_triv_coord_change_eq
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(i j : ι)
{b : B}
(hb : b ∈ Z.base_set i ∩ Z.base_set j)
(v : F) :
⇑(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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(b : B) :
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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(b : B) :
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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(b : B)
(a : F) :
⟨b, 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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(p : Z.total_space) :
@[simp]
theorem
vector_bundle_core.local_triv_at_apply_mk
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(b : B)
(a : F) :
⇑(Z.local_triv_at b) ⟨b, a⟩ = (b, a)
@[simp]
theorem
vector_bundle_core.mem_local_triv_at_base_set
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι)
(b : B) :
b ∈ (Z.local_triv_at b).base_set
@[protected, instance]
def
vector_bundle_core.fiber_bundle
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι) :
fiber_bundle F Z.fiber
Equations
@[protected, instance]
def
vector_bundle_core.vector_bundle
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι) :
vector_bundle R F Z.fiber
@[continuity]
theorem
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 : 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_3}
{F : Type u_4}
[nontrivially_normed_field R]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
{ι : Type u_6}
(Z : vector_bundle_core R B F ι) :
The projection on the base of a vector bundle created from core is an open map
Vector prebundle #
@[nolint]
structure
vector_prebundle
(R : Type u_1)
{B : Type u_3}
(F : Type u_4)
(E : B → Type u_5)
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B] :
Type (max u_3 u_4 u_5)
- 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' (bundle.total_space_mk b (e.symm b v))).snd)
This structure permits to define a vector bundle when trivializations are given as local equivalences but there is not yet a topology on the total space or the fibers. The total space is hence given a topology in such a way that there is a fiber bundle structure for which the local equivalences are also local homeomorphisms and hence vector bundle trivializations. The topology on the fibers is induced from the one on the total space.
The field exists_coord_change is stated as an existential statement (instead of 3 separate
fields), since it depends on propositional information (namely e e' ∈ pretrivialization_atlas).
This makes it inconvenient to explicitly define a coord_change function when constructing a
vector_prebundle.
Instances for vector_prebundle
- vector_prebundle.has_sizeof_inst
noncomputable
def
vector_prebundle.coord_change
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
(a : vector_prebundle R F E)
{e e' : pretrivialization F bundle.total_space.proj}
(he : e ∈ a.pretrivialization_atlas)
(he' : e' ∈ a.pretrivialization_atlas)
(b : B) :
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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
(a : vector_prebundle R F E)
{e e' : pretrivialization F bundle.total_space.proj}
(he : e ∈ a.pretrivialization_atlas)
(he' : e' ∈ a.pretrivialization_atlas) :
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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
(a : vector_prebundle R F E)
{e e' : pretrivialization F bundle.total_space.proj}
(he : e ∈ a.pretrivialization_atlas)
(he' : e' ∈ a.pretrivialization_atlas)
{b : B}
(hb : b ∈ e.base_set ∩ e'.base_set)
(v : F) :
⇑(a.coord_change he he' b) v = (⇑e' (bundle.total_space_mk b (e.symm b v))).snd
theorem
vector_prebundle.mk_coord_change
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
(a : vector_prebundle R F E)
{e e' : pretrivialization F bundle.total_space.proj}
(he : e ∈ a.pretrivialization_atlas)
(he' : e' ∈ a.pretrivialization_atlas)
{b : B}
(hb : b ∈ e.base_set ∩ e'.base_set)
(v : F) :
(b, ⇑(a.coord_change he he' b) v) = ⇑e' (bundle.total_space_mk b (e.symm b v))
def
vector_prebundle.to_fiber_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]
(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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
(a : vector_prebundle R F E) :
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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
(a : vector_prebundle R F E)
{e : 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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
(a : vector_prebundle R F E)
{e : 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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
(a : vector_prebundle R F E)
(b : B)
(x : E b) :
@[simp]
theorem
vector_prebundle.total_space_mk_preimage_source
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
(a : vector_prebundle R F E)
(b : B) :
def
vector_prebundle.fiber_topology
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
(a : vector_prebundle R F E)
(b : B) :
topological_space (E b)
Topology on the fibers E b induced by the map E b → E.total_space.
Equations
@[continuity]
theorem
vector_prebundle.inducing_total_space_mk
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
(a : vector_prebundle R F E)
(b : B) :
@[continuity]
theorem
vector_prebundle.continuous_total_space_mk
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
(a : vector_prebundle R F E)
(b : B) :
def
vector_prebundle.to_fiber_bundle
{R : Type u_1}
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
(a : vector_prebundle R F E) :
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_3}
{F : Type u_4}
{E : B → Type u_5}
[nontrivially_normed_field R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
[normed_add_comm_group F]
[normed_space R F]
[topological_space B]
(a : vector_prebundle R F E) :
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).