Moment maps of cotangent-lifted linear actions

A linear map A of a real normed space V acts on the linear cotangent space V × StrongDual ℝ V, with its canonical symplectic form ω((q, p), (q', p')) = p'(q) - p(q'), by the cotangent lift of A. Its moment map is

⟨μ(q, p), A⟩ = p(A q) (TauCeti.cotangentMomentMap),

the pairing of the covector p with the vector A q generated at the base point q. This file proves the moment map identities at the level of the linear group GL(V) and of its Lie algebra.

For a continuous linear equivalence g : V ≃L[ℝ] W, the cotangent lift (q, p) ↦ (g q, p ∘ g⁻¹) (ContinuousLinearEquiv.cotangent) is a symplectomorphism preserving the Liouville forms. The moment map is coadjoint equivariant along it: μ(g · x)(A) = μ(x)(g⁻¹ A g) (ContinuousLinearEquiv.cotangentMomentMap_cotangent).

For finite-dimensional V, the infinitesimal cotangent lift (q, p) ↦ (A q, -(p ∘ A)) is a Lie algebra homomorphism from Module.End ℝ V to the endomorphisms of V × StrongDual ℝ V (TauCeti.cotangentLiftLieHom). It defines an infinitesimal action of gl(V) by linear vector fields (TauCeti.InfinitesimalAction.cotangentLinear). Then:

• the infinitesimal cotangent lift takes values in sp(V × StrongDual ℝ V) (TauCeti.cotangentLiftLieHom_mem_skewAdjointLieSubalgebra), giving a Lie algebra homomorphism into it (TauCeti.cotangentLiftSpLieHom), and μ_A(x) = ½ ω(A_{T*V} x, x) is the linear symplectic moment map along it (TauCeti.cotangentMomentMap_apply_eq_linearMomentMap);
• μ is a moment map of this action (TauCeti.isMomentMap_cotangentMomentMap), and it is the contraction of the Liouville form with the generating vector fields, ⟨μ, A⟩ = λ(A_{T*V}) (TauCeti.cotangentLiouvilleForm_cotangentLiftLieHom);
• μ is infinitesimally equivariant, {μ_A, μ_B} = μ_{⁅A, B⁆} (TauCeti.poissonBracket_cotangentMomentMap);
• the cotangent lift of g carries the generating field of A to that of g A g⁻¹ (ContinuousLinearEquiv.cotangent_cotangentLiftLieHom).

Restricting along a Lie algebra homomorphism ρ : 𝔤 → gl(V) with TauCeti.SmoothTwoForm.IsMomentMap.comp gives the moment map ⟨μ(q, p), Z⟩ = p(ρ(Z) q) of the cotangent lift of any linear representation. For the rotations 𝔤 = so(V) of a Euclidean space this is the angular momentum.

Main declarations

• TauCeti.cotangentMomentMap: the moment map ⟨μ(q, p), A⟩ = p(A q).
• TauCeti.cotangentLiftLieHom: the infinitesimal cotangent lift (q, p) ↦ (A q, -(p ∘ A)).
• TauCeti.cotangentLiftSpLieHom: the infinitesimal cotangent lift as a Lie algebra homomorphism into sp(V × StrongDual ℝ V).
• TauCeti.InfinitesimalAction.cotangentLinear: the cotangent-lifted linear action of gl(V).
• TauCeti.isMomentMap_cotangentMomentMap: μ is a moment map of this action.

References

• J. E. Marsden, T. S. Ratiu, Introduction to Mechanics and Symmetry, 2nd ed., Texts in Applied Mathematics 17, Springer, 1999, Section 12.1 (momentum maps of cotangent lifts).
• V. Guillemin, S. Sternberg, Symplectic Techniques in Physics, Cambridge University Press, 1984, Section 26.

