The tangent-space adjoint action of a Lie group

The tangent-space adjoint action is the differential at the identity of conjugation. We first prove that this differential transports left-invariant vector fields. Naturality of the manifold Lie bracket then shows that it is a Lie algebra automorphism, and the composition law for conjugation gives the representation law. A subsequent file transports this construction to the roadmap-facing Lie algebra of left-invariant derivations.

The construction works over any nontrivially normed field. Its differential only requires a C¹ Lie group; preservation of the bracket uses Mathlib's regularity threshold minSmoothness 𝕜 3, which is 3 over the real and complex numbers.

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

Main definitions

• TauCeti.Lie.tangentAd: the resulting tangent Lie algebra automorphism.

Main results

• TauCeti.Lie.mfderiv_mul_right_mulInvariantVectorField: right translation by g carries the left-invariant vector field of X to that of Ad_{g⁻¹} X.
• TauCeti.Lie.adjointContinuousLinearMap_lie: the differential preserves the Lie bracket.
• TauCeti.Lie.tangentAd_mul: the tangent adjoint automorphism respects group multiplication.
• MonoidHom.groupLieAlgebraMap_adjointContinuousLinearMap: a homomorphism intertwines the adjoint actions of its differential at the identity, dφ (Ad_k ξ) = Ad_{φ k} (dφ ξ).

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1, "The group adjoint".
• Sébastien Gouëzel's Mathlib.Geometry.Manifold.GroupLieAlgebra, especially inverse_mfderiv_mul_left, mpullback_mulInvariantVectorField, and mulInvariantVector_mlieBracket; the corresponding conjugation arguments below adapt the derivative-inverse and pullback/bracket proof patterns developed there.

noncomputable def TauCeti.Lie.adjointContinuousLinearEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I 1 G] (g : G) : GroupLieAlgebra I G ≃L[𝕜] GroupLieAlgebra I G

The continuous linear equivalence given by the differential of conjugation at the identity.

@[simp]

theorem TauCeti.Lie.adjointContinuousLinearEquiv_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I 1 G] (g : G) : ↑(adjointContinuousLinearEquiv g) = mfderiv% ⇑(conjDiffeomorph g) 1

noncomputable def TauCeti.Lie.adjointContinuousLinearMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I 1 G] (g : G) : GroupLieAlgebra I G →L[𝕜] GroupLieAlgebra I G

The continuous linear map underlying the differential of conjugation at the identity.

@[simp]

theorem TauCeti.Lie.adjointContinuousLinearMap_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I 1 G] (g : G) (X : GroupLieAlgebra I G) : (adjointContinuousLinearMap g) X = (mfderiv% ⇑(conjDiffeomorph g) 1) X

@[simp]

theorem TauCeti.Lie.adjointContinuousLinearMap_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I 1 G] : adjointContinuousLinearMap 1 = ContinuousLinearMap.id 𝕜 (GroupLieAlgebra I G)

@[simp]

theorem TauCeti.Lie.adjointContinuousLinearMap_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I 1 G] (g h : G) : adjointContinuousLinearMap (g * h) = adjointContinuousLinearMap g ∘SL adjointContinuousLinearMap h

theorem MonoidHom.groupLieAlgebraMap_adjointContinuousLinearMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I 1 G] {F : Type u_5} {HK : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace HK] {J : ModelWithCorners 𝕜 F HK} {K : Type u_7} [TopologicalSpace K] [ChartedSpace HK K] [Group K] [LieGroup J 1 K] (φ : K →* G) (k : K) (ξ : GroupLieAlgebra J K) : (φ.groupLieAlgebraMap J I) ((TauCeti.Lie.adjointContinuousLinearMap k) ξ) = (TauCeti.Lie.adjointContinuousLinearMap (φ k)) ((φ.groupLieAlgebraMap J I) ξ)

Naturality of the adjoint action. A group homomorphism φ : K →* G intertwines the adjoint actions: dφ (Ad_k ξ) = Ad_{φ k} (dφ ξ), where dφ is the differential of φ at the identity (zero if φ is not differentiable there, in which case both sides vanish).

theorem TauCeti.Lie.inverse_mfderiv_conjugation {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I 1 G] (g x : G) : (mfderiv% ⇑(conjDiffeomorph g) x).inverse = mfderiv% ⇑(conjDiffeomorph g⁻¹) ((conjDiffeomorph g) x)

The inverse of the derivative of conjugation by g is the derivative of conjugation by g⁻¹ at the conjugated point.

theorem TauCeti.Lie.mfderiv_conjugation_mulInvariantVectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I 1 G] (g x : G) (X : GroupLieAlgebra I G) : (mfderiv% ⇑(conjDiffeomorph g) x) (mulInvariantVectorField X x) = mulInvariantVectorField ((adjointContinuousLinearMap g) X) ((conjDiffeomorph g) x)

The derivative of conjugation by g transports a left-invariant vector field to the field whose value at the identity is the adjoint image.

theorem TauCeti.Lie.mfderiv_mul_right_mulInvariantVectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I 1 G] (g x : G) (X : GroupLieAlgebra I G) : ((mfderiv% fun (x : G) => x * g) x) (mulInvariantVectorField X x) = mulInvariantVectorField ((adjointContinuousLinearMap g⁻¹) X) (x * g)

The derivative of right translation by g transports the left-invariant vector field generated by X to the one generated by its adjoint image Ad_{g⁻¹} X.

theorem TauCeti.Lie.mpullback_conjugation {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I 1 G] (g x : G) (V : (y : G) → TangentSpace I y) : VectorField.mpullback I I (⇑(conjDiffeomorph g⁻¹)) V x = (mfderiv% ⇑(conjDiffeomorph g) ((conjDiffeomorph g⁻¹) x)) (V ((conjDiffeomorph g⁻¹) x))

Pullback through inverse conjugation is the derivative of forward conjugation.

theorem TauCeti.Lie.mpullback_conjugation_mulInvariantVectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I 1 G] (g : G) (X : GroupLieAlgebra I G) : VectorField.mpullback I I (⇑(conjDiffeomorph g⁻¹)) (mulInvariantVectorField X) = mulInvariantVectorField ((adjointContinuousLinearMap g) X)

Pullback by conjugation by g⁻¹ sends the left-invariant field of X to the left-invariant field of the adjoint image of X.

theorem TauCeti.Lie.mpullback_conjugation_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I 1 G] (g : G) (V : (x : G) → TangentSpace I x) : VectorField.mpullback I I (⇑(conjDiffeomorph g⁻¹)) V 1 = (adjointContinuousLinearMap g) (V 1)

At the identity, pullback by conjugation by g⁻¹ is the adjoint differential of g.

theorem TauCeti.Lie.lieGroupOne {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I (minSmoothness 𝕜 3) G] : LieGroup I 1 G

theorem TauCeti.Lie.adjointContinuousLinearMap_lie {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I (minSmoothness 𝕜 3) G] [CompleteSpace E] (g : G) (X Y : GroupLieAlgebra I G) : (adjointContinuousLinearMap g) ⁅X, Y⁆ = ⁅(adjointContinuousLinearMap g) X, (adjointContinuousLinearMap g) Y⁆

The differential of conjugation preserves the manifold Lie bracket.

noncomputable def TauCeti.Lie.tangentAd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I (minSmoothness 𝕜 3) G] [CompleteSpace E] (g : G) : GroupLieAlgebra I G ≃ₗ⁅𝕜⁆ GroupLieAlgebra I G

The group adjoint automorphism: the differential at the identity of conjugation by g.

@[simp]

theorem TauCeti.Lie.tangentAd_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I (minSmoothness 𝕜 3) G] [CompleteSpace E] (g : G) (X : GroupLieAlgebra I G) : (tangentAd g) X = (adjointContinuousLinearMap g) X

@[simp]

theorem TauCeti.Lie.tangentAd_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I (minSmoothness 𝕜 3) G] [CompleteSpace E] : tangentAd 1 = LieEquiv.refl

The tangent adjoint automorphism at the identity is the identity Lie equivalence.

@[simp]

theorem TauCeti.Lie.tangentAd_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I (minSmoothness 𝕜 3) G] [CompleteSpace E] (g h : G) : tangentAd (g * h) = (tangentAd h).trans (tangentAd g)

The tangent adjoint action sends a product to the composite of the two adjoint maps.

@[simp]

theorem TauCeti.Lie.tangentAd_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I (minSmoothness 𝕜 3) G] [CompleteSpace E] (g : G) : tangentAd g⁻¹ = (tangentAd g).symm

The tangent adjoint automorphism of g⁻¹ is the inverse of that of g.