# 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) [] [NormedSpace ๐ F] [] :
Equations
• โฏ = โฏ
theorem Bundle.Trivial.trivialization.coordChangeL {๐ : Type u_1} (B : Type u_2) (F : Type u_3) [] [NormedSpace ๐ F] [] (b : B) :
=
instance Bundle.Trivial.vectorBundle (๐ : Type u_1) (B : Type u_2) (F : Type u_3) [] [NormedSpace ๐ F] [] :
VectorBundle ๐ F ()
Equations
• โฏ = โฏ

### Direct sum of two vector bundles #

instance Trivialization.prod.isLinear (๐ : Type u_1) {B : Type u_2} [] [] {Fโ : Type u_3} [] [NormedSpace ๐ Fโ] {Eโ : B โ Type u_4} [TopologicalSpace (Bundle.TotalSpace Fโ Eโ)] {Fโ : Type u_5} [] [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)] (eโ : Trivialization Fโ Bundle.TotalSpace.proj) (eโ : Trivialization Fโ Bundle.TotalSpace.proj) [Trivialization.IsLinear ๐ eโ] [Trivialization.IsLinear ๐ eโ] :
Trivialization.IsLinear ๐ (eโ.prod eโ)
Equations
• โฏ = โฏ
@[simp]
theorem Trivialization.coordChangeL_prod (๐ : Type u_1) {B : Type u_2} [] [] {Fโ : Type u_3} [] [NormedSpace ๐ Fโ] {Eโ : B โ Type u_4} [TopologicalSpace (Bundle.TotalSpace Fโ Eโ)] {Fโ : Type u_5} [] [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)] (eโ : Trivialization Fโ Bundle.TotalSpace.proj) (eโ' : Trivialization Fโ Bundle.TotalSpace.proj) (eโ : Trivialization Fโ Bundle.TotalSpace.proj) (eโ' : Trivialization Fโ Bundle.TotalSpace.proj) [Trivialization.IsLinear ๐ eโ] [Trivialization.IsLinear ๐ eโ'] [Trivialization.IsLinear ๐ eโ] [Trivialization.IsLinear ๐ eโ'] โฆb : Bโฆ (hb : b โ (eโ.prod eโ).baseSet โฉ (eโ'.prod eโ').baseSet) :
โ(Trivialization.coordChangeL ๐ (eโ.prod eโ) (eโ'.prod eโ') b) = (โ(Trivialization.coordChangeL ๐ eโ eโ' b)).prodMap โ(Trivialization.coordChangeL ๐ eโ eโ' b)
theorem Trivialization.prod_apply (๐ : Type u_1) {B : Type u_2} [] [] {Fโ : Type u_3} [] [NormedSpace ๐ Fโ] {Eโ : B โ Type u_4} [TopologicalSpace (Bundle.TotalSpace Fโ Eโ)] {Fโ : Type u_5} [] [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)] {eโ : Trivialization Fโ Bundle.TotalSpace.proj} {eโ : Trivialization Fโ Bundle.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, (Trivialization.continuousLinearEquivAt ๐ eโ x hxโ) vโ, (Trivialization.continuousLinearEquivAt ๐ eโ x hxโ) vโ)
instance VectorBundle.prod (๐ : Type u_1) {B : Type u_2} [] [] (Fโ : Type u_3) [] [NormedSpace ๐ Fโ] (Eโ : B โ Type u_4) [TopologicalSpace (Bundle.TotalSpace Fโ Eโ)] (Fโ : Type u_5) [] [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.

Equations
• โฏ = โฏ
@[simp]
theorem Trivialization.continuousLinearEquivAt_prod {๐ : Type u_1} {B : Type u_2} [] [] {Fโ : Type u_3} [] [NormedSpace ๐ Fโ] {Eโ : B โ Type u_4} [TopologicalSpace (Bundle.TotalSpace Fโ Eโ)] {Fโ : Type u_5} [] [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โ] {eโ : Trivialization Fโ Bundle.TotalSpace.proj} {eโ : Trivialization Fโ Bundle.TotalSpace.proj} [Trivialization.IsLinear ๐ eโ] [Trivialization.IsLinear ๐ eโ] {x : B} (hx : x โ (eโ.prod eโ).baseSet) :
Trivialization.continuousLinearEquivAt ๐ (eโ.prod eโ) x hx = (Trivialization.continuousLinearEquivAt ๐ eโ x โฏ).prod (Trivialization.continuousLinearEquivAt ๐ eโ x โฏ)

### Pullbacks of vector bundles #

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') :
Equations
• = i (f x)
instance instModulePullback (R : Type u_1) {B : Type u_3} (E : B โ Type u_5) {B' : Type u_6} (f : B' โ B) [] [(x : B) โ AddCommMonoid (E x)] [i : (x : B) โ Module R (E x)] (x : B') :
Module R ((f *แต E) x)
Equations
• = i (f x)
instance Trivialization.pullback_linear (๐ : Type u_2) {B : Type u_3} {F : Type u_4} {E : B โ Type u_5} {B' : Type u_6} [] [] [] [NormedSpace ๐ F] [] [(x : B) โ AddCommMonoid (E x)] [(x : B) โ Module ๐ (E x)] {K : Type u_7} [FunLike K B' B] [] (e : Trivialization F Bundle.TotalSpace.proj) [] (f : K) :
Trivialization.IsLinear ๐ (e.pullback f)
Equations
• โฏ = โฏ
instance VectorBundle.pullback (๐ : Type u_2) {B : Type u_3} {F : Type u_4} {E : B โ Type u_5} {B' : Type u_6} [] [] [] [NormedSpace ๐ F] [] [(x : B) โ AddCommMonoid (E x)] [(x : B) โ Module ๐ (E x)] {K : Type u_7} [FunLike K B' B] [] [(x : B) โ TopologicalSpace (E x)] [] [VectorBundle ๐ F E] (f : K) :
VectorBundle ๐ F (โf *แต E)
Equations
• โฏ = โฏ