sl₂ commutation relations in an associative algebra #
Let A be an associative ring and let H, E, F be elements of A satisfying the sl₂
relations for the ring commutator,
E * F - F * E = H, H * E - E * H = 2 • E, H * F - F * H = -(2 • F).
This file computes how E and F commute past powers, and past divided powers, of one another.
It uses the general integer-eigenvalue identities from
TauCeti.Algebra.Ring.Commutator and TauCeti.RingTheory.DividedPowers.Associative.
Over a ℚ-algebra the divided-power forms are
E * F⁽ⁿ⁺¹⁾ = F⁽ⁿ⁺¹⁾ * E + F⁽ⁿ⁾ * (H - n),
F * E⁽ⁿ⁺¹⁾ = E⁽ⁿ⁺¹⁾ * F - E⁽ⁿ⁾ * (H + n),
H * F⁽ⁿ⁾ = F⁽ⁿ⁾ * (H - 2 * n),
H * E⁽ⁿ⁾ = E⁽ⁿ⁾ * (H + 2 * n),
and the point of the normalisation is visible in them: although each divided power is a rational multiple of a power, no denominator survives on the right-hand sides. This is the first characteristic instance of Kostant's normal-ordering formula needed toward proving that the subring generated by divided powers of root vectors and by binomial coefficients of Cartan elements is closed under multiplication.
The relations are stated with the hypotheses each one needs, and not as a bundled IsSl2Triple:
the intended consumer is the universal enveloping algebra, where the image of the Cartan element
is not known to be nonzero, so the IsSl2Triple.h_ne_zero field is unavailable there. The last
section transports the individual bracket hypotheses through the canonical map to the enveloping
algebra; a genuine IsSl2Triple supplies them through its bracket fields.
Main results #
TauCeti.Sl2.e_mul_f_pow_succandTauCeti.Sl2.f_mul_e_pow_succ: the classical formulas⁅E, Fⁿ⁆ = n Fⁿ⁻¹ (H - (n - 1))and⁅F, Eⁿ⁆ = -n Eⁿ⁻¹ (H + (n - 1)), written with the index shifted so that no truncated subtraction appears.TauCeti.Sl2.h_mul_f_powandTauCeti.Sl2.h_mul_e_pow: moving a Cartan element past a power translates it by∓2n.TauCeti.Sl2.e_mul_dividedPower_succ_fandTauCeti.Sl2.f_mul_dividedPower_succ_e: their divided-power forms, in which the structure constants are units±1.TauCeti.Sl2.h_mul_dividedPower_fandTauCeti.Sl2.h_mul_dividedPower_e: moving a Cartan element past a divided power translates it by∓2n.TauCeti.Sl2.dividedPower_succ_e_mul_fandTauCeti.Sl2.dividedPower_succ_f_mul_e: the reversed-product forms, with the Cartan factor on the left.TauCeti.Sl2.ι_e_mul_dividedPower_succ_ι_fandTauCeti.Sl2.ι_f_mul_dividedPower_succ_ι_e: the two divided-power relations in a universal enveloping algebra overℚ.TauCeti.Sl2.dividedPower_succ_ι_e_mul_ι_fandTauCeti.Sl2.dividedPower_succ_ι_f_mul_ι_e: their reversed-product specializations.
Mathlib's IsSl2Triple.HasPrimitiveVectorWith.lie_e_pow_succ_toEnd_f and lie_h_pow_toEnd_f
prove the corresponding identities applied to a primitive vector, that is under the extra
hypothesis ⁅e, m⁆ = 0, and follow by applying the unconditional operator identities below to that
vector. The converse does not follow: identities on one primitive vector do not determine the
operators. The operator identities are what closure of an integral form under multiplication
requires.
References #
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §26.2.
- J. C. Jantzen, Representations of Algebraic Groups, 2nd ed., II.1.
The raising element commuted past a power of the lowering element: this is the classical
⁅E, Fⁿ⁆ = n Fⁿ⁻¹ (H - (n - 1)), with the index shifted so that no truncated subtraction
appears.
The lowering element commuted past a power of the raising element:
⁅F, Eⁿ⁺¹⁆ = -(n + 1) Eⁿ (H + n), the mirror of e_mul_f_pow_succ under the Chevalley
involution.
The raising element commuted past a divided power of the lowering element. Every structure
constant on the right is 1: this is the first case of Kostant's normal-ordering formula, and the
first step toward proving that the relevant ℤ-form is closed under multiplication.
The lowering element commuted past a divided power of the raising element.
The reversed-product form of f_mul_dividedPower_succ_e:
E⁽ⁿ⁺¹⁾ F = F E⁽ⁿ⁺¹⁾ + (H - n) E⁽ⁿ⁾. This is the orientation that occurs as the
one-lowering-vector case of the full Kostant straightening formula.
The reversed-product form of e_mul_dividedPower_succ_f:
F⁽ⁿ⁺¹⁾ E = E F⁽ⁿ⁺¹⁾ - (H + n) F⁽ⁿ⁾.
The divided-power relation e * f⁽ⁿ⁺¹⁾ = f⁽ⁿ⁺¹⁾ * e + f⁽ⁿ⁾ * (h - n) in a universal
enveloping algebra over ℚ. This is the relation used after specialization to the enveloping
algebra of a Chevalley Lie algebra.
The divided-power relation f * e⁽ⁿ⁺¹⁾ = e⁽ⁿ⁺¹⁾ * f - e⁽ⁿ⁾ * (h + n) in a universal
enveloping algebra over ℚ.
The reversed-product form of ι_f_mul_dividedPower_succ_ι_e:
e⁽ⁿ⁺¹⁾ f = f e⁽ⁿ⁺¹⁾ + (h - n) e⁽ⁿ⁾. This is the orientation that occurs as the
one-lowering-vector case of the full Kostant straightening formula.
The reversed-product form of ι_e_mul_dividedPower_succ_ι_f:
f⁽ⁿ⁺¹⁾ e = e f⁽ⁿ⁺¹⁾ - (h + n) f⁽ⁿ⁾.