Invariant vector fields on Lie groups

This file records regularity properties of invariant vector fields expressed through Mathlib's tangent Lie algebra. These results depend only on GroupLieAlgebra, not on the separate left-invariant-derivation model of a Lie algebra. The regularity proofs reuse generic tangent-bundle smoothness inputs from TauCeti.Geometry.Manifold.VectorField.Regularity.

It also defines the left Maurer-Cartan form evaluated on a vector field V, g ↦ d(L_{g⁻¹})_g (V g), the value of V translated back to the identity. Since it is read off the tangent map of multiplication, it is differentiable wherever V is.

Main definitions

• TauCeti.leftMaurerCartanEval V: the left Maurer-Cartan form evaluated on a vector field V.

Main results

• GroupLieAlgebra.mulInvariantVectorField_apply: evaluation as the differential of left translation.
• mulInvariantVectorField_one: at the identity, an invariant vector field equals its generator.
• mulInvariantVectorField_zero: the invariant field generated by zero is zero.
• contMDiff_tangentMap_mul_prod: the tangent map of multiplication is smooth on a pair of tangent bundles.
• tangentMap_mul_prod_apply: the value of that tangent map is the sum of the two partial derivatives of multiplication.
• mfderiv_mul_apply_one: at the identity pair, the derivative of multiplication is addition.
• GroupLieAlgebra.mfderiv_inv_one_apply: at the identity, the derivative of inversion is negation.
• mfderiv_mul_left_mulInvariantVectorField: left translation intertwines a left-invariant vector field with itself.
• contMDiff_tangentMap_mul_prod_comp: regularity after feeding two smooth tangent-bundle inputs into the tangent map of multiplication.
• contMDiff_mulInvariantVectorField_infty: a left-invariant vector field on a smooth Lie group is smooth.
• contMDiff_mulInvariantVectorField_modelSpace: the invariant vector field is jointly C^m in its model-space generator and group argument when multiplication is C^n and m + 1 ≤ n.
• TauCeti.mfderiv_inv_mul_mulInvariantVectorField, TauCeti.mulInvariantVectorField_mfderiv_inv_mul: translating to the identity and the invariant vector field construction are inverse to each other at each point; hence every tangent vector is the value of an invariant vector field (TauCeti.exists_mulInvariantVectorField_eq) and translation to the identity is injective (TauCeti.mfderiv_inv_mul_injective).
• TauCeti.mfderiv_eq_zero_of_mfderiv_mul_left_one_eq_zero: a map whose left translate by g has vanishing derivative at the identity has vanishing derivative at g.
• MDifferentiableAt.leftMaurerCartanEval: the left Maurer-Cartan form evaluated on a differentiable vector field is differentiable.

Implementation notes

The Lie algebra GroupLieAlgebra I G is the tangent space at the identity, which is the model space E by definition but carries no norm of its own. The left Maurer-Cartan form evaluated on a vector field therefore takes values in E, so that its differentiability can be stated.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 0, "The Lie algebra and the tangent space at 1".
• The proofs of contMDiff_mulInvariantVectorField_modelSpace and contMDiff_mulInvariantVectorField_infty adapt Sébastien Gouëzel's proof of Mathlib's contMDiff_mulInvariantVectorField.

theorem contMDiff_tangentMap_mul_prod {𝕜 : 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] [Mul G] {m n : WithTop ℕ∞} [ContMDiffMul I n G] (hmn : m + 1 ≤ n) : have x := ⋯; ContMDiff (I.tangent.prod I.tangent) I.tangent m ((tangentMap (I.prod I) I fun (p : G × G) => p.1 * p.2) ∘ ⇑(equivTangentBundleProd I G I G).symm)

The tangent map of multiplication, expressed on a pair of tangent bundles, is C^m when multiplication is C^n and m + 1 ≤ n.

@[simp]

theorem tangentMap_mul_prod_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] [Mul G] [ContMDiffMul I 1 G] (p q : TangentBundle I G) : tangentMap (I.prod I) I (fun (r : G × G) => r.1 * r.2) ((equivTangentBundleProd I G I G).symm (p, q)) = ⟨p.proj * q.proj, ((mfderiv% fun (x : G) => x * q.proj) p.proj) p.snd + ((mfderiv% fun (x : G) => p.proj * x) q.proj) q.snd⟩

The tangent map of multiplication is the sum of its two partial derivatives.

theorem mfderiv_mul_apply_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] [ContMDiffMul I 1 G] (v w : GroupLieAlgebra I G) : ((mfderiv% fun (p : G × G) => p.1 * p.2) (1, 1)) (v, w) = v + w

At the identity pair, the derivative of multiplication is addition on the tangent Lie algebra.

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

At the identity, the derivative of inversion is negation on the tangent Lie algebra.

