Standard constructions on vector bundles #
This file contains several standard constructions on vector bundles:
-
bundle.trivial.vector_bundle 𝕜 B F
: the trivial vector bundle with scalar field𝕜
and model fibreF
over the baseB
-
vector_bundle.prod
: for vector bundlesE₁
andE₂
with scalar field𝕜
over a common base, a vector bundle structure on their direct sumE₁ ×ᵇ E₂
(the notation stands forλ x, E₁ x × E₂ x
). -
vector_bundle.pullback
: for a vector bundleE
overB
, a vector bundle structure on its pullbackf *ᵖ E
by a mapf : B' → B
(the notation is a type synonym forE ∘ f
).
Tags #
Vector bundle, direct sum, pullback
The trivial vector bundle #
@[protected, instance]
def
bundle.trivial.trivialization.is_linear
(𝕜 : Type u_1)
(B : Type u_2)
(F : Type u_3)
[nontrivially_normed_field 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
[topological_space B] :
theorem
bundle.trivial.trivialization.coord_changeL
{𝕜 : Type u_1}
(B : Type u_2)
(F : Type u_3)
[nontrivially_normed_field 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
[topological_space B]
(b : B) :
@[protected, instance]
def
bundle.trivial.vector_bundle
(𝕜 : Type u_1)
(B : Type u_2)
(F : Type u_3)
[nontrivially_normed_field 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
[topological_space B] :
vector_bundle 𝕜 F (bundle.trivial B F)
Direct sum of two vector bundles #
@[protected, instance]
def
trivialization.prod.is_linear
(𝕜 : Type u_1)
{B : Type u_2}
[nontrivially_normed_field 𝕜]
[topological_space B]
{F₁ : Type u_3}
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
{E₁ : B → Type u_4}
[topological_space (bundle.total_space E₁)]
{F₂ : Type u_5}
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
{E₂ : B → Type u_6}
[topological_space (bundle.total_space E₂)]
[Π (x : B), add_comm_monoid (E₁ x)]
[Π (x : B), module 𝕜 (E₁ x)]
[Π (x : B), add_comm_monoid (E₂ x)]
[Π (x : B), module 𝕜 (E₂ x)]
(e₁ : trivialization F₁ bundle.total_space.proj)
(e₂ : trivialization F₂ bundle.total_space.proj)
[trivialization.is_linear 𝕜 e₁]
[trivialization.is_linear 𝕜 e₂] :
trivialization.is_linear 𝕜 (e₁.prod e₂)
theorem
trivialization.prod_apply
(𝕜 : Type u_1)
{B : Type u_2}
[nontrivially_normed_field 𝕜]
[topological_space B]
{F₁ : Type u_3}
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
{E₁ : B → Type u_4}
[topological_space (bundle.total_space E₁)]
{F₂ : Type u_5}
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
{E₂ : B → Type u_6}
[topological_space (bundle.total_space E₂)]
[Π (x : B), add_comm_monoid (E₁ x)]
[Π (x : B), module 𝕜 (E₁ x)]
[Π (x : B), add_comm_monoid (E₂ x)]
[Π (x : B), module 𝕜 (E₂ x)]
{e₁ : trivialization F₁ bundle.total_space.proj}
{e₂ : trivialization F₂ bundle.total_space.proj}
[Π (x : B), topological_space (E₁ x)]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₁ E₁]
[fiber_bundle F₂ E₂]
[trivialization.is_linear 𝕜 e₁]
[trivialization.is_linear 𝕜 e₂]
{x : B}
(hx₁ : x ∈ e₁.base_set)
(hx₂ : x ∈ e₂.base_set)
(v₁ : E₁ x)
(v₂ : E₂ x) :
⇑(e₁.prod e₂) ⟨x, (v₁, v₂)⟩ = (x, ⇑(trivialization.continuous_linear_equiv_at 𝕜 e₁ x hx₁) v₁, ⇑(trivialization.continuous_linear_equiv_at 𝕜 e₂ x hx₂) v₂)
@[protected, instance]
def
vector_bundle.prod
(𝕜 : Type u_1)
{B : Type u_2}
[nontrivially_normed_field 𝕜]
[topological_space B]
(F₁ : Type u_3)
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
(E₁ : B → Type u_4)
[topological_space (bundle.total_space E₁)]
(F₂ : Type u_5)
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
(E₂ : B → Type u_6)
[topological_space (bundle.total_space E₂)]
[Π (x : B), add_comm_monoid (E₁ x)]
[Π (x : B), module 𝕜 (E₁ x)]
[Π (x : B), add_comm_monoid (E₂ x)]
[Π (x : B), module 𝕜 (E₂ x)]
[Π (x : B), topological_space (E₁ x)]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₁ E₁]
[fiber_bundle F₂ E₂]
[vector_bundle 𝕜 F₁ E₁]
[vector_bundle 𝕜 F₂ E₂] :
vector_bundle 𝕜 (F₁ × F₂) (λ (x : B), E₁ x × E₂ x)
The product of two vector bundles is a vector bundle.
@[simp]
theorem
trivialization.continuous_linear_equiv_at_prod
{𝕜 : Type u_1}
{B : Type u_2}
[nontrivially_normed_field 𝕜]
[topological_space B]
{F₁ : Type u_3}
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
{E₁ : B → Type u_4}
[topological_space (bundle.total_space E₁)]
{F₂ : Type u_5}
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
{E₂ : B → Type u_6}
[topological_space (bundle.total_space E₂)]
[Π (x : B), add_comm_monoid (E₁ x)]
[Π (x : B), module 𝕜 (E₁ x)]
[Π (x : B), add_comm_monoid (E₂ x)]
[Π (x : B), module 𝕜 (E₂ x)]
[Π (x : B), topological_space (E₁ x)]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₁ E₁]
[fiber_bundle F₂ E₂]
{e₁ : trivialization F₁ bundle.total_space.proj}
{e₂ : trivialization F₂ bundle.total_space.proj}
[trivialization.is_linear 𝕜 e₁]
[trivialization.is_linear 𝕜 e₂]
{x : B}
(hx₁ : x ∈ e₁.base_set)
(hx₂ : x ∈ e₂.base_set) :
trivialization.continuous_linear_equiv_at 𝕜 (e₁.prod e₂) x _ = (trivialization.continuous_linear_equiv_at 𝕜 e₁ x hx₁).prod (trivialization.continuous_linear_equiv_at 𝕜 e₂ x hx₂)
Pullbacks of vector bundles #
@[protected, instance]
def
bundle.pullback.add_comm_monoid
{B : Type u_3}
(E : B → Type u_5)
{B' : Type u_6}
(f : B' → B)
[Π (x : B), add_comm_monoid (E x)]
(x : B') :
add_comm_monoid ((f *ᵖ E) x)
Equations
- bundle.pullback.add_comm_monoid E f = λ (x : B'), _inst_1 (f x)
@[protected, instance]
def
bundle.pullback.module
(R : Type u_1)
{B : Type u_3}
(E : B → Type u_5)
{B' : Type u_6}
(f : B' → B)
[semiring R]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module R (E x)]
(x : B') :
Equations
- bundle.pullback.module R E f = λ (x : B'), _inst_3 (f x)
@[protected, instance]
def
trivialization.pullback_linear
(𝕜 : Type u_2)
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
{B' : Type u_6}
[topological_space B']
[topological_space (bundle.total_space E)]
[nontrivially_normed_field 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
[topological_space B]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module 𝕜 (E x)]
{K : Type u_7}
[continuous_map_class K B' B]
(e : trivialization F bundle.total_space.proj)
[trivialization.is_linear 𝕜 e]
(f : K) :
trivialization.is_linear 𝕜 (e.pullback f)
@[protected, instance]
def
vector_bundle.pullback
(𝕜 : Type u_2)
{B : Type u_3}
{F : Type u_4}
{E : B → Type u_5}
{B' : Type u_6}
[topological_space B']
[topological_space (bundle.total_space E)]
[nontrivially_normed_field 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
[topological_space B]
[Π (x : B), add_comm_monoid (E x)]
[Π (x : B), module 𝕜 (E x)]
{K : Type u_7}
[continuous_map_class K B' B]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
[vector_bundle 𝕜 F E]
(f : K) :
vector_bundle 𝕜 F (⇑f *ᵖ E)