def TauCeti.cotangentMomentMap {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (x : V × StrongDual ℝ V) : Module.Dual ℝ (Module.End ℝ V)

The moment map of the cotangent-lifted linear action: at a point (q, p) of the linear cotangent space V × StrongDual ℝ V, the linear form A ↦ p(A q) on the endomorphisms of V.

@[simp]

theorem TauCeti.cotangentMomentMap_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (x : V × StrongDual ℝ V) (A : Module.End ℝ V) : (cotangentMomentMap x) A = x.2 (A x.1)

theorem ContinuousLinearEquiv.cotangentMomentMap_cotangent {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (g : V ≃L[ℝ] W) (x : V × StrongDual ℝ V) (A : Module.End ℝ W) : (TauCeti.cotangentMomentMap (g.cotangent x)) A = (TauCeti.cotangentMomentMap x) ((↑g).symm.conj A)

Coadjoint equivariance of the cotangent moment map. For a continuous linear equivalence g : V ≃L[ℝ] W, μ(g · x)(A) = μ(x)(g⁻¹ A g). For W = V this says μ(g · x) = Ad*_g μ(x) for the adjoint action Ad_g A = g A g⁻¹ of GL(V) on gl(V).

noncomputable def TauCeti.cotangentLiftLieHom (V : Type u_1) [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] : Module.End ℝ V →ₗ⁅ℝ⁆ Module.End ℝ (V × StrongDual ℝ V)

The infinitesimal cotangent lift (q, p) ↦ (A q, -(p ∘ A)) of an endomorphism A of a finite-dimensional space V, as a Lie algebra homomorphism from gl(V) to the endomorphisms of the linear cotangent space V × StrongDual ℝ V.

@[simp]

theorem TauCeti.cotangentLiftLieHom_apply_fst {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (A : Module.End ℝ V) (x : V × StrongDual ℝ V) : (((cotangentLiftLieHom V) A) x).1 = A x.1

@[simp]

theorem TauCeti.cotangentLiftLieHom_apply_snd_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (A : Module.End ℝ V) (x : V × StrongDual ℝ V) (v : V) : (((cotangentLiftLieHom V) A) x).2 v = -x.2 (A v)

theorem TauCeti.cotangentLiftLieHom_mem_skewAdjointLieSubalgebra {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (A : Module.End ℝ V) : (cotangentLiftLieHom V) A ∈ skewAdjointLieSubalgebra strongDualCotangentSymplecticForm.toBilinForm

The infinitesimal cotangent lift of an endomorphism is skew-adjoint for the canonical symplectic form: it lies in sp(V × StrongDual ℝ V).

theorem TauCeti.cotangentLiouvilleForm_cotangentLiftLieHom {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (A : Module.End ℝ V) (x : V × StrongDual ℝ V) : ((cotangentLiouvilleForm x) fun (x_1 : Fin 1) => ((cotangentLiftLieHom V) A) x) = (cotangentMomentMap x) A

The cotangent moment map is the contraction of the Liouville form with the generating vector fields of the cotangent lift: ⟨μ(x), A⟩ = λ_x(A_{T*V}(x)).

noncomputable def TauCeti.InfinitesimalAction.cotangentLinear (V : Type u_1) [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] : InfinitesimalAction (Module.End ℝ V) (modelWithCornersSelf ℝ (V × StrongDual ℝ V)) (V × StrongDual ℝ V)

The cotangent-lifted linear action of gl(V) = Module.End ℝ V on the linear cotangent space V × StrongDual ℝ V of a finite-dimensional space V, by the linear vector fields (q, p) ↦ (A q, -(p ∘ A)).

@[simp]

theorem TauCeti.InfinitesimalAction.cotangentLinear_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (A : Module.End ℝ V) (x : V × StrongDual ℝ V) : (cotangentLinear V) A x = ((cotangentLiftLieHom V) A) x

noncomputable def TauCeti.cotangentLiftSpLieHom {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] : Module.End ℝ V →ₗ⁅ℝ⁆ ↥(skewAdjointLieSubalgebra strongDualCotangentSymplecticForm.toBilinForm)

The infinitesimal cotangent lift as a Lie algebra homomorphism into sp(V × StrongDual ℝ V).

@[simp]

theorem TauCeti.coe_cotangentLiftSpLieHom {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (A : Module.End ℝ V) : ↑(cotangentLiftSpLieHom A) = (cotangentLiftLieHom V) A

theorem TauCeti.cotangentMomentMap_apply_eq_linearMomentMap {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (x : V × StrongDual ℝ V) (A : Module.End ℝ V) : (cotangentMomentMap x) A = (strongDualCotangentSymplecticForm.linearMomentMap x) (cotangentLiftSpLieHom A)

The cotangent moment map is the linear symplectic moment map ½ ω(Ã x, x) of the cotangent lift Ã of A.

theorem TauCeti.isMomentMap_cotangentMomentMap {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] : strongDualCotangentSymplecticForm.constSmooth.IsMomentMap (InfinitesimalAction.cotangentLinear V) cotangentMomentMap

The moment map of the cotangent-lifted linear action. On the linear cotangent space of a finite-dimensional space V, ⟨μ(q, p), A⟩ = p(A q) is a moment map of the action of gl(V) by the cotangent-lifted linear vector fields (q, p) ↦ (A q, -(p ∘ A)).

theorem TauCeti.poissonBracket_cotangentMomentMap {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (A B : Module.End ℝ V) (x : V × StrongDual ℝ V) : strongDualCotangentSymplecticForm.constSmooth.poissonBracket (fun (y : V × StrongDual ℝ V) => (cotangentMomentMap y) A) (fun (y : V × StrongDual ℝ V) => (cotangentMomentMap y) B) x = (cotangentMomentMap x) ⁅A, B⁆

The cotangent moment map is infinitesimally equivariant: it intertwines the commutator bracket of gl(V) with the Poisson bracket, {μ_A, μ_B} = μ_{⁅A, B⁆}.

theorem ContinuousLinearEquiv.cotangent_cotangentLiftLieHom {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W] (g : V ≃L[ℝ] W) (A : Module.End ℝ V) (x : V × StrongDual ℝ V) : g.cotangent (((TauCeti.cotangentLiftLieHom V) A) x) = ((TauCeti.cotangentLiftLieHom W) ((↑g).conj A)) (g.cotangent x)

Equivariance of the infinitesimal cotangent lift. The cotangent lift of a continuous linear equivalence g carries the generating vector field of A to that of g A g⁻¹.