Derivative of the Lie-group exponential

Let center = extChartAt I 1 1 and let F be the tangent-space exponential written in the extended chart at the identity. Smoothness of the exponential makes F differentiable at zero. Along each line t ↦ t • v, the scaling law identifies F with the coordinate expression of the canonical integral curve generated by v. Its initial velocity is v, so F has derivative the identity at zero; equivalently, F(v) = F(0) + v + o(‖v‖). The same integral-curve calculation supplies reusable chain rules for functions along translated exponential lines.

Main results

• hasFDerivAt_extChartAt_mulInvariantExp_zero: in model-space identity coordinates, the tangent-space exponential has derivative the identity at zero.
• hasFDerivAt_extChartAt_lieExp_zero: the identity-chart derivative of the derivation-based exponential is the canonical linear isometry to the model space.
• hasFDerivAt_extChartAt_mulInvariantExp_smul_mul_mulInvariantExp_smul_zero: two exponential lines multiplied together have initial coordinate derivative X + Y.
• contMDiff_mulInvariantExp_smul: an exponential line is smooth.
• contMDiff_mulInvariantExp_smul_mul_mul_mulInvariantExp_smul: two exponential lines multiplied around a fixed group element give a smooth two-parameter map.
• hasMFDerivAt_mulInvariantExp_smul_zero: an exponential line has its generator as initial velocity.
• hasMFDerivAt_mulInvariantExp_smul: at every time, an exponential line's velocity is its generating left-invariant vector field at the current point.
• HasMFDerivAt.hasDerivAt_comp_mulInvariantExp_smul_zero: the chain rule along an exponential line at zero.
• HasMFDerivAt.hasDerivAt_comp_mul_mulInvariantExp_smul_zero: the chain rule after left translation at zero.
• HasMFDerivAt.hasDerivAt_comp_mulInvariantExp_smul_mul_zero: the chain rule after right translation at zero.
• LeftInvariantDerivation.hasDerivAt_apply_mul_lieExp_smul: a left-invariant derivation X is the derivative along the exponential lines t ↦ g * lieExp (t • X) it generates.

theorem exponentialLineContMDiffMulOne {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I (↑⊤) G] : ContMDiffMul I 1 G

theorem exponentialLineBoundarylessManifold {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I (↑⊤) G] : BoundarylessManifold I G

theorem contMDiff_mulInvariantExp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [CompleteSpace E] [LieGroup I (↑⊤) G] (X : GroupLieAlgebra I G) : have x := ⋯; ContMDiff (modelWithCornersSelf ℝ ℝ) I ↑⊤ fun (t : ℝ) => mulInvariantExp (t • X)

The exponential line generated by X is smooth.

theorem contMDiff_mulInvariantExp_smul_mul_mul_mulInvariantExp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [CompleteSpace E] [LieGroup I (↑⊤) G] (g : G) (X Y : GroupLieAlgebra I G) : have x := ⋯; ContMDiff (modelWithCornersSelf ℝ (ℝ × ℝ)) I ↑⊤ fun (p : ℝ × ℝ) => mulInvariantExp (p.1 • X) * g * mulInvariantExp (p.2 • Y)

Two exponential lines multiplied around a fixed group element give a smooth two-parameter map.

theorem hasMFDerivAt_mulInvariantExp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [CompleteSpace E] [LieGroup I (minSmoothness ℝ 3) G] [T2Space G] [BoundarylessManifold I G] (X : GroupLieAlgebra I G) (t : ℝ) : HasMFDerivAt% (fun (s : ℝ) => mulInvariantExp (s • X)) t (ContinuousLinearMap.smulRight 1 (mulInvariantVectorField X (mulInvariantExp (t • X))))

At time t, an exponential line has velocity the left-invariant vector field generated by X, evaluated at the point mulInvariantExp (t • X) reached by the line.

theorem hasMFDerivAt_mulInvariantExp_smul_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [CompleteSpace E] [LieGroup I (minSmoothness ℝ 3) G] [T2Space G] [BoundarylessManifold I G] (X : GroupLieAlgebra I G) : HasMFDerivAt% (fun (t : ℝ) => mulInvariantExp (t • X)) 0 (ContinuousLinearMap.smulRight 1 X)

The exponential line generated by X has initial velocity X.

