Right-invariant vector fields on Lie groups

Mathlib's mulInvariantVectorField is the left-invariant field generated by a tangent vector at the identity. This file supplies its right-invariant counterpart and the regularity needed to compare the two fields in the infinitesimal adjoint calculation.

This supplies a prerequisite for Deliverable A, Layer 1 of TauCetiRoadmap/RepresentationTheory/LieGroups/README.md.

Main definitions

• mulRightInvariantVectorField: the right-invariant field generated at the identity.

Main results

• mulRightInvariantVectorField_one: the field has the prescribed value at the identity.
• mulRightInvariantVectorField_apply: its value is the derivative of right multiplication.
• mulRightInvariantVectorField_add: the construction preserves addition.
• mulRightInvariantVectorField_smul: the construction preserves scalar multiplication.
• inverse_mfderiv_mul_right: derivatives of inverse right translations are inverse maps.
• TauCeti.injective_mfderiv_mul_right: derivatives of right translations are injective.
• mpullback_mulRightInvariantVectorField: right-invariant fields are invariant under right translations.
• mulRightInvariantVectorField_eq_mpullback: the field generated by V 1 agrees with a pullback of V at the specified point.
• contMDiff_mulRightInvariantVectorField_modelSpace: jointly C^m in the generator and group point when multiplication is C^n and m + 1 ≤ n.
• contMDiff_mulRightInvariantVectorField_infty: a right-invariant field is smooth.
• contMDiff_mvfderiv_mulRightInvariantVectorField: differentiating a smooth scalar function along a right-invariant field gives a smooth function.
• rightInvariantDerivative: right-invariant differentiation bundled as a smooth scalar function.
• GroupLieAlgebra.mfderiv_inv_mulInvariantVectorField: inversion carries the left-invariant field of v to minus its right-invariant field, d(inv)_g (v^L g) = -v^R g⁻¹.
• GroupLieAlgebra.contMDiffAt_mulRightInvariantVectorField, GroupLieAlgebra.mdifferentiableAt_mulRightInvariantVectorField: on a Lie group, right-invariant fields are C^(minSmoothness 𝕜 2), hence differentiable.
• GroupLieAlgebra.mlieBracket_mulRightInvariantVectorField: the bracket of right-invariant fields is minus the right-invariant field of the bracket, [v^R, w^R] = -⁅v, w⁆^R. So v ↦ v^R is an antihomomorphism of Lie algebras, unlike the homomorphism v ↦ v^L defining ⁅v, w⁆.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1, "The infinitesimal adjoint".
• The definition mirrors Sébastien Gouëzel's Mathlib mulInvariantVectorField.
• The smoothness proofs adapt contMDiff_mulInvariantVectorField_modelSpace and contMDiff_mulInvariantVectorField_infty from TauCeti.Geometry.Lie.InvariantVectorField.Basic; those results in turn adapt Gouëzel's proof of Mathlib's contMDiff_mulInvariantVectorField.
• The bracket of right-invariant fields is computed by transporting the left-invariant bracket along inversion, by the naturality of the Lie bracket for related vector fields: John M. Lee, Introduction to Smooth Manifolds, second edition, Chapter 8.
• The pullback results inverse_mfderiv_mul_right, mpullback_mulRightInvariantVectorField, and mulRightInvariantVectorField_eq_mpullback, together with the addition and scalar-multiplication statements, transpose the corresponding left-translation results in Sébastien Gouëzel's Mathlib.Geometry.Manifold.GroupLieAlgebra from left to right.

noncomputable def mulRightInvariantVectorField {𝕜 : 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] (v : GroupLieAlgebra I G) (g : G) : TangentSpace I g

The right-invariant vector field generated by a tangent vector at the identity. At a point g, it is the image of the generator under the derivative at 1 of right multiplication by g.

theorem mulRightInvariantVectorField_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] (v : GroupLieAlgebra I G) (g : G) : mulRightInvariantVectorField v g = ((mfderiv% fun (x : G) => x * g) 1) v

The value of a generated right-invariant vector field is the derivative of right multiplication applied to its generator.

@[simp]

theorem mulRightInvariantVectorField_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] (v : GroupLieAlgebra I G) : mulRightInvariantVectorField v 1 = v

At the identity, the right-invariant vector field generated by v equals v.

theorem mulRightInvariantVectorField_add {𝕜 : 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] (v w : GroupLieAlgebra I G) : mulRightInvariantVectorField (v + w) = mulRightInvariantVectorField v + mulRightInvariantVectorField w

The right-invariant vector field construction preserves addition of its generators.

