Derivations of smooth functions are smooth vector fields

Differentiating along a smooth vector field X is a derivation f ↦ (x ↦ df_x (X x)) of the algebra of smooth scalar functions. On a finite-dimensional, Hausdorff, boundaryless real manifold every derivation of C^∞(M, ℝ) arises this way from a unique smooth vector field. No continuity of the derivation is assumed: at each point it is a point derivation, hence a tangent vector, and smoothness of the resulting field is read off from the values of the derivation on bump-localized coordinate functions.

Main definitions

• TauCeti.vectorFieldDerivation: the derivation of smooth functions given by differentiation along a smooth vector field, as a linear map in the vector field.
• TauCeti.lineDerivation: on a normed space, differentiation of smooth functions in a fixed direction, the derivation of a constant vector field.
• Derivation.vectorField: the tangent vector field of a derivation, read pointwise through pointDerivationEquivTangentSpace.
• TauCeti.derivationEquivSmoothVectorField: the C^∞(M, ℝ)-linear equivalence between derivations of C^∞(M, ℝ) and smooth vector fields.

Main results

• TauCeti.commute_lineDerivation: directional derivatives of smooth functions commute.
• Module.Basis.lineDerivation_smoothCoord: the partial derivatives along a basis are dual to its coordinate functions.
• Derivation.mvfderiv_vectorField: the inverse evaluation equation δ f x = df_x (X x).
• Derivation.contMDiff_vectorField: the vector field of a derivation is smooth.
• TauCeti.exists_derivationEquivSmoothVectorField: derivations of C^∞(M, ℝ) are C^∞(M, ℝ)-linearly equivalent to smooth vector fields, compatibly with the evaluation equation.
• Derivation.vectorField_smul: multiplying a derivation by a smooth function multiplies its vector field pointwise.
• Derivation.vectorField_lie: the commutator of derivations corresponds to the manifold Lie bracket of vector fields.

References

• I. Kolář, P. W. Michor, J. Slovák, Natural Operations in Differential Geometry, Springer, 1993, Lemma 3.3, p. 16.

noncomputable def TauCeti.vectorFieldDerivation {𝕜 : 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 (↑⊤) M] : ContMDiffSection I E (↑⊤) (TangentSpace I) →ₗ[𝕜] Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤)

Differentiation of smooth scalar functions along a smooth vector field X is a derivation: it sends f to the smooth function x ↦ df_x (X x).

@[simp]

theorem ContMDiffSection.vectorFieldDerivation_apply_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] [IsManifold I (↑⊤) M] (X : ContMDiffSection I E (↑⊤) (TangentSpace I)) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤) (x : M) : ((TauCeti.vectorFieldDerivation X) f) x = (d% ⇑f x) (X x)

The derivation of a smooth vector field differentiates a smooth function along the field.

