Model-space and directional-derivative formulas for the manifold Lie bracket

This file transports Mathlib's normed-space identity fderivWithin_apply_lieBracket through a manifold chart. It identifies the differential of a vector-valued function on the manifold Lie bracket with the commutator of its directional derivatives. It also records that constant vector fields on a model space have zero manifold Lie bracket.

The chart argument follows the pullback idiom used for the manifold bracket in Mathlib/Geometry/Manifold/VectorField/LieBracket.lean. The resulting lemma is a general manifold prerequisite for Deliverable A, Layer 1 of the Lie-groups roadmap.

Main results

• VectorField.mlieBracket_eq_lieBracket: on a normed space, the manifold Lie bracket is the Lie bracket of vector fields on that space.
• VectorField.mlieBracket_const_model_space: constant model-space vector fields have zero manifold Lie bracket.
• VectorField.mlieBracket_continuousLinearMap_model_space: the manifold Lie bracket of the linear vector fields y ↦ A y and y ↦ B y is x ↦ B (A x) - A (B x).
• mvfderiv_mlieBracket: a differential sends the manifold bracket to the commutator of directional derivatives.
• TauCeti.mvfderiv_div_mvfderiv_sub_eq_mlieBracket: the logarithmic differential df / f of a nonvanishing function is closed, i.e. X (df(Y) / f) - Y (df(X) / f) = df([X, Y]) / f.
• TauCeti.eq_mlieBracket_of_mvfderiv_extChartAt: tested against the extended chart at a point, this identity characterises the manifold bracket at that point.
• VectorField.lieBracketWithin_mpullbackWithin_extChartAt_symm: at the chart centre, the flat bracket of the coordinate expressions of two fields is their manifold bracket.
• VectorField.lieBracketWithin_neg_right and VectorField.mlieBracket_neg_right: the flat and manifold brackets are odd in their second argument.
• VectorField.mlieBracket_neg_left: the manifold bracket is odd in its first argument.
• VectorField.jacobi_identity_mlieBracket_apply: the cyclic Jacobi identity for the manifold bracket.
• VectorField.contMDiff_mlieBracket: the bracket of two smooth vector fields is smooth.

References

• Mathlib/Analysis/Calculus/VectorField.lean, theorem fderivWithin_apply_lieBracket.
• Mathlib/Geometry/Manifold/VectorField/LieBracket.lean, for the chart-transport construction.
• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1.

theorem VectorField.mlieBracket_eq_lieBracket {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V W : (y : F) → TangentSpace (modelWithCornersSelf 𝕜 F) y} : mlieBracket (modelWithCornersSelf 𝕜 F) V W = lieBracket 𝕜 V W

On a normed space, the manifold Lie bracket of two vector fields is their Lie bracket as maps of the space.

@[simp]

theorem VectorField.mlieBracket_const_left_model_space {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (a : F) (W : (y : F) → TangentSpace (modelWithCornersSelf 𝕜 F) y) (x : F) : mlieBracket (modelWithCornersSelf 𝕜 F) (fun (x : F) => a) W x = (fderiv 𝕜 W x) a

The manifold Lie bracket of a constant vector field a with a vector field W on a normed space is the derivative of W in the direction a.

@[simp]

theorem VectorField.mlieBracket_const_model_space {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (a b x : F) : mlieBracket (modelWithCornersSelf 𝕜 F) (fun (x : F) => a) (fun (x : F) => b) x = 0

Constant vector fields on a normed vector space have zero manifold Lie bracket.

@[simp]

theorem VectorField.mlieBracket_const_right_model_space {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (V : (y : F) → TangentSpace (modelWithCornersSelf 𝕜 F) y) (b x : F) : mlieBracket (modelWithCornersSelf 𝕜 F) V (fun (x : F) => b) x = -(fderiv 𝕜 V x) b

The manifold Lie bracket of a vector field V with a constant vector field b on a normed space is minus the derivative of V in the direction b.

theorem VectorField.mlieBracket_continuousLinearMap_model_space {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (A B : F →L[𝕜] F) (x : F) : mlieBracket (modelWithCornersSelf 𝕜 F) (fun (y : F) => A y) (fun (y : F) => B y) x = B (A x) - A (B x)

The manifold Lie bracket of the linear vector fields y ↦ A y and y ↦ B y on a normed vector space is the linear vector field x ↦ B (A x) - A (B x).

theorem mvfderiv_mlieBracket {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (minSmoothness 𝕜 2) M] {f : M → F} {V W : (x : M) → TangentSpace I x} {x : M} (hf : ContMDiffAt I (modelWithCornersSelf 𝕜 F) n f x) (hn : minSmoothness 𝕜 2 ≤ n) (hV : (MDiffAt fun (y : M) => ⟨y, V y⟩) x) (hW : (MDiffAt fun (y : M) => ⟨y, W y⟩) x) : (d% f x) (VectorField.mlieBracket I V W x) = ((d% fun (y : M) => (d% f y) (W y)) x) (V x) - ((d% fun (y : M) => (d% f y) (V y)) x) (W x)

Let f have enough derivatives for symmetry of its second derivative at x, and let V and W be differentiable vector fields there. Then the differential of f on the manifold bracket is the commutator of its directional derivatives. This is the manifold counterpart of Mathlib's fderivWithin_apply_lieBracket.

theorem TauCeti.mvfderiv_div_mvfderiv_sub_eq_mlieBracket {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (minSmoothness 𝕜 2) M] {n : WithTop ℕ∞} {f : M → 𝕜} {X Y : (x : M) → TangentSpace I x} {p : M} (hf : ContMDiffAt I (modelWithCornersSelf 𝕜 𝕜) n f p) (hn : minSmoothness 𝕜 2 ≤ n) (hX : (MDiffAt fun (x : M) => ⟨x, X x⟩) p) (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) p) (hp : f p ≠ 0) : ((d% fun (x : M) => (d% f x) (Y x) / f x) p) (X p) - ((d% fun (x : M) => (d% f x) (X x) / f x) p) (Y p) = (d% f p) (VectorField.mlieBracket I X Y p) / f p

The second derivatives of a scalar function f cancel in the commutator of the logarithmic differentials df(U) / f: the logarithmic differential is closed, so X (df(Y) / f) - Y (df(X) / f) = df([X, Y]) / f at a point p where f is C^n with minSmoothness 𝕜 2 ≤ n and nonzero and the vector fields X, Y are differentiable.

theorem TauCeti.eq_mlieBracket_of_mvfderiv_extChartAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (minSmoothness 𝕜 2) M] {V W : (y : M) → TangentSpace I y} {x : M} (hV : (MDiffAt fun (y : M) => ⟨y, V y⟩) x) (hW : (MDiffAt fun (y : M) => ⟨y, W y⟩) x) {v : TangentSpace I x} (hv : (d% ↑(extChartAt I x) x) v = ((d% fun (y : M) => (d% ↑(extChartAt I x) y) (W y)) x) (V x) - ((d% fun (y : M) => (d% ↑(extChartAt I x) y) (V y)) x) (W x)) : v = VectorField.mlieBracket I V W x

A tangent vector v at x is the Lie bracket of the differentiable vector fields V and W at x as soon as the differential of the extended chart at x sends v to the commutator of the directional derivatives of the chart along V and W, since that differential is injective.

theorem VectorField.lieBracketWithin_mpullbackWithin_extChartAt_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] (V W : (y : M) → TangentSpace I y) (s : Set M) (x : M) : lieBracketWithin 𝕜 (mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) V (Set.range ↑I)) (mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) W (Set.range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x) = mlieBracketWithin I V W s x

At the centre of the preferred chart, the Lie bracket of the inverse-chart pullbacks of two vector fields is their manifold Lie bracket.

theorem VectorField.lieBracketWithin_neg_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {x : E} (hs : UniqueDiffWithinAt 𝕜 s x) : lieBracketWithin 𝕜 V (-W) s x = -lieBracketWithin 𝕜 V W s x

On a normed space, negating the second vector field negates the Lie bracket at any point where the set has unique derivatives.

theorem VectorField.mlieBracket_neg_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] {V W : (y : M) → TangentSpace I y} {x : M} : mlieBracket I V (-W) x = -mlieBracket I V W x

Negating the second vector field negates the manifold Lie bracket.

theorem VectorField.mlieBracket_neg_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] {V W : (y : M) → TangentSpace I y} {x : M} : mlieBracket I (-V) W x = -mlieBracket I V W x

Negating the first vector field negates the manifold Lie bracket.

theorem VectorField.jacobi_identity_mlieBracket_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (minSmoothness 𝕜 3) M] {U V W : (y : M) → TangentSpace I y} {x : M} (hU : ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun (y : M) => ⟨y, U y⟩) x) (hV : ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun (y : M) => ⟨y, V y⟩) x) (hW : ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun (y : M) => ⟨y, W y⟩) x) : mlieBracket I U (mlieBracket I V W) x + mlieBracket I V (mlieBracket I W U) x + mlieBracket I W (mlieBracket I U V) x = 0

The Jacobi identity for the manifold Lie bracket, in cyclic form: [U, [V, W]] + [V, [W, U]] + [W, [U, V]] = 0. This rearranges Mathlib's Leibniz form leibniz_identity_mlieBracket_apply.

theorem VectorField.contMDiff_mlieBracket {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] [IsRCLikeNormedField 𝕜] [IsManifold I (↑⊤) M] {V W : (y : M) → TangentSpace I y} (hV : ContMDiff I I.tangent ↑⊤ fun (y : M) => ⟨y, V y⟩) (hW : ContMDiff I I.tangent ↑⊤ fun (y : M) => ⟨y, W y⟩) : ContMDiff I I.tangent ↑⊤ fun (x₀ : M) => ⟨x₀, mlieBracket I V W x₀⟩

The Lie bracket of two smooth vector fields is smooth.