theorem HasMFDerivAt.hasDerivAt_comp_mulInvariantExp_smul_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [CompleteSpace E] [LieGroup I (minSmoothness ℝ 3) G] [T2Space G] [BoundarylessManifold I G] {f : G → F} {f' : TangentSpace I 1 →L[ℝ] F} (hf : HasMFDerivAt% f 1 f') (X : GroupLieAlgebra I G) : HasDerivAt (fun (t : ℝ) => f (mulInvariantExp (t • X))) (f' X) 0

Differentiating a function that is manifold-differentiable at the identity along an exponential line gives its directional derivative there.

theorem HasMFDerivAt.hasDerivAt_comp_mul_mulInvariantExp_smul_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [CompleteSpace E] [LieGroup I (minSmoothness ℝ 3) G] [T2Space G] [BoundarylessManifold I G] {f : G → F} {g : G} {f' : TangentSpace I g →L[ℝ] F} (hf : HasMFDerivAt% f g f') (Y : GroupLieAlgebra I G) : HasDerivAt (fun (t : ℝ) => f (g * mulInvariantExp (t • Y))) (f' (mulInvariantVectorField Y g)) 0

Differentiating a function after left multiplication along an exponential line gives its left-invariant directional derivative.

theorem HasMFDerivAt.hasDerivAt_comp_mulInvariantExp_smul_mul_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [CompleteSpace E] [LieGroup I (minSmoothness ℝ 3) G] [T2Space G] [BoundarylessManifold I G] {f : G → F} {g : G} {f' : TangentSpace I g →L[ℝ] F} (hf : HasMFDerivAt% f g f') (X : GroupLieAlgebra I G) : HasDerivAt (fun (t : ℝ) => f (mulInvariantExp (t • X) * g)) (f' (mulRightInvariantVectorField X g)) 0

Differentiating a function after right multiplication along an exponential line gives its right-invariant directional derivative.

theorem hasFDerivAt_extChartAt_mulInvariantExp_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] [BoundarylessManifold I G] : HasFDerivAt (fun (v : E) => ↑(extChartAt I 1) (mulInvariantExp v)) (ContinuousLinearMap.id ℝ E) 0

In model-space identity coordinates, the tangent-space exponential has derivative the identity at zero.

theorem hasFDerivAt_extChartAt_lieExp_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] [BoundarylessManifold I G] : HasFDerivAt (fun (X : LeftInvariantDerivation I G) => ↑(extChartAt I 1) (lieExp X)) (↑↑leftInvariantDerivationLinearIsometryEquivModelVectorSpace) 0

In identity-chart coordinates, the derivative of the derivation-based Lie exponential at zero is the canonical linear isometry from left-invariant derivations to the model space.

theorem hasFDerivAt_extChartAt_mulInvariantExp_smul_mul_mulInvariantExp_smul_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [CompleteSpace E] [LieGroup I (minSmoothness ℝ 3) G] (X Y : GroupLieAlgebra I G) : have x := ⋯; have x := ⋯; have x_1 := ⋯; HasFDerivAt (fun (t : ℝ) => ↑(extChartAt I 1) (mulInvariantExp (t • X) * mulInvariantExp (t • Y))) (ContinuousLinearMap.smulRight 1 ((have this := X; this) + have this := Y; this)) 0

In identity-chart coordinates, the product of the exponential lines generated by X and Y has initial derivative X + Y.

Derivatives along exponential lines of left-invariant derivations

theorem LeftInvariantDerivation.hasDerivAt_apply_mul_lieExp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] [BoundarylessManifold I G] (X : LeftInvariantDerivation I G) (f : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) G ℝ ↑⊤) (g : G) (t : ℝ) : HasDerivAt (fun (s : ℝ) => f (g * lieExp (s • X))) ((X f) (g * lieExp (t • X))) t

A left-invariant derivation differentiates along its exponential lines. The derivative of t ↦ f (g * lieExp (t • X)) at every time t is X f at the current point.

theorem LeftInvariantDerivation.deriv_apply_mul_lieExp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] [BoundarylessManifold I G] (X : LeftInvariantDerivation I G) (f : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) G ℝ ↑⊤) (g : G) : (deriv fun (s : ℝ) => f (g * lieExp (s • X))) = fun (t : ℝ) => (X f) (g * lieExp (t • X))

The derivative of f along the exponential lines of X is X f along the same lines.