Naturality of the Lie-group exponential under conjugation

Conjugation transports the integral curve generated by a tangent vector to the integral curve generated by its tangent adjoint image. Evaluating at time one gives the conjugation formula for the Lie-group exponential. No separate Hausdorff or boundaryless hypotheses are needed: both follow from the Lie-group structure.

This advances Deliverable A, Layer 1 of TauCetiRoadmap/RepresentationTheory/LieGroups/README.md.

Main results

• TauCeti.Lie.conj_mulInvariantIntegralCurve: conjugation transports canonical invariant integral curves and their basepoints through tangentAd.
• TauCeti.Lie.conj_mulInvariantExp: conjugating mulInvariantExp X by g gives the exponential of tangentAd g X.
• TauCeti.Lie.conj_lieExp: conjugating lieExp X by g gives the exponential of Ad g X.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1, "The conjugation formulas".

theorem TauCeti.Lie.lieGroupOneAdjointExponential {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] [LieGroup I 3 G] : LieGroup I 1 G

@[simp]

theorem TauCeti.Lie.conj_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 3 G] (g : G) (X : GroupLieAlgebra I G) (x : G) (t : ℝ) : have x_1 := ⋯; g * mulInvariantIntegralCurve X x t * g⁻¹ = mulInvariantIntegralCurve ((tangentAd g) X) (g * x * g⁻¹) t

Conjugation transports the canonical invariant integral curve generated by X to the one generated by the tangent adjoint image of X, with the basepoint conjugated as well.

@[simp]

theorem TauCeti.Lie.conj_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 3 G] (g : G) (X : GroupLieAlgebra I G) : have x := ⋯; g * mulInvariantExp X * g⁻¹ = mulInvariantExp ((tangentAd g) X)

Conjugating mulInvariantExp X by g gives the exponential of tangentAd g X.

@[simp]

theorem TauCeti.Lie.conj_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] (g : G) (X : LeftInvariantDerivation I G) : have x := ⋯; g * lieExp X * g⁻¹ = lieExp ((Ad g) X)

Conjugating the group-valued exponential of X by g gives the exponential of Ad g X.