Pullbacks of smooth vector bundles #

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

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

Main definitions #

smooth_vector_bundle.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.

@[protected, instance]

def smooth_vector_bundle.pullback {𝕜 : Type u_1} {B : Type u_2} {B' : Type u_3} (F : Type u_5) (E : B → Type u_6) [nontrivially_normed_field 𝕜] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module 𝕜 (E x)] [normed_add_comm_group F] [normed_space 𝕜 F] [topological_space (bundle.total_space F E)] [Π (x : B), topological_space (E x)] {EB : Type u_7} [normed_add_comm_group EB] [normed_space 𝕜 EB] {HB : Type u_8} [topological_space HB] (IB : model_with_corners 𝕜 EB HB) [topological_space B] [charted_space HB B] [smooth_manifold_with_corners IB B] {EB' : Type u_9} [normed_add_comm_group EB'] [normed_space 𝕜 EB'] {HB' : Type u_10} [topological_space HB'] (IB' : model_with_corners 𝕜 EB' HB') [topological_space B'] [charted_space HB' B'] [smooth_manifold_with_corners IB' B'] [fiber_bundle F E] [vector_bundle 𝕜 F E] [smooth_vector_bundle F E IB] (f : smooth_map IB' IB B' B) :

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.