Infinitesimal actions of Lie algebras by vector fields #
An infinitesimal action of a real Lie algebra π€ on a manifold M is a linear map Z β¦ Z_M
from π€ to smooth vector fields on M satisfying (β
Z, Z'β)_M = -[Z_M, Z'_M], where [Β·, Β·]
is Mathlib's Lie bracket of vector fields VectorField.mlieBracket (in a chart,
[V, W] = DW Β· V - DV Β· W). The sign is the one satisfied by the fundamental vector fields
ΞΎ_M(x) = d/dt|β exp(t ΞΎ) β’ x of a left action of a Lie group, so an infinitesimal action is an
antihomomorphism into the Lie algebra of vector fields. Infinitesimal actions are the input of
moment maps (TauCeti.SmoothTwoForm.IsMomentMap).
An infinitesimal action restricts along a Lie algebra homomorphism π₯ β π€
(TauCeti.InfinitesimalAction.comp), for instance to a Lie subalgebra. Two infinitesimal actions of
the same Lie algebra on M and on N give the diagonal action Z β¦ (Z_M, Z_N) on M Γ N
(TauCeti.InfinitesimalAction.prod), because Lie brackets of product vector fields are computed
factor by factor. The basic example is the
action of the Lie algebra of all endomorphisms of a finite-dimensional real vector space V on V
by the linear vector fields x β¦ A x (TauCeti.InfinitesimalAction.linear), which restricts to
the linear actions of the classical subalgebras, such as the symplectic Lie algebra. An abelian Lie
algebra acts by translations, through the constant vector fields x β¦ Ο Z of a linear map Ο
(TauCeti.InfinitesimalAction.translation).
At a point x, an infinitesimal action has an orbit tangent space π€ Β· x = {Z_M(x)}
(TauCeti.InfinitesimalAction.orbitTangent) and an isotropy algebra π€_x = {Z | Z_M(x) = 0}
(TauCeti.InfinitesimalAction.isotropy), the range and the kernel of the linear map
Z β¦ Z_M(x) (TauCeti.InfinitesimalAction.eval). The isotropy algebra is a Lie subalgebra, since
the Lie bracket of two vector fields vanishing at x vanishes at x, and rankβnullity gives
dim (π€ Β· x) + dim π€_x = dim π€. For the fundamental vector fields of a Lie group action, π€ Β· x
and π€_x are the image and the kernel of the differential at the identity of the orbit map
g β¦ g β’ x. These are the pointwise data entering the differential of a moment map.
Main definitions #
TauCeti.InfinitesimalAction π€ I M: infinitesimal actions ofπ€onM.TauCeti.InfinitesimalAction.comp: the restriction of an infinitesimal action along a Lie algebra homomorphism.TauCeti.InfinitesimalAction.prod: the diagonal action on a product of two manifolds.TauCeti.InfinitesimalAction.eval a x: the linear mapZ β¦ Z_M(x).TauCeti.InfinitesimalAction.orbitTangent a x: the orbit tangent spaceπ€ Β· x.TauCeti.InfinitesimalAction.isotropy a x: the isotropy Lie subalgebraπ€_x.TauCeti.InfinitesimalAction.linear V: the action ofModule.End β VonVby linear vector fields.TauCeti.InfinitesimalAction.translation Ο: the action of an abelian Lie algebra on a vector space by the constant vector fields of a linear mapΟ.
References #
- V. Guillemin, S. Sternberg, Symplectic Techniques in Physics, Cambridge University Press, 1984, Section 26.
- J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics 218, Springer, 2013, Chapter 20 (infinitesimal generators of group actions).
An infinitesimal action of a real Lie algebra π€ on a manifold M: a linear map
Z β¦ Z_M from π€ to smooth vector fields on M with (β
Z, Z'β)_M = -[Z_M, Z'_M].
The vector field
Z_Mgenerated byZ, as a linear map inZ.- contMDiff_toLinearMap' (Z : π€) : ContMDiff I I.tangent ββ€ fun (x : M) => β¨x, self.toLinearMap Z xβ©
Each generated vector field is smooth.
- toLinearMap_lie' (Z Z' : π€) : self.toLinearMap β Z, Z'β = -VectorField.mlieBracket I (self.toLinearMap Z) (self.toLinearMap Z')
The generated vector fields form an antihomomorphism of Lie algebras.
Instances For
Two infinitesimal actions generating the same vector fields are equal.
The vector field generated by an element of the Lie algebra is smooth.
An infinitesimal action is an antihomomorphism of Lie algebras:
(β
Z, Z'β)_M = -[Z_M, Z'_M].
The restriction Z β¦ (f Z)_M of an infinitesimal action of π€ along a Lie algebra
homomorphism f : π₯ β π€, for instance the inclusion of a Lie subalgebra.
Instances For
The linear map Z β¦ Z_M(x) from π€ to the tangent space at x. For the fundamental vector
fields of a Lie group action it is the differential at the identity of the orbit map
g β¦ g β’ x.
Instances For
The orbit tangent space π€ Β· x = {Z_M(x) | Z β π€} of an infinitesimal action at x, the
range of Z β¦ Z_M(x).
Instances For
The isotropy algebra π€_x = {Z β π€ | Z_M(x) = 0} of an infinitesimal action at x. It is
a Lie subalgebra because the Lie bracket of two vector fields vanishing at x vanishes at x.
Instances For
The isotropy algebra is trivial exactly when Z β¦ Z_M(x) is injective, that is, when the
action is locally free at x.
Rankβnullity for the orbit map: dim (π€ Β· x) + dim π€_x = dim π€.
Where the action is locally free, the orbit tangent space has the dimension of π€.
The isotropy algebra of a restricted action is the preimage of the isotropy algebra.
The orbit tangent space of a restricted action is the image of the restricting Lie algebra.
The diagonal infinitesimal action Z β¦ (Z_M, Z_N) of π€ on M Γ N of infinitesimal actions
of π€ on M and on N: the product of the vector fields generated on the two factors.
Instances For
The diagonal action of Z is the product of the fields generated on the factors.
The isotropy algebra of the diagonal action at (x, y) is the intersection of the isotropy
algebras of the two factors.
The infinitesimal action of the Lie algebra Module.End β V of a finite-dimensional real
vector space V on V by the linear vector fields x β¦ A x.
Instances For
The infinitesimal action of an abelian Lie algebra π€ on a normed space V by the constant
vector fields x β¦ Ο Z of a linear map Ο : π€ β V, the generators of the translations
x β¦ x + t β’ Ο Z.