The infinitesimal adjoint action

This file identifies the derivative of the tangent-space adjoint action at the identity with Mathlib's Lie-algebra adjoint map. This is the geometric prerequisite for transporting the result to the derivation-valued group adjoint representation.

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

Main results

• TauCeti.Lie.hasDerivAt_tangentAd_mulInvariantExp_smul_apply_zero: at t = 0, the derivative of the tangent adjoint action along the exponential line of X is the Lie bracket.
• TauCeti.Lie.mvfderiv_tangentAd_apply_one: the differential of the tangent adjoint action at the identity is the Lie-algebra adjoint action.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1, "The infinitesimal adjoint".
• The two-parameter Clairaut argument adapts TauCeti.Lie.mvfderiv_mulRightInvariantVectorField_mulInvariantVectorField_commute; its mixed-partial step uses TauCeti.Analysis.Calculus.ParametricFDeriv, which in turn adapts Sébastien Gouëzel's ContDiffAt.isSymmSndFDerivAt.

theorem TauCeti.Lie.hasDerivAt_tangentAd_mulInvariantExp_smul_apply_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] (X Y : GroupLieAlgebra I G) : have x := ⋯; HasDerivAt (fun (t : ℝ) => have this := (tangentAd (mulInvariantExp (t • X))) Y; this) (have this := ((LieAlgebra.ad ℝ (GroupLieAlgebra I G)) X) Y; this) 0

At t = 0, the derivative of t ↦ tangentAd (mulInvariantExp (t • X)) Y along the exponential line of X is ⁅X, Y⁆.

GroupLieAlgebra I G reduces definitionally to the model E; the show E from ascriptions expose that model to the normed-space derivative API.

theorem TauCeti.Lie.mvfderiv_tangentAd_apply_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] (X Y : GroupLieAlgebra I G) : have x := ⋯; ((d% fun (g : G) => have this := (tangentAd g) Y; this) 1) X = have this := ((LieAlgebra.ad ℝ (GroupLieAlgebra I G)) X) Y; this

The derivative at 1 of g ↦ tangentAd g Y, in the direction X, is the Lie-algebra adjoint LieAlgebra.ad ℝ _ X Y.

GroupLieAlgebra I G reduces definitionally to the model E; the show E from ascriptions expose that model to the manifold derivative API.