Local inverse of the Lie-group exponential

The smooth coordinate exponential has derivative the identity at zero, so the inverse function theorem supplies a chosen smooth local logarithm in model-space identity coordinates.

Transporting that logarithm through the identity chart gives a group-level local inverse for the tangent-space exponential.

Main results

• mulInvariantLog: a local logarithm from the group to its tangent Lie algebra.
• lieLog: the same chosen local logarithm, valued in left-invariant derivations.
• hasFDerivAt_mulInvariantLogChart_one: the coordinate logarithm has derivative the identity at the identity coordinate.
• eventually_mulInvariantExp_log: exponential followed after logarithm is locally the identity.
• eventually_mulInvariantLog_exp: logarithm followed after exponential is locally the identity.
• TauCeti.eventuallyEq_of_tendsto_of_lieExp_eventuallyEq: lieExp is locally injective at zero, in filter form.
• isLocalDiffeomorphAt_lieExp_zero: the canonical Lie-group exponential is a local C∞ local diffeomorphism at zero.
• isLocalDiffeomorphAt_mulInvariantExpChart_zero: the fully charted exponential is a local C∞ local diffeomorphism at zero.
• exists_injOn_mulInvariantExp_modelSpace: exponential is injective near zero.
• TauCeti.exists_contMDiffMap_eventually_apply_lieExp_eq: every smooth germ on the Lie algebra at zero is the pullback along lieExp of a globally smooth function on the group.

References

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

noncomputable def mulInvariantExpChart {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] (v : E) : E

The tangent-space exponential with both domain and codomain expressed in identity-chart coordinates.

theorem mulInvariantExpChart_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] (v : E) : mulInvariantExpChart v = ↑(extChartAt I 1) (mulInvariantExp v)

The fully charted exponential is the identity chart applied to the tangent-space exponential.

@[simp]

theorem mulInvariantExpChart_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] : mulInvariantExpChart 0 = ↑(extChartAt I 1) 1

The coordinate exponential sends zero to the identity coordinate.

theorem contDiffAt_mulInvariantExpChart_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] : ContDiffAt ℝ (↑⊤) mulInvariantExpChart 0

The coordinate exponential is smooth at zero.

theorem hasFDerivAt_mulInvariantExpChart_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] : HasFDerivAt mulInvariantExpChart (ContinuousLinearMap.id ℝ E) 0

The coordinate exponential has derivative the identity at zero.

noncomputable def mulInvariantExpOpenPartialHomeomorph {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] : OpenPartialHomeomorph E E

The fully charted exponential on the neighborhoods selected by the inverse function theorem.

@[simp]

theorem mulInvariantExpOpenPartialHomeomorph_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] (v : E) : ↑mulInvariantExpOpenPartialHomeomorph v = mulInvariantExpChart v

The local homeomorphism agrees with the coordinate exponential.

theorem zero_mem_mulInvariantExpOpenPartialHomeomorph_source {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] : 0 ∈ mulInvariantExpOpenPartialHomeomorph.source

Zero belongs to the source of the local coordinate exponential.

theorem one_mem_mulInvariantExpOpenPartialHomeomorph_target {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] : ↑(extChartAt I 1) 1 ∈ mulInvariantExpOpenPartialHomeomorph.target

The identity coordinate belongs to the target of the local coordinate exponential.

noncomputable def mulInvariantLogChart {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] : E → E

The logarithm selected by the inverse function theorem, with domain and codomain in identity-chart coordinates. Its values outside the selected target neighborhood carry no logarithmic meaning.

theorem mulInvariantLogChart_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] (y : E) : mulInvariantLogChart y = ↑mulInvariantExpOpenPartialHomeomorph.symm y

The fully charted logarithm is the inverse of the chosen local homeomorphism.

@[simp]

theorem mulInvariantLogChart_one {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] : mulInvariantLogChart (↑I (↑(chartAt H 1) 1)) = 0

The coordinate logarithm sends the identity coordinate to zero.

theorem eventually_mulInvariantLogChart_exp {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] : ∀ᶠ (v : E) in nhds 0, mulInvariantLogChart (mulInvariantExpChart v) = v

Locally around zero, logarithm is a left inverse to the coordinate exponential.

theorem eventually_mulInvariantExpChart_log {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] : ∀ᶠ (y : E) in nhds (↑(extChartAt I 1) 1), mulInvariantExpChart (mulInvariantLogChart y) = y

Locally around the identity coordinate, exponential is a left inverse to logarithm.

theorem contDiffAt_mulInvariantLogChart_one {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] : ContDiffAt ℝ (↑⊤) mulInvariantLogChart (↑(extChartAt I 1) 1)

The coordinate logarithm is smooth at the identity coordinate.

theorem hasFDerivAt_mulInvariantLogChart_one {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] : HasFDerivAt mulInvariantLogChart (ContinuousLinearMap.id ℝ E) (↑(extChartAt I 1) 1)

