Pullbacks of C^n vector bundles

This file defines pullbacks of C^n vector bundles over a manifold.

Main definitions

• ContMDiffVectorBundle.pullback: For a C^n vector bundle E over a manifold B and a C^n map f : B' → B, the pullback vector bundle f *ᵖ E is a C^n vector bundle.

instance ContMDiffVectorBundle.pullback {𝕜 : Type u_1} {B : Type u_2} {B' : Type u_3} (F : Type u_4) (E : B → Type u_5) {n : WithTop ℕ∞} [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_6} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_7} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EB' : Type u_8} [NormedAddCommGroup EB'] [NormedSpace 𝕜 EB'] {HB' : Type u_9} [TopologicalSpace HB'] (IB' : ModelWithCorners 𝕜 EB' HB') [TopologicalSpace B'] [ChartedSpace HB' B'] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] (f : ContMDiffMap IB' IB B' B n) : ContMDiffVectorBundle n F (⇑f *ᵖ E) IB'

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