The Lie derivative of differential forms on manifolds #
The Lie derivative mlieDerivFormWithin V φ s x of a rough fixed-coefficient form φ along a
vector field V is the flat Lie derivative TauCeti.lieDerivFormWithin of the coordinate
expressions of φ and V in the preferred chart at x, with derivatives taken within
(extChartAt I x).symm ⁻¹' s ∩ range I. This is the construction of mextDerivWithin and of
Mathlib's VectorField.mlieBracketWithin, so it is meaningful at boundary and corner points.
Like them, it is total, with junk values where φ or V is not differentiable, and needs no
flow.
The two characterizations below show that the definition is intrinsic.
- The bracket formula [Lee, Cor. 12.33]: on differentiable vector fields
X₀, …, Xₖ₋₁,L_V φ (X₀, …, Xₖ₋₁) = V (φ (X₀, …, Xₖ₋₁)) - ∑ i, φ (X₀, …, [V, Xᵢ], …, Xₖ₋₁). - Cartan's magic formula [Lee, Thm. 14.35]:
L_V φ = ι_V dφ + d (ι_V φ)for a differentiable form and a differentiable vector field, andL_V f = ι_V dfin degree zero without hypotheses. On a closed form it readsL_V φ = d (ι_V φ).
Main declarations #
TauCeti.mlieDerivFormWithin,TauCeti.mlieDerivForm: the Lie derivative of a rough form.TauCeti.mlieDerivFormWithin_add,TauCeti.mlieDerivFormWithin_smul: linearity in the form.TauCeti.mlieDerivFormWithin_add_left,TauCeti.mlieDerivForm_add_left: additivity in the vector field.TauCeti.mlieDerivFormWithin_apply_vectorField,TauCeti.mlieDerivForm_apply_vectorField: the bracket formula.TauCeti.mlieDerivForm_apply_one: the bracket formula for a one-form.TauCeti.mlieDerivFormWithin_eq_interior_mextDerivWithin_add,TauCeti.mlieDerivForm_eq_interior_mextDeriv_add: Cartan's magic formula.TauCeti.mlieDerivForm_apply_eq_mextDeriv_add: Cartan's magic formula for a one-form, evaluated on a tangent vector.TauCeti.mlieDerivFormWithin_eq_mextDerivWithin_interior,TauCeti.mlieDerivForm_eq_mextDeriv_interior: on closed forms,L_V φ = d (ι_V φ).TauCeti.mlieDerivFormWithin_eq_lieDerivFormWithin: over the model space, the manifold Lie derivative is the flat one.TauCeti.SmoothForm.mlieDerivForm_eq_interior_mextDeriv_add,TauCeti.SmoothForm.mlieDerivForm_eq_mextDeriv_interior: bundled smooth-form entry points.TauCeti.SmoothForm.mlieDerivForm_mem_smoothBundleForms: the Lie derivative of a smooth form along a smooth vector field is smooth.
References #
- John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Corollary 12.33 and Theorem 14.35.
The Lie derivative of a rough form along a vector field within a set s, at a point x: the
flat Lie derivative of the coordinate expressions of the form and of the field in the chart at
x, within (extChartAt I x).symm ⁻¹' s ∩ range I at the chart point of x. Tangent vectors at
x are read in that same chart. Total, with junk values where the form or the field is not
differentiable.
Instances For
The Lie derivative of a rough form along a vector field.
Instances For
Linearity in the form #
The Lie derivative within a set is additive on forms whose coordinate expressions in the chart at the point are differentiable there.
The Lie derivative is additive on forms whose coordinate expressions in the chart at the point
are differentiable within range I there.
The Lie derivative within a set commutes with real scalars wherever derivatives within the set are unique; no differentiability of the form is needed.
The model space #
Over the model space 𝓘(ℝ, E), the manifold Lie derivative within a set is the flat Lie
derivative lieDerivFormWithin.
Over the model space 𝓘(ℝ, E), the manifold Lie derivative is the flat Lie derivative
lieDerivForm.
Linearity in the vector field #
The Lie derivative within a set is additive in the vector field, at a point where both fields are differentiable within the set and derivatives within it are unique. No differentiability of the form is needed.
The Lie derivative is additive in the vector field, at a point where both fields are differentiable. No differentiability of the form is needed.
The bracket formula #
The bracket formula within a set: evaluated on differentiable vector fields
X₀, …, Xₖ₋₁, the Lie derivative of a differentiable form is the derivative of
φ (X₀, …, Xₖ₋₁) along V minus the evaluations of φ with one field Xᵢ replaced by the
bracket [V, Xᵢ]. No regularity of V is needed.
The bracket formula: evaluated on differentiable vector fields X₀, …, Xₖ₋₁, the Lie
derivative of a differentiable form is the derivative of φ (X₀, …, Xₖ₋₁) along V minus the
evaluations of φ with one field Xᵢ replaced by the bracket [V, Xᵢ].
The bracket formula for a one-form φ and a differentiable vector field W:
L_V φ (W) = V (φ (W)) - φ ([V, W]).
Cartan's magic formula #
Cartan's magic formula within a set, L_V φ = ι_V dφ + d (ι_V φ), for a form and a vector
field differentiable within the set at the point.
Cartan's magic formula at a point, L_V φ = ι_V dφ + d (ι_V φ), for a form and a vector
field differentiable at the point.
Cartan's magic formula for a one-form φ, evaluated on a tangent vector:
L_V φ (v) = dφ (V, v) + df (v), where the function f = φ(V) is the contraction ι_V φ.
Cartan's magic formula L_V = ι_V ∘ d + d ∘ ι_V on differentiable forms, along a
differentiable vector field.
For a form whose exterior derivative within the set vanishes at the point, Cartan's
formula within the set reduces to L_V φ = d (ι_V φ).
For a form whose exterior derivative vanishes at the point, Cartan's formula reduces to
L_V φ = d (ι_V φ).
On a differentiable closed form, along a differentiable vector field, Cartan's formula
reduces to L_V φ = d (ι_V φ).
Cartan's formula in degree zero within a set, L_V f = ι_V df, holds for every rough
0-form and every vector field.
Cartan's formula in degree zero, L_V f = ι_V df, holds for every rough 0-form and every
vector field.
Cartan's magic formula for a smooth fixed-coefficient form, exposed through the bundled
SmoothForm carrier. The vector field is supplied as a differentiable tangent-valued map.
On a smooth closed form, along a differentiable vector field, the Lie derivative is the exterior derivative of its contraction.
The Lie derivative of a smooth fixed-coefficient form along a smooth vector field is smooth.