Smooth scalar rescaling of vector bundles #
Multiplying a vector in a bundle by a smooth scalar preserves smoothness even when its base
point varies. A nowhere-zero scalar function on the base therefore defines a diffeomorphism
of the total space, with inverse given by reciprocal multiplication. This construction fixes
the zero section and preserves the projection, without a choice of global trivialization.
More generally, over a 𝕜-charted base, scalar multiplication by 𝕜'-valued maps along a normed
field extension 𝕜 ⊆ 𝕜' preserves C^n regularity and equips C^n sections with compatible
Module 𝕜' and IsScalarTower 𝕜 𝕜' instances (ContMDiffSection.instModuleOfNormedAlgebra);
multiplication by a constant of 𝕜' also preserves differentiability of sections
(MDifferentiableAt.const_smul_section).
For normal bundles, positive rescaling converts unit-radius fibre coordinates to a radius varying over the submanifold. It is the rescaling step in the variable-radius tubular neighbourhood construction of J. M. Lee, Introduction to Smooth Manifolds, second edition, Theorem 6.24.
theorem
ContMDiffWithinAt.smul_totalSpace
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{B : Type u_5}
[TopologicalSpace B]
[ChartedSpace H B]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{V : B → Type u_7}
[(b : B) → AddCommMonoid (V b)]
[(b : B) → Module 𝕜' (V b)]
[(b : B) → TopologicalSpace (V b)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜' F V]
{n : WithTop ℕ∞}
{E' : Type u_8}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_9}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H' M]
{a : M → 𝕜'}
{g : M → Bundle.TotalSpace F V}
{s : Set M}
{x : M}
(ha : ContMDiffWithinAt J (modelWithCornersSelf 𝕜 𝕜') n a s x)
(hg : ContMDiffWithinAt J (I.prod (modelWithCornersSelf 𝕜 F)) n g s x)
:
ContMDiffWithinAt J (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (y : M) => ⟨(g y).proj, a y • (g y).snd⟩) s x
Multiplying a bundle-valued map by a scalar-valued map preserves C^n regularity within
a set at a point. The base point of the bundle-valued map may vary.
theorem
ContMDiffAt.smul_totalSpace
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{B : Type u_5}
[TopologicalSpace B]
[ChartedSpace H B]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{V : B → Type u_7}
[(b : B) → AddCommMonoid (V b)]
[(b : B) → Module 𝕜' (V b)]
[(b : B) → TopologicalSpace (V b)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜' F V]
{n : WithTop ℕ∞}
{E' : Type u_8}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_9}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H' M]
{a : M → 𝕜'}
{g : M → Bundle.TotalSpace F V}
{x : M}
(ha : ContMDiffAt J (modelWithCornersSelf 𝕜 𝕜') n a x)
(hg : ContMDiffAt J (I.prod (modelWithCornersSelf 𝕜 F)) n g x)
:
ContMDiffAt J (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (y : M) => ⟨(g y).proj, a y • (g y).snd⟩) x
Multiplying a bundle-valued map by a scalar-valued map preserves C^n regularity at
a point, with the base point of the vector allowed to vary.
theorem
ContMDiffOn.smul_totalSpace
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{B : Type u_5}
[TopologicalSpace B]
[ChartedSpace H B]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{V : B → Type u_7}
[(b : B) → AddCommMonoid (V b)]
[(b : B) → Module 𝕜' (V b)]
[(b : B) → TopologicalSpace (V b)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜' F V]
{n : WithTop ℕ∞}
{E' : Type u_8}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_9}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H' M]
{a : M → 𝕜'}
{g : M → Bundle.TotalSpace F V}
{s : Set M}
(ha : ContMDiffOn J (modelWithCornersSelf 𝕜 𝕜') n a s)
(hg : ContMDiffOn J (I.prod (modelWithCornersSelf 𝕜 F)) n g s)
:
ContMDiffOn J (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (y : M) => ⟨(g y).proj, a y • (g y).snd⟩) s
Multiplying a bundle-valued map by a scalar-valued map preserves C^n regularity
on a set.
theorem
ContMDiff.smul_totalSpace
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{B : Type u_5}
[TopologicalSpace B]
[ChartedSpace H B]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{V : B → Type u_7}
[(b : B) → AddCommMonoid (V b)]
[(b : B) → Module 𝕜' (V b)]
[(b : B) → TopologicalSpace (V b)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜' F V]
{n : WithTop ℕ∞}
{E' : Type u_8}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_9}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H' M]
{a : M → 𝕜'}
{g : M → Bundle.TotalSpace F V}
(ha : ContMDiff J (modelWithCornersSelf 𝕜 𝕜') n a)
(hg : ContMDiff J (I.prod (modelWithCornersSelf 𝕜 F)) n g)
:
Multiplying a bundle-valued map by a scalar-valued map preserves C^n regularity.
theorem
MDifferentiableAt.const_smul_section
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{B : Type u_5}
[TopologicalSpace B]
[ChartedSpace H B]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{V : B → Type u_7}
[(b : B) → AddCommMonoid (V b)]
[(b : B) → Module 𝕜' (V b)]
[(b : B) → TopologicalSpace (V b)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜' F V]
{σ : (b : B) → V b}
{x : B}
(hσ : (MDiffAt fun (b : B) => ⟨b, σ b⟩) x)
(c : 𝕜')
:
(MDiffAt fun (b : B) => ⟨b, (c • σ) b⟩) x
Multiplying a section of a 𝕜'-linear vector bundle by a constant of 𝕜' preserves
differentiability at a point, where differentiability is taken over 𝕜.
def
TauCeti.vectorBundleScalarDiffeomorph
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{B : Type u_5}
[TopologicalSpace B]
[ChartedSpace H B]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{V : B → Type u_7}
[(b : B) → AddCommMonoid (V b)]
[(b : B) → Module 𝕜' (V b)]
[(b : B) → TopologicalSpace (V b)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜' F V]
{n : WithTop ℕ∞}
(a : B → 𝕜')
(ha : ContMDiff I (modelWithCornersSelf 𝕜 𝕜') n a)
(ha0 : ∀ (b : B), a b ≠ 0)
:
Diffeomorph (I.prod (modelWithCornersSelf 𝕜 F)) (I.prod (modelWithCornersSelf 𝕜 F)) (Bundle.TotalSpace F V)
(Bundle.TotalSpace F V) n
A nowhere-zero C^n scalar function on the base rescales each fibre by a C^n
diffeomorphism of the total space. Its inverse multiplies by the reciprocal scalar.
Instances For
@[simp]
theorem
TauCeti.vectorBundleScalarDiffeomorph_apply
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{B : Type u_5}
[TopologicalSpace B]
[ChartedSpace H B]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{V : B → Type u_7}
[(b : B) → AddCommMonoid (V b)]
[(b : B) → Module 𝕜' (V b)]
[(b : B) → TopologicalSpace (V b)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜' F V]
{n : WithTop ℕ∞}
(a : B → 𝕜')
(ha : ContMDiff I (modelWithCornersSelf 𝕜 𝕜') n a)
(ha0 : ∀ (b : B), a b ≠ 0)
(p : Bundle.TotalSpace F V)
:
Scalar rescaling acts fibrewise by the given scalar.
@[simp]
theorem
TauCeti.vectorBundleScalarDiffeomorph_one
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{B : Type u_5}
[TopologicalSpace B]
[ChartedSpace H B]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{V : B → Type u_7}
[(b : B) → AddCommMonoid (V b)]
[(b : B) → Module 𝕜' (V b)]
[(b : B) → TopologicalSpace (V b)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜' F V]
{n : WithTop ℕ∞}
:
vectorBundleScalarDiffeomorph (fun (x : B) => 1) ⋯ ⋯ = Diffeomorph.refl (I.prod (modelWithCornersSelf 𝕜 F)) (Bundle.TotalSpace F V) n
Rescaling by the constant one function is the identity diffeomorphism.
theorem
TauCeti.vectorBundleScalarDiffeomorph_trans
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{B : Type u_5}
[TopologicalSpace B]
[ChartedSpace H B]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{V : B → Type u_7}
[(b : B) → AddCommMonoid (V b)]
[(b : B) → Module 𝕜' (V b)]
[(b : B) → TopologicalSpace (V b)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜' F V]
{n : WithTop ℕ∞}
(a b : B → 𝕜')
(ha : ContMDiff I (modelWithCornersSelf 𝕜 𝕜') n a)
(hb : ContMDiff I (modelWithCornersSelf 𝕜 𝕜') n b)
(ha0 : ∀ (x : B), a x ≠ 0)
(hb0 : ∀ (x : B), b x ≠ 0)
:
(vectorBundleScalarDiffeomorph a ha ha0).trans (vectorBundleScalarDiffeomorph b hb hb0) = vectorBundleScalarDiffeomorph (fun (x : B) => b x * a x) ⋯ ⋯
Successive fibre rescalings multiply the scalar functions on the base.
@[simp]
theorem
TauCeti.vectorBundleScalarDiffeomorph_symm
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{B : Type u_5}
[TopologicalSpace B]
[ChartedSpace H B]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{V : B → Type u_7}
[(b : B) → AddCommMonoid (V b)]
[(b : B) → Module 𝕜' (V b)]
[(b : B) → TopologicalSpace (V b)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜' F V]
{n : WithTop ℕ∞}
(a : B → 𝕜')
(ha : ContMDiff I (modelWithCornersSelf 𝕜 𝕜') n a)
(ha0 : ∀ (b : B), a b ≠ 0)
:
(vectorBundleScalarDiffeomorph a ha ha0).symm = vectorBundleScalarDiffeomorph (fun (b : B) => (a b)⁻¹) ⋯ ⋯
The inverse rescaling is the rescaling associated to the reciprocal function.
theorem
TauCeti.vectorBundleScalarDiffeomorph_image_setOf_norm_lt
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{B : Type u_5}
[TopologicalSpace B]
[ChartedSpace H B]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{V : B → Type u_7}
[(b : B) → AddCommMonoid (V b)]
[(b : B) → Module 𝕜' (V b)]
[(b : B) → TopologicalSpace (V b)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜' F V]
{n : WithTop ℕ∞}
[(b : B) → Norm (V b)]
[∀ (b : B), NormSMulClass 𝕜' (V b)]
(a : B → 𝕜')
(ha : ContMDiff I (modelWithCornersSelf 𝕜 𝕜') n a)
(ha0 : ∀ (b : B), a b ≠ 0)
(r : B → ℝ)
:
Rescaling sends a variable-radius open ball bundle to the open ball bundle whose radii are multiplied by the norms of the scalars. No positivity assumption on the old radii is needed.
theorem
TauCeti.vectorBundleScalarDiffeomorph_image_setOf_norm_le
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{B : Type u_5}
[TopologicalSpace B]
[ChartedSpace H B]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{V : B → Type u_7}
[(b : B) → AddCommMonoid (V b)]
[(b : B) → Module 𝕜' (V b)]
[(b : B) → TopologicalSpace (V b)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜' F V]
{n : WithTop ℕ∞}
[(b : B) → Norm (V b)]
[∀ (b : B), NormSMulClass 𝕜' (V b)]
(a : B → 𝕜')
(ha : ContMDiff I (modelWithCornersSelf 𝕜 𝕜') n a)
(ha0 : ∀ (b : B), a b ≠ 0)
(r : B → ℝ)
:
Rescaling sends closed ball bundles to closed ball bundles with rescaled radii.
theorem
TauCeti.vectorBundleScalarDiffeomorph_image_setOf_norm_eq
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{B : Type u_5}
[TopologicalSpace B]
[ChartedSpace H B]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{V : B → Type u_7}
[(b : B) → AddCommMonoid (V b)]
[(b : B) → Module 𝕜' (V b)]
[(b : B) → TopologicalSpace (V b)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜' F V]
{n : WithTop ℕ∞}
[(b : B) → Norm (V b)]
[∀ (b : B), NormSMulClass 𝕜' (V b)]
(a : B → 𝕜')
(ha : ContMDiff I (modelWithCornersSelf 𝕜 𝕜') n a)
(ha0 : ∀ (b : B), a b ≠ 0)
(r : B → ℝ)
:
Rescaling sends sphere bundles to sphere bundles with rescaled radii.
@[instance_reducible, instance 100]
noncomputable instance
ContMDiffSection.instSMulOfNormedAlgebra
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{B : Type u_5}
[TopologicalSpace B]
[ChartedSpace H B]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{V : B → Type u_7}
[(b : B) → AddCommMonoid (V b)]
[(b : B) → Module 𝕜' (V b)]
[(b : B) → TopologicalSpace (V b)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜' F V]
{n : WithTop ℕ∞}
:
SMul 𝕜' (ContMDiffSection I F n V)
Low-priority SMul 𝕜' instance on C^n sections of a 𝕜'-linear vector bundle over a
𝕜-charted base; when 𝕜' = 𝕜, ContMDiffSection.instSMul takes precedence and is definitionally
equal to this action.
@[simp]
theorem
ContMDiffSection.coe_smul_of_normedAlgebra
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{B : Type u_5}
[TopologicalSpace B]
[ChartedSpace H B]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{V : B → Type u_7}
[(b : B) → AddCommMonoid (V b)]
[(b : B) → Module 𝕜' (V b)]
[(b : B) → TopologicalSpace (V b)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜' F V]
{n : WithTop ℕ∞}
(c : 𝕜')
(s : ContMDiffSection I F n V)
:
@[instance_reducible, instance 100]
noncomputable instance
ContMDiffSection.instModuleOfNormedAlgebra
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{B : Type u_5}
[TopologicalSpace B]
[ChartedSpace H B]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{n : WithTop ℕ∞}
{W : B → Type u_11}
[(x : B) → TopologicalSpace (W x)]
[TopologicalSpace (Bundle.TotalSpace F W)]
[FiberBundle F W]
[(x : B) → AddCommGroup (W x)]
[(x : B) → Module 𝕜 (W x)]
[(x : B) → Module 𝕜' (W x)]
[VectorBundle 𝕜 F W]
[VectorBundle 𝕜' F W]
:
Module 𝕜' (ContMDiffSection I F n W)
Low-priority Module 𝕜' instance on C^n sections of a vector bundle carrying compatible 𝕜-
and 𝕜'-vector-bundle structures (in particular 𝕜 = ℝ, 𝕜' = ℂ).
instance
ContMDiffSection.instIsScalarTower
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{B : Type u_5}
[TopologicalSpace B]
[ChartedSpace H B]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{n : WithTop ℕ∞}
{W : B → Type u_11}
[(x : B) → TopologicalSpace (W x)]
[TopologicalSpace (Bundle.TotalSpace F W)]
[FiberBundle F W]
[(x : B) → AddCommGroup (W x)]
[(x : B) → Module 𝕜 (W x)]
[(x : B) → Module 𝕜' (W x)]
[VectorBundle 𝕜 F W]
[VectorBundle 𝕜' F W]
[∀ (x : B), IsScalarTower 𝕜 𝕜' (W x)]
:
IsScalarTower 𝕜 𝕜' (ContMDiffSection I F n W)