Invariant forms on the Lie algebra of a Lie group #
The Lie algebra of a compact Lie group carries an inner product invariant under the adjoint
representation, obtained by averaging over the group. Differentiating the invariance along a
one-parameter subgroup shows that each ad X is skew for such a form. This is the form that
turns a critical point of an adjoint orbit into a vanishing bracket, the argument behind the
conjugacy of maximal tori.
The tangent-algebra API also characterizes Ad-invariance by infinitesimal invariance on
connected groups, without symmetry or positivity assumptions. This connects the inner products
defining bi-invariant metrics with their Levi-Civita connection and curvature calculations.
It uses TauCeti.Lie.hasDerivAt_tangentAd_mulInvariantExp_smul_apply_zero for d Ad = ad.
Main results #
TauCeti.Lie.lieInvariant_of_isInvariantForm: a bilinear form invariant underAdis invariant underad, in the sense of Mathlib'sLinearMap.BilinForm.lieInvariant.TauCeti.Lie.exists_isSymm_bilinForm_Ad_invariant: the Lie algebra of a compact Lie group has anAd-invariant symmetric positive-definite bilinear form.TauCeti.Lie.averageAdjointBilinForm: the normalized Haar average of a given real form.TauCeti.Lie.averageAdjointBilinForm_apply: its inverse-adjoint integral formula.TauCeti.Lie.averageAdjointBilinForm_idempotent: averaging is a linear projection on forms.TauCeti.Lie.isSymm_averageAdjointBilinFormandposDef_averageAdjointBilinForm: preservation of symmetry and positive definiteness.TauCeti.Lie.isInvariantForm_averageAdjointBilinFormandlieInvariant_averageAdjointBilinForm: group and infinitesimal invariance.TauCeti.Lie.averageAdjointBilinForm_eq_selfandaverageAdjointBilinForm_eq_self_iff: fixed forms are exactly the adjoint-invariant forms.LeftInvariantDerivation.exists_Ad_lie_eq_zero: Hunt's lemma, forX Y : π€in the Lie algebra of a compact Lie group, some adjoint translate ofXbrackets to zero withY.TauCeti.Lie.lieInvariant_iff_adjoint_invariant: on a connected group, tangent bilinear forms are infinitesimally invariant exactly when they are Ad-invariant.TauCeti.Lie.exists_isSymm_posDef_continuousBilinearMap_adjoint_invariant: a continuous symmetric positive adjoint-invariant form on the tangent Lie algebra of a compact Lie group.
References #
- J. Hilgert and K.-H. Neeb, Structure and Geometry of Lie Groups, Springer Monographs in Mathematics (2012), Lemma 10.4.14, for averaging an arbitrary starting inner product.
- J. M. Lee, Introduction to Riemannian Manifolds, second edition, Chapter 3.
- J. Milnor, Curvatures of left invariant metrics on Lie groups, Advances in Math. 21 (1976), 293β329.
- T. BrΓΆcker and T. tom Dieck, Representations of Compact Lie Groups, Springer GTM 98 (1985), Chapter II, Β§ 1.
- G. A. Hunt, A theorem of Γlie Cartan, Proc. Amer. Math. Soc. 7 (1956), 307β308.
A form invariant under Ad is invariant under ad: if
B (Ad g X) (Ad g Y) = B X Y for all g, then B β
Z, Xβ Y = -B X β
Z, Yβ.
The Lie algebra of a compact Lie group has an Ad-invariant inner product, presented as a
symmetric positive-definite bilinear form.
The normalized Haar average of real bilinear forms on the Lie algebra, as a linear operator using inverse-adjoint pullback.
Instances For
The adjoint average is the inverse-adjoint pullback integral of its starting form.
Haar averaging under the adjoint action preserves symmetry.
Haar averaging under the adjoint action preserves positive definiteness.
The adjoint average is invariant under the group adjoint representation.
The adjoint average is invariant under every infinitesimal adjoint operator.
The adjoint average fixes every form invariant under the adjoint representation.
Adjoint Haar averaging is idempotent.
A form is fixed by adjoint averaging exactly when it is adjoint-invariant.
The tangent Lie algebra of a compact Lie group has a continuous symmetric positive form invariant under the adjoint action. No connectedness or boundaryless-model hypothesis is needed.
Hunt's lemma. For X and Y in the Lie algebra of a compact Lie group, some adjoint
translate of X brackets to zero with Y.
Along an exponential line, the derivative at zero of a bilinear form applied to two adjoint orbits is the sum of its two Lie-bracket terms.
An Ad-invariant bilinear form is invariant under the tangent Lie algebra. The group may be disconnected, and the form need not be symmetric or nondegenerate.
On a connected Lie group, an infinitesimally invariant bilinear form is Ad-invariant.
On a connected Lie group, group-level and infinitesimal invariance of a bilinear form are equivalent.