Standard constructions on vector bundles #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains several standard constructions on vector bundles:

bundle.trivial.vector_bundle 𝕜 B F: the trivial vector bundle with scalar field 𝕜 and model fiber F over the base B
vector_bundle.prod: for vector bundles E₁ and E₂ with scalar field 𝕜 over a common base, a vector bundle structure on their direct sum E₁ ×ᵇ E₂ (the notation stands for λ x, E₁ x × E₂ x).
vector_bundle.pullback: for a vector bundle E over B, a vector bundle structure on its pullback f *ᵖ E by a map f : B' → B (the notation is a type synonym for E ∘ 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] :

trivialization.is_linear 𝕜 (bundle.trivial.trivialization B F)

source

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) :

trivialization.coord_changeL 𝕜 (bundle.trivial.trivialization B F) (bundle.trivial.trivialization B F) b = continuous_linear_equiv.refl 𝕜 F

source

@[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 #

source

@[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₂)

source

@[simp]

theorem trivialization.coord_changeL_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)] (e₁ e₁' : trivialization F₁ bundle.total_space.proj) (e₂ e₂' : trivialization F₂ bundle.total_space.proj) [trivialization.is_linear 𝕜 e₁] [trivialization.is_linear 𝕜 e₁'] [trivialization.is_linear 𝕜 e₂] [trivialization.is_linear 𝕜 e₂'] ⦃b : B⦄ (hb : b ∈ (e₁.prod e₂).base_set ∩ (e₁'.prod e₂').base_set) :

↑(trivialization.coord_changeL 𝕜 (e₁.prod e₂) (e₁'.prod e₂') b) = ↑(trivialization.coord_changeL 𝕜 e₁ e₁' b).prod_map ↑(trivialization.coord_changeL 𝕜 e₂ e₂' b)

source

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₂)

source

@[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.

source

@[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 #

source

@[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)

source

@[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') :

module R ((f *ᵖ E) x)

Equations

bundle.pullback.module R E f = λ (x : B'), _inst_3 (f x)

source

@[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)

source

@[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)