Standard constructions on vector bundles

This file contains several standard constructions on vector bundles:

• Bundle.Trivial.vectorBundle 𝕜 B F: the trivial vector bundle with scalar field 𝕜 and model fiber F over the base B

• VectorBundle.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 fun x ↦ E₁ x × E₂ x).

• VectorBundle.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

instance Bundle.Trivial.trivialization.isLinear (𝕜 : Type u_1) (B : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] : Trivialization.IsLinear 𝕜 (trivialization B F)

theorem Bundle.Trivial.trivialization.coordChangeL {𝕜 : Type u_1} (B : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] (b : B) : Trivialization.coordChangeL 𝕜 (trivialization B F) (trivialization B F) b = ContinuousLinearEquiv.refl 𝕜 F

instance Bundle.Trivial.vectorBundle (𝕜 : Type u_1) (B : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] : VectorBundle 𝕜 F (Trivial B F)

@[simp]

theorem Bundle.Trivial.linearMapAt_trivialization (𝕜 : Type u_1) (B : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] (x : B) : Trivialization.linearMapAt 𝕜 (trivialization B F) x = LinearMap.id

@[simp]

theorem Bundle.Trivial.continuousLinearMapAt_trivialization (𝕜 : Type u_1) (B : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] (x : B) : Trivialization.continuousLinearMapAt 𝕜 (trivialization B F) x = ContinuousLinearMap.id 𝕜 F

@[simp]

theorem Bundle.Trivial.symmₗ_trivialization (𝕜 : Type u_1) (B : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] (x : B) : Trivialization.symmₗ 𝕜 (trivialization B F) x = LinearMap.id

@[simp]

theorem Bundle.Trivial.symmL_trivialization (𝕜 : Type u_1) (B : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] (x : B) : Trivialization.symmL 𝕜 (trivialization B F) x = ContinuousLinearMap.id 𝕜 F

@[simp]

theorem Bundle.Trivial.continuousLinearEquivAt_trivialization (𝕜 : Type u_1) (B : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] (x : B) : Trivialization.continuousLinearEquivAt 𝕜 (trivialization B F) x ⋯ = ContinuousLinearEquiv.refl 𝕜 F

Direct sum of two vector bundles

