The Euler vector field of a vector bundle

The fibres of a vector bundle V → B are vector spaces, so every vector z in the total space lies on the line t ↦ t • z through the origin of its fibre. The velocity of that line at t = 1 is the Euler vector field (or radial vector field) of the bundle (TauCeti.vectorBundleEulerField). In a bundle chart with coordinates (x, ξ) it is ξ ∂_ξ: at z its coordinates are (0, ξ), where ξ is the fibre coordinate of z (TauCeti.vectorBundleEulerField_eq_trivializationAt). It is vertical, that is, killed by the derivative of the projection (TauCeti.mfderiv_proj_vectorBundleEulerField), it vanishes along the zero section (TauCeti.vectorBundleEulerField_zero), and it is smooth (TauCeti.contMDiff_vectorBundleEulerField). The differential of a map sends it to the velocity of the image of the line t ↦ t • z (TauCeti.mfderiv_vectorBundleEulerField), so maps between vector bundles which are linear on fibres preserve Euler vector fields (TauCeti.mfderiv_vectorBundleEulerField_of_linear).

It is the infinitesimal generator of the fibre dilations z ↦ c • z (TauCeti.vectorBundleScalarDiffeomorph): on a real vector bundle, the curve t ↦ e^t • z is an integral curve of the Euler vector field (TauCeti.isMIntegralCurve_vectorBundleEulerField). These curves are defined for all time, so the Euler vector field is complete (TauCeti.isCompleteVectorField_vectorBundleEulerField). On a cotangent bundle it is the field p ∂_p, the Liouville vector field of the canonical symplectic structure.

Main declarations

• TauCeti.vectorBundleEulerField: the Euler vector field.
• TauCeti.hasMFDerivAt_vectorBundleEulerField: it is the velocity at t = 1 of t ↦ t • z.
• TauCeti.mfderiv_vectorBundleEulerField: its image under a differential is the velocity of the image of the line t ↦ t • z.
• TauCeti.mfderiv_vectorBundleEulerField_of_linear: fibrewise linear maps preserve it.
• TauCeti.vectorBundleEulerField_eq_trivializationAt: its coordinates in the chart at z.
• TauCeti.mfderiv_proj_vectorBundleEulerField: it is vertical.
• TauCeti.contMDiff_vectorBundleEulerField: it is a smooth section of the tangent bundle of the total space.
• TauCeti.isMIntegralCurve_vectorBundleEulerField: on a real vector bundle, the curves t ↦ e^t • z are integral curves of it.
• TauCeti.isCompleteVectorField_vectorBundleEulerField: it is complete.

References

• S. Lang, Fundamentals of Differential Geometry, Graduate Texts in Mathematics 191, Springer, 1999, Chapter IV (sprays, and the dilations of the fibres of a vector bundle).

noncomputable def TauCeti.vectorBundleEulerField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {B : Type u_4} [TopologicalSpace B] [ChartedSpace H B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [(b : B) → AddCommMonoid (V b)] [(b : B) → Module 𝕜 (V b)] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] (z : Bundle.TotalSpace F V) : TangentSpace (I.prod (modelWithCornersSelf 𝕜 F)) z

The Euler vector field of a vector bundle: at a vector z of the total space, the velocity at t = 1 of the line t ↦ t • z in the fibre of z. In a bundle chart with coordinates (x, ξ) it is ξ ∂_ξ (TauCeti.vectorBundleEulerField_eq_trivializationAt).

theorem TauCeti.vectorBundleEulerField_eq_trivializationAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {B : Type u_4} [TopologicalSpace B] [ChartedSpace H B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [(b : B) → AddCommMonoid (V b)] [(b : B) → Module 𝕜 (V b)] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle 𝕜 F V] (z : Bundle.TotalSpace F V) : vectorBundleEulerField I z = (0, (↑(trivializationAt F V z.proj) z).2)

Chart formula for the Euler vector field. Read in the chart at z, where tangent vectors at z are their own coordinates, the Euler vector field at z is (0, ξ), with ξ the fibre coordinate of z in the trivialization at its base point.

theorem TauCeti.hasMFDerivAt_vectorBundleEulerField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {B : Type u_4} [TopologicalSpace B] [ChartedSpace H B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [(b : B) → AddCommMonoid (V b)] [(b : B) → Module 𝕜 (V b)] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle 𝕜 F V] (z : Bundle.TotalSpace F V) : HasMFDerivAt% (fun (t : 𝕜) => ⟨z.proj, t • z.snd⟩) 1 (ContinuousLinearMap.smulRight 1 (vectorBundleEulerField I z))

The Euler vector field at z is the velocity at t = 1 of the line t ↦ t • z.

theorem TauCeti.mfderiv_vectorBundleEulerField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {B : Type u_4} [TopologicalSpace B] [ChartedSpace H B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [(b : B) → AddCommMonoid (V b)] [(b : B) → Module 𝕜 (V b)] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle 𝕜 F V] {E' : Type u_7} {H' : Type u_8} {M' : Type u_9} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] {f : Bundle.TotalSpace F V → M'} {z : Bundle.TotalSpace F V} (hf : MDiffAt f z) : (mfderiv% f z) (vectorBundleEulerField I z) = (mfderiv% (f ∘ fun (t : 𝕜) => ⟨z.proj, t • z.snd⟩) 1) 1