theorem contMDiff_tangentMap_mul_prod_comp {𝕜 : 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] [Mul G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {m n : WithTop ℕ∞} [ContMDiffMul I n G] (hmn : m + 1 ≤ n) (f g : M → TangentBundle I G) : have x := ⋯; ContMDiff J I.tangent m f → ContMDiff J I.tangent m g → ContMDiff J I.tangent m fun (p : M) => tangentMap (I.prod I) I (fun (q : G × G) => q.1 * q.2) ((equivTangentBundleProd I G I G).symm (f p, g p))

Composing the tangent map of multiplication with two smoothly varying tangent-bundle inputs preserves the regularity allowed by multiplication.

theorem GroupLieAlgebra.mulInvariantVectorField_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) : mulInvariantVectorField v g = ((mfderiv% fun (x : G) => g * x) 1) v

The invariant vector field at g is the generator translated by the differential of left multiplication by g.

@[simp]

theorem mulInvariantVectorField_zero {𝕜 : 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] : mulInvariantVectorField 0 = 0

The invariant vector field generated by zero is the zero field.

@[simp]

theorem mulInvariantVectorField_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) : mulInvariantVectorField v 1 = v

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

@[simp]

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

The derivative of left translation carries a left-invariant vector field to itself.

theorem contMDiff_mulInvariantVectorField_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, mulInvariantVectorField p.1 p.2⟩

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

theorem contMDiff_mulInvariantVectorField_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, mulInvariantVectorField v g⟩

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

theorem TauCeti.mfderiv_inv_mul_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 1 G] (w : GroupLieAlgebra I G) (g : G) : ((mfderiv% fun (x : G) => g⁻¹ * x) g) (mulInvariantVectorField w g) = w

Translating the value at g of an invariant vector field back to the identity recovers its generator.

@[simp]

theorem TauCeti.mulInvariantVectorField_mfderiv_inv_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] [ContMDiffMul I 1 G] {g : G} (v : TangentSpace I g) : mulInvariantVectorField (((mfderiv% fun (x : G) => g⁻¹ * x) g) v) g = v

Every tangent vector at g is the value at g of the invariant vector field generated by its translate to the identity.

theorem TauCeti.exists_mulInvariantVectorField_eq {𝕜 : 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 : TangentSpace I g) : ∃ (w : GroupLieAlgebra I G), mulInvariantVectorField w g = v

Every tangent vector at g is the value at g of some invariant vector field.

theorem TauCeti.mfderiv_inv_mul_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 1 G] (g : G) : Function.Injective ⇑((mfderiv% fun (x : G) => g⁻¹ * x) g)

The derivative at g of left translation by g⁻¹ is injective.

theorem TauCeti.mfderiv_eq_zero_of_mfderiv_mul_left_one_eq_zero {𝕜 : 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] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : G → M'} {g : G} (h : (mfderiv% fun (k : G) => f (g * k)) 1 = 0) : mfderiv% f g = 0

A map on a Lie group whose left translate k ↦ f (g * k) has vanishing derivative at the identity has vanishing derivative at g, since every tangent vector at g is the left translate of one at the identity.

noncomputable def TauCeti.leftMaurerCartanEval {𝕜 : 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 : (g : G) → TangentSpace I g) (g : G) : E

The left Maurer-Cartan form evaluated on a vector field V: the value of V at g, translated back to the identity by left multiplication by g⁻¹. It is a function on G with values in the model space, which is the Lie algebra GroupLieAlgebra I G.

theorem TauCeti.leftMaurerCartanEval_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 : (g : G) → TangentSpace I g) (g : G) : leftMaurerCartanEval V g = ((mfderiv% fun (x : G) => g⁻¹ * x) g) (V g)

The defining formula of the left Maurer-Cartan form evaluated on a vector field.

@[simp]

theorem TauCeti.mulInvariantVectorField_leftMaurerCartanEval {𝕜 : 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] (V : (g : G) → TangentSpace I g) (g : G) : mulInvariantVectorField (leftMaurerCartanEval V g) g = V g

A vector field takes at g the value of the invariant vector field generated by the left Maurer-Cartan form evaluated on it at g.

@[simp]

theorem TauCeti.leftMaurerCartanEval_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 1 G] (w : GroupLieAlgebra I G) (g : G) : leftMaurerCartanEval (mulInvariantVectorField w) g = w

The left Maurer-Cartan form evaluated on an invariant vector field is constant, with value its generator.

theorem MDifferentiableAt.leftMaurerCartanEval {𝕜 : 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 2 G] {V : (g : G) → TangentSpace I g} {x : G} (hV : (MDiffAt fun (g : G) => ⟨g, V g⟩) x) : MDiffAt (TauCeti.leftMaurerCartanEval V) x

The left Maurer-Cartan form evaluated on a vector field is differentiable wherever the vector field is.