The smooth-function module of bundle sections

The native ContMDiffSection carrier is a module over scalar-valued ContMDiffMaps, with pointwise multiplication. This extends its vector-space structure: constant functions act by the original scalar action, and the two actions form a scalar tower and commute. These structures allow function-linear maps on sections, in particular tensorial bundle operators, to be expressed using the usual LinearMap API.

Pullback along a C^n map takes values in the pullback bundle. It is linear over the ground field and intertwines multiplication with composition of scalar functions. Restriction to an open subset is pullback along its inclusion. No finite-dimensionality, compactness, or boundary assumption is needed, and the construction works at every differentiability order.

More generally, for a normed field extension 𝕜 ⊆ 𝕜', the sections of a 𝕜'-vector bundle over a 𝕜-manifold form a module over the 𝕜'-valued functions (ContMDiffSection.instModuleContMDiffMapOfNormedAlgebra). This action extends the 𝕜-valued function action and the 𝕜'-scalar action through constant functions, and commutes with pullback and restriction. For 𝕜 = ℝ and 𝕜' = ℂ it makes the sections of a complex bundle over a real manifold a module over the complex-valued functions.

@[instance_reducible]

instance ContMDiffSection.instModuleContMDiffMap {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] : Module (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n) (ContMDiffSection I F n V)

Sections form a module over the ring of scalar-valued functions of the same regularity.

instance ContMDiffSection.instIsScalarTowerContMDiffMap {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] : IsScalarTower 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n) (ContMDiffSection I F n V)

Ground-field scalars and smooth scalar functions form a tower on sections.

instance ContMDiffSection.instSMulCommClassContMDiffMap {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] : SMulCommClass 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n) (ContMDiffSection I F n V)

Ground-field multiplication commutes with smooth-function multiplication on sections.

def ContMDiffSection.evalLinearMap {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) [TopologicalSpace M] [ChartedSpace H M] (F : Type u_5) [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : WithTop ℕ∞) (V : M → Type u_6) [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (x : M) : ContMDiffSection I F n V →ₗ[𝕜] V x

Evaluation of sections at a point as a ground-field linear map.

@[simp]

theorem ContMDiffSection.evalLinearMap_apply {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (x : M) (s : ContMDiffSection I F n V) : (evalLinearMap I F n V x) s = s x

def ContMDiffSection.pullback {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {E' : Type u_7} {H' : Type u_8} {N : Type u_9} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] [∀ (x : M), Nonempty (V x)] (s : ContMDiffSection I F n V) (g : ContMDiffMap I' I N M n) : ContMDiffSection I' F n (⇑↑g *ᵖ V)

Pull a section back along a C^n map, with values in the pullback bundle.

@[simp]

theorem ContMDiffSection.pullback_apply {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {E' : Type u_7} {H' : Type u_8} {N : Type u_9} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] [∀ (x : M), Nonempty (V x)] (s : ContMDiffSection I F n V) (g : ContMDiffMap I' I N M n) (x : N) : (s.pullback g) x = s (g x)

Pullback evaluates the original section at the image point.

@[simp]

theorem ContMDiffSection.pullback_zero {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {E' : Type u_7} {H' : Type u_8} {N : Type u_9} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (g : ContMDiffMap I' I N M n) : pullback 0 g = 0

@[simp]

theorem ContMDiffSection.pullback_add {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {E' : Type u_7} {H' : Type u_8} {N : Type u_9} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (s t : ContMDiffSection I F n V) (g : ContMDiffMap I' I N M n) : (s + t).pullback g = s.pullback g + t.pullback g

@[simp]

theorem ContMDiffSection.pullback_smul {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {E' : Type u_7} {H' : Type u_8} {N : Type u_9} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (c : 𝕜) (s : ContMDiffSection I F n V) (g : ContMDiffMap I' I N M n) : (c • s).pullback g = c • s.pullback g

@[simp]

theorem ContMDiffSection.pullback_smul_function {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {E' : Type u_7} {H' : Type u_8} {N : Type u_9} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n) (s : ContMDiffSection I F n V) (g : ContMDiffMap I' I N M n) : (f • s).pullback g = f.comp g • s.pullback g

Pullback intertwines smooth-function multiplication with composition of functions.

def ContMDiffSection.pullbackLinearMap {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) [TopologicalSpace M] [ChartedSpace H M] (F : Type u_5) [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : WithTop ℕ∞) (V : M → Type u_6) [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {E' : Type u_7} {H' : Type u_8} {N : Type u_9} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (g : ContMDiffMap I' I N M n) : ContMDiffSection I F n V →ₗ[𝕜] ContMDiffSection I' F n (⇑↑g *ᵖ V)

Pullback of sections along a C^n map as a ground-field linear map.

@[simp]

theorem ContMDiffSection.pullbackLinearMap_apply {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {E' : Type u_7} {H' : Type u_8} {N : Type u_9} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (g : ContMDiffMap I' I N M n) (s : ContMDiffSection I F n V) : (pullbackLinearMap I F n V g) s = s.pullback g

noncomputable def ContMDiffSection.restrict {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [∀ (x : M), Nonempty (V x)] (s : ContMDiffSection I F n V) (U : TopologicalSpace.Opens M) : ContMDiffSection I F n (⇑{ toFun := Subtype.val, continuous_toFun := ⋯ } *ᵖ V)

Restriction of a section to an open subset, in the pullback bundle along its inclusion.

@[simp]

theorem ContMDiffSection.restrict_apply {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [∀ (x : M), Nonempty (V x)] (s : ContMDiffSection I F n V) (U : TopologicalSpace.Opens M) (x : ↥U) : (s.restrict U) x = s ↑x

Restriction keeps the value at each point of the open subset.

@[simp]

theorem ContMDiffSection.restrict_zero {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (U : TopologicalSpace.Opens M) : restrict 0 U = 0

@[simp]

theorem ContMDiffSection.restrict_add {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (s t : ContMDiffSection I F n V) (U : TopologicalSpace.Opens M) : (s + t).restrict U = s.restrict U + t.restrict U

@[simp]

theorem ContMDiffSection.restrict_smul {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (c : 𝕜) (s : ContMDiffSection I F n V) (U : TopologicalSpace.Opens M) : (c • s).restrict U = c • s.restrict U

@[simp]

theorem ContMDiffSection.restrict_smul_function {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n) (s : ContMDiffSection I F n V) (U : TopologicalSpace.Opens M) : (f • s).restrict U = f.comp ⟨Subtype.val, ⋯⟩ • s.restrict U

Restriction intertwines smooth-function multiplication with restriction of functions.

noncomputable def ContMDiffSection.restrictLinearMap {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) [TopologicalSpace M] [ChartedSpace H M] (F : Type u_5) [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : WithTop ℕ∞) (V : M → Type u_6) [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (U : TopologicalSpace.Opens M) : ContMDiffSection I F n V →ₗ[𝕜] ContMDiffSection I F n (⇑{ toFun := Subtype.val, continuous_toFun := ⋯ } *ᵖ V)

Restriction of sections to an open subset as a ground-field linear map.

@[simp]

theorem ContMDiffSection.restrictLinearMap_apply {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (U : TopologicalSpace.Opens M) (s : ContMDiffSection I F n V) : (restrictLinearMap I F n V U) s = s.restrict U

Functions with values in a normed algebra

@[instance_reducible, instance 100]

instance ContMDiffSection.instSMulContMDiffMapOfNormedAlgebra {𝕜 : Type u_7} {𝕜' : Type u_8} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_9} {H : Type u_10} {M : Type u_11} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_12} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {n : WithTop ℕ∞} {V : M → Type u_13} [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜' (V x)] [VectorBundle 𝕜' F V] : SMul (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜') M 𝕜' n) (ContMDiffSection I F n V)

Functions with values in a normed algebra 𝕜' act by pointwise multiplication on the sections of a 𝕜'-vector bundle over a 𝕜-manifold. When 𝕜' = 𝕜, ContMDiffSection.instSMulContMDiffMap takes precedence; both actions are pointwise.

@[simp]

theorem ContMDiffSection.smul_apply_of_normedAlgebra {𝕜 : Type u_7} {𝕜' : Type u_8} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_9} {H : Type u_10} {M : Type u_11} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_12} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {n : WithTop ℕ∞} {V : M → Type u_13} [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜' (V x)] [VectorBundle 𝕜' F V] (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜') M 𝕜' n) (s : ContMDiffSection I F n V) (x : M) : (f • s) x = f x • s x

Evaluation of the 𝕜'-valued function action is fibrewise scalar multiplication.

instance ContMDiffSection.instSMulCommClassContMDiffMapOfNormedAlgebra {𝕜 : Type u_7} {𝕜' : Type u_8} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_9} {H : Type u_10} {M : Type u_11} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_12} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {n : WithTop ℕ∞} {V : M → Type u_13} [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜' (V x)] [VectorBundle 𝕜' F V] : SMulCommClass 𝕜' (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜') M 𝕜' n) (ContMDiffSection I F n V)

Constant 𝕜'-scalars commute with 𝕜'-valued functions acting on sections.

@[simp]

theorem ContMDiffSection.const_smul_of_normedAlgebra {𝕜 : Type u_7} {𝕜' : Type u_8} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_9} {H : Type u_10} {M : Type u_11} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_12} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {n : WithTop ℕ∞} {V : M → Type u_13} [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜' (V x)] [VectorBundle 𝕜' F V] (c : 𝕜') (s : ContMDiffSection I F n V) : ContMDiffMap.const c • s = c • s

A constant 𝕜'-valued function acts on sections by its value.

@[simp]

theorem ContMDiffSection.pullback_smul_function_of_normedAlgebra {𝕜 : Type u_7} {𝕜' : Type u_8} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_9} {H : Type u_10} {M : Type u_11} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_12} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {n : WithTop ℕ∞} {V : M → Type u_13} [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜' (V x)] [VectorBundle 𝕜' F V] {E' : Type u_14} {H' : Type u_15} {N : Type u_16} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜') M 𝕜' n) (s : ContMDiffSection I F n V) (g : ContMDiffMap I' I N M n) : (f • s).pullback g = f.comp g • s.pullback g

Pullback intertwines the 𝕜'-valued function action with composition of functions.

@[simp]

theorem ContMDiffSection.restrict_smul_function_of_normedAlgebra {𝕜 : Type u_7} {𝕜' : Type u_8} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_9} {H : Type u_10} {M : Type u_11} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_12} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {n : WithTop ℕ∞} {V : M → Type u_13} [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜' (V x)] [VectorBundle 𝕜' F V] (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜') M 𝕜' n) (s : ContMDiffSection I F n V) (U : TopologicalSpace.Opens M) : (f • s).restrict U = f.comp ⟨Subtype.val, ⋯⟩ • s.restrict U

Restriction intertwines the 𝕜'-valued function action with restriction of functions.

@[instance_reducible, instance 100]

instance ContMDiffSection.instModuleContMDiffMapOfNormedAlgebra {𝕜 : Type u_7} {𝕜' : Type u_8} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_9} {H : Type u_10} {M : Type u_11} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_12} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {n : WithTop ℕ∞} {V : M → Type u_13} [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜' (V x)] [VectorBundle 𝕜' F V] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] [ContMDiffRing (modelWithCornersSelf 𝕜 𝕜') n 𝕜'] : Module (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜') M 𝕜' n) (ContMDiffSection I F n V)

The sections of a 𝕜'-vector bundle over a 𝕜-manifold form a module over the ring of 𝕜'-valued functions of the same regularity.

instance ContMDiffSection.instIsScalarTowerContMDiffMapOfNormedAlgebra {𝕜 : Type u_7} {𝕜' : Type u_8} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_9} {H : Type u_10} {M : Type u_11} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_12} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {n : WithTop ℕ∞} {V : M → Type u_13} [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜' (V x)] [VectorBundle 𝕜' F V] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] [ContMDiffRing (modelWithCornersSelf 𝕜 𝕜') n 𝕜'] [∀ (x : M), IsScalarTower 𝕜 𝕜' (V x)] : IsScalarTower 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜') M 𝕜' n) (ContMDiffSection I F n V)

Ground-field scalars, acting on 𝕜'-valued functions, and these functions form a tower on sections.

instance ContMDiffSection.instIsScalarTowerContMDiffMapContMDiffMapOfNormedAlgebra {𝕜 : Type u_7} {𝕜' : Type u_8} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_9} {H : Type u_10} {M : Type u_11} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_12} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {n : WithTop ℕ∞} {V : M → Type u_13} [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜' (V x)] [VectorBundle 𝕜' F V] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] [∀ (x : M), IsScalarTower 𝕜 𝕜' (V x)] : IsScalarTower (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜') M 𝕜' n) (ContMDiffSection I F n V)

𝕜-valued functions, acting on 𝕜'-valued functions by ContMDiffMap.instSMul', and 𝕜'-valued functions form a tower on sections.