The Euler vector field along a map. The differential at z of a map f sends the Euler vector field to the velocity at t = 1 of the image under f of the line t ↦ t • z.

theorem TauCeti.mfderiv_vectorBundleEulerField_of_linear {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {B : Type u_4} [TopologicalSpace B] [ChartedSpace H B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [(b : B) → AddCommMonoid (V b)] [(b : B) → Module 𝕜 (V b)] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle 𝕜 F V] {E' : Type u_7} {H' : Type u_8} {B' : Type u_9} {F' : Type u_10} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace B'] [ChartedSpace H' B'] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {V' : B' → Type u_11} [(b : B') → AddCommMonoid (V' b)] [(b : B') → Module 𝕜 (V' b)] [(b : B') → TopologicalSpace (V' b)] [TopologicalSpace (Bundle.TotalSpace F' V')] [FiberBundle F' V'] {f : Bundle.TotalSpace F V → Bundle.TotalSpace F' V'} {g : B → B'} (φ : (b : B) → V b →ₗ[𝕜] V' (g b)) (hfφ : ∀ (w : Bundle.TotalSpace F V), f w = ⟨g w.proj, (φ w.proj) w.snd⟩) {z : Bundle.TotalSpace F V} (hf : MDiffAt f z) : (mfderiv% f z) (vectorBundleEulerField I z) = vectorBundleEulerField I' (f z)

Fibrewise linear maps preserve Euler vector fields. A map between the total spaces of two vector bundles which covers a map g of the bases and is linear on each fibre sends the Euler vector field to the Euler vector field, at every point where it is differentiable.

@[simp]

theorem TauCeti.vectorBundleEulerField_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {B : Type u_4} [TopologicalSpace B] [ChartedSpace H B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [(b : B) → AddCommMonoid (V b)] [(b : B) → Module 𝕜 (V b)] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle 𝕜 F V] (b : B) : vectorBundleEulerField I ⟨b, 0⟩ = 0

The Euler vector field vanishes along the zero section.

@[simp]

theorem TauCeti.mfderiv_proj_vectorBundleEulerField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {B : Type u_4} [TopologicalSpace B] [ChartedSpace H B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [(b : B) → AddCommMonoid (V b)] [(b : B) → Module 𝕜 (V b)] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle 𝕜 F V] (z : Bundle.TotalSpace F V) : (mfderiv% Bundle.TotalSpace.proj z) (vectorBundleEulerField I z) = 0

The Euler vector field is vertical: the derivative of the bundle projection kills it.

theorem TauCeti.contMDiff_vectorBundleEulerField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {B : Type u_4} [TopologicalSpace B] [ChartedSpace H B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [(b : B) → AddCommMonoid (V b)] [(b : B) → Module 𝕜 (V b)] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle 𝕜 F V] {m : WithTop ℕ∞} [IsManifold (I.prod (modelWithCornersSelf 𝕜 F)) 1 (Bundle.TotalSpace F V)] : ContMDiff (I.prod (modelWithCornersSelf 𝕜 F)) (I.prod (modelWithCornersSelf 𝕜 F)).tangent m fun (z : Bundle.TotalSpace F V) => ⟨z, vectorBundleEulerField I z⟩

Smoothness of the Euler vector field. The Euler vector field is a C^m section of the tangent bundle of the total space, for every m.

The flow of the Euler vector field

theorem TauCeti.isMIntegralCurve_vectorBundleEulerField {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {B : Type u_3} [TopologicalSpace B] [ChartedSpace H B] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : B → Type u_5} [(b : B) → AddCommMonoid (V b)] [(b : B) → Module ℝ (V b)] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] (z : Bundle.TotalSpace F V) : IsMIntegralCurve (fun (t : ℝ) => ⟨z.proj, Real.exp t • z.snd⟩) (vectorBundleEulerField I)

The flow of the Euler vector field is fibre dilation. For every vector z of a real vector bundle, the curve t ↦ e^t • z is an integral curve of the Euler vector field.

theorem TauCeti.isCompleteVectorField_vectorBundleEulerField {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {B : Type u_3} [TopologicalSpace B] [ChartedSpace H B] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : B → Type u_5} [(b : B) → AddCommMonoid (V b)] [(b : B) → Module ℝ (V b)] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [T2Space (Bundle.TotalSpace F V)] [IsManifold (I.prod (modelWithCornersSelf ℝ F)) 1 (Bundle.TotalSpace F V)] [BoundarylessManifold (I.prod (modelWithCornersSelf ℝ F)) (Bundle.TotalSpace F V)] : IsCompleteVectorField (vectorBundleEulerField I)

The Euler vector field is complete: through every vector z of a real vector bundle, the fibre dilation t ↦ e^t • z is an integral curve defined for all time.