The coordinate logarithm has derivative the identity at the identity coordinate.

noncomputable def mulInvariantLog {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] (g : G) : GroupLieAlgebra I G

The local logarithm of a group element, valued in the tangent Lie algebra at the identity. It is the coordinate logarithm transported back from the manifold model space. Its values outside the selected identity neighborhood carry no logarithmic meaning.

theorem mulInvariantLog_eq_chart {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] (g : G) : (have this := mulInvariantLog g; this) = mulInvariantLogChart (↑(extChartAt I 1) g)

The group-level local logarithm is the coordinate logarithm after applying the identity chart.

theorem contMDiffAt_mulInvariantLog_one {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 I (modelWithCornersSelf ℝ E) (↑⊤) (fun (g : G) => have this := mulInvariantLog g; this) 1

The tangent-valued local logarithm is smooth at the group identity.

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

The local Lie logarithm, valued in the canonical Lie algebra of left-invariant derivations. Its values outside the identity neighborhood selected by the inverse function theorem carry no logarithmic meaning.

theorem lieLog_eq {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] (g : G) : lieLog g = leftInvariantDerivationLinearIsometryEquivModelVectorSpace.symm (mulInvariantLog g)

The derivation-valued local Lie logarithm is the tangent-valued logarithm transported through the derivation–tangent equivalence.

theorem contMDiffAt_lieLog_one {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 I (modelWithCornersSelf ℝ (LeftInvariantDerivation I G)) (↑⊤) lieLog 1

The derivation-valued local Lie logarithm is smooth at the group identity.

theorem eventually_mulInvariantLog_exp {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] : ∀ᶠ (v : GroupLieAlgebra I G) in nhds 0, (have this := mulInvariantLog (mulInvariantExp v); this) = v

Locally around zero, taking the local logarithm after exponentiating recovers the original tangent vector.

@[simp]

theorem mulInvariantLog_one {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] : mulInvariantLog 1 = 0

The local logarithm sends the group identity to the zero tangent vector.

@[simp]

theorem lieLog_one {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] : lieLog 1 = 0

The derivation-valued local Lie logarithm sends the group identity to the zero derivation.

theorem eventually_lieLog_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) in nhds 0, lieLog (lieExp X) = X

Locally around zero, the derivation-valued Lie logarithm is a left inverse to lieExp.

theorem eventually_mulInvariantExp_log {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] : ∀ᶠ (g : G) in nhds 1, mulInvariantExp (mulInvariantLog g) = g

Locally around the identity, exponentiating the local logarithm recovers the original group element.

theorem eventually_lieExp_lieLog {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] : ∀ᶠ (g : G) in nhds 1, lieExp (lieLog g) = g

Locally around the identity, lieExp is a left inverse to the derivation-valued Lie logarithm.

theorem TauCeti.eventuallyEq_of_tendsto_of_lieExp_eventuallyEq {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] {α : Type u_4} {l : Filter α} {f g : α → LeftInvariantDerivation I G} (hf : Filter.Tendsto f l (nhds 0)) (hg : Filter.Tendsto g l (nhds 0)) (h : (fun (a : α) => lieExp (f a)) =ᶠ[l] fun (a : α) => lieExp (g a)) : f =ᶠ[l] g

The Lie-group exponential is locally injective at zero. Two functions into the Lie algebra that tend to zero along a filter and have eventually equal exponentials are eventually equal.

theorem exists_injOn_mulInvariantExp_modelSpace {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] : ∃ U ∈ nhds 0, Set.InjOn (fun (v : E) => mulInvariantExp v) U

In model-space coordinates, the tangent-space exponential is injective on a neighborhood of zero.

theorem isLocalDiffeomorphAt_mulInvariantExpChart_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] : IsLocalDiffeomorphAt (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E) (↑⊤) mulInvariantExpChart 0

The fully charted exponential is a smooth local diffeomorphism at zero.

theorem isLocalDiffeomorphAt_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] : IsLocalDiffeomorphAt (modelWithCornersSelf ℝ E) I (↑⊤) (fun (v : E) => mulInvariantExp v) 0

The tangent-space exponential, viewed as a group-valued map on model coordinates, is a smooth local diffeomorphism at zero.

theorem isLocalDiffeomorphAt_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] : IsLocalDiffeomorphAt (modelWithCornersSelf ℝ (LeftInvariantDerivation I G)) I (↑⊤) lieExp 0

The canonical Lie-group exponential is a smooth local diffeomorphism at zero.

theorem TauCeti.exists_contMDiffMap_eventually_apply_lieExp_eq {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] {φ : LeftInvariantDerivation I G → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : ∃ (f : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) G ℝ ↑⊤), ∀ᶠ (Y : LeftInvariantDerivation I G) in nhds 0, f (lieExp Y) = φ Y

Smooth functions with a prescribed germ along the exponential. Every smooth function φ on the Lie algebra is, near 0, the composite of a globally smooth function on G with the exponential.