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 bundleEover a manifoldBand a smooth mapf : B' โ B, the pullback vector bundlef *แต Eis 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) :
smooth_vector_bundle 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.
