Cartan and root-vector commutation in a universal enveloping algebra

Let h and x be elements of a Lie algebra over ℚ satisfying

[h, x] = z x,     z : ℤ.

Inside the universal enveloping algebra this becomes h x = x (h + z). The generic binomial/divided-power reordering identities therefore give

(h choose m) x⁽ⁿ⁾ = x⁽ⁿ⁾ (h + n z choose m),
x⁽ⁿ⁾ (h choose m) = (h - n z choose m) x⁽ⁿ⁾.

Here an integer such as n z denotes that integer times the unit of the enveloping algebra. For the Chevalley generators, z is the integral Cartan integer pairing a simple coroot with a root. These formulas are the Cartan/root-vector part of normal ordering the generators of the Kostant integral form; the root/root part requires the separate root-string formulas.

Main results

• TauCeti.UniversalEnvelopingAlgebra.ι_mul_ι_eq_ι_mul_ι_add_zsmul_one: the associative-ring form of an integral weight relation.
• TauCeti.UniversalEnvelopingAlgebra.ringChoose_ι_mul_dividedPower_ι: move a Cartan binomial coefficient to the right of a root-vector divided power.
• TauCeti.UniversalEnvelopingAlgebra.dividedPower_ι_mul_ringChoose_ι: the reverse reordering.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §26.2.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

theorem TauCeti.UniversalEnvelopingAlgebra.ι_mul_ι_eq_ι_mul_ι_add_zsmul_one {L : Type u} [LieRing L] {R : Type u_1} [CommRing R] [LieAlgebra R L] {h x : L} {z : ℤ} (hz : ⁅h, x⁆ = z • x) : (UniversalEnvelopingAlgebra.ι R) h * (UniversalEnvelopingAlgebra.ι R) x = (UniversalEnvelopingAlgebra.ι R) x * ((UniversalEnvelopingAlgebra.ι R) h + z • 1)

The associative-ring form of an integral weight relation in a Lie algebra.

theorem TauCeti.UniversalEnvelopingAlgebra.ringChoose_ι_mul_dividedPower_ι {L : Type u} [LieRing L] [LieAlgebra ℚ L] {h x : L} {z : ℤ} (hz : ⁅h, x⁆ = z • x) (m n : ℕ) : Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) h) m * Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) x) = Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) x) * Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) h + ↑(↑n * z)) m

A Cartan binomial coefficient moves to the right of a root-vector divided power by adding n copies of the integral weight to its argument.

theorem TauCeti.UniversalEnvelopingAlgebra.dividedPower_ι_mul_ringChoose_ι {L : Type u} [LieRing L] [LieAlgebra ℚ L] {h x : L} {z : ℤ} (hz : ⁅h, x⁆ = z • x) (m n : ℕ) : Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) x) * Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) h) m = Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) h - ↑(↑n * z)) m * Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) x)

A Cartan binomial coefficient moves to the left of a root-vector divided power by subtracting n copies of the integral weight from its argument.