Commutation of left- and right-invariant vector fields #
This file proves that left- and right-invariant differentiation commute. The proof uses Clairaut symmetry for a smooth scalar function evaluated on two multiplied exponential lines, then uses the tangent-vector/point-derivation equivalence to identify the vector-field bracket.
This supplies a prerequisite for Deliverable A, Layer 1 of
TauCetiRoadmap/RepresentationTheory/LieGroups/README.md.
Main results #
contDiff_comp_mulInvariantExp_mul_mulInvariantExp: a vector-valued function on two exponential lines multiplied around a fixed group element is smooth in both parameters.spatialFDeriv_mulInvariantExp_mul_mulInvariantExpandtimeFDeriv_mulInvariantExp_mul_mulInvariantExp: identify its two partial derivatives with left- and right-invariant differentiation.mvfderiv_mulRightInvariantVectorField_mulInvariantVectorField_commute: left- and right-invariant scalar differentiation commute at every group point.mlieBracket_mulRightInvariantVectorField_mulInvariantVectorField: the corresponding vector-field bracket vanishes everywhere.mlieBracket_mulInvariantVectorField_mulRightInvariantVectorField: the same vanishing result with the bracket arguments reversed.
References #
- Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1, "The infinitesimal adjoint".
theorem
TauCeti.Lie.contDiff_comp_mulInvariantExp_mul_mulInvariantExp
{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]
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{f : G → F'}
(hf : ContMDiff I (modelWithCornersSelf ℝ F') (↑⊤) f)
(g : G)
(X Y : GroupLieAlgebra I G)
:
A smooth vector-valued function evaluated on two exponential lines multiplied around a fixed group element is smooth in both parameters.
theorem
TauCeti.Lie.spatialFDeriv_mulInvariantExp_mul_mulInvariantExp
{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]
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
(f : ContMDiffMap I (modelWithCornersSelf ℝ F') G F' ↑⊤)
(g : G)
(X Y : GroupLieAlgebra I G)
(s : ℝ)
:
have x := ⋯;
(spatialFDeriv (fun (p : ℝ × ℝ) => f (mulInvariantExp (p.1 • X) * g * mulInvariantExp (p.2 • Y))) 0 s) 1 = (d% ⇑f (mulInvariantExp (s • X) * g)) (mulInvariantVectorField Y (mulInvariantExp (s • X) * g))
Differentiating the second exponential parameter gives left-invariant differentiation by
Y.
theorem
TauCeti.Lie.timeFDeriv_mulInvariantExp_mul_mulInvariantExp
{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]
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
(f : ContMDiffMap I (modelWithCornersSelf ℝ F') G F' ↑⊤)
(g : G)
(X Y : GroupLieAlgebra I G)
(t : ℝ)
:
have x := ⋯;
timeFDeriv (fun (p : ℝ × ℝ) => f (mulInvariantExp (p.1 • X) * g * mulInvariantExp (p.2 • Y))) 0 t = (d% ⇑f (g * mulInvariantExp (t • Y))) (mulRightInvariantVectorField X (g * mulInvariantExp (t • Y)))
Differentiating the first exponential parameter gives right-invariant differentiation by
X.
theorem
TauCeti.Lie.mvfderiv_mulRightInvariantVectorField_mulInvariantVectorField_commute
{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]
(f : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) G ℝ ↑⊤)
(g : G)
(X Y : GroupLieAlgebra I G)
:
(d% ⇑((tangentToLeftInvariantDerivation Y) f) g) (mulRightInvariantVectorField X g) = (d% ⇑(rightInvariantDerivative X f) g) (mulInvariantVectorField Y g)
Left- and right-invariant scalar differentiation commute at every group point.
@[simp]
theorem
TauCeti.Lie.mlieBracket_mulRightInvariantVectorField_mulInvariantVectorField
{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]
(X Y : GroupLieAlgebra I G)
:
Right- and left-invariant vector fields commute everywhere.
@[simp]
theorem
TauCeti.Lie.mlieBracket_mulInvariantVectorField_mulRightInvariantVectorField
{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]
(X Y : GroupLieAlgebra I G)
:
Left- and right-invariant vector fields commute everywhere, with the bracket arguments in the opposite order.