The exponential map of a Lie group

This file defines the tangent-space exponential of a real Lie group modeled on a complete normed space by evaluating the canonical invariant one-parameter subgroup at time one. For a finite-dimensional smooth Lie group, it transports this construction across the canonical equivalence between left-invariant derivations and tangent vectors at the identity to obtain the roadmap-facing Lie-group exponential.

Main results

• mulInvariantExp: the time-one value of the invariant curve attached to a tangent vector.
• mulInvariantExp_smul: scaling a tangent vector is evaluation at the corresponding time.
• mulInvariantOneParameterSubgroup_eq_mulInvariantExp_smul: the bundled subgroup is the exponential along a line.
• mulInvariantExp_add_smul: the exponential along a fixed line is a one-parameter subgroup.
• mulInvariantExp_nsmul: natural scaling of a tangent vector becomes a group power.
• mulInvariantExp_zero, mulInvariantExp_neg: the identity and inverse laws.
• lieExp: the exponential map on Mathlib's Lie algebra of left-invariant derivations.
• lieExp_nsmul: natural scaling of a derivation becomes a group power.
• lieExp_inv_natCast_smul_pow: the n-th power of the exponential of X / n is that of X.
• oneParameterSubgroup: the continuous one-parameter subgroup generated by a derivation.
• oneParameterSubgroup_eq_mulInvariantOneParameterSubgroup: the public rewrite theorem exposing the transported tangent-space subgroup across the module boundary.
• contMDiff_oneParameterSubgroup: the generated subgroup is smooth in its real parameter.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 0, "The exponential map".

noncomputable def 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] [CompleteSpace E] [LieGroup I (minSmoothness ℝ 3) G] [T2Space G] [BoundarylessManifold I G] (v : GroupLieAlgebra I G) : G

The tangent-space exponential obtained by evaluating the canonical invariant curve at time one. This is the tangent-vector precursor of the roadmap's derivation-based lieExp.

theorem mulInvariantExp_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) : mulInvariantExp v = mulInvariantIntegralCurve v 1 1

The tangent-space exponential is the canonical invariant integral curve evaluated at time one.

theorem mulInvariantExp_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) (t : ℝ) : mulInvariantExp (t • v) = mulInvariantIntegralCurve v 1 t

Scaling a tangent vector corresponds to evaluating its invariant integral curve at the scale factor.

theorem mulInvariantOneParameterSubgroup_eq_mulInvariantExp_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) (t : ℝ) : (mulInvariantOneParameterSubgroup v) (Multiplicative.ofAdd t) = mulInvariantExp (t • v)

The canonical one-parameter subgroup is the tangent-space exponential along its generating line.

@[simp]

theorem mulInvariantExp_add_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) (s t : ℝ) : mulInvariantExp ((s + t) • v) = mulInvariantExp (s • v) * mulInvariantExp (t • v)

The exponential along a line satisfies the one-parameter subgroup law.

theorem mulInvariantExp_nsmul {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) (m : ℕ) : mulInvariantExp (m • v) = mulInvariantExp v ^ m

Scaling a tangent vector by a natural number corresponds to taking the associated group element to that power.

@[simp]

theorem mulInvariantExp_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] : mulInvariantExp 0 = 1

The tangent-space exponential sends zero to the group identity.

@[simp]

theorem mulInvariantExp_neg {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) : mulInvariantExp (-v) = (mulInvariantExp v)⁻¹

The tangent-space exponential sends negation to inversion.

noncomputable def 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] (X : LeftInvariantDerivation I G) : G

The exponential map of a finite-dimensional smooth real Lie group, obtained by evaluating at time one the invariant integral curve whose tangent vector corresponds to a left-invariant derivation.

theorem lieExp_eq_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] (X : LeftInvariantDerivation I G) : lieExp X = mulInvariantExp ((leftInvariantDerivationEquivGroupLieAlgebra ⋯) X)

The derivation-based exponential is the tangent-space exponential transported through the canonical equivalence at the identity.

@[simp]

theorem lieExp_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] : lieExp 0 = 1

The Lie-group exponential sends the zero derivation to the group identity.

@[simp]

theorem lieExp_neg {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] (X : LeftInvariantDerivation I G) : lieExp (-X) = (lieExp X)⁻¹

The Lie-group exponential sends negation to inversion.

@[simp]

theorem lieExp_add_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] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] [BoundarylessManifold I G] (X : LeftInvariantDerivation I G) (s t : ℝ) : lieExp ((s + t) • X) = lieExp (s • X) * lieExp (t • X)

The exponential along a fixed derivation satisfies the one-parameter subgroup law.

theorem lieExp_nsmul {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] (X : LeftInvariantDerivation I G) (m : ℕ) : lieExp (m • X) = lieExp X ^ m

Scaling a derivation by a natural number corresponds to taking its exponential to that power.

theorem lieExp_inv_natCast_smul_pow {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] (X : LeftInvariantDerivation I G) {n : ℕ} (hn : n ≠ 0) : lieExp ((↑n)⁻¹ • X) ^ n = lieExp X

The n-th power of the exponential of X / n is the exponential of X.

noncomputable def oneParameterSubgroup {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] (X : LeftInvariantDerivation I G) : Multiplicative ℝ →ₜ* G

The continuous one-parameter subgroup generated by a left-invariant derivation.

theorem oneParameterSubgroup_eq_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] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] [BoundarylessManifold I G] (X : LeftInvariantDerivation I G) : oneParameterSubgroup X = mulInvariantOneParameterSubgroup ((leftInvariantDerivationEquivGroupLieAlgebra ⋯) X)

The derivation-based one-parameter subgroup is the invariant tangent-space subgroup after transporting its generator through evaluation at the identity. This theorem exposes the defining equation across the module boundary, where the definition body itself is not reducible.

@[simp]

theorem oneParameterSubgroup_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] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] [BoundarylessManifold I G] (X : LeftInvariantDerivation I G) (t : ℝ) : (oneParameterSubgroup X) (Multiplicative.ofAdd t) = lieExp (t • X)

Evaluating the one-parameter subgroup generated by X at time t gives lieExp (t • X).

theorem contMDiff_oneParameterSubgroup {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] (X : LeftInvariantDerivation I G) : ContMDiff (modelWithCornersSelf ℝ ℝ) I ↑⊤ fun (t : ℝ) => (oneParameterSubgroup X) (Multiplicative.ofAdd t)

The one-parameter subgroup generated by a left-invariant derivation is smooth in its additive real parameter.