Lie brackets of vector fields on manifolds #
We define the Lie bracket of two vector fields, denoted with
VectorField.mlieBracket I V W x, as the pullback in the manifold of the corresponding notion
in the model space (through extChartAt I x).
The main results are the following:
VectorField.mpullback_mlieBracketstates that the pullback of the Lie bracket is the Lie bracket of the pullbacks.VectorField.leibniz_identity_mlieBracketis the Leibniz (or Jacobi) identity[U, [V, W]] = [[U, V], W] + [V, [U, W]].
The Lie bracket of vector fields in manifolds #
def
VectorField.mlieBracketWithin
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
(I : ModelWithCorners ๐ E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
(V W : (x : M) โ TangentSpace I x)
(s : Set M)
(xโ : M)
:
TangentSpace I xโ
The Lie bracket of two vector fields in a manifold, within a set.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
VectorField.mlieBracket
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
(I : ModelWithCorners ๐ E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
(V W : (x : M) โ TangentSpace I x)
(xโ : M)
:
TangentSpace I xโ
The Lie bracket of two vector fields in a manifold.
Equations
- VectorField.mlieBracket I V W xโ = VectorField.mlieBracketWithin I V W Set.univ xโ
Instances For
theorem
VectorField.mlieBracketWithin_def
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{V W : (x : M) โ TangentSpace I x}
:
mlieBracketWithin I V W s = fun (xโ : M) =>
mpullback I (modelWithCornersSelf ๐ E) (โ(extChartAt I xโ))
(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))
xโ
theorem
VectorField.mlieBracketWithin_apply
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{xโ : M}
{V W : (x : M) โ TangentSpace I x}
:
mlieBracketWithin I V W s xโ = (mfderiv I (modelWithCornersSelf ๐ E) (โ(extChartAt I xโ)) xโ).inverse
(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โ))
theorem
VectorField.mlieBracketWithin_eq_lieBracketWithin
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{V W : (x : E) โ TangentSpace (modelWithCornersSelf ๐ E) x}
{s : Set E}
:
@[simp]
theorem
VectorField.mlieBracketWithin_univ
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{V W : (x : M) โ TangentSpace I x}
:
theorem
VectorField.mlieBracketWithin_eq_zero_of_eq_zero
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W : (x : M) โ TangentSpace I x}
(hV : V x = 0)
(hW : W x = 0)
:
theorem
VectorField.mlieBracketWithin_swap_apply
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W : (x : M) โ TangentSpace I x}
:
theorem
VectorField.mlieBracketWithin_swap
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{V W : (x : M) โ TangentSpace I x}
:
theorem
VectorField.mlieBracket_swap_apply
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
{V W : (x : M) โ TangentSpace I x}
:
theorem
VectorField.mlieBracket_swap
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{V W : (x : M) โ TangentSpace I x}
:
@[simp]
theorem
VectorField.mlieBracketWithin_self
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{V : (x : M) โ TangentSpace I x}
:
@[simp]
theorem
VectorField.mlieBracket_self
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{V : (x : M) โ TangentSpace I x}
:
theorem
VectorField.mlieBracketWithin_congr_set'
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s t : Set M}
{x : M}
{V W : (x : M) โ TangentSpace I x}
(y : M)
(h : s =แถ [nhdsWithin x {y}แถ] t)
:
Variant of mlieBracketWithin_congr_set where one requires the sets to coincide only in
the complement of a point.
theorem
VectorField.mlieBracketWithin_congr_set
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s t : Set M}
{x : M}
{V W : (x : M) โ TangentSpace I x}
(h : s =แถ [nhds x] t)
:
theorem
VectorField.mlieBracketWithin_inter
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s t : Set M}
{x : M}
{V W : (x : M) โ TangentSpace I x}
(ht : t โ nhds x)
:
theorem
VectorField.mlieBracketWithin_of_mem_nhds
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W : (x : M) โ TangentSpace I x}
(h : s โ nhds x)
:
theorem
VectorField.mlieBracketWithin_of_isOpen
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W : (x : M) โ TangentSpace I x}
(hs : IsOpen s)
(hx : x โ s)
:
theorem
VectorField.mlieBracketWithin_eventually_congr_set'
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s t : Set M}
{x : M}
{V W : (x : M) โ TangentSpace I x}
(y : M)
(h : s =แถ [nhdsWithin x {y}แถ] t)
:
Variant of mlieBracketWithin_eventually_congr_set where one requires the sets to coincide only
in the complement of a point.
theorem
VectorField.mlieBracketWithin_eventually_congr_set
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s t : Set M}
{x : M}
{V W : (x : M) โ TangentSpace I x}
(h : s =แถ [nhds x] t)
:
theorem
Filter.EventuallyEq.mlieBracketWithin_vectorField_eq
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W Vโ Wโ : (x : M) โ TangentSpace I x}
(hV : Vโ =แถ [nhdsWithin x s] V)
(hxV : Vโ x = V x)
(hW : Wโ =แถ [nhdsWithin x s] W)
(hxW : Wโ x = W x)
:
theorem
Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_of_mem
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W Vโ Wโ : (x : M) โ TangentSpace I x}
(hV : Vโ =แถ [nhdsWithin x s] V)
(hW : Wโ =แถ [nhdsWithin x s] W)
(hx : x โ s)
:
theorem
Filter.EventuallyEq.mlieBracketWithin_vectorField'
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s t : Set M}
{x : M}
{V W Vโ Wโ : (x : M) โ TangentSpace I x}
(hV : Vโ =แถ [nhdsWithin x s] V)
(hW : Wโ =แถ [nhdsWithin x s] W)
(ht : t โ s)
:
VectorField.mlieBracketWithin I Vโ Wโ t =แถ [nhdsWithin x s] VectorField.mlieBracketWithin I V W t
If vector fields coincide on a neighborhood of a point within a set, then the Lie brackets also coincide on a neighborhood of this point within this set. Version where one considers the Lie bracket within a subset.
theorem
Filter.EventuallyEq.mlieBracketWithin_vectorField
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W Vโ Wโ : (x : M) โ TangentSpace I x}
(hV : Vโ =แถ [nhdsWithin x s] V)
(hW : Wโ =แถ [nhdsWithin x s] W)
:
VectorField.mlieBracketWithin I Vโ Wโ s =แถ [nhdsWithin x s] VectorField.mlieBracketWithin I V W s
theorem
Filter.EventuallyEq.mlieBracketWithin_vectorField_of_insert
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W Vโ Wโ : (x : M) โ TangentSpace I x}
(hV : Vโ =แถ [nhdsWithin x (insert x s)] V)
(hW : Wโ =แถ [nhdsWithin x (insert x s)] W)
:
theorem
Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_nhds
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W Vโ Wโ : (x : M) โ TangentSpace I x}
(hV : Vโ =แถ [nhds x] V)
(hW : Wโ =แถ [nhds x] W)
:
theorem
VectorField.mlieBracketWithin_congr
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W Vโ Wโ : (x : M) โ TangentSpace I x}
(hV : Set.EqOn Vโ V s)
(hVx : Vโ x = V x)
(hW : Set.EqOn Wโ W s)
(hWx : Wโ x = W x)
:
theorem
VectorField.mlieBracketWithin_congr'
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W Vโ Wโ : (x : M) โ TangentSpace I x}
(hV : Set.EqOn Vโ V s)
(hW : Set.EqOn Wโ W s)
(hx : x โ s)
:
Version of mlieBracketWithin_congr in which one assumes that the point belongs to the
given set.
theorem
Filter.EventuallyEq.mlieBracket_vectorField_eq
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
{V W Vโ Wโ : (x : M) โ TangentSpace I x}
(hV : Vโ =แถ [nhds x] V)
(hW : Wโ =แถ [nhds x] W)
:
theorem
Filter.EventuallyEq.mlieBracket_vectorField
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
{V W Vโ Wโ : (x : M) โ TangentSpace I x}
(hV : Vโ =แถ [nhds x] V)
(hW : Wโ =แถ [nhds x] W)
:
theorem
MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V : (x : M) โ TangentSpace I x}
[IsManifold I 2 M]
[CompleteSpace E]
(hV : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := V x }) s x)
:
DifferentiableWithinAt ๐
(VectorField.mpullbackWithin (modelWithCornersSelf ๐ E) I (โ(extChartAt I x).symm) V (Set.range โI))
(โ(extChartAt I x).symm โปยน' s โฉ Set.range โI) (โ(extChartAt I x) x)
theorem
VectorField.mlieBracketWithin_smul_left
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W : (x : M) โ TangentSpace I x}
{c : ๐}
[IsManifold I 2 M]
[CompleteSpace E]
(hV : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := V x }) s x)
(hs : UniqueMDiffWithinAt I s x)
:
theorem
VectorField.mlieBracket_smul_left
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
{V W : (x : M) โ TangentSpace I x}
{c : ๐}
[IsManifold I 2 M]
[CompleteSpace E]
(hV : MDifferentiableAt I I.tangent (fun (x : M) => { proj := x, snd := V x }) x)
:
theorem
VectorField.mlieBracketWithin_smul_right
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W : (x : M) โ TangentSpace I x}
{c : ๐}
[IsManifold I 2 M]
[CompleteSpace E]
(hW : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := W x }) s x)
(hs : UniqueMDiffWithinAt I s x)
:
theorem
VectorField.mlieBracket_smul_right
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
{V W : (x : M) โ TangentSpace I x}
{c : ๐}
[IsManifold I 2 M]
[CompleteSpace E]
(hW : MDifferentiableAt I I.tangent (fun (x : M) => { proj := x, snd := W x }) x)
:
theorem
VectorField.mlieBracketWithin_add_left
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W Vโ : (x : M) โ TangentSpace I x}
[IsManifold I 2 M]
[CompleteSpace E]
(hV : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := V x }) s x)
(hVโ : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := Vโ x }) s x)
(hs : UniqueMDiffWithinAt I s x)
:
theorem
VectorField.mlieBracket_add_left
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
{V W Vโ : (x : M) โ TangentSpace I x}
[IsManifold I 2 M]
[CompleteSpace E]
(hV : MDifferentiableAt I I.tangent (fun (x : M) => { proj := x, snd := V x }) x)
(hVโ : MDifferentiableAt I I.tangent (fun (x : M) => { proj := x, snd := Vโ x }) x)
:
theorem
VectorField.mlieBracketWithin_add_right
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W Wโ : (x : M) โ TangentSpace I x}
[IsManifold I 2 M]
[CompleteSpace E]
(hW : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := W x }) s x)
(hWโ : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := Wโ x }) s x)
(hs : UniqueMDiffWithinAt I s x)
:
theorem
VectorField.mlieBracket_add_right
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
{V W Wโ : (x : M) โ TangentSpace I x}
[IsManifold I 2 M]
[CompleteSpace E]
(hW : MDifferentiableAt I I.tangent (fun (x : M) => { proj := x, snd := W x }) x)
(hWโ : MDifferentiableAt I I.tangent (fun (x : M) => { proj := x, snd := Wโ x }) x)
:
theorem
VectorField.mlieBracketWithin_of_mem_nhdsWithin
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s t : Set M}
{x : M}
{V W : (x : M) โ TangentSpace I x}
[IsManifold I 2 M]
[CompleteSpace E]
(st : t โ nhdsWithin x s)
(hs : UniqueMDiffWithinAt I s x)
(hV : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := V x }) t x)
(hW : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := W x }) t x)
:
theorem
VectorField.mlieBracketWithin_subset
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s t : Set M}
{x : M}
{V W : (x : M) โ TangentSpace I x}
[IsManifold I 2 M]
[CompleteSpace E]
(st : s โ t)
(ht : UniqueMDiffWithinAt I s x)
(hV : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := V x }) t x)
(hW : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := W x }) t x)
:
theorem
VectorField.mlieBracketWithin_eq_mlieBracket
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W : (x : M) โ TangentSpace I x}
[IsManifold I 2 M]
[CompleteSpace E]
(hs : UniqueMDiffWithinAt I s x)
(hV : MDifferentiableAt I I.tangent (fun (x : M) => { proj := x, snd := V x }) x)
(hW : MDifferentiableAt I I.tangent (fun (x : M) => { proj := x, snd := W x }) x)
:
theorem
DifferentiableWithinAt.mlieBracketWithin_congr_mono
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s t : Set M}
{x : M}
{V W Vโ Wโ : (x : M) โ TangentSpace I x}
[IsManifold I 2 M]
[CompleteSpace E]
(hV : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := V x }) s x)
(hVs : Set.EqOn Vโ V t)
(hVx : Vโ x = V x)
(hW : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := W x }) s x)
(hWs : Set.EqOn Wโ W t)
(hWx : Wโ x = W x)
(hxt : UniqueMDiffWithinAt I t x)
(hโ : t โ s)
:
theorem
VectorField.mpullbackWithin_mlieBracketWithin_of_isSymmSndFDerivWithinAt
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I 2 M]
[IsManifold I' 2 M']
[CompleteSpace E]
{f : M โ M'}
{V W : (x : M') โ TangentSpace I' x}
{xโ : M}
{s : Set M}
{t : Set M'}
(hV : MDifferentiableWithinAt I' I'.tangent (fun (x : M') => { proj := x, snd := V x }) t (f xโ))
(hW : MDifferentiableWithinAt I' I'.tangent (fun (x : M') => { proj := x, snd := W x }) t (f xโ))
(hu : UniqueMDiffOn I s)
(hf : ContMDiffWithinAt I I' 2 f s xโ)
(hxโ : xโ โ s)
(hst : f โปยน' t โ nhdsWithin xโ s)
(hsymm :
IsSymmSndFDerivWithinAt ๐ (โ(extChartAt I' (f xโ)) โ f โ โ(extChartAt I xโ).symm)
(โ(extChartAt I xโ).symm โปยน' s โฉ Set.range โI) (โ(extChartAt I xโ) xโ))
:
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โ
theorem
VectorField.mpullbackWithin_mlieBracketWithin'
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I (minSmoothness ๐ 2) M]
[IsManifold I' (minSmoothness ๐ 2) M']
[CompleteSpace E]
{n : WithTop โโ}
{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 : M') => { proj := x, snd := V x }) t (f xโ))
(hW : MDifferentiableWithinAt I' I'.tangent (fun (x : M') => { proj := x, snd := W x }) 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 โ nhdsWithin xโ s)
(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โ
The pullback commutes with the Lie bracket of vector fields on manifolds. Version where one
assumes that the map is smooth on a larget set u (so that the
condition xโ โ closure (interior u), needed to guarantee the symmetry of the second derivative,
becomes easier to check.)
theorem
VectorField.mpullbackWithin_mlieBracketWithin
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I (minSmoothness ๐ 2) M]
[IsManifold I' (minSmoothness ๐ 2) M']
[CompleteSpace E]
{n : WithTop โโ}
{f : M โ M'}
{V W : (x : M') โ TangentSpace I' x}
{xโ : M}
{s : Set M}
{t : Set M'}
(hV : MDifferentiableWithinAt I' I'.tangent (fun (x : M') => { proj := x, snd := V x }) t (f xโ))
(hW : MDifferentiableWithinAt I' I'.tangent (fun (x : M') => { proj := x, snd := W x }) t (f xโ))
(hu : UniqueMDiffOn I s)
(hf : ContMDiffWithinAt I I' n f s xโ)
(hxโ : xโ โ s)
(hn : minSmoothness ๐ 2 โค n)
(hst : f โปยน' t โ nhdsWithin xโ s)
(h'xโ : xโ โ closure (interior s))
:
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โ
The pullback commutes with the Lie bracket of vector fields on manifolds.
theorem
VectorField.mpullback_mlieBracketWithin
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I (minSmoothness ๐ 2) M]
[IsManifold I' (minSmoothness ๐ 2) M']
[CompleteSpace E]
{n : WithTop โโ}
{f : M โ M'}
{V W : (x : M') โ TangentSpace I' x}
{xโ : M}
{s : Set M}
{t : Set M'}
(hV : MDifferentiableWithinAt I' I'.tangent (fun (x : M') => { proj := x, snd := V x }) t (f xโ))
(hW : MDifferentiableWithinAt I' I'.tangent (fun (x : M') => { proj := x, snd := W x }) t (f xโ))
(hu : UniqueMDiffOn I s)
(hf : ContMDiffAt I I' n f xโ)
(hxโ : xโ โ s)
(hn : minSmoothness ๐ 2 โค n)
(hst : f โปยน' t โ nhdsWithin xโ s)
:
mpullback I I' f (mlieBracketWithin I' V W t) xโ = mlieBracketWithin I (mpullback I I' f V) (mpullback I I' f W) s xโ
The pullback commutes with the Lie bracket of vector fields on manifolds.
theorem
VectorField.mpullback_mlieBracket
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I (minSmoothness ๐ 2) M]
[IsManifold I' (minSmoothness ๐ 2) M']
[CompleteSpace E]
{n : WithTop โโ}
{f : M โ M'}
{V W : (x : M') โ TangentSpace I' x}
{xโ : M}
(hV : MDifferentiableAt I' I'.tangent (fun (x : M') => { proj := x, snd := V x }) (f xโ))
(hW : MDifferentiableAt I' I'.tangent (fun (x : M') => { proj := x, snd := W x }) (f xโ))
(hf : ContMDiffAt I I' n f xโ)
(hn : minSmoothness ๐ 2 โค n)
:
mpullback I I' f (mlieBracket I' V W) xโ = mlieBracket I (mpullback I I' f V) (mpullback I I' f W) xโ
theorem
ContMDiffWithinAt.mlieBracketWithin_vectorField
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (minSmoothness ๐ 2) M]
[CompleteSpace E]
{n : WithTop โโ}
[IsManifold I (n + 1) M]
{m : WithTop โโ}
{U V : (x : M) โ TangentSpace I x}
{s : Set M}
{x : M}
(hU : ContMDiffWithinAt I I.tangent n (fun (x : M) => { proj := x, snd := U x }) s x)
(hV : ContMDiffWithinAt I I.tangent n (fun (x : M) => { proj := x, snd := V x }) s x)
(hs : UniqueMDiffOn I s)
(hx : x โ s)
(hmn : minSmoothness ๐ (m + 1) โค n)
:
ContMDiffWithinAt I I.tangent m (fun (x : M) => { proj := x, snd := VectorField.mlieBracketWithin I U V s x }) s x
If two vector fields are C^n with n โฅ m + 1, then their Lie bracket is C^m.
theorem
ContMDiffAt.mlieBracket_vectorField
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (minSmoothness ๐ 2) M]
[CompleteSpace E]
{m n : โโ}
[IsManifold I (โn + 1) M]
{U V : (x : M) โ TangentSpace I x}
{x : M}
(hU : ContMDiffAt I I.tangent (โn) (fun (x : M) => { proj := x, snd := U x }) x)
(hV : ContMDiffAt I I.tangent (โn) (fun (x : M) => { proj := x, snd := V x }) x)
(hmn : minSmoothness ๐ (โm + 1) โค โn)
:
ContMDiffAt I I.tangent (โm) (fun (x : M) => { proj := x, snd := VectorField.mlieBracket I U V x }) x
If two vector fields are C^n with n โฅ m + 1, then their Lie bracket is C^m.
theorem
ContMDiffOn.mlieBracketWithin_vectorField
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
[IsManifold I (minSmoothness ๐ 2) M]
[CompleteSpace E]
{m n : โโ}
[IsManifold I (โn + 1) M]
{U V : (x : M) โ TangentSpace I x}
(hU : ContMDiffOn I I.tangent (โn) (fun (x : M) => { proj := x, snd := U x }) s)
(hV : ContMDiffOn I I.tangent (โn) (fun (x : M) => { proj := x, snd := V x }) s)
(hs : UniqueMDiffOn I s)
(hmn : minSmoothness ๐ (โm + 1) โค โn)
:
ContMDiffOn I I.tangent (โm) (fun (x : M) => { proj := x, snd := VectorField.mlieBracketWithin I U V s x }) s
If two vector fields are C^n with n โฅ m + 1, then their Lie bracket is C^m.
theorem
ContDiff.mlieBracket_vectorField
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (minSmoothness ๐ 2) M]
[CompleteSpace E]
{m n : โโ}
[IsManifold I (โn + 1) M]
{U V : (x : M) โ TangentSpace I x}
(hU : ContMDiff I I.tangent โn fun (x : M) => { proj := x, snd := U x })
(hV : ContMDiff I I.tangent โn fun (x : M) => { proj := x, snd := V x })
(hmn : minSmoothness ๐ (โm + 1) โค โn)
:
ContMDiff I I.tangent โm fun (x : M) => { proj := x, snd := VectorField.mlieBracket I U V x }
If two vector fields are C^n with n โฅ m + 1, then their Lie bracket is C^m.
theorem
VectorField.leibniz_identity_mlieBracketWithin_apply
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (minSmoothness ๐ 3) M]
[CompleteSpace E]
{U V W : (x : M) โ TangentSpace I x}
{s : Set M}
{x : M}
(hs : UniqueMDiffOn I s)
(h's : x โ closure (interior s))
(hx : x โ s)
(hU : ContMDiffWithinAt I I.tangent (minSmoothness ๐ 2) (fun (x : M) => { proj := x, snd := U x }) s x)
(hV : ContMDiffWithinAt I I.tangent (minSmoothness ๐ 2) (fun (x : M) => { proj := x, snd := V x }) s x)
(hW : ContMDiffWithinAt I I.tangent (minSmoothness ๐ 2) (fun (x : M) => { proj := x, snd := W x }) s x)
:
mlieBracketWithin I U (mlieBracketWithin I V W s) s x = mlieBracketWithin I (mlieBracketWithin I U V s) W s x + mlieBracketWithin I V (mlieBracketWithin I U W s) s x
The Lie bracket of vector fields in manifolds satisfies the Leibniz identity
[U, [V, W]] = [[U, V], W] + [V, [U, W]] (also called Jacobi identity).
theorem
VectorField.leibniz_identity_mlieBracket_apply
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (minSmoothness ๐ 3) M]
[CompleteSpace E]
{U V W : (x : M) โ TangentSpace I x}
{x : M}
(hU : ContMDiffAt I I.tangent (minSmoothness ๐ 2) (fun (x : M) => { proj := x, snd := U x }) x)
(hV : ContMDiffAt I I.tangent (minSmoothness ๐ 2) (fun (x : M) => { proj := x, snd := V x }) x)
(hW : ContMDiffAt I I.tangent (minSmoothness ๐ 2) (fun (x : M) => { proj := x, snd := W x }) x)
:
mlieBracket I U (mlieBracket I V W) x = mlieBracket I (mlieBracket I U V) W x + mlieBracket I V (mlieBracket I U W) x
The Lie bracket of vector fields in manifolds satisfies the Leibniz identity
[U, [V, W]] = [[U, V], W] + [V, [U, W]] (also called Jacobi identity).
theorem
VectorField.leibniz_identity_mlieBracket
{๐ : Type u_1}
[NontriviallyNormedField ๐]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ๐ E]
{I : ModelWithCorners ๐ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (minSmoothness ๐ 3) M]
[CompleteSpace E]
{U V W : (x : M) โ TangentSpace I x}
(hU : ContMDiff I I.tangent (minSmoothness ๐ 2) fun (x : M) => { proj := x, snd := U x })
(hV : ContMDiff I I.tangent (minSmoothness ๐ 2) fun (x : M) => { proj := x, snd := V x })
(hW : ContMDiff I I.tangent (minSmoothness ๐ 2) fun (x : M) => { proj := x, snd := W x })
:
mlieBracket I U (mlieBracket I V W) = mlieBracket I (mlieBracket I U V) W + mlieBracket I V (mlieBracket I U W)
The Lie bracket of vector fields in manifolds satisfies the Leibniz identity
[U, [V, W]] = [[U, V], W] + [V, [U, W]] (also called Jacobi identity).