Integral curves of invariant vector fields #
Left-invariant vector fields on real Lie groups modeled on complete spaces are complete. Local integral curves around the identity can be translated to give a uniform existence interval around every point, after which Mathlib's uniform-time theorem produces global integral curves.
Main results #
IsMIntegralCurveOn.const_mul_mulInvariantVectorField: left translation preserves invariant integral curves.IsMIntegralCurve.const_mul_mulInvariantVectorField: the global version of that translation law.exists_isMIntegralCurve_mulInvariantVectorField: every left-invariant vector field has a global integral curve through every point.existsUnique_isMIntegralCurve_mulInvariantVectorField: that global curve is unique.mulInvariantIntegralCurve: the resulting canonical global integral curve.hasDerivAt_extChartAt_mulInvariantIntegralCurve_zero: in identity-chart coordinates, the canonical curve has initial velocity equal to its generator.contMDiff_mulInvariantIntegralCurve: canonical invariant integral curves are smooth.mulInvariantIntegralCurve_eq_const_mul: curves through arbitrary points are left translates of the curve through the identity.mulInvariantIntegralCurve_add: the identity curve satisfies the one-parameter subgroup law.mulInvariantIntegralCurve_smul: scaling the vector field rescales time along its curves.mulInvariantOneParameterSubgroup: the identity curve bundled as a continuous homomorphism.contMDiff_mulInvariantOneParameterSubgroup: canonical one-parameter subgroups are smooth.
References #
- Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 0, "The exponential map".
theorem
IsMIntegralCurveOn.const_mul_mulInvariantVectorField
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[ContMDiffMul I 1 G]
{v : GroupLieAlgebra I G}
{γ : ℝ → G}
{s : Set ℝ}
(hγ : IsMIntegralCurveOn γ (mulInvariantVectorField v) s)
(g : G)
:
IsMIntegralCurveOn (fun (t : ℝ) => g * γ t) (mulInvariantVectorField v) s
Left translation preserves integral curves of a left-invariant vector field.
theorem
IsMIntegralCurve.const_mul_mulInvariantVectorField
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[ContMDiffMul I 1 G]
{v : GroupLieAlgebra I G}
{γ : ℝ → G}
(hγ : IsMIntegralCurve γ (mulInvariantVectorField v))
(g : G)
:
IsMIntegralCurve (fun (t : ℝ) => g * γ t) (mulInvariantVectorField v)
Left translation preserves global integral curves of a left-invariant vector field.
theorem
exists_isMIntegralCurve_mulInvariantVectorField
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[CompleteSpace E]
[LieGroup I (minSmoothness ℝ 3) G]
[T2Space G]
[BoundarylessManifold I G]
(v : GroupLieAlgebra I G)
(x : G)
:
∃ (γ : ℝ → G), γ 0 = x ∧ IsMIntegralCurve γ (mulInvariantVectorField v)
Every left-invariant vector field on a real Lie group modeled on a complete space has a global integral curve through every point.
theorem
existsUnique_isMIntegralCurve_mulInvariantVectorField
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[CompleteSpace E]
[LieGroup I (minSmoothness ℝ 3) G]
[T2Space G]
[BoundarylessManifold I G]
(v : GroupLieAlgebra I G)
(x : G)
:
Every left-invariant vector field on a real Lie group modeled on a complete space has a unique global integral curve through every point.
noncomputable def
mulInvariantIntegralCurve
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[CompleteSpace E]
[LieGroup I (minSmoothness ℝ 3) G]
[T2Space G]
[BoundarylessManifold I G]
(v : GroupLieAlgebra I G)
(x : G)
:
ℝ → G
The unique global integral curve of a left-invariant vector field through a given point.
Instances For
@[simp]
theorem
mulInvariantIntegralCurve_zero
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[CompleteSpace E]
[LieGroup I (minSmoothness ℝ 3) G]
[T2Space G]
[BoundarylessManifold I G]
(v : GroupLieAlgebra I G)
(x : G)
:
The canonical invariant integral curve starts at its specified point.
theorem
isMIntegralCurve_mulInvariantIntegralCurve
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[CompleteSpace E]
[LieGroup I (minSmoothness ℝ 3) G]
[T2Space G]
[BoundarylessManifold I G]
(v : GroupLieAlgebra I G)
(x : G)
:
The canonical invariant curve is a global integral curve of its left-invariant vector field.
theorem
hasDerivAt_extChartAt_mulInvariantIntegralCurve_zero
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[CompleteSpace E]
[LieGroup I (minSmoothness ℝ 3) G]
[T2Space G]
[BoundarylessManifold I G]
(v : E)
:
HasDerivAt (↑(extChartAt I 1) ∘ mulInvariantIntegralCurve v 1) v 0
In the extended chart at the identity, the canonical invariant curve through the identity has initial velocity equal to its generator.
theorem
contMDiff_mulInvariantIntegralCurve
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[CompleteSpace E]
[LieGroup I (↑⊤) G]
[T2Space G]
[BoundarylessManifold I G]
(v : GroupLieAlgebra I G)
(x : G)
:
ContMDiff (modelWithCornersSelf ℝ ℝ) I (↑⊤) (mulInvariantIntegralCurve v x)
The canonical integral curve of an invariant vector field on a smooth Lie group is smooth.
theorem
eq_mulInvariantIntegralCurve
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[CompleteSpace E]
[LieGroup I (minSmoothness ℝ 3) G]
[T2Space G]
[BoundarylessManifold I G]
(v : GroupLieAlgebra I G)
(x : G)
{γ : ℝ → G}
(hγ0 : γ 0 = x)
(hγ : IsMIntegralCurve γ (mulInvariantVectorField v))
:
Any global integral curve of a left-invariant vector field is the canonical one determined by its value at zero.
theorem
mulInvariantIntegralCurve_eq_const_mul
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[CompleteSpace E]
[LieGroup I (minSmoothness ℝ 3) G]
[T2Space G]
[BoundarylessManifold I G]
(v : GroupLieAlgebra I G)
(x : G)
:
The canonical invariant integral curve through x is the left translate by x of the
canonical curve through the identity.
@[simp]
theorem
mulInvariantIntegralCurve_add
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[CompleteSpace E]
[LieGroup I (minSmoothness ℝ 3) G]
[T2Space G]
[BoundarylessManifold I G]
(v : GroupLieAlgebra I G)
(s t : ℝ)
:
mulInvariantIntegralCurve v 1 (s + t) = mulInvariantIntegralCurve v 1 s * mulInvariantIntegralCurve v 1 t
The canonical invariant curve through the identity satisfies the one-parameter subgroup law.
theorem
mulInvariantIntegralCurve_smul
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[CompleteSpace E]
[LieGroup I (minSmoothness ℝ 3) G]
[T2Space G]
[BoundarylessManifold I G]
(v : GroupLieAlgebra I G)
(x : G)
(t s : ℝ)
:
Scaling an invariant vector field rescales time along its canonical integral curves.
noncomputable def
mulInvariantOneParameterSubgroup
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[CompleteSpace E]
[LieGroup I (minSmoothness ℝ 3) G]
[T2Space G]
[BoundarylessManifold I G]
(v : GroupLieAlgebra I G)
:
The canonical invariant curve through the identity, bundled as a continuous one-parameter subgroup.
Instances For
@[simp]
theorem
mulInvariantOneParameterSubgroup_apply
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[CompleteSpace E]
[LieGroup I (minSmoothness ℝ 3) G]
[T2Space G]
[BoundarylessManifold I G]
(v : GroupLieAlgebra I G)
(t : ℝ)
:
Evaluating the invariant one-parameter subgroup at time t recovers the canonical integral
curve through the identity.
theorem
contMDiff_mulInvariantOneParameterSubgroup
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[CompleteSpace E]
[LieGroup I (↑⊤) G]
[T2Space G]
[BoundarylessManifold I G]
(v : GroupLieAlgebra I G)
:
ContMDiff (modelWithCornersSelf ℝ ℝ) I ↑⊤ fun (t : ℝ) => (mulInvariantOneParameterSubgroup v) (Multiplicative.ofAdd t)
The one-parameter subgroup generated by an invariant vector field is smooth in its additive real parameter.