Smoothness of the Lie-group exponential #
This file upgrades the continuous local invariant flow to smooth parameter dependence, proves that the Lie-group exponential is smooth at the zero vector, and globalizes that result using its one-parameter-subgroup law.
Main results #
contMDiffAt_mulInvariantExp_modelSpace_zero: the tangent-space exponential is smooth at zero.contMDiff_mulInvariantExp: the tangent-space exponential is smooth everywhere.contMDiff_lieExp: the derivation-based Lie-group exponential is smooth everywhere.
References #
- Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 0, "The exponential map".
theorem
contMDiffAt_mulInvariantExp_modelSpace_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]
[FiniteDimensional ℝ E]
[LieGroup I (↑⊤) G]
[T2Space G]
[BoundarylessManifold I G]
:
ContMDiffAt (modelWithCornersSelf ℝ E) I (↑⊤) (fun (v : E) => mulInvariantExp v) 0
The tangent-space exponential of a finite-dimensional smooth Lie group is smooth at zero.
theorem
contMDiff_mulInvariantExp
{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]
[FiniteDimensional ℝ E]
[LieGroup I (↑⊤) G]
[T2Space G]
[BoundarylessManifold I G]
:
ContMDiff (modelWithCornersSelf ℝ E) I ↑⊤ fun (v : E) => mulInvariantExp v
The tangent-space exponential of a finite-dimensional smooth Lie group is smooth.
theorem
contMDiff_lieExp
{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]
[FiniteDimensional ℝ E]
[LieGroup I (↑⊤) G]
[T2Space G]
[BoundarylessManifold I G]
:
ContMDiff (modelWithCornersSelf ℝ (LeftInvariantDerivation I G)) I (↑⊤) lieExp
The derivation-based exponential of a finite-dimensional smooth Lie group is smooth.