Identities for the trace form of a Lie module

Let M be a representation of a Lie algebra L over a commutative ring R. Its trace form B = LieModule.traceForm R L M is symmetric and invariant, B ⁅a, b⁆ c = B a ⁅b, c⁆. Together with the Leibniz rule those two properties give an identity in four elements,

B ⁅a, b⁆ ⁅c, d⁆ + B ⁅b, c⁆ ⁅a, d⁆ + B ⁅c, a⁆ ⁅b, d⁆ = 0,

which is the Jacobi identity rewritten so that each summand pairs two brackets against each other rather than iterating them. No hypothesis at all is needed on the four elements: this is a consequence of invariance and symmetry, and it holds in every Lie algebra.

Its purpose is downstream: when a, b, c, d are root vectors of a split semisimple Lie algebra and B is the Killing form, each summand evaluates to a product of two structure constants weighted by the Killing pairing of an opposite pair of root vectors, and the identity becomes the four-term relation between the structure constants. Grouping the brackets in pairs is exactly what makes that evaluation possible, since a summand with an iterated bracket would mix root spaces of three different roots.

A second, unrelated identity is collected here: over a reduced ring the trace form kills a pair that brackets to zero as soon as one of the two acts nilpotently, because the composite of the two actions is then nilpotent and a nilpotent scalar in a reduced ring is zero. Specialized to the adjoint representation this says that an ad-nilpotent element is Killing-orthogonal to its own centraliser.

Main results

• TauCeti.traceForm_lie_lie_cyclic_eq_zero: the four-element cyclic identity above.
• TauCeti.traceForm_eq_zero_of_isNilpotent_of_lie_eq_zero: elements bracketing to zero, one of them acting nilpotently, are orthogonal for the trace form.

References

• R. W. Carter, Simple Groups of Lie Type, §4.1.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §25.1.

theorem TauCeti.traceForm_lie_lie_cyclic_eq_zero (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (a b c d : L) : ((LieModule.traceForm R L M) ⁅a, b⁆) ⁅c, d⁆ + ((LieModule.traceForm R L M) ⁅b, c⁆) ⁅a, d⁆ + ((LieModule.traceForm R L M) ⁅c, a⁆) ⁅b, d⁆ = 0

The four-element cyclic identity for an invariant trace form. Pairing the three ways of splitting a, b, c, d into two brackets, with d always in the second, gives zero.

theorem TauCeti.traceForm_eq_zero_of_isNilpotent_of_lie_eq_zero {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [IsReduced R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {x y : L} (hx : IsNilpotent ((LieModule.toEnd R L M) x)) (hxy : ⁅x, y⁆ = 0) : ((LieModule.traceForm R L M) x) y = 0

An element acting nilpotently is orthogonal, for the trace form of any representation, to everything it brackets to zero with. The trace form pairs x and y by the trace of the composite of their actions; bracketing to zero in L makes those actions commute, since toEnd R L M is a morphism of Lie rings, and the trace of a composite with a commuting nilpotent factor vanishes over a reduced ring.