Fibrewise scalar multiplication on a topological vector bundle

Scalar multiplication in the fibres of a topological vector bundle E → B is jointly continuous as a map 𝕜 × TotalSpace F E → TotalSpace F E: in a linear trivialization it becomes scalar multiplication in the model fibre F. Consequently a continuous map into the total space, rescaled fibrewise by a continuous scalar function, is again continuous. This is the topological counterpart of ContMDiff.smul_totalSpace, needing no charts on the base, and it supplies, for instance, the straight-line homotopy t • s from the zero section to a section s over an arbitrary topological space.

Conversely, the scalar function is recovered continuously from the two maps: if one map into the total space is a scalar multiple of another, nonzero at a point, and both are continuous there, then so is the scalar (TauCeti.VectorBundle.continuousAt_of_eventually_eq_smul). This is how a reparametrization factor between two vector fields along a curve is shown to be continuous.

theorem TauCeti.VectorBundle.continuous_smul (𝕜 : Type u_1) {B : Type u_2} (F : Type u_3) [NontriviallyNormedField 𝕜] [TopologicalSpace B] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (E : B → Type u_5) [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module 𝕜 (E b)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle 𝕜 F E] : Continuous fun (p : 𝕜 × Bundle.TotalSpace F E) => Bundle.TotalSpace.mk' F p.2.proj (p.1 • p.2.snd)

Fibrewise scalar multiplication on the total space of a topological vector bundle is jointly continuous.

theorem TauCeti.VectorBundle.continuousAt_of_eventually_eq_smul {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {X : Type u_4} [NontriviallyNormedField 𝕜] [TopologicalSpace B] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module 𝕜 (E b)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle 𝕜 F E] [TopologicalSpace X] [SeparatingDual 𝕜 F] {c : X → 𝕜} {φ ψ : X → Bundle.TotalSpace F E} {x₀ : X} (hφ : ContinuousAt φ x₀) (hψ : ContinuousAt ψ x₀) (hψφ : ∀ᶠ (x : X) in nhds x₀, ψ x = Bundle.TotalSpace.mk' F (φ x).proj (c x • (φ x).snd)) (h0 : (φ x₀).snd ≠ 0) : ContinuousAt c x₀

Continuity of a fibrewise scalar factor. Let φ and ψ be maps into the total space of a vector bundle, continuous at x₀, with ψ x = c x • φ x in the fibre over (φ x).proj near x₀. If φ x₀ is a nonzero vector, then the scalar function c is continuous at x₀.

theorem Continuous.smul_totalSpace {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {X : Type u_4} [NontriviallyNormedField 𝕜] [TopologicalSpace B] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module 𝕜 (E b)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle 𝕜 F E] [TopologicalSpace X] {c : X → 𝕜} {φ : X → Bundle.TotalSpace F E} (hc : Continuous c) (hφ : Continuous φ) : Continuous fun (x : X) => Bundle.TotalSpace.mk' F (φ x).proj (c x • (φ x).snd)

A continuous map into the total space of a vector bundle, rescaled fibrewise by a continuous scalar function, is continuous.

theorem Continuous.smul_totalSpace_of_norm_le {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {X : Type u_4} [NontriviallyNormedField 𝕜] [TopologicalSpace B] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module 𝕜 (E b)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle 𝕜 F E] [TopologicalSpace X] {c : X → 𝕜} {φ : X → Bundle.TotalSpace F E} {C : ℝ} (hφ : Continuous φ) (hcC : ∀ (x : X), ‖c x‖ ≤ C) (hc : ∀ (x : X), (φ x).snd ≠ 0 → ContinuousAt c x) : Continuous fun (x : X) => Bundle.TotalSpace.mk' F (φ x).proj (c x • (φ x).snd)

A bounded fibrewise rescaling is continuous. Let φ be a continuous map into the total space of a vector bundle and c a bounded scalar function which is continuous at every point where φ takes a nonzero value. Then φ rescaled fibrewise by c is continuous. No continuity of c is needed at the zeros of φ: there the rescaled vector tends to zero because c is bounded. This covers radial retractions, whose scalar factor jumps where the vector vanishes.