instance Bundle.Trivialization.prod.isLinear (𝕜 : Type u_1) {B : Type u_2} [NontriviallyNormedField 𝕜] [TopologicalSpace B] {F₁ : Type u_3} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {E₁ : B → Type u_4} [TopologicalSpace (TotalSpace F₁ E₁)] {F₂ : Type u_5} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {E₂ : B → Type u_6} [TopologicalSpace (TotalSpace F₂ E₂)] [(x : B) → AddCommMonoid (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [(x : B) → AddCommMonoid (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] (e₁ : Trivialization F₁ TotalSpace.proj) (e₂ : Trivialization F₂ TotalSpace.proj) [Trivialization.IsLinear 𝕜 e₁] [Trivialization.IsLinear 𝕜 e₂] : Trivialization.IsLinear 𝕜 (e₁.prod e₂)

@[simp]

theorem Bundle.Trivialization.coordChangeL_prod (𝕜 : Type u_1) {B : Type u_2} [NontriviallyNormedField 𝕜] [TopologicalSpace B] {F₁ : Type u_3} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {E₁ : B → Type u_4} [TopologicalSpace (TotalSpace F₁ E₁)] {F₂ : Type u_5} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {E₂ : B → Type u_6} [TopologicalSpace (TotalSpace F₂ E₂)] [(x : B) → AddCommMonoid (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [(x : B) → AddCommMonoid (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] (e₁ e₁' : Trivialization F₁ TotalSpace.proj) (e₂ e₂' : Trivialization F₂ TotalSpace.proj) [Trivialization.IsLinear 𝕜 e₁] [Trivialization.IsLinear 𝕜 e₁'] [Trivialization.IsLinear 𝕜 e₂] [Trivialization.IsLinear 𝕜 e₂'] ⦃b : B⦄ (hb : (b ∈ e₁.baseSet ∧ b ∈ e₂.baseSet) ∧ b ∈ e₁'.baseSet ∧ b ∈ e₂'.baseSet) : ↑(coordChangeL 𝕜 (e₁.prod e₂) (e₁'.prod e₂') b) = (↑(coordChangeL 𝕜 e₁ e₁' b)).prodMap ↑(coordChangeL 𝕜 e₂ e₂' b)

theorem Bundle.Trivialization.prod_apply' (𝕜 : Type u_1) {B : Type u_2} [NontriviallyNormedField 𝕜] [TopologicalSpace B] {F₁ : Type u_3} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {E₁ : B → Type u_4} [TopologicalSpace (TotalSpace F₁ E₁)] {F₂ : Type u_5} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {E₂ : B → Type u_6} [TopologicalSpace (TotalSpace F₂ E₂)] [(x : B) → AddCommMonoid (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [(x : B) → AddCommMonoid (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] {e₁ : Trivialization F₁ TotalSpace.proj} {e₂ : Trivialization F₂ TotalSpace.proj} [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₁ E₁] [FiberBundle F₂ E₂] [Trivialization.IsLinear 𝕜 e₁] [Trivialization.IsLinear 𝕜 e₂] {x : B} (hx₁ : x ∈ e₁.baseSet) (hx₂ : x ∈ e₂.baseSet) (v₁ : E₁ x) (v₂ : E₂ x) : ↑(e₁.prod e₂) { proj := x, snd := (v₁, v₂) } = (x, (continuousLinearEquivAt 𝕜 e₁ x hx₁) v₁, (continuousLinearEquivAt 𝕜 e₂ x hx₂) v₂)

instance VectorBundle.prod (𝕜 : Type u_1) {B : Type u_2} [NontriviallyNormedField 𝕜] [TopologicalSpace B] (F₁ : Type u_3) [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] (E₁ : B → Type u_4) [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] (F₂ : Type u_5) [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] (E₂ : B → Type u_6) [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → AddCommMonoid (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [(x : B) → AddCommMonoid (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₁ E₁] [VectorBundle 𝕜 F₂ E₂] : VectorBundle 𝕜 (F₁ × F₂) fun (x : B) => E₁ x × E₂ x

The product of two vector bundles is a vector bundle.

@[simp]

theorem Bundle.Trivialization.continuousLinearEquivAt_prod {𝕜 : Type u_1} {B : Type u_2} [NontriviallyNormedField 𝕜] [TopologicalSpace B] {F₁ : Type u_3} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {E₁ : B → Type u_4} [TopologicalSpace (TotalSpace F₁ E₁)] {F₂ : Type u_5} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {E₂ : B → Type u_6} [TopologicalSpace (TotalSpace F₂ E₂)] [(x : B) → AddCommMonoid (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [(x : B) → AddCommMonoid (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₁ E₁] [FiberBundle F₂ E₂] {e₁ : Trivialization F₁ TotalSpace.proj} {e₂ : Trivialization F₂ TotalSpace.proj} [Trivialization.IsLinear 𝕜 e₁] [Trivialization.IsLinear 𝕜 e₂] {x : B} (hx : x ∈ (e₁.prod e₂).baseSet) : continuousLinearEquivAt 𝕜 (e₁.prod e₂) x hx = (continuousLinearEquivAt 𝕜 e₁ x ⋯).prodCongr (continuousLinearEquivAt 𝕜 e₂ x ⋯)

Pullbacks of vector bundles

@[instance_reducible]

instance instSMulPullbackOfModule (R : Type u_1) {B : Type u_3} (E : B → Type u_5) {B' : Type u_6} (f : B' → B) [Semiring R] [(x : B) → AddCommMonoid (E x)] [i : (x : B) → Module R (E x)] (x : B') : SMul R ((f *ᵖ E) x)

Equations

• instSMulPullbackOfModule R E f x = instSMulPullbackOfModule._aux_1 R E f x

@[instance_reducible]

instance instAddCommMonoidPullback {B : Type u_3} (E : B → Type u_5) {B' : Type u_6} (f : B' → B) [i : (x : B) → AddCommMonoid (E x)] (x : B') : AddCommMonoid ((f *ᵖ E) x)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance instModulePullback (R : Type u_1) {B : Type u_3} (E : B → Type u_5) {B' : Type u_6} (f : B' → B) [Semiring R] [(x : B) → AddCommMonoid (E x)] [i : (x : B) → Module R (E x)] (x : B') : Module R ((f *ᵖ E) x)

Equations

• instModulePullback R E f x = { toSMul := instSMulPullbackOfModule R E f x, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

instance Bundle.Trivialization.pullback_linear (𝕜 : Type u_2) {B : Type u_3} {F : Type u_4} {E : B → Type u_5} {B' : Type u_6} [TopologicalSpace B'] [TopologicalSpace (TotalSpace F E)] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {K : Type u_7} [FunLike K B' B] [ContinuousMapClass K B' B] (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] (f : K) : Trivialization.IsLinear 𝕜 (e.pullback f)

instance VectorBundle.pullback (𝕜 : Type u_2) {B : Type u_3} {F : Type u_4} {E : B → Type u_5} {B' : Type u_6} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {K : Type u_7} [FunLike K B' B] [ContinuousMapClass K B' B] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] (f : K) : VectorBundle 𝕜 F (⇑f *ᵖ E)