Evaluation of left-invariant derivations

A left-invariant derivation on a Lie group is determined by its value at any point. For a finite-dimensional smooth real Lie group whose identity is an interior point, evaluation there gives a canonical linear equivalence between left-invariant derivations and the tangent Lie algebra. The latter is the manifold model vector space, so this also determines the Lie algebra's dimension.

Main results

• LeftInvariantDerivation.evalAt_one_injective: identity evaluation is injective for monoids.
• LeftInvariantDerivation.evalAt_injective: evaluation at any point is injective.
• tangentToLeftInvariantDerivation: the left-invariant derivation associated to a tangent vector at the identity.
• leftInvariantDerivationEquivGroupLieAlgebra: the canonical linear equivalence between left-invariant derivations and the tangent Lie algebra.
• leftInvariantDerivationLinearIsometryEquivModelVectorSpace: the canonical isometric linear equivalence with the manifold model vector space.
• finiteDimensional_leftInvariantDerivation: the Lie algebra is finite-dimensional.
• finrank_leftInvariantDerivation_eq_modelVectorSpace: its dimension equals that of the manifold model vector space.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 0, "The Lie algebra and the tangent space at 1".

theorem LeftInvariantDerivation.evalAt_one_injective {𝕜 : 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] [Monoid G] [ContMDiffMul I (↑⊤) G] : Function.Injective ⇑(evalAt 1)

A left-invariant derivation on a monoid is determined by its value at the identity.

theorem LeftInvariantDerivation.evalAt_injective {𝕜 : 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] [ContMDiffMul I (↑⊤) G] (g₀ : G) : Function.Injective ⇑(evalAt g₀)

A left-invariant derivation is determined by its value at any point.

theorem contMDiff_mvfderiv_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] [ContMDiffMul I (↑⊤) G] (v : GroupLieAlgebra I G) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤) : ContMDiff I (modelWithCornersSelf 𝕜 𝕜) ↑⊤ fun (g : G) => (d% ⇑f g) (mulInvariantVectorField v g)

Differentiating a smooth scalar function along a left-invariant vector field gives a smooth scalar function.

noncomputable def tangentToLeftInvariantDerivation {𝕜 : 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] [ContMDiffMul I (↑⊤) G] : GroupLieAlgebra I G →ₗ[𝕜] LeftInvariantDerivation I G

The left-invariant derivation associated to a tangent vector at the identity. At every point it acts by differentiating along Mathlib's corresponding left-invariant vector field.

@[simp]

theorem tangentToLeftInvariantDerivation_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] [ContMDiffMul I (↑⊤) G] (v : GroupLieAlgebra I G) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤) (g : G) : ((tangentToLeftInvariantDerivation v) f) g = (d% ⇑f g) (mulInvariantVectorField v g)

The derivation built from a tangent vector acts pointwise along its invariant vector field.

@[simp]

theorem LeftInvariantDerivation.evalAt_one_tangentToLeftInvariantDerivation {𝕜 : 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] [ContMDiffMul I (↑⊤) G] (v : GroupLieAlgebra I G) : (evalAt 1) (tangentToLeftInvariantDerivation v) = (tangentToPointDerivation 1) v

Evaluating the derivation associated to v at the identity gives directional differentiation along v.

theorem LeftInvariantDerivation.evalAt_one_surjective {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] [ContMDiffMul I (↑⊤) G] [T2Space G] (h₁ : I.IsInteriorPoint 1) : Function.Surjective ⇑(evalAt 1)

Evaluation at the identity is onto point derivations on a finite-dimensional smooth real Lie group.

noncomputable def leftInvariantDerivationEquivGroupLieAlgebra {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] [ContMDiffMul I (↑⊤) G] [T2Space G] (h₁ : I.IsInteriorPoint 1) : LeftInvariantDerivation I G ≃ₗ[ℝ] GroupLieAlgebra I G

Left-invariant derivations are canonically linearly equivalent to the tangent Lie algebra at the identity.

@[instance_reducible]

noncomputable instance LeftInvariantDerivation.instNormedAddCommGroup {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] [ContMDiffMul I (↑⊤) G] [T2Space G] [BoundarylessManifold I G] : NormedAddCommGroup (LeftInvariantDerivation I G)

@[instance_reducible]

noncomputable instance LeftInvariantDerivation.instNormedSpace {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] [ContMDiffMul I (↑⊤) G] [T2Space G] [BoundarylessManifold I G] : NormedSpace ℝ (LeftInvariantDerivation I G)

@[simp]

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

The derivation–tangent equivalence is evaluation at the identity followed by the point-derivation–tangent equivalence.

@[simp]

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

The inverse derivation–tangent equivalence is the explicit invariant-derivation construction.

noncomputable def leftInvariantDerivationLinearIsometryEquivModelVectorSpace {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] [ContMDiffMul I (↑⊤) G] [T2Space G] [BoundarylessManifold I G] : LeftInvariantDerivation I G ≃ₗᵢ[ℝ] E

Evaluation at the identity identifies left-invariant derivations isometrically with the manifold model vector space.

@[simp]

theorem leftInvariantDerivationLinearIsometryEquivModelVectorSpace_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] [FiniteDimensional ℝ E] [ContMDiffMul I (↑⊤) G] [T2Space G] [BoundarylessManifold I G] (X : LeftInvariantDerivation I G) : leftInvariantDerivationLinearIsometryEquivModelVectorSpace X = (leftInvariantDerivationEquivGroupLieAlgebra ⋯) X

The isometric derivation–model-space equivalence is evaluation at the identity followed by the canonical identification of the identity tangent space with the model vector space.

@[simp]

theorem leftInvariantDerivationLinearIsometryEquivModelVectorSpace_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] [FiniteDimensional ℝ E] [ContMDiffMul I (↑⊤) G] [T2Space G] [BoundarylessManifold I G] (v : E) : leftInvariantDerivationLinearIsometryEquivModelVectorSpace.symm v = tangentToLeftInvariantDerivation v

The inverse isometric model-space equivalence constructs the canonical left-invariant derivation generated by the corresponding tangent vector.

@[simp]

theorem norm_leftInvariantDerivation_eq_norm_modelVectorSpace {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] [ContMDiffMul I (↑⊤) G] [T2Space G] [BoundarylessManifold I G] (X : LeftInvariantDerivation I G) : ‖X‖ = ‖leftInvariantDerivationLinearIsometryEquivModelVectorSpace X‖

The norm of a left-invariant derivation is the norm of its tangent vector at the identity.

@[reducible, inline]

noncomputable abbrev groupLieAlgebraEquivModelVectorSpace {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] : GroupLieAlgebra I G ≃ₗ[ℝ] E

The canonical linear identification of the identity tangent space with the model vector space.

theorem finiteDimensional_leftInvariantDerivation {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] [ContMDiffMul I (↑⊤) G] [T2Space G] (h₁ : I.IsInteriorPoint 1) : FiniteDimensional ℝ (LeftInvariantDerivation I G)

Left-invariant derivations on a finite-dimensional smooth real Lie group form a finite-dimensional vector space.

theorem finrank_leftInvariantDerivation_eq_modelVectorSpace {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] [ContMDiffMul I (↑⊤) G] [T2Space G] (h₁ : I.IsInteriorPoint 1) : Module.finrank ℝ (LeftInvariantDerivation I G) = Module.finrank ℝ E

The Lie algebra of a finite-dimensional smooth real Lie group has the dimension of the manifold model vector space.