noncomputable def TauCeti.lineDerivation (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (v : E) : Derivation 𝕜 (ContMDiffMap (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 𝕜) E 𝕜 ↑⊤) (ContMDiffMap (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 𝕜) E 𝕜 ↑⊤)

Differentiation of smooth functions on E in the direction v, f ↦ (x ↦ df_x v), as a derivation of C^∞(E): the derivation TauCeti.vectorFieldDerivation of the constant vector field v.

@[simp]

theorem TauCeti.lineDerivation_apply_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (v : E) (f : ContMDiffMap (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 𝕜) E 𝕜 ↑⊤) (x : E) : ((lineDerivation 𝕜 v) f) x = (fderiv 𝕜 (⇑f) x) v

theorem TauCeti.commute_lineDerivation {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (v w : E) : Commute ↑(lineDerivation 𝕜 v) ↑(lineDerivation 𝕜 w)

Directional derivatives of smooth functions commute, by the symmetry of second derivatives.

theorem Module.Basis.lineDerivation_smoothCoord {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ι : Type u_3} (b : Basis ι 𝕜 E) [DecidableEq ι] (i j : ι) : (TauCeti.lineDerivation 𝕜 (b i)) (b.smoothCoord j) = if j = i then 1 else 0

The partial derivatives along a basis are dual to its coordinate functions.

noncomputable def Derivation.vectorField {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [BoundarylessManifold I M] (δ : Derivation ℝ (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤)) (x : M) : TangentSpace I x

The tangent vector field of a derivation of smooth functions: at each point x, the derivation followed by evaluation at x is a point derivation, hence a tangent vector.

theorem Derivation.mvfderiv_vectorField {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [BoundarylessManifold I M] (δ : Derivation ℝ (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤)) (f : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (x : M) : (d% ⇑f x) (δ.vectorField x) = (δ f) x

Inverse evaluation. A derivation differentiates every smooth function along its vector field: δ f x = df_x (X x).

@[simp]

theorem Derivation.mfderiv_vectorField {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [BoundarylessManifold I M] (δ : Derivation ℝ (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤)) (f : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (x : M) : (mfderiv% ⇑f x) (δ.vectorField x) = (δ f) x

The inverse evaluation equation in the mfderiv normal form.

theorem Derivation.eq_vectorField_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [BoundarylessManifold I M] {δ : Derivation ℝ (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤)} {x : M} {v : TangentSpace I x} : v = δ.vectorField x ↔ ∀ (f : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤), (d% ⇑f x) v = (δ f) x

The value of the vector field of a derivation at x is the unique tangent vector along which every smooth function is differentiated by the derivation at x.

@[simp]

theorem Derivation.vectorField_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [BoundarylessManifold I M] (x : M) : vectorField 0 x = 0

The zero derivation has the zero vector field.

@[simp]

theorem Derivation.vectorField_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [BoundarylessManifold I M] (δ₁ δ₂ : Derivation ℝ (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤)) (x : M) : (δ₁ + δ₂).vectorField x = δ₁.vectorField x + δ₂.vectorField x

The vector field of a sum of derivations is the sum of their vector fields.

@[simp]

theorem Derivation.vectorField_const_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [BoundarylessManifold I M] (r : ℝ) (δ : Derivation ℝ (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤)) (x : M) : (r • δ).vectorField x = r • δ.vectorField x

The vector field of a real multiple of a derivation is the same multiple of its vector field.

theorem Derivation.contMDiff_vectorField {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [BoundarylessManifold I M] (δ : Derivation ℝ (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤)) : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, δ.vectorField x⟩

Smoothness of the vector field of a derivation. In the chart at x₀, the coordinates of δ.vectorField are the values of δ on bump-localized coordinate functions, which are smooth because δ takes values in smooth functions.

@[simp]

theorem Derivation.vectorField_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [BoundarylessManifold I M] (g : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (δ : Derivation ℝ (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤)) (x : M) : (g • δ).vectorField x = g x • δ.vectorField x

Multiplying a derivation by a smooth function multiplies its vector field pointwise.

theorem Derivation.vectorField_lie {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [BoundarylessManifold I M] (δ₁ δ₂ : Derivation ℝ (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤)) (x : M) : ⁅δ₁, δ₂⁆.vectorField x = VectorField.mlieBracket I δ₁.vectorField δ₂.vectorField x

Commutators of derivations are Lie brackets. The vector field of the commutator of two derivations is the manifold Lie bracket of their vector fields.

@[simp]

theorem ContMDiffSection.vectorField_vectorFieldDerivation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [BoundarylessManifold I M] (X : ContMDiffSection I E (↑⊤) (TangentSpace I)) (x : M) : (TauCeti.vectorFieldDerivation X).vectorField x = X x

The vector field of the derivation along a smooth vector field is that field.

noncomputable def TauCeti.derivationEquivSmoothVectorField {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [BoundarylessManifold I M] : Derivation ℝ (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) ≃ₗ[ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤] ContMDiffSection I E (↑⊤) (TangentSpace I)

Derivations are smooth vector fields. On a finite-dimensional, Hausdorff, boundaryless real manifold, sending a derivation of C^∞(M, ℝ) to its vector field is a C^∞(M, ℝ)-linear equivalence onto the smooth sections of the tangent bundle; its inverse differentiates along the field. No continuity of the derivations is assumed.

theorem TauCeti.exists_derivationEquivSmoothVectorField {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [BoundarylessManifold I M] : ∃ (e : Derivation ℝ (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) ≃ₗ[ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤] ContMDiffSection I E (↑⊤) (TangentSpace I)), ∀ (δ : Derivation ℝ (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤)) (f : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (x : M), (δ f) x = (d% ⇑f x) ((e δ) x)

Derivations and smooth vector fields. On a finite-dimensional, Hausdorff, boundaryless real manifold there is a C^∞(M, ℝ)-linear equivalence between derivations of C^∞(M, ℝ) and smooth vector fields under which δ f x = df_x (X x).

@[simp]

theorem Derivation.derivationEquivSmoothVectorField_apply_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [BoundarylessManifold I M] (δ : Derivation ℝ (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤)) (x : M) : (TauCeti.derivationEquivSmoothVectorField δ) x = δ.vectorField x

The equivalence sends a derivation to its vector field.

theorem Derivation.coe_derivationEquivSmoothVectorField {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [BoundarylessManifold I M] (δ : Derivation ℝ (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤)) : ⇑(TauCeti.derivationEquivSmoothVectorField δ) = δ.vectorField

The equivalence sends a derivation to its vector field, as functions.

@[simp]

theorem ContMDiffSection.derivationEquivSmoothVectorField_symm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [BoundarylessManifold I M] (X : ContMDiffSection I E (↑⊤) (TangentSpace I)) : TauCeti.derivationEquivSmoothVectorField.symm X = TauCeti.vectorFieldDerivation X

The inverse equivalence sends a smooth vector field to differentiation along it.