The Lie equivalence between derivations and the identity tangent space

For a finite-dimensional smooth real Lie group whose identity is an interior point, the canonical linear equivalence between left-invariant derivations and the tangent space at the identity is an equivalence of Lie algebras. This supplies the bracket-compatible dictionary needed to transport the tangent adjoint action to Mathlib's roadmap-facing Lie algebra LeftInvariantDerivation I G.

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

Main results

• tangentToLeftInvariantDerivation_lie: the invariant derivation construction preserves brackets.
• leftInvariantDerivationLieEquivGroupLieAlgebra: the canonical derivation–tangent Lie equivalence.
• leftInvariantDerivationLinearIsometryEquivModelVectorSpace_apply_eq_lieEquiv_apply: the isometric and Lie equivalences agree after viewing the tangent Lie algebra as the model space.

References

• Mathlib/Geometry/Manifold/GroupLieAlgebra.lean, whose compatibility TODO this file discharges.
• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1, "The group adjoint".

@[simp]

theorem tangentToLeftInvariantDerivation_lie {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] [CompleteSpace E] (v w : GroupLieAlgebra I G) : tangentToLeftInvariantDerivation ⁅v, w⁆ = ⁅tangentToLeftInvariantDerivation v, tangentToLeftInvariantDerivation w⁆

The map sending a tangent vector at the identity to its left-invariant derivation preserves the Lie bracket.

noncomputable def leftInvariantDerivationLieEquivGroupLieAlgebra {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] [FiniteDimensional ℝ E] (h₁ : I.IsInteriorPoint 1) : LeftInvariantDerivation I G ≃ₗ⁅ℝ⁆ GroupLieAlgebra I G

Evaluation at the identity identifies left-invariant derivations with the tangent Lie algebra as Lie algebras.

@[simp]

theorem leftInvariantDerivationLieEquivGroupLieAlgebra_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] [LieGroup I (↑⊤) G] [FiniteDimensional ℝ E] [T2Space G] (h₁ : I.IsInteriorPoint 1) (D : LeftInvariantDerivation I G) : (leftInvariantDerivationLieEquivGroupLieAlgebra h₁) D = (leftInvariantDerivationEquivGroupLieAlgebra h₁) D

The Lie equivalence acts as the underlying linear equivalence given by evaluation at the identity.

@[simp]

theorem leftInvariantDerivationLieEquivGroupLieAlgebra_symm_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] [LieGroup I (↑⊤) G] [FiniteDimensional ℝ E] (h₁ : I.IsInteriorPoint 1) (v : GroupLieAlgebra I G) : (leftInvariantDerivationLieEquivGroupLieAlgebra h₁).symm v = tangentToLeftInvariantDerivation v

The inverse Lie equivalence sends a tangent vector to its left-invariant derivation.

theorem leftInvariantDerivationLinearIsometryEquivModelVectorSpace_apply_eq_lieEquiv_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] [LieGroup I (↑⊤) G] [FiniteDimensional ℝ E] (D : LeftInvariantDerivation I G) : have x := ⋯; have x_1 := ⋯; leftInvariantDerivationLinearIsometryEquivModelVectorSpace D = have this := (leftInvariantDerivationLieEquivGroupLieAlgebra ⋯) D; this

The canonical isometric and Lie equivalences agree after viewing the tangent Lie algebra as the model vector space.

@[simp]

theorem leftInvariantDerivationEquivGroupLieAlgebra_lie {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] [FiniteDimensional ℝ E] [T2Space G] (h₁ : I.IsInteriorPoint 1) (D D' : LeftInvariantDerivation I G) : (pointDerivationEquivTangentSpace 1 h₁) ((LeftInvariantDerivation.evalAt 1) ⁅D, D'⁆) = ⁅(pointDerivationEquivTangentSpace 1 h₁) ((LeftInvariantDerivation.evalAt 1) D), (pointDerivationEquivTangentSpace 1 h₁) ((LeftInvariantDerivation.evalAt 1) D')⁆

Evaluation at the identity preserves the Lie bracket.