Complementary exponential-product charts

For linear subspaces p and q of the Lie algebra of a finite-dimensional real Lie group, define the ordered product

(X, Y) ↦ lieExp X * lieExp Y

The definition, its smoothness, and its derivative formula hold for arbitrary p and q. When they are complementary, the map is a local diffeomorphism at (0, 0), with derivative the addition equivalence p × q ≃ Lie(G) transported through the canonical tangent-space coordinates.

This is the local product chart used to compare a subgroup with a linear complement of its infinitesimal directions. The result is stated for arbitrary complementary subspaces, independently of any subgroup.

Main definitions

• Submodule.lieExpMulLieExp: the ordered product of the exponentials of two linear coordinates.

Main results

• Submodule.contMDiff_lieExpMulLieExp: the exponential-product map is globally smooth.
• Submodule.groupLieAlgebraEquivModelVectorSpace_mfderiv_lieExpMulLieExp_zero_apply: for arbitrary subspaces, the derivative at zero sends a tangent vector to the coordinate of the sum of its two source components.
• Submodule.hasMFDerivAt_lieExpMulLieExp_zero_of_isCompl: for complementary subspaces, the derivative is the canonical addition equivalence in tangent-space coordinates.
• Submodule.isLocalDiffeomorphAt_lieExpMulLieExp_zero_of_isCompl: complementary subspaces give a local exponential-product chart at the identity.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd edition (2013), Theorem 20.12.

noncomputable def Submodule.lieExpMulLieExp {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] (p q : Submodule ℝ (LeftInvariantDerivation I G)) (z : ↥p × ↥q) : G

The ordered product (X, Y) ↦ lieExp X * lieExp Y for two Lie-algebra subspaces, with the p-coordinate exponential as the left factor.

@[simp]

theorem Submodule.lieExpMulLieExp_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] (p q : Submodule ℝ (LeftInvariantDerivation I G)) (z : ↥p × ↥q) : have x := ⋯; have x_1 := ⋯; have x_2 := ⋯; p.lieExpMulLieExp q z = lieExp ↑z.1 * lieExp ↑z.2

The exponential-product map evaluates by exponentiating its two coordinates in order.

theorem Submodule.lieExpMulLieExp_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] (p q : Submodule ℝ (LeftInvariantDerivation I G)) : have x := ⋯; have x := ⋯; have x := ⋯; p.lieExpMulLieExp q 0 = 1

The exponential-product map sends the zero pair to the group identity.

theorem Submodule.contMDiff_lieExpMulLieExp {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] (p q : Submodule ℝ (LeftInvariantDerivation I G)) : have x := ⋯; have x_1 := ⋯; have x_2 := ⋯; have x_3 := ⋯; ContMDiff (modelWithCornersSelf ℝ (↥p × ↥q)) I (↑⊤) (p.lieExpMulLieExp q)

The exponential-product map on two linear subspaces is smooth.

theorem Submodule.groupLieAlgebraEquivModelVectorSpace_mfderiv_lieExpMulLieExp_zero_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] (p q : Submodule ℝ (LeftInvariantDerivation I G)) : have x := ⋯; have x_1 := ⋯; have x_2 := ⋯; have x_3 := ⋯; ∀ (v : TangentSpace (modelWithCornersSelf ℝ (↥p × ↥q)) 0), groupLieAlgebraEquivModelVectorSpace ((tangentSpaceCast I 1 (p.lieExpMulLieExp q 0)).symm ((mfderiv% (p.lieExpMulLieExp q) 0) v)) = leftInvariantDerivationLinearIsometryEquivModelVectorSpace (↑((NormedSpace.fromTangentSpace 0) v).1 + ↑((NormedSpace.fromTangentSpace 0) v).2)

After the canonical source and target coordinate equivalences, the derivative of the exponential-product map at the zero pair sends (X, Y) to the coordinate of X + Y.

noncomputable def Submodule.lieExpMulLieExpMFDerivEquiv {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] (p q : Submodule ℝ (LeftInvariantDerivation I G)) (h : IsCompl p q) : have x := ⋯; have x_1 := ⋯; have x_2 := ⋯; have x_3 := ⋯; TangentSpace (modelWithCornersSelf ℝ (↥p × ↥q)) 0 ≃L[ℝ] TangentSpace I (p.lieExpMulLieExp q 0)

The tangent-space derivative equivalence of the complementary exponential-product chart.

@[simp]

theorem Submodule.lieExpMulLieExpMFDerivEquiv_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] (p q : Submodule ℝ (LeftInvariantDerivation I G)) (h : IsCompl p q) : have x := ⋯; have x_1 := ⋯; have x_2 := ⋯; have x_3 := ⋯; ∀ (z : TangentSpace (modelWithCornersSelf ℝ (↥p × ↥q)) 0), (p.lieExpMulLieExpMFDerivEquiv q h) z = (tangentSpaceCast I 1 (p.lieExpMulLieExp q 0)) (groupLieAlgebraEquivModelVectorSpace.symm (leftInvariantDerivationLinearIsometryEquivModelVectorSpace (↑((NormedSpace.fromTangentSpace 0) z).1 + ↑((NormedSpace.fromTangentSpace 0) z).2)))

The named derivative equivalence evaluates by adding source coordinates and transporting them to the target tangent space.

theorem Submodule.hasMFDerivAt_lieExpMulLieExp_zero_of_isCompl {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] (p q : Submodule ℝ (LeftInvariantDerivation I G)) (h : IsCompl p q) : have x := ⋯; have x_1 := ⋯; have x_2 := ⋯; have x_3 := ⋯; HasMFDerivAt% (p.lieExpMulLieExp q) 0 ↑(p.lieExpMulLieExpMFDerivEquiv q h)

For complementary subspaces, the derivative of the exponential-product map at zero is the canonical addition equivalence, transported through the source and target tangent-space coordinates.

theorem Submodule.isLocalDiffeomorphAt_lieExpMulLieExp_zero_of_isCompl {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] (p q : Submodule ℝ (LeftInvariantDerivation I G)) (h : IsCompl p q) : have x := ⋯; have x_1 := ⋯; have x_2 := ⋯; have x_3 := ⋯; IsLocalDiffeomorphAt (modelWithCornersSelf ℝ (↥p × ↥q)) I (↑⊤) (p.lieExpMulLieExp q) 0

Complementary linear subspaces of the Lie algebra give a local product chart at the group identity by multiplying their exponentials in order.