Tensoriality of globally smooth operations

This file complements Mathlib's pointwise tensoriality API with a criterion for operations whose additivity and smooth-function linearity laws are available for globally smooth sections. The criterion applies to finite-rank smooth real vector bundles over finite-dimensional Hausdorff manifolds. The target only needs addition and scalar multiplication; no algebraic laws on these operations are required beyond the stated laws for the section operation.

Main results

• TauCeti.Manifold.eq_of_contMDiff_smul_of_eventuallyEq: smooth-function linearity implies locality.
• TauCeti.Manifold.eq_of_contMDiff_tensorial: an operation satisfying these laws has equal values on globally smooth sections which agree at the point of evaluation.

theorem TauCeti.Manifold.map_sum_eq_of_contMDiff_additive {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {W : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace G W)] [(x : M) → AddCommGroup (W x)] [(x : M) → Module 𝕜 (W x)] [(x : M) → TopologicalSpace (W x)] [FiberBundle G W] [VectorBundle 𝕜 G W] {A : Type u_7} [Add A] (Φ : ((x : M) → W x) → A) (hadd : ∀ {s s' : (x : M) → W x}, (ContMDiff I (I.prod (modelWithCornersSelf 𝕜 G)) n fun (x : M) => ⟨x, s x⟩) → (ContMDiff I (I.prod (modelWithCornersSelf 𝕜 G)) n fun (x : M) => ⟨x, s' x⟩) → Φ (s + s') = Φ s + Φ s') {ι : Type u_8} (q : Finset ι) (u v : ι → (x : M) → W x) (hu : ∀ i ∈ q, ContMDiff I (I.prod (modelWithCornersSelf 𝕜 G)) n fun (x : M) => ⟨x, u i x⟩) (hv : ∀ i ∈ q, ContMDiff I (I.prod (modelWithCornersSelf 𝕜 G)) n fun (x : M) => ⟨x, v i x⟩) (huv : ∀ i ∈ q, Φ (u i) = Φ (v i)) : Φ (∑ i ∈ q, u i) = Φ (∑ i ∈ q, v i)

An operation on sections which is additive on globally smooth sections takes equal values on two finite sums of globally smooth sections whenever it takes equal values on the summands. The target needs only an addition, without any algebraic laws.

theorem TauCeti.Manifold.eq_of_contMDiff_smul_of_eventuallyEq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {W : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace G W)] [(x : M) → AddCommGroup (W x)] [(x : M) → Module ℝ (W x)] [(x : M) → TopologicalSpace (W x)] [FiberBundle G W] {A : Type u_6} [SMul ℝ A] (Φ : ((x : M) → W x) → A) (x : M) (hsmul : ∀ {f : M → ℝ} {s : (x : M) → W x}, ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f → (ContMDiff I (I.prod (modelWithCornersSelf ℝ G)) ↑⊤ fun (x : M) => ⟨x, s x⟩) → Φ (f • s) = f x • Φ s) {s s' : (x : M) → W x} (hs : ContMDiff I (I.prod (modelWithCornersSelf ℝ G)) ↑⊤ fun (x : M) => ⟨x, s x⟩) (hs' : ContMDiff I (I.prod (modelWithCornersSelf ℝ G)) ↑⊤ fun (x : M) => ⟨x, s' x⟩) (hss' : ∀ᶠ (y : M) in nhds x, s y = s' y) : Φ s = Φ s'

An operation on globally smooth sections which respects multiplication by globally smooth functions depends only on the germ of the section at the evaluation point. Neither additivity nor any laws for scalar multiplication on the target are required. This is the smooth bump-function version of TensorialAt.local, whose cutoff need only be differentiable at the evaluation point.

theorem TauCeti.Manifold.eq_of_contMDiff_tensorial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G] {W : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace G W)] [(x : M) → AddCommGroup (W x)] [(x : M) → Module ℝ (W x)] [(x : M) → TopologicalSpace (W x)] [FiberBundle G W] [VectorBundle ℝ G W] [ContMDiffVectorBundle (↑⊤) G W I] {A : Type u_6} [Add A] [SMul ℝ A] (Φ : ((x : M) → W x) → A) (x : M) (hadd : ∀ {s s' : (x : M) → W x}, (ContMDiff I (I.prod (modelWithCornersSelf ℝ G)) ↑⊤ fun (x : M) => ⟨x, s x⟩) → (ContMDiff I (I.prod (modelWithCornersSelf ℝ G)) ↑⊤ fun (x : M) => ⟨x, s' x⟩) → Φ (s + s') = Φ s + Φ s') (hsmul : ∀ {f : M → ℝ} {s : (x : M) → W x}, ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f → (ContMDiff I (I.prod (modelWithCornersSelf ℝ G)) ↑⊤ fun (x : M) => ⟨x, s x⟩) → Φ (f • s) = f x • Φ s) {s s' : (x : M) → W x} (hs : ContMDiff I (I.prod (modelWithCornersSelf ℝ G)) ↑⊤ fun (x : M) => ⟨x, s x⟩) (hs' : ContMDiff I (I.prod (modelWithCornersSelf ℝ G)) ↑⊤ fun (x : M) => ⟨x, s' x⟩) (hss' : s x = s' x) : Φ s = Φ s'

On a finite-rank smooth real vector bundle over a finite-dimensional Hausdorff manifold, an operation which is additive and linear over globally smooth functions on globally smooth sections depends only on the value of such a section at the point of evaluation. The target need only carry addition and scalar multiplication, without any algebraic laws.