Scalar restriction and linearity upgrades of topological vector bundles #
Along a normed field extension 𝕜' ⊆ 𝕜, scalar restriction (G →L[𝕜] G) → (G →L[𝕜'] G) is an
isometry. Consequently, any VectorBundle 𝕜 G W restricts to a VectorBundle 𝕜' G W sharing the
exact same total-space topology and trivialization atlas (VectorBundle.restrictScalars), and
conversely any VectorBundle 𝕜' G W whose atlas trivializations are 𝕜-linear upgrades to a
VectorBundle 𝕜 G W (VectorBundle.ofLinear).
theorem
VectorBundle.restrictScalars
{B : Type u_1}
[TopologicalSpace B]
(𝕜' : Type u_2)
(𝕜 : Type u_3)
[NontriviallyNormedField 𝕜']
[NontriviallyNormedField 𝕜]
[NormedAlgebra 𝕜' 𝕜]
(G : Type u_4)
[NormedAddCommGroup G]
[NormedSpace 𝕜' G]
[NormedSpace 𝕜 G]
[IsScalarTower 𝕜' 𝕜 G]
(W : B → Type u_5)
[(x : B) → AddCommMonoid (W x)]
[(x : B) → Module 𝕜' (W x)]
[(x : B) → Module 𝕜 (W x)]
[TopologicalSpace (Bundle.TotalSpace G W)]
[(x : B) → TopologicalSpace (W x)]
[FiberBundle G W]
[∀ (x : B), IsScalarTower 𝕜' 𝕜 (W x)]
[VectorBundle 𝕜 G W]
:
VectorBundle 𝕜' G W
Restrict a VectorBundle 𝕜 G W to a VectorBundle 𝕜' G W along a normed field extension
𝕜' ⊆ 𝕜, keeping the exact same total-space topology and trivialization atlas.
theorem
VectorBundle.ofLinear
{B : Type u_1}
[TopologicalSpace B]
(𝕜' : Type u_2)
(𝕜 : Type u_3)
[NontriviallyNormedField 𝕜']
[NontriviallyNormedField 𝕜]
[NormedAlgebra 𝕜' 𝕜]
(G : Type u_4)
[NormedAddCommGroup G]
[NormedSpace 𝕜' G]
[NormedSpace 𝕜 G]
[IsScalarTower 𝕜' 𝕜 G]
(W : B → Type u_5)
[(x : B) → AddCommMonoid (W x)]
[(x : B) → Module 𝕜' (W x)]
[(x : B) → Module 𝕜 (W x)]
[TopologicalSpace (Bundle.TotalSpace G W)]
[(x : B) → TopologicalSpace (W x)]
[FiberBundle G W]
[VectorBundle 𝕜' G W]
(hlin :
∀ (e : Bundle.Trivialization G Bundle.TotalSpace.proj), MemTrivializationAtlas e → Bundle.Trivialization.IsLinear 𝕜 e)
:
VectorBundle 𝕜 G W
Upgrade a VectorBundle 𝕜' G W to VectorBundle 𝕜 G W along a normed field extension
𝕜' ⊆ 𝕜 once every trivialization in the atlas is 𝕜-linear.