Smoothness of the tangent adjoint action

The differential of conjugation depends smoothly on the conjugating group element. Mathlib's smoothness theorem for manifold derivatives expresses the derivative in a moving chart frame. Since conjugation fixes the identity, this file cancels the resulting fixed tangent trivialization to recover the unframed tangent adjoint operator and its jointly smooth evaluation action.

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

Main results

• TauCeti.Lie.contMDiff_adjointContinuousLinearMap: the adjoint operator depends smoothly on the group element.
• TauCeti.Lie.contMDiff_tangentAd_apply: the bundled tangent adjoint action is jointly smooth.
• TauCeti.Lie.contMDiff_tangentAd_apply_const: the bundled tangent adjoint action on a fixed model vector is smooth in the group element.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1, "The group adjoint".
• Sébastien Gouëzel and Floris van Doorn's Mathlib.Geometry.Manifold.ContMDiffMFDeriv, especially ContMDiffAt.mfderiv, supplies smoothness of the conjugation differential in a fixed frame. The frame cancellation follows the argument for Pretrivialization.continuousLinearMap in Mathlib.Topology.VectorBundle.Hom.

theorem TauCeti.Lie.contMDiff_adjointContinuousLinearMap {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 (↑⊤) G] : ContMDiff I (modelWithCornersSelf ℝ (E →L[ℝ] E)) ↑⊤ fun (g : G) => have this := adjointContinuousLinearMap g; this

The continuous linear operator underlying the tangent adjoint action depends smoothly on the group element.

theorem TauCeti.Lie.contMDiff_tangentAd_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] [CompleteSpace E] [LieGroup I (↑⊤) G] : ContMDiff (I.prod (modelWithCornersSelf ℝ E)) (modelWithCornersSelf ℝ E) ↑⊤ fun (p : G × E) => have this := (tangentAd p.1) p.2; this

The bundled tangent adjoint action is jointly smooth in the group element and model vector.

theorem TauCeti.Lie.contMDiff_tangentAd_apply_const {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 (↑⊤) G] (Y : E) : ContMDiff I (modelWithCornersSelf ℝ E) ↑⊤ fun (g : G) => have this := (tangentAd g) Y; this

The bundled tangent adjoint action on a fixed model vector is smooth in the group element.