Lie brackets of related vector fields

Let f : N → M be a map of manifolds. A vector field V on N and a vector field V' on M are f-related when df_z (V z) = V' (f z) for every z. The Lie bracket is natural for this relation: if V, V' and W, W' are f-related, then so are [V, W] and [V', W']. This file proves the pointwise form of this statement, with the relations only assumed near the point.

Unlike Mathlib's VectorField.mpullback_mlieBracket, no invertibility of the derivative of f is assumed, so the statement applies to maps that are neither immersions nor submersions. The basic example is the orbit map g ↦ g • x of a Lie group action, which relates the right-invariant vector fields of the group to the fundamental vector fields of the action.

Main results

• TauCeti.mfderiv_mlieBracket_of_eventually_related: if V, V' and W, W' are f-related near y, then df_y ([V, W] y) = [V', W'] (f y).

References

• John M. Lee, Introduction to Smooth Manifolds, second edition, Graduate Texts in Mathematics 218, Springer, 2013, Chapter 8 (naturality of the Lie bracket for F-related vector fields).

theorem TauCeti.mfderiv_mlieBracket_of_eventually_related {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (minSmoothness 𝕜 2) M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [CompleteSpace E'] {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J (minSmoothness 𝕜 2) N] {f : N → M} {V W : (y : N) → TangentSpace J y} {V' W' : (x : M) → TangentSpace I x} {y : N} (hf : ContMDiffAt J I n f y) (hn : minSmoothness 𝕜 2 ≤ n) (hV : (MDiffAt fun (y : N) => ⟨y, V y⟩) y) (hW : (MDiffAt fun (y : N) => ⟨y, W y⟩) y) (hV' : (MDiffAt fun (x : M) => ⟨x, V' x⟩) (f y)) (hW' : (MDiffAt fun (x : M) => ⟨x, W' x⟩) (f y)) (hVV' : ∀ᶠ (z : N) in nhds y, (mfderiv% f z) (V z) = V' (f z)) (hWW' : ∀ᶠ (z : N) in nhds y, (mfderiv% f z) (W z) = W' (f z)) : (mfderiv% f y) (VectorField.mlieBracket J V W y) = VectorField.mlieBracket I V' W' (f y)

Naturality of the Lie bracket. Let f : N → M be C² at y, and let the differentiable vector fields V, W on N be f-related near y to the vector fields V', W' on M, which are differentiable at f y: df_z (V z) = V' (f z) and df_z (W z) = W' (f z) for z near y. Then df_y ([V, W] y) = [V', W'] (f y).