Coordinate frames of manifold charts

The canonical trivialization of the tangent bundle at x₀ is read off the chart at x₀, so the local frame it induces from a basis b of the model space is the classical coordinate frame of that chart. This file identifies that frame with the pullback of constant model-space vector fields, shows that the chart derivative reads it back as the basis, and proves that its vector fields commute.

Main results

• TauCeti.Manifold.eqOn_symm_trivializationAt_mpullbackWithin and TauCeti.Manifold.eqOn_localFrame_trivializationAt_mpullbackWithin: over the chart source, a vector field with constant coordinates in the canonical trivialization at x₀, in particular a member of its local frame, is the pullback along the extended chart of a constant model-space vector field.
• TauCeti.Manifold.mfderiv_extChartAt_localFrame_trivializationAt: the derivative of the chart sends the coordinate frame to the basis of the model space it is built from.
• TauCeti.Manifold.mlieBracket_symm_trivializationAt and TauCeti.Manifold.mlieBracket_localFrame_trivializationAt: vector fields with constant coordinates commute, and so does the coordinate frame.

theorem TauCeti.Manifold.eqOn_symm_trivializationAt_mpullbackWithin {𝕜 : 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] [IsManifold I 1 M] (x₀ : M) (v : E) : Set.EqOn (fun (y : M) => (trivializationAt E (TangentSpace I) x₀).symm y v) (VectorField.mpullbackWithin I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x₀)) (fun (x : E) => v) (extChartAt I x₀).source) (extChartAt I x₀).source

Vector fields with constant coordinates are coordinate vector fields. Over the source of the chart at x₀, the vector field whose coordinates in the canonical trivialization at x₀ are the constant v is the pullback, along the extended chart, of the constant model-space vector field with value v.

theorem TauCeti.Manifold.eqOn_localFrame_trivializationAt_mpullbackWithin {𝕜 : 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] {ι : Type u_5} [IsManifold I 1 M] (b : Module.Basis ι 𝕜 E) (x₀ : M) (i : ι) : Set.EqOn ((trivializationAt E (TangentSpace I) x₀).localFrame b i) (VectorField.mpullbackWithin I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x₀)) (fun (x : E) => b i) (extChartAt I x₀).source) (extChartAt I x₀).source

The local frame of the canonical trivialization is the coordinate frame of the chart. Over the source of the chart at x₀, the i-th section of the local frame induced by a basis b is the pullback, along the extended chart, of the constant model-space vector field with value b i.

theorem TauCeti.Manifold.mfderiv_extChartAt_localFrame_trivializationAt {𝕜 : 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] {ι : Type u_5} {x : M} [IsManifold I 1 M] (b : Module.Basis ι 𝕜 E) (x₀ : M) (hx : x ∈ (extChartAt I x₀).source) (i : ι) : (mfderiv% ↑(extChartAt I x₀) x) ((trivializationAt E (TangentSpace I) x₀).localFrame b i x) = b i

The chart reads the coordinate frame as the basis. At a point of the source of the chart at x₀, the derivative of the extended chart sends the i-th vector of the local frame induced by a basis b to b i.

theorem TauCeti.Manifold.mlieBracket_symm_trivializationAt {𝕜 : 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] {x : M} [CompleteSpace E] [IsManifold I (minSmoothness 𝕜 2) M] (x₀ : M) (hx : x ∈ (extChartAt I x₀).source) (v w : E) : VectorField.mlieBracket I (fun (y : M) => (trivializationAt E (TangentSpace I) x₀).symm y v) (fun (y : M) => (trivializationAt E (TangentSpace I) x₀).symm y w) x = 0

Vector fields with constant coordinates commute. Two vector fields whose coordinates in the canonical tangent-bundle trivialization at x₀ are constant have vanishing Lie bracket on the source of the chart at x₀.

theorem TauCeti.Manifold.mlieBracket_localFrame_trivializationAt {𝕜 : 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] {ι : Type u_5} {x : M} [CompleteSpace E] [IsManifold I (minSmoothness 𝕜 2) M] (b : Module.Basis ι 𝕜 E) (x₀ : M) (hx : x ∈ (extChartAt I x₀).source) (i j : ι) : VectorField.mlieBracket I ((trivializationAt E (TangentSpace I) x₀).localFrame b i) ((trivializationAt E (TangentSpace I) x₀).localFrame b j) x = 0

The coordinate frame of a chart commutes. The local frame that a basis of the model space induces through the canonical tangent-bundle trivialization at x₀ has vanishing Lie brackets on the source of the chart at x₀.