English
The Lie bracket of vector fields on a manifold satisfies the Jacobi identity: [U, [V, W]] = [[U, V], W] + [V, [U, W]].
Русский
Скобка Ли векторных полей удовлетворяет тождеству Якоби: [U, [V, W]] = [[U, V], W] + [V, [U, W]].
LaTeX
$$$[U, [V, W]] = [[U, V], W] + [V, [U, W]]$$$
Lean4
/-- The pullback commutes with the Lie bracket of vector fields on manifolds. Version where one
assumes that the map is smooth on a larger set `u` (so that the
condition `x₀ ∈ closure (interior u)`, needed to guarantee the symmetry of the second derivative,
becomes easier to check.) -/
theorem mpullbackWithin_mlieBracketWithin' {f : M → M'} {V W : Π (x : M'), TangentSpace I' x} {x₀ : M} {s u : Set M}
{t : Set M'} (hV : MDifferentiableWithinAt I' I'.tangent (fun x ↦ (V x : TangentBundle I' M')) t (f x₀))
(hW : MDifferentiableWithinAt I' I'.tangent (fun x ↦ (W x : TangentBundle I' M')) t (f x₀)) (hs : UniqueMDiffOn I s)
(hu : UniqueMDiffOn I u) (hf : ContMDiffWithinAt I I' n f u x₀) (hx₀ : x₀ ∈ s) (hn : minSmoothness 𝕜 2 ≤ n)
(hst : f ⁻¹' t ∈ 𝓝[s] x₀) (h'x₀ : x₀ ∈ closure (interior u)) (hsu : s ⊆ u) :
mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀ =
mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀ :=
by
have B :
ContDiffWithinAt 𝕜 n ((extChartAt I' (f x₀)) ∘ f ∘ (extChartAt I x₀).symm)
((extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target) (extChartAt I x₀ x₀) :=
by
apply (contMDiffWithinAt_iff.1 hf).2.congr_set
exact EventuallyEq.inter (by rfl) extChartAt_target_eventuallyEq.symm
apply
mpullbackWithin_mlieBracketWithin_of_isSymmSndFDerivWithinAt hV hW hs
((hf.mono hsu).of_le (le_minSmoothness.trans hn)) hx₀ hst
have :
((extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target : Set E) =ᶠ[𝓝 (extChartAt I x₀ x₀)]
((extChartAt I x₀).symm ⁻¹' s ∩ range I : Set E) :=
EventuallyEq.inter (by rfl) extChartAt_target_eventuallyEq
apply IsSymmSndFDerivWithinAt.congr_set _ this
have :
IsSymmSndFDerivWithinAt 𝕜 ((extChartAt I' (f x₀)) ∘ f ∘ (extChartAt I x₀).symm)
((extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target) (extChartAt I x₀ x₀) :=
by
apply ContDiffWithinAt.isSymmSndFDerivWithinAt (n := minSmoothness 𝕜 2) _ le_rfl
· rw [inter_comm]
exact UniqueMDiffOn.uniqueDiffOn_target_inter hu x₀
· apply extChartAt_mem_closure_interior h'x₀ (mem_extChartAt_source x₀)
· simp [hsu hx₀]
· exact B.of_le hn
apply IsSymmSndFDerivWithinAt.mono_of_mem_nhdsWithin this
· apply mem_of_superset self_mem_nhdsWithin (inter_subset_inter_left _ (preimage_mono hsu))
· exact (B.of_le hn).of_le le_minSmoothness
· rw [inter_comm]
exact UniqueMDiffOn.uniqueDiffOn_target_inter hs x₀
· rw [inter_comm]
exact UniqueMDiffOn.uniqueDiffOn_target_inter hu x₀
· simp [hx₀]