theorem mulRightInvariantVectorField_smul {𝕜 : 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] (c : 𝕜) (v : GroupLieAlgebra I G) : mulRightInvariantVectorField (c • v) = c • mulRightInvariantVectorField v

The right-invariant vector field construction preserves scalar multiplication.

@[simp]

theorem inverse_mfderiv_mul_right {𝕜 : 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 1 G] {g h : G} : ((mfderiv% fun (x : G) => x * g) h).inverse = (mfderiv% fun (x : G) => x * g⁻¹) (h * g)

The inverse of the derivative at h of right translation by g is the derivative at h * g of right translation by g⁻¹.

theorem TauCeti.injective_mfderiv_mul_right {𝕜 : 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 1 G] (g h : G) : Function.Injective ⇑((mfderiv% fun (x : G) => x * g) h)

The derivatives of right translations are injective: the derivative at h * g of right translation by g⁻¹ is a left inverse of the derivative at h of right translation by g.

theorem mpullback_mulRightInvariantVectorField {𝕜 : 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 1 G] (g : G) (v : GroupLieAlgebra I G) : VectorField.mpullback I I (fun (x : G) => x * g) (mulRightInvariantVectorField v) = mulRightInvariantVectorField v

Right-invariant vector fields are invariant under pullback by right translations.

theorem mulRightInvariantVectorField_eq_mpullback {𝕜 : 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 1 G] (g : G) (V : (g : G) → TangentSpace I g) : mulRightInvariantVectorField (V 1) g = VectorField.mpullback I I (fun (x : G) => x * g⁻¹) V g

For any field V, the right-invariant field generated by V 1 agrees at g with the pullback of V along right translation by g⁻¹.

theorem contMDiff_mulRightInvariantVectorField_modelSpace {𝕜 : 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] {m n : WithTop ℕ∞} [ContMDiffMul I n G] (hmn : m + 1 ≤ n) : have x := ⋯; ContMDiff ((modelWithCornersSelf 𝕜 E).prod I) I.tangent m fun (p : E × G) => ⟨p.2, mulRightInvariantVectorField p.1 p.2⟩

In model coordinates, the right-invariant vector field is jointly C^m in its generating tangent vector and group point when multiplication is C^n and m + 1 ≤ n.

theorem contMDiff_mulRightInvariantVectorField_infty {𝕜 : 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) : ContMDiff I I.tangent ↑⊤ fun (g : G) => ⟨g, mulRightInvariantVectorField v g⟩

A right-invariant vector field on a smooth Lie group is smooth.

theorem contMDiff_mvfderiv_mulRightInvariantVectorField {𝕜 : 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) (mulRightInvariantVectorField v g)

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

noncomputable def rightInvariantDerivative {𝕜 : 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 𝕜 ↑⊤) : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤

Right-invariant differentiation of a smooth scalar function, bundled as a smooth scalar function.

@[simp]

theorem rightInvariantDerivative_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) : (rightInvariantDerivative v f) g = (d% ⇑f g) (mulRightInvariantVectorField v g)

Right-invariant differentiation acts pointwise along the corresponding vector field.

theorem GroupLieAlgebra.mfderiv_inv_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] (v : GroupLieAlgebra I G) (g : G) : ((mfderiv% fun (h : G) => h⁻¹) g) (mulInvariantVectorField v g) = -mulRightInvariantVectorField v g⁻¹

Inversion carries the left-invariant vector field of v to minus its right-invariant vector field: d(inv)_g (v^L g) = -v^R g⁻¹.

theorem GroupLieAlgebra.contMDiffAt_mulRightInvariantVectorField {𝕜 : 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] (v : GroupLieAlgebra I G) {g : G} : ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun (g : G) => ⟨g, mulRightInvariantVectorField v g⟩) g

A right-invariant vector field on a Lie group is C^(minSmoothness 𝕜 2); this is C² over ℝ and ℂ.

theorem GroupLieAlgebra.mdifferentiableAt_mulRightInvariantVectorField {𝕜 : 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] (v : GroupLieAlgebra I G) {g : G} : (MDiffAt fun (g : G) => ⟨g, mulRightInvariantVectorField v g⟩) g

A right-invariant vector field on a Lie group is differentiable.

theorem GroupLieAlgebra.mlieBracket_mulRightInvariantVectorField {𝕜 : 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] (v w : GroupLieAlgebra I G) : VectorField.mlieBracket I (mulRightInvariantVectorField v) (mulRightInvariantVectorField w) = -mulRightInvariantVectorField ⁅v, w⁆

The bracket of right-invariant vector fields. The Lie bracket of the right-invariant vector fields of v and w is minus the right-invariant vector field of their bracket in the tangent Lie algebra: [v^R, w^R] = -⁅v, w⁆^R.