Product rule for Lie Bracket of vector fields

Stream: Is there code for X?

[Jens Lindekamp]

I'm currently reading through the API for Lie brackets of vector fields on vector spaces and on manifolds. Both seem to lack statements about [X, f*Y] = df(X) * Y + f * [X, Y] (aka product rule).

Is this missing? And if so, worth adding?

On vector spaces, it should follow more or less directly from the definition and the product rule for the Fréchet derivative.

Further I wonder whether it is proven that the definition of the Lie bracket on manifolds is actually well-defined and how one would formalize it. The Lie bracket on manifolds is defined in terms of a chart - but if we have two charts at a point - who guarantees that the result is the same?

[Eric Wieser]

Can you state this a little more explicitly with the types of f, X, and Y?

[Michael Rothgang]

Product rule: that definitely seems worth adding (if it is indeed missing; I didn't search hard)

[Michael Rothgang]

Well-definedness is actually not an issue --- mathlib's definition is slightly different from how you describe it.

In textbooks, manifolds are usually defined as "there is a compatible atlas"; around each point, there is a manifold chart around this point (and in proofs, you choose some charts, and need to argue your result is independent of the choice of charts).
Mathlib's definition is slightly different. As part of the data of a manifold, there is a preferred chart at each point. The Lie bracket on manifolds is defined point-wise using these preferred charts. There is thus no arbitrary choice and no need to check anything about well-definedness.

[Michael Rothgang]

Granted, this definition may be a bit unexpected (coming from textbook mathematics) --- but this has all the usual properties, it is (for instance) alternating, anti-symmetric and satisfies the Leibniz identity.

[Jens Lindekamp]

Agree to the preferred chart and being well-defined, but what happens when you move from one point to another point with different preferred charts? “Suddenly” / “somewhere in between” you have a different chart and one would need to prove that the lie bracket is well behaved at this point. Which it is, because of smooth coordinate changes and compatibility with pullbacks.

But how is this hidden in Mathlib?

[Jens Lindekamp]

Concerning the product rule: I will try to formalize the statement in a mwe tomorrow.

[Sébastien Gouëzel]

You're absolutely right that, to prove anything nontrivial on the Lie bracket of vector fields on manifolds, for instance its smoothness, we need to know that it is canonical, i.e., it does not depend on the chart. An equivalent way to say it is to say that the Lie bracket is invariant under local diffeomorphisms (because then applying this invariance to the composition of two charts says that using one chart or the other will end up with the same result).

The invariance of the Lie bracket of vector fields in vector spaces is docs#VectorField.pullback_lieBracket . This one is then leveraged to get invariance in manifolds, in docs#VectorField.mpullback_mlieBracket . Which in turn is used to show that the Lie bracket of two smooth vector fields is smooth, in docs#ContMDiffAt.mlieBracket_vectorField .

[Sébastien Gouëzel]

(You can have a look at the comment at the beginning of the proof of docs#ContMDiffWithinAt.mlieBracketWithin_vectorField, which repeats exactly what you were saying)

[Jens Lindekamp]

This is my idea to formalize the product rule; there would also be variants of it. Probably we could also relax the hypothesis for the vector fields and the function.

import Mathlib.Geometry.Manifold.IsManifold.Basic
import Mathlib.Geometry.Manifold.VectorField.LieBracket

open Manifold VectorField Bundle

variable
  (n : WithTop ℕ∞)
  {𝕜 : Type*} [NontriviallyNormedField 𝕜]
  {H : Type*} [TopologicalSpace H]
  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H}
  {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M]

/--
Product rule for Lie Brackets:Given two differentiable vector fields `V W : Π (x:M), TangentSpace I x` and a diffentiable function `f:M → 𝕜`, we have `[V, f • W] = (df V) • W + f • [V, W]`
-/
theorem mlieBracketWithinAt_fmul_right
  (f : M → 𝕜)
  (V W : Π (x:M), TangentSpace I x)
  (s : Set M) (x₀ : M)
  (hV : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2)
      (fun x ↦ (V x : TangentBundle I M)) s x₀)
  (hW : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2)
      (fun x ↦ (V x : TangentBundle I M)) s x₀)
  (hf : ContMDiffWithinAt I 𝓘(𝕜, 𝕜) (minSmoothness 𝕜 2) f s x₀):
  mlieBracketWithin I V (f • W) s x₀ = (mfderivWithin I 𝓘(𝕜, 𝕜) f s x₀) (V x₀) • (W x₀)  + (f • mlieBracketWithin I V W s) x₀ := by
  sorry

[Sébastien Gouëzel]

That's definitely the right kind of statement. You will probably need an additional uniqueDiffAt assumption on s, and you can probably weaken the assumption on f to differentiability.

If you want to try your hands on a proof, my advice would be to first prove it in vector spaces (where everything is more concrete, therefore easier) and then pull it back to the manifold using the chart and invariance of the Lie bracket under diffeos.

[Jens Lindekamp]

first prove it in vector spaces (where everything is more concrete

I thought so.

[Jens Lindekamp]

Actually, the proofs on vector spaces are done. Could you me write access to the repo so that I could push my branch (jkanschik on github)?

[Johan Commelin]

@Jens Lindekamp you may view your invitation here: https://github.com/leanprover-community/mathlib4/invitations

[Michael Rothgang]

@Jens Lindekamp Thanks again for your pull request #24932. Patrick Massot and I are working on covariant derivatives right now, and will have the Levi-Civita connection defined soon. Completing all the sorries requires #24932 and its manifold version, so your work is really valuable! I'm wondering:

• Do you mind if I push your PR to completion? I'd like to have it in mathlib soon, so I can build on it.
• Can you share what you had for the manifold version? I could develop it on my own, but I'd much rather credit you and build on your work, if that's reasonable. A link to a branch is totally fine (no need to worry about collaboration access or anything like that).

[Sébastien Gouëzel]

Wow, Levi-Civita, that's awesome! Did the Riemannian manifold definition work well for you, or did you have to tweak the definition somehow to make it better?

[Michael Rothgang]

We're not at that stage yet, but it's coming soon - and we will report back to you!