Pullbacks of smooth vector bundles

This file defines pullbacks of smooth vector bundles over a smooth manifold.

Main definitions

• SmoothVectorBundle.pullback: For a smooth vector bundle E over a manifold B and a smooth map f : B' → B, the pullback vector bundle f *ᵖ E is a smooth vector bundle.

instance SmoothVectorBundle.pullback {𝕜 : Type u_1} {B : Type u_2} {B' : Type u_3} (F : Type u_5) (E : B → Type u_6) [NontriviallyNormedField 𝕜] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] {EB' : Type u_9} [NormedAddCommGroup EB'] [NormedSpace 𝕜 EB'] {HB' : Type u_10} [TopologicalSpace HB'] (IB' : ModelWithCorners 𝕜 EB' HB') [TopologicalSpace B'] [ChartedSpace HB' B'] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] (f : SmoothMap IB' IB B' B) : SmoothVectorBundle F (⇑f *ᵖ E) IB'

For a smooth vector bundle E over a manifold B and a smooth map f : B' → B, the pullback vector bundle f *ᵖ E is a smooth vector bundle.

Equations

• (_ : SmoothVectorBundle F (⇑f *ᵖ E) IB') = (_ : SmoothVectorBundle F (⇑f *ᵖ E) IB')