Exterior differentiation evaluated on vector fields

The invariant formula for the exterior derivative expresses its evaluation on differentiable vector fields as an alternating sum of directional derivatives and a sum of Lie-bracket terms. It is useful when the fields are adapted to a distribution rather than to a coordinate chart. For pairwise commuting fields, such as a coordinate frame, the bracket terms drop out and the formula holds in every degree (TauCeti.mextDeriv_apply_vectorField_of_mlieBracket_eq_zero). The within-set statements also apply at boundary and corner points.

For vector fields V and W tangent to the kernel of a real one-form α near x, the formula reduces to α_x ([V, W]_x) = -dα_x (V_x, W_x) (TauCeti.RoughForm.apply_mlieBracket_eq_neg_mextDeriv), so the bracket stays in the kernel exactly when dα vanishes on the fields (TauCeti.RoughForm.mlieBracket_mem_ker_iff).

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Proposition 14.29 and Proposition 14.32.
• Mathlib's extDerivWithin_apply_vectorField, the flat invariant formula transported here through the preferred extended chart.

theorem TauCeti.fderivWithin_inChartAt_apply_mpullbackWithin {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {k : ℕ} {s : Set M} {x : M} (φ : RoughForm I M F k) (V : Fin k → (y : M) → TangentSpace I y) (hφ : DifferentiableWithinAt ℝ (φ.inChartAt x) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)) (hV : ∀ (i : Fin k), DifferentiableWithinAt ℝ (VectorField.mpullbackWithin (modelWithCornersSelf ℝ E) I (↑(extChartAt I x).symm) (V i) (Set.range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)) : fderivWithin ℝ (fun (z : E) => (φ.inChartAt x z) fun (i : Fin k) => VectorField.mpullbackWithin (modelWithCornersSelf ℝ E) I (↑(extChartAt I x).symm) (V i) (Set.range ↑I) z) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x) = (d[s] fun (y : M) => (φ y) fun (x : Fin k) => V x y) x

In the preferred chart at x, differentiating the evaluation of a form's coordinate expression on the coordinate expressions of vector fields gives the manifold derivative of the evaluation of the form on the fields.

theorem TauCeti.mextDerivWithin_apply_vectorField {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {s : Set M} {x : M} {n : ℕ} {φ : RoughForm I M F (n + 1)} {V : Fin (n + 2) → (y : M) → TangentSpace I y} (hφ : (MDiffAt[s] fun (y : M) => ⟨y, φ y⟩) x) (hV : ∀ (i : Fin (n + 2)), (MDiffAt[s] fun (y : M) => ⟨y, V i y⟩) x) (hs : UniqueMDiffAt[s] x) : ((mextDerivWithin φ s x) fun (x_1 : Fin (n + 1 + 1)) => V x_1 x) = ∑ i : Fin (n + 2), (-1) ^ ↑i • ((d[s] fun (y : M) => (φ y) (i.removeNth fun (x : Fin (n + 1 + 1)) => V x y)) x) (V i x) - ∑ i : Fin (n + 1), ∑ j ≥ i, (-1) ^ (↑i + ↑j) • (φ x) (Matrix.vecCons (VectorField.mlieBracketWithin I (V i.castSucc) (V j.succ) s x) (j.removeNth (i.castSucc.removeNth fun (x_1 : Fin (n + 1 + 1)) => V x_1 x)))

The invariant exterior-derivative formula within a subset, in positive degree. The bracket sum uses pairs (i.castSucc, j.succ) with i ≤ j, so its sign is the negative of the usual sum indexed by strictly increasing pairs.

theorem TauCeti.mextDeriv_apply_vectorField {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {x : M} {n : ℕ} {φ : RoughForm I M F (n + 1)} {V : Fin (n + 2) → (y : M) → TangentSpace I y} (hφ : (MDiffAt fun (y : M) => ⟨y, φ y⟩) x) (hV : ∀ (i : Fin (n + 2)), (MDiffAt fun (y : M) => ⟨y, V i y⟩) x) : ((mextDeriv φ x) fun (x_1 : Fin (n + 1 + 1)) => V x_1 x) = ∑ i : Fin (n + 2), (-1) ^ ↑i • ((d% fun (y : M) => (φ y) (i.removeNth fun (x : Fin (n + 1 + 1)) => V x y)) x) (V i x) - ∑ i : Fin (n + 1), ∑ j ≥ i, (-1) ^ (↑i + ↑j) • (φ x) (Matrix.vecCons (VectorField.mlieBracket I (V i.castSucc) (V j.succ) x) (j.removeNth (i.castSucc.removeNth fun (x_1 : Fin (n + 1 + 1)) => V x_1 x)))

The invariant exterior-derivative formula on positive-degree forms. Each directional term differentiates the scalar or vector-valued evaluation of the form on the other fields.

theorem TauCeti.mextDeriv_apply_vectorField_of_mlieBracket_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {x : M} {n : ℕ} {φ : RoughForm I M F n} {V : Fin (n + 1) → (y : M) → TangentSpace I y} (hφ : (MDiffAt fun (y : M) => ⟨y, φ y⟩) x) (hV : ∀ (i : Fin (n + 1)), (MDiffAt fun (y : M) => ⟨y, V i y⟩) x) (hVV : ∀ (i j : Fin (n + 1)), VectorField.mlieBracket I (V i) (V j) x = 0) : ((mextDeriv φ x) fun (x_1 : Fin (n + 1)) => V x_1 x) = ∑ i : Fin (n + 1), (-1) ^ ↑i • ((d% fun (y : M) => (φ y) (i.removeNth fun (x : Fin (n + 1)) => V x y)) x) (V i x)

The invariant exterior-derivative formula for pairwise commuting vector fields, in every degree: dφ(V₀, …, Vₙ) = ∑ᵢ (-1)ⁱ Vᵢ(φ(V₀, …, V̂ᵢ, …, Vₙ)).

theorem TauCeti.mextDerivWithin_apply_one {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {s : Set M} {x : M} {φ : RoughForm I M F 1} {V W : (y : M) → TangentSpace I y} (hφ : (MDiffAt[s] fun (y : M) => ⟨y, φ y⟩) x) (hV : (MDiffAt[s] fun (y : M) => ⟨y, V y⟩) x) (hW : (MDiffAt[s] fun (y : M) => ⟨y, W y⟩) x) (hs : UniqueMDiffAt[s] x) : (mextDerivWithin φ s x) ![V x, W x] = ((d[s] fun (y : M) => (φ y) ![W y]) x) (V x) - ((d[s] fun (y : M) => (φ y) ![V y]) x) (W x) - (φ x) ![VectorField.mlieBracketWithin I V W s x]

The exterior derivative of a one-form on two differentiable vector fields, within a subset: dφ(V, W) = V(φ(W)) - W(φ(V)) - φ([V, W]).

theorem TauCeti.mextDeriv_apply_one {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {x : M} {φ : RoughForm I M F 1} {V W : (y : M) → TangentSpace I y} (hφ : (MDiffAt fun (y : M) => ⟨y, φ y⟩) x) (hV : (MDiffAt fun (y : M) => ⟨y, V y⟩) x) (hW : (MDiffAt fun (y : M) => ⟨y, W y⟩) x) : (mextDeriv φ x) ![V x, W x] = ((d% fun (y : M) => (φ y) ![W y]) x) (V x) - ((d% fun (y : M) => (φ y) ![V y]) x) (W x) - (φ x) ![VectorField.mlieBracket I V W x]

For a one-form and vector fields differentiable at a point, the exterior derivative is the commutator of directional evaluations, corrected by evaluating the form on the Lie bracket.

theorem TauCeti.mextDeriv_apply_two {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {x : M} {φ : RoughForm I M F 2} {U V W : (y : M) → TangentSpace I y} (hφ : (MDiffAt fun (y : M) => ⟨y, φ y⟩) x) (hU : (MDiffAt fun (y : M) => ⟨y, U y⟩) x) (hV : (MDiffAt fun (y : M) => ⟨y, V y⟩) x) (hW : (MDiffAt fun (y : M) => ⟨y, W y⟩) x) : (mextDeriv φ x) ![U x, V x, W x] = ((d% fun (y : M) => (φ y) ![V y, W y]) x) (U x) - ((d% fun (y : M) => (φ y) ![U y, W y]) x) (V x) + ((d% fun (y : M) => (φ y) ![U y, V y]) x) (W x) - (φ x) ![VectorField.mlieBracket I U V x, W x] + (φ x) ![VectorField.mlieBracket I U W x, V x] - (φ x) ![VectorField.mlieBracket I V W x, U x]

For a two-form and three vector fields differentiable at a point, the invariant formula dφ(U, V, W) = U(φ(V, W)) - V(φ(U, W)) + W(φ(U, V)) - φ([U, V], W) + φ([U, W], V) - φ([V, W], U).

theorem TauCeti.RoughForm.apply_mlieBracket_eq_neg_mextDeriv {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {x : M} {α : RoughForm I M ℝ 1} {V W : (y : M) → TangentSpace I y} (hα : (MDiffAt fun (y : M) => ⟨y, α y⟩) x) (hV : (MDiffAt fun (y : M) => ⟨y, V y⟩) x) (hW : (MDiffAt fun (y : M) => ⟨y, W y⟩) x) (hVα : ∀ᶠ (y : M) in nhds x, V y ∈ α.ker y) (hWα : ∀ᶠ (y : M) in nhds x, W y ∈ α.ker y) : (α x) ![VectorField.mlieBracket I V W x] = -(mextDeriv α x) ![V x, W x]

Cartan's formula for the Levi form. For vector fields V and W tangent to the kernel of a one-form α near x, α_x ([V, W]_x) = -dα_x (V_x, W_x).

theorem TauCeti.RoughForm.mlieBracket_mem_ker_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {x : M} {α : RoughForm I M ℝ 1} {V W : (y : M) → TangentSpace I y} (hα : (MDiffAt fun (y : M) => ⟨y, α y⟩) x) (hV : (MDiffAt fun (y : M) => ⟨y, V y⟩) x) (hW : (MDiffAt fun (y : M) => ⟨y, W y⟩) x) (hVα : ∀ᶠ (y : M) in nhds x, V y ∈ α.ker y) (hWα : ∀ᶠ (y : M) in nhds x, W y ∈ α.ker y) : VectorField.mlieBracket I V W x ∈ α.ker x ↔ (mextDeriv α x) ![V x, W x] = 0

For vector fields V and W tangent to the kernel of a one-form α near x, the bracket [V, W]_x lies in ker α_x exactly when dα_x (V_x, W_x) = 0.

theorem TauCeti.SmoothForm.mextDeriv_apply_vectorField {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {x : M} {n : ℕ} {φ : SmoothForm I M F (n + 1)} {V : Fin (n + 2) → (y : M) → TangentSpace I y} (hV : ∀ (i : Fin (n + 2)), (MDiffAt fun (y : M) => ⟨y, V i y⟩) x) : ((mextDeriv (↑φ) x) fun (x_1 : Fin (n + 1 + 1)) => V x_1 x) = ∑ i : Fin (n + 2), (-1) ^ ↑i • ((d% fun (y : M) => (↑φ y) (i.removeNth fun (x : Fin (n + 1 + 1)) => V x y)) x) (V i x) - ∑ i : Fin (n + 1), ∑ j ≥ i, (-1) ^ (↑i + ↑j) • (↑φ x) (Matrix.vecCons (VectorField.mlieBracket I (V i.castSucc) (V j.succ) x) (j.removeNth (i.castSucc.removeNth fun (x_1 : Fin (n + 1 + 1)) => V x_1 x)))

The invariant exterior-derivative formula for a bundled smooth form.

theorem TauCeti.SmoothForm.mextDeriv_apply_one {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {x : M} {φ : SmoothForm I M F 1} {V W : (y : M) → TangentSpace I y} (hV : (MDiffAt fun (y : M) => ⟨y, V y⟩) x) (hW : (MDiffAt fun (y : M) => ⟨y, W y⟩) x) : (mextDeriv (↑φ) x) ![V x, W x] = ((d% fun (y : M) => (↑φ y) ![W y]) x) (V x) - ((d% fun (y : M) => (↑φ y) ![V y]) x) (W x) - (↑φ x) ![VectorField.mlieBracket I V W x]

The invariant formula for the exterior derivative of a bundled smooth one-form.

theorem TauCeti.SmoothForm.mextDeriv_apply_two {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {x : M} {φ : SmoothForm I M F 2} {U V W : (y : M) → TangentSpace I y} (hU : (MDiffAt fun (y : M) => ⟨y, U y⟩) x) (hV : (MDiffAt fun (y : M) => ⟨y, V y⟩) x) (hW : (MDiffAt fun (y : M) => ⟨y, W y⟩) x) : (mextDeriv (↑φ) x) ![U x, V x, W x] = ((d% fun (y : M) => (↑φ y) ![V y, W y]) x) (U x) - ((d% fun (y : M) => (↑φ y) ![U y, W y]) x) (V x) + ((d% fun (y : M) => (↑φ y) ![U y, V y]) x) (W x) - (↑φ x) ![VectorField.mlieBracket I U V x, W x] + (↑φ x) ![VectorField.mlieBracket I U W x, V x] - (↑φ x) ![VectorField.mlieBracket I V W x, U x]

The invariant formula for the exterior derivative of a bundled smooth two-form on three vector fields: dφ(U, V, W) = U(φ(V, W)) - V(φ(U, W)) + W(φ(U, V)) - φ([U, V], W) + φ([U, W], V) - φ([V, W], U).