Local frames: duality with the coefficient functionals, and testing hom-bundle sections

Let V → M be a smooth vector bundle, let e be a trivialization of V and let b be a basis of the model fibre, so that e.localFrame b is a local frame of V over e.baseSet with coefficient functionals e.localFrameCoeff I b. This file records that over e.baseSet the frame and its coefficient functionals are dual to each other: the i-th functional takes the value 1 on the i-th frame vector and 0 on the others.

It then uses a local frame of the source bundle to test smoothness of a section of a bundle of continuous linear maps: such a section is C^n on an open subset of the two base sets as soon as its evaluations on the frame sections are. Read through a trivialization, a continuous linear map out of a finite-dimensional space is recovered from its values on a basis by T = ∑ j, (b.coord j).smulRight (T (b j)), and each summand depends continuously linearly on T (b j). This is the criterion through which a covariant derivative is proved to be C^n: ContMDiffCovariantDerivativeOn asks for smoothness of the hom-bundle section ∇σ, while the constructions of connections produce smoothness of the vector fields ∇_X σ one direction X at a time.

Main results

• TauCeti.Manifold.localFrameCoeff_basisAt: the coefficient functionals are dual to the basis e.basisAt b hx of the fibre at a point of e.baseSet.
• TauCeti.Manifold.localFrameCoeff_localFrame: the same duality, stated for the frame sections themselves.
• TauCeti.Manifold.symmL_basis_eq_localFrame and TauCeti.Manifold.continuousLinearMapAt_localFrame: a trivialization transports basis vectors to its local frame and reads those frame vectors back as basis vectors.
• TauCeti.Manifold.coordChangeL_toMatrix: a trivialization coordinate change has the change-of-basis matrix between the corresponding local frames.
• TauCeti.Manifold.contMDiffOn_hom_of_localFrame: a section of the bundle of continuous linear maps is C^n once its evaluations on a local frame of the source bundle are.

@[simp]

theorem TauCeti.Manifold.localFrameCoeff_basisAt {𝕜 : 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] [VectorBundle 𝕜 F V] [ContMDiffVectorBundle 1 F V I] {x : M} {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [DecidableEq ι] (hx : x ∈ e.baseSet) (i j : ι) : (Bundle.Trivialization.localFrameCoeff I e b i x) ((e.basisAt b hx) j) = if i = j then 1 else 0

A local frame is dual to its own coefficient functionals on the basis sections at x.

theorem TauCeti.Manifold.localFrameCoeff_localFrame {𝕜 : 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] [VectorBundle 𝕜 F V] [ContMDiffVectorBundle 1 F V I] {x : M} {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [DecidableEq ι] (hx : x ∈ e.baseSet) (i j : ι) : (Bundle.Trivialization.localFrameCoeff I e b i x) (e.localFrame b j x) = if i = j then 1 else 0

A local frame is dual to its own coefficient functionals.

theorem TauCeti.Manifold.symmL_basis_eq_localFrame {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {M : Type u_4} [TopologicalSpace 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] [VectorBundle 𝕜 F V] {x : M} {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] (hx : x ∈ e.baseSet) (i : ι) : (Bundle.Trivialization.symmL 𝕜 e x) (b i) = e.localFrame b i x

The continuous inverse of a trivialization transports a model-fibre basis vector to the corresponding local-frame vector.

theorem TauCeti.Manifold.continuousLinearMapAt_localFrame {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {M : Type u_4} [TopologicalSpace 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] [VectorBundle 𝕜 F V] {x : M} {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] (hx : x ∈ e.baseSet) (i : ι) : (Bundle.Trivialization.continuousLinearMapAt 𝕜 e x) (e.localFrame b i x) = b i

A trivialization reads a vector of its local frame as the corresponding model-fibre basis vector.

theorem TauCeti.Manifold.coordChangeL_toMatrix {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {M : Type u_4} [TopologicalSpace 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] [VectorBundle 𝕜 F V] {x : M} {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [Fintype ι] [DecidableEq ι] {e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e'] (hx : x ∈ e.baseSet) (hx' : x ∈ e'.baseSet) : (LinearMap.toMatrix b b) ↑↑(Bundle.Trivialization.coordChangeL 𝕜 e e' x) = (e'.basisAt b hx').toMatrix ⇑(e.basisAt b hx)

The matrix of a coordinate change between two vector-bundle trivializations is the change-of-basis matrix between the corresponding local frames.

Testing a hom-bundle section on a local frame

theorem TauCeti.Manifold.contMDiffOn_hom_of_localFrame {𝕜 : 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] [VectorBundle 𝕜 F V] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [Finite ι] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 F] {F' : Type u_8} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {V' : M → Type u_9} [TopologicalSpace (Bundle.TotalSpace F' V')] [(x : M) → AddCommGroup (V' x)] [(x : M) → Module 𝕜 (V' x)] [(x : M) → TopologicalSpace (V' x)] [FiberBundle F' V'] [VectorBundle 𝕜 F' V'] {e' : Bundle.Trivialization F' Bundle.TotalSpace.proj} [MemTrivializationAtlas e'] {n : WithTop ℕ∞} {u : Set M} [∀ (x : M), IsTopologicalAddGroup (V' x)] [∀ (x : M), ContinuousSMul 𝕜 (V' x)] [ContMDiffVectorBundle n F V I] [ContMDiffVectorBundle n F' V' I] (hu : IsOpen u) (hu' : u ⊆ e.baseSet ∩ e'.baseSet) {A : (y : M) → V y →L[𝕜] V' y} (hA : ∀ (j : ι), ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F')) n (fun (y : M) => ⟨y, (A y) (e.localFrame b j y)⟩) u) : ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 (F →L[𝕜] F'))) n (fun (y : M) => ⟨y, A y⟩) u

A hom-bundle section is tested on a local frame. A section A of the bundle of continuous linear maps from V to V' is C^n on an open subset of e.baseSet ∩ e'.baseSet as soon as each of its evaluations A (e.localFrame b j) on the local frame of the source bundle is.