English
The pullback along a map f of a vector bundle yields another vector bundle: if E is a vector bundle over B, then the pullback f* E is a vector bundle over B'.
Русский
Тягоделение вдоль отображения f векторного расслоения даёт другое векторное расслоение: если E над B является векторным расслоением, то f* E над B' — это векторное расслоение.
LaTeX
$$$ (f^* E) \\text{ is a vector bundle over } B' \\text{ if } E \\text{ is a vector bundle over } B$$$
Lean4
instance pullback [∀ x, TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] (f : K) :
VectorBundle 𝕜 F ((f : B' → B) *ᵖ E)
where
trivialization_linear' := by
rintro _ ⟨e, he, rfl⟩
infer_instance
continuousOn_coordChange' := by
rintro _ _ ⟨e, he, rfl⟩ ⟨e', he', rfl⟩
refine ((continuousOn_coordChange 𝕜 e e').comp (map_continuous f).continuousOn 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]
