English
For a C^n vector bundle E over B and a C^n map f: B' → B, the pullback bundle f*E is a C^n vector bundle.
Русский
Для векторного расслоения E над B и карты f: B' → B, гладкого класса C^n, тягі вытягивания f*E является C^n векторным расслоением.
LaTeX
$$$\\text{Pullback of ContMDiffVectorBundle: } f^*E \\text{ is a } ContMDiffVectorBundle\\, n\\, F\\, E \\text{ over } B'.$$$
Lean4
/-- 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 pullback : ContMDiffVectorBundle n F (f *ᵖ E) IB' where
contMDiffOn_coordChangeL := by
rintro _ _ ⟨e, he, rfl⟩ ⟨e', he', rfl⟩
refine ((contMDiffOn_coordChangeL e e').comp f.contMDiff.contMDiffOn fun b hb => hb).congr ?_
rintro b (hb : f b ∈ e.baseSet ∩ e'.baseSet); ext v
change ((e.pullback f).coordChangeL 𝕜 (e'.pullback f) b) v = (e.coordChangeL 𝕜 e' (f b)) v
rw [e.coordChangeL_apply e' hb, (e.pullback f).coordChangeL_apply' _]
exacts [rfl, hb]
