The tensoriality criterion

Given vector bundles V and W over a manifold M, one can construct a section of the hom-bundle Π x, V x →L[𝕜] W x from a tensorial operation sending sections of V to sections of W. This file provides this construction.

In fact, we define tensoriality, and provide the above criterion, in slightly greater generality: for operations sending sections of V to a vector space A (which in the above application is the fibre W x), the construction produces a continuous linear map V x →L[𝕜] A.

Main definitions

• TensorialAt: Propositional structure stating that an operation on sections of a vector bundle V is tensorial.

• TensorialAt.mkHom: An operation on sections of V which is tensorial at x defines a continuous linear map out of V x.

• TensorialAt.mkHom₂: An operation on sections of V and V' which is tensorial at x in both arguments defines a continuous bilinear map out of V x and V' x.

structure TensorialAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {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] (F : Type u_5) [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {A : Type u_9} [AddCommGroup A] [Module 𝕜 A] (Φ : ((x : M) → V x) → A) (x : M) : Prop

An operation Φ on sections of a vector bundle V over M is tensorial at x : M, if it respects addition and scalar multiplication by germs of diffentiable functions at f.

• smul {f : M → 𝕜} {σ : (x : M) → V x} : MDiffAt f x → MDiffAt (T% σ) x → Φ (f • σ) = f x • Φ σ
• add {σ σ' : (x : M) → V x} : MDiffAt (T% σ) x → MDiffAt (T% σ') x → Φ (σ + σ') = Φ σ + Φ σ'

theorem TensorialAt.local {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {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] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {A : Type u_9} [AddCommGroup A] [Module 𝕜 A] {Φ : ((x : M) → V x) → A} {x : M} (hΦ : TensorialAt I F Φ x) {σ σ' : (x : M) → V x} (hσ : MDiffAt (T% σ) x) (hσ' : MDiffAt (T% σ') x) (hσσ' : ∀ᶠ (x' : M) in nhds x, σ x' = σ' x') : Φ σ = Φ σ'

If the operation Φ on sections of a vector bundle V is tensorial at x, then it depends only on the germ of the section at x.

This is later superseded by TensorialAt.pointwise, showing that Φ depends only on the value at x itself.

theorem TensorialAt.zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {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] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {A : Type u_9} [AddCommGroup A] [Module 𝕜 A] {Φ : ((x : M) → V x) → A} {x : M} [VectorBundle 𝕜 F V] (hΦ : TensorialAt I F Φ x) : Φ 0 = 0

A tensorial operation on sections of a vector bundle respects zero (since it respects scalar multiplication).

theorem TensorialAt.sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {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] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {A : Type u_9} [AddCommGroup A] [Module 𝕜 A] {Φ : ((x : M) → V x) → A} {x : M} [VectorBundle 𝕜 F V] (hΦ : TensorialAt I F Φ x) {ι : Type u_10} {s : Finset ι} (σ : ι → (x : M) → V x) (hσ : ∀ (i : ι), MDiffAt (T% σ) x) : (Φ fun (x' : M) => ∑ i ∈ s, σ i x') = ∑ i ∈ s, Φ (σ i)

A tensorial operation on sections of a vector bundle respects sums (since it respects binary addition).

theorem TensorialAt.pointwise {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {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] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {A : Type u_9} [AddCommGroup A] [Module 𝕜 A] {Φ : ((x : M) → V x) → A} {x : M} [VectorBundle 𝕜 F V] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 F] [ContMDiffVectorBundle 1 F V I] (hΦ : TensorialAt I F Φ x) {σ σ' : (x : M) → V x} (hσ : MDiffAt (T% σ) x) (hσ' : MDiffAt (T% σ') x) (hσσ' : σ x = σ' x) : Φ σ = Φ σ'

If the operation Φ on sections of a vector bundle V is tensorial at x, then it depends only on the value of the section at x.

theorem TensorialAt.pointwise₂ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {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] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {F' : Type u_7} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {V' : M → Type u_8} [TopologicalSpace (Bundle.TotalSpace F' V')] [(x : M) → AddCommGroup (V' x)] [(x : M) → Module 𝕜 (V' x)] [(x : M) → TopologicalSpace (V' x)] [FiberBundle F' V'] {A : Type u_9} [AddCommGroup A] [Module 𝕜 A] [VectorBundle 𝕜 F V] [VectorBundle 𝕜 F' V'] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 F'] [ContMDiffVectorBundle 1 F V I] [ContMDiffVectorBundle 1 F' V' I] {Φ : ((x : M) → V x) → ((x : M) → V' x) → A} {x : M} (hΦ₁ : ∀ (τ : (x : M) → V' x), MDiffAt (T% τ) x → TensorialAt I F (fun (x : (x : M) → V x) => Φ x τ) x) (hΦ₂ : ∀ (σ : (x : M) → V x), MDiffAt (T% σ) x → TensorialAt I F' (fun (x : (x : M) → V' x) => Φ σ x) x) {σ σ' : (x : M) → V x} {τ τ' : (x : M) → V' x} (hσ : MDiffAt (T% σ) x) (hσ' : MDiffAt (T% σ') x) (hτ : MDiffAt (T% τ) x) (hτ' : MDiffAt (T% τ') x) (hσσ' : σ x = σ' x) (hττ' : τ x = τ' x) : Φ σ τ = Φ σ' τ'

If the operation Φ on sections of vector bundles V and V' is tensorial at x in each argument, then it depends only on the value of the sections at x.

noncomputable def TensorialAt.mkHom {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {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] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {A : Type u_9} [AddCommGroup A] [Module 𝕜 A] [VectorBundle 𝕜 F V] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 F] [ContMDiffVectorBundle 1 F V I] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul 𝕜 (V x)] [TopologicalSpace A] [IsTopologicalAddGroup A] [ContinuousSMul 𝕜 A] (Φ : ((x : M) → V x) → A) (x : M) (hΦ : TensorialAt I F Φ x) : V x →L[𝕜] A

Given an A-valued operation Φ on sections of a vector bundle V which is tensorial at x, the construction TensorialAt.mkHom provides the associated continuous linear map V x →L[𝕜] A.

Equations

• TensorialAt.mkHom Φ x hΦ = LinearMap.toContinuousLinearMap { toFun := fun (v : V x) => Φ (FiberBundle.extend F v), map_add' := ⋯, map_smul' := ⋯ }

theorem TensorialAt.mkHom_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {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] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {A : Type u_9} [AddCommGroup A] [Module 𝕜 A] [VectorBundle 𝕜 F V] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 F] [ContMDiffVectorBundle 1 F V I] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul 𝕜 (V x)] [TopologicalSpace A] [IsTopologicalAddGroup A] [ContinuousSMul 𝕜 A] {Φ : ((x : M) → V x) → A} {x : M} (hΦ : TensorialAt I F (fun (x : (x : M) → V x) => Φ x) x) {σ : (x : M) → V x} (hσ : MDiffAt (T% σ) x) : (mkHom Φ x hΦ) (σ x) = Φ σ

theorem TensorialAt.mkHom_apply_eq_extend {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {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] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {A : Type u_9} [AddCommGroup A] [Module 𝕜 A] [VectorBundle 𝕜 F V] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 F] [ContMDiffVectorBundle 1 F V I] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul 𝕜 (V x)] [TopologicalSpace A] [IsTopologicalAddGroup A] [ContinuousSMul 𝕜 A] {Φ : ((x : M) → V x) → A} {x : M} (hΦ : TensorialAt I F Φ x) (σ : V x) : (mkHom Φ x hΦ) σ = Φ (FiberBundle.extend F σ)

noncomputable def TensorialAt.mkHom₂ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {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] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {F' : Type u_7} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {V' : M → Type u_8} [TopologicalSpace (Bundle.TotalSpace F' V')] [(x : M) → AddCommGroup (V' x)] [(x : M) → Module 𝕜 (V' x)] [(x : M) → TopologicalSpace (V' x)] [FiberBundle F' V'] {A : Type u_9} [AddCommGroup A] [Module 𝕜 A] [VectorBundle 𝕜 F V] [VectorBundle 𝕜 F' V'] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 F'] [ContMDiffVectorBundle 1 F V I] [ContMDiffVectorBundle 1 F' V' I] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul 𝕜 (V x)] [∀ (x : M), IsTopologicalAddGroup (V' x)] [∀ (x : M), ContinuousSMul 𝕜 (V' x)] [TopologicalSpace A] [IsTopologicalAddGroup A] [ContinuousSMul 𝕜 A] (Φ : ((x : M) → V x) → ((x : M) → V' x) → A) (x : M) (hΦ₁ : ∀ (τ : (x : M) → V' x), MDiffAt (T% τ) x → TensorialAt I F (fun (x : (x : M) → V x) => Φ x τ) x) (hΦ₂ : ∀ (σ : (x : M) → V x), MDiffAt (T% σ) x → TensorialAt I F' (Φ σ) x) : V x →L[𝕜] V' x →L[𝕜] A

Given an A-valued operation Φ on sections of vector bundles V and V' which is tensorial at x in each argument, the construction TensorialAt.mkHom₂ provides the associated continuous linear map V x →L[𝕜] V' x →L[𝕜] A.

Equations

• TensorialAt.mkHom₂ Φ x hΦ₁ hΦ₂ = ⋯.toLinearMap.toContinuousBilinearMap

theorem TensorialAt.mkHom₂_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {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] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {F' : Type u_7} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {V' : M → Type u_8} [TopologicalSpace (Bundle.TotalSpace F' V')] [(x : M) → AddCommGroup (V' x)] [(x : M) → Module 𝕜 (V' x)] [(x : M) → TopologicalSpace (V' x)] [FiberBundle F' V'] {A : Type u_9} [AddCommGroup A] [Module 𝕜 A] [VectorBundle 𝕜 F V] [VectorBundle 𝕜 F' V'] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 F'] [ContMDiffVectorBundle 1 F V I] [ContMDiffVectorBundle 1 F' V' I] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul 𝕜 (V x)] [∀ (x : M), IsTopologicalAddGroup (V' x)] [∀ (x : M), ContinuousSMul 𝕜 (V' x)] [TopologicalSpace A] [IsTopologicalAddGroup A] [ContinuousSMul 𝕜 A] {Φ : ((x : M) → V x) → ((x : M) → V' x) → A} {x : M} (hΦ₁ : ∀ (τ : (x : M) → V' x), MDiffAt (T% τ) x → TensorialAt I F (fun (x : (x : M) → V x) => Φ x τ) x) (hΦ₂ : ∀ (σ : (x : M) → V x), MDiffAt (T% σ) x → TensorialAt I F' (Φ σ) x) {σ : (x : M) → V x} (hσ : MDiffAt (T% σ) x) {τ : (x : M) → V' x} (hτ : MDiffAt (T% τ) x) : ((mkHom₂ Φ x hΦ₁ hΦ₂) (σ x)) (τ x) = Φ σ τ

theorem TensorialAt.mkHom₂_apply_eq_extend {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {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] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {F' : Type u_7} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {V' : M → Type u_8} [TopologicalSpace (Bundle.TotalSpace F' V')] [(x : M) → AddCommGroup (V' x)] [(x : M) → Module 𝕜 (V' x)] [(x : M) → TopologicalSpace (V' x)] [FiberBundle F' V'] {A : Type u_9} [AddCommGroup A] [Module 𝕜 A] [VectorBundle 𝕜 F V] [VectorBundle 𝕜 F' V'] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 F'] [ContMDiffVectorBundle 1 F V I] [ContMDiffVectorBundle 1 F' V' I] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul 𝕜 (V x)] [∀ (x : M), IsTopologicalAddGroup (V' x)] [∀ (x : M), ContinuousSMul 𝕜 (V' x)] [TopologicalSpace A] [IsTopologicalAddGroup A] [ContinuousSMul 𝕜 A] {Φ : ((x : M) → V x) → ((x : M) → V' x) → A} {x : M} (hΦ₁ : ∀ (τ : (x : M) → V' x), MDiffAt (T% τ) x → TensorialAt I F (fun (x : (x : M) → V x) => Φ x τ) x) (hΦ₂ : ∀ (σ : (x : M) → V x), MDiffAt (T% σ) x → TensorialAt I F' (Φ σ) x) (σ : V x) (τ : V' x) : ((mkHom₂ Φ x hΦ₁ hΦ₂) σ) τ = Φ (FiberBundle.extend F σ) (FiberBundle.extend F' τ)