Tangent vectors as point derivations

A tangent vector acts on smooth scalar-valued functions by directional differentiation. This gives a canonical linear map from the ordinary tangent space to the algebraic point derivations.

Main results

• tangentToPointDerivation: the point derivation associated to a tangent vector.
• tangentToPointDerivation_injective: distinct tangent vectors induce distinct point derivations on finite-dimensional Hausdorff real manifolds.
• tangentToPointDerivation_surjective: at an interior point of a finite-dimensional Hausdorff real manifold, every point derivation comes from a tangent vector.
• pointDerivationEquivTangentSpace: the resulting canonical linear equivalence.
• PointDerivation.congr_of_eventuallyEq: on a finite-dimensional Hausdorff real manifold, a point derivation depends only on the germ of a smooth function at its basepoint.
• Derivation.apply_congr_of_eventuallyEq: derivations of smooth functions are local operators.
• tangentToPointDerivation_mfderiv: this association commutes with differentials.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 0, "The Lie algebra and the tangent space at 1".

noncomputable def tangentToPointDerivation {𝕜 : 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) : TangentSpace I x →ₗ[𝕜] PointDerivation I x

A tangent vector acts on smooth functions by directional differentiation.

@[simp]

theorem tangentToPointDerivation_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] (x : M) (v : TangentSpace I x) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤) : ((tangentToPointDerivation x) v) f = (d% ⇑f x) v

The point derivation associated to a tangent vector evaluates a smooth function by its directional derivative.

theorem tangentToPointDerivation_injective {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] (x : M) : Function.Injective ⇑(tangentToPointDerivation x)

On a finite-dimensional Hausdorff real manifold, smooth scalar-valued functions distinguish tangent vectors.

theorem PointDerivation.congr_of_eventuallyEq {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] {x : M} (v : PointDerivation I x) (f g : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (hfg : ⇑f =ᶠ[nhds x] ⇑g) : v f = v g

A point derivation on a finite-dimensional Hausdorff real manifold depends only on the germ of a smooth function at its basepoint.

theorem Derivation.apply_congr_of_eventuallyEq {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] (δ : Derivation ℝ (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤)) {f g : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤} {x : M} (hfg : ⇑f =ᶠ[nhds x] ⇑g) : (δ f) x = (δ g) x

Locality of derivations. On a finite-dimensional Hausdorff real manifold, a derivation of C^∞(M, ℝ) evaluated at x depends only on the germ of the function at x.

theorem tangentToPointDerivation_mfderiv {𝕜 : 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] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] (f : ContMDiffMap I I' M M' ↑⊤) (x : M) (v : TangentSpace I x) : (tangentToPointDerivation (f x)) ((mfderiv% ⇑f x) v) = (fdifferential f x) ((tangentToPointDerivation x) v)

Sending tangent vectors to point derivations commutes with the differential of a smooth map.

theorem tangentToPointDerivation_surjective {E : Type u_8} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_9} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] (x : M) (hx : I.IsInteriorPoint x) : Function.Surjective ⇑(tangentToPointDerivation x)

Every point derivation at an interior point of a finite-dimensional Hausdorff real manifold is directional differentiation along a tangent vector.

noncomputable def pointDerivationEquivTangentSpace {E : Type u_8} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_9} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] (x : M) (hx : I.IsInteriorPoint x) : PointDerivation I x ≃ₗ[ℝ] TangentSpace I x

Point derivations and tangent vectors are canonically linearly equivalent at an interior point of a finite-dimensional Hausdorff real manifold.

@[simp]

theorem pointDerivationEquivTangentSpace_symm_apply {E : Type u_8} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_9} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] (x : M) (hx : I.IsInteriorPoint x) (v : TangentSpace I x) : (pointDerivationEquivTangentSpace x hx).symm v = (tangentToPointDerivation x) v

The inverse of the point-derivation equivalence is directional differentiation.

@[simp]

theorem tangentToPointDerivation_pointDerivationEquivTangentSpace {E : Type u_8} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_9} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] (x : M) (hx : I.IsInteriorPoint x) (D : PointDerivation I x) : (tangentToPointDerivation x) ((pointDerivationEquivTangentSpace x hx) D) = D

Converting a point derivation to a tangent vector and back recovers the derivation.

@[simp]

theorem pointDerivationEquivTangentSpace_tangentToPointDerivation {E : Type u_8} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_9} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] (x : M) (hx : I.IsInteriorPoint x) (v : TangentSpace I x) : (pointDerivationEquivTangentSpace x hx) ((tangentToPointDerivation x) v) = v

Converting a tangent vector to a point derivation and back recovers the vector.

@[simp]

theorem pointDerivationEquivTangentSpace_fdifferential {E : Type u_8} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_9} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] {E' : Type u_11} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_12} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_13} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] [T2Space M'] (f : ContMDiffMap I I' M M' ↑⊤) (x : M) (hx : I.IsInteriorPoint x) (hfx : I'.IsInteriorPoint (f x)) (D : PointDerivation I x) : (pointDerivationEquivTangentSpace (f x) hfx) ((fdifferential f x) D) = (mfderiv% ⇑f x) ((pointDerivationEquivTangentSpace x hx) D)

The equivalence between point derivations and tangent vectors is natural under smooth maps.