Product vector fields #
Vector fields X on M and Y on N combine to the vector field (X, Y) on M × N, whose value
at (x, y) is (X x, Y y) under the identification of the tangent space of a product with the
product of the tangent spaces. Such a field is differentiable, respectively C^n, at (x, y) when
X is at x and Y is at y, and the Lie bracket of two product fields is computed factor by
factor: [(X₁, X₂), (Y₁, Y₂)] = ([X₁, Y₁], [X₂, Y₂]).
Product fields are the fields along which the geometry of a product manifold splits. The tangent space at every point is spanned by values of product fields, and differential operators such as the Levi-Civita connection of a product metric are computed on them.
A vector-valued function on M composed with the projection M × N → M differentiates a product
field (X, Y) along X only (TauCeti.mvfderiv_comp_fst_apply), and symmetrically for N; this
is what makes the bracket of product fields split.
Main definitions #
TauCeti.Manifold.prodVectorField: the vector field(X, Y)onM × N.
Main results #
TauCeti.Manifold.prodVectorField_add,TauCeti.Manifold.prodVectorField_smul,TauCeti.Manifold.prodVectorField_neg: product fields are linear in the pair of their factors.TauCeti.Manifold.mdifferentiableAt_prodVectorField,TauCeti.Manifold.contMDiffAt_prodVectorFieldandTauCeti.Manifold.contMDiff_prodVectorField: regularity of product fields.TauCeti.Manifold.mlieBracket_prodVectorField: the Lie bracket of product fields is the product of the Lie brackets.TauCeti.Manifold.mlieBracket_prodVectorField_horizontal_vertical: horizontal and vertical lifts commute.
References #
- J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Chapter 8 (vector fields and Lie brackets).
Product vector fields #
def
TauCeti.Manifold.prodVectorField
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
(X : (x : M) → TangentSpace I x)
(Y : (y : N) → TangentSpace J y)
(p : M × N)
:
TangentSpace (I.prod J) p
The vector field on M × N whose value at p is (X p.1, Y p.2).
Instances For
theorem
TauCeti.Manifold.tangentSpaceProdEquiv_prodVectorField
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
(X : (x : M) → TangentSpace I x)
(Y : (y : N) → TangentSpace J y)
(p : M × N)
:
The components of a product field are the values of its factors. Not a simp lemma, since
simp already removes tangentSpaceProdEquiv by TauCeti.Manifold.tangentSpaceProdEquiv_apply.
@[simp]
theorem
TauCeti.Manifold.prodVectorField_fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
(X : (x : M) → TangentSpace I x)
(Y : (y : N) → TangentSpace J y)
(p : M × N)
:
The first component of a product field is the value of its first factor.
@[simp]
theorem
TauCeti.Manifold.prodVectorField_snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
(X : (x : M) → TangentSpace I x)
(Y : (y : N) → TangentSpace J y)
(p : M × N)
:
The second component of a product field is the value of its second factor.
@[simp]
theorem
TauCeti.Manifold.prodVectorField_add
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
(X X' : (x : M) → TangentSpace I x)
(Y Y' : (y : N) → TangentSpace J y)
:
Product fields are additive in the pair of their factors.
@[simp]
theorem
TauCeti.Manifold.prodVectorField_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
(c : 𝕜)
(X : (x : M) → TangentSpace I x)
(Y : (y : N) → TangentSpace J y)
:
Scaling both factors of a product field scales the field.
@[simp]
theorem
TauCeti.Manifold.prodVectorField_neg
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
(X : (x : M) → TangentSpace I x)
(Y : (y : N) → TangentSpace J y)
:
Negating both factors of a product field negates the field.
theorem
TauCeti.Manifold.contMDiffAt_prodVectorField
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold I 1 M]
[IsManifold J 1 N]
{X : (x : M) → TangentSpace I x}
{Y : (y : N) → TangentSpace J y}
{p : M × N}
{n : WithTop ℕ∞}
(hX : ContMDiffAt I I.tangent n (fun (x : M) => ⟨x, X x⟩) p.1)
(hY : ContMDiffAt J J.tangent n (fun (y : N) => ⟨y, Y y⟩) p.2)
:
ContMDiffAt (I.prod J) (I.prod J).tangent n (fun (p : M × N) => ⟨p, prodVectorField X Y p⟩) p
A product of vector fields is C^n at p when the factors are C^n at p.1 and p.2.
theorem
TauCeti.Manifold.contMDiff_prodVectorField
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold I 1 M]
[IsManifold J 1 N]
{X : (x : M) → TangentSpace I x}
{Y : (y : N) → TangentSpace J y}
{n : WithTop ℕ∞}
(hX : ContMDiff I I.tangent n fun (x : M) => ⟨x, X x⟩)
(hY : ContMDiff J J.tangent n fun (y : N) => ⟨y, Y y⟩)
:
A product of C^n vector fields is C^n.
theorem
TauCeti.Manifold.mdifferentiableAt_prodVectorField
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold I 1 M]
[IsManifold J 1 N]
{X : (x : M) → TangentSpace I x}
{Y : (y : N) → TangentSpace J y}
{p : M × N}
(hX : (MDiffAt fun (x : M) => ⟨x, X x⟩) p.1)
(hY : (MDiffAt fun (y : N) => ⟨y, Y y⟩) p.2)
:
(MDiffAt fun (p : M × N) => ⟨p, prodVectorField X Y p⟩) p
A product of vector fields is differentiable at p when the factors are differentiable at
p.1 and p.2.
The Lie bracket of product vector fields #
theorem
TauCeti.Manifold.mlieBracket_prodVectorField
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
[CompleteSpace E]
[CompleteSpace E']
[IsManifold I (minSmoothness 𝕜 2) M]
[IsManifold J (minSmoothness 𝕜 2) N]
{X₁ Y₁ : (x : M) → TangentSpace I x}
{X₂ Y₂ : (y : N) → TangentSpace J y}
{p : M × N}
(hX₁ : (MDiffAt fun (x : M) => ⟨x, X₁ x⟩) p.1)
(hY₁ : (MDiffAt fun (x : M) => ⟨x, Y₁ x⟩) p.1)
(hX₂ : (MDiffAt fun (y : N) => ⟨y, X₂ y⟩) p.2)
(hY₂ : (MDiffAt fun (y : N) => ⟨y, Y₂ y⟩) p.2)
:
VectorField.mlieBracket (I.prod J) (prodVectorField X₁ X₂) (prodVectorField Y₁ Y₂) p = prodVectorField (VectorField.mlieBracket I X₁ Y₁) (VectorField.mlieBracket J X₂ Y₂) p
The Lie bracket of two product vector fields is the product of the Lie brackets of their
factors: [(X₁, X₂), (Y₁, Y₂)] = ([X₁, Y₁], [X₂, Y₂]) at every point where the four factors are
differentiable.
@[simp]
theorem
TauCeti.Manifold.mlieBracket_prodVectorField_horizontal_vertical
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
[CompleteSpace E]
[CompleteSpace E']
[IsManifold I (minSmoothness 𝕜 2) M]
[IsManifold J (minSmoothness 𝕜 2) N]
{p : M × N}
{X : (x : M) → TangentSpace I x}
{V : (y : N) → TangentSpace J y}
(hX : (MDiffAt fun (x : M) => ⟨x, X x⟩) p.1)
(hV : (MDiffAt fun (y : N) => ⟨y, V y⟩) p.2)
:
Horizontal and vertical lifts of vector fields on a product manifold commute at every point where the two fields are differentiable.