Rank-one Kostant straightening

This file proves the rank-one straightening formula for divided powers in an associative ℚ-algebra. If H, E, and F satisfy the sl₂ commutator relations, then

E * F - F * E = H,   H * E - E * H = 2 • E,   H * F - F * H = -(2 • F),

E⁽ᵐ⁾ F⁽ⁿ⁾ =
  ∑ k ≤ min(m,n), F⁽ⁿ⁻ᵏ⁾ (H - m - n + 2k choose k) E⁽ᵐ⁻ᵏ⁾.

All coefficients are generalized binomial coefficients, so the formula is integral even though the individual divided powers are defined using rational factorial denominators. This is the rank-one normal-ordering relation needed for the integral PBW theorem for a Kostant form.

The proof follows the usual induction on m. Moving one additional E through the lowering divided power produces two adjacent summands. TauCeti.Ring.mul_weighted_choose_add_mul_choose combines their Cartan coefficients without division.

Main results

• TauCeti.Sl2.dividedPower_e_mul_dividedPower_f: the rank-one Kostant straightening formula in an arbitrary associative ℚ-algebra satisfying the three displayed commutator relations.
• TauCeti.Sl2.dividedPower_ι_e_mul_dividedPower_ι_f: its specialization to the canonical map into a universal enveloping algebra, stated from the corresponding Lie-bracket relations.

References

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

theorem TauCeti.Sl2.dividedPower_e_mul_dividedPower_f {A : Type u} [Ring A] [Algebra ℚ A] {H E F : A} (hef : E * F - F * E = H) (hhe : H * E - E * H = 2 • E) (hhf : H * F - F * H = -(2 • F)) (m n : ℕ) : Associative.dividedPower m E * Associative.dividedPower n F = ∑ k ∈ Finset.range (min m n + 1), Associative.dividedPower (n - k) F * Ring.choose (H - ↑(m + n) + ↑(2 * k)) k * Associative.dividedPower (m - k) E

The rank-one Kostant straightening formula. If H, E, and F satisfy the sl₂ commutator relations in an associative ℚ-algebra, then the product of a raising divided power and a lowering divided power is an integral sum in PBW order F, H, E.

The argument of the Cartan binomial is written as H - (m + n) + 2 * k; the natural numbers are coerced to the algebra, so this is the standard coefficient (H - m - n + 2k choose k).

theorem TauCeti.Sl2.dividedPower_ι_e_mul_dividedPower_ι_f {L : Type u_1} [LieRing L] [LieAlgebra ℚ L] {h e f : L} (hef : ⁅e, f⁆ = h) (hhe : ⁅h, e⁆ = 2 • e) (hhf : ⁅h, f⁆ = -(2 • f)) (m n : ℕ) : Associative.dividedPower m ((UniversalEnvelopingAlgebra.ι ℚ) e) * Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) f) = ∑ k ∈ Finset.range (min m n + 1), Associative.dividedPower (n - k) ((UniversalEnvelopingAlgebra.ι ℚ) f) * Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) h - ↑(m + n) + ↑(2 * k)) k * Associative.dividedPower (m - k) ((UniversalEnvelopingAlgebra.ι ℚ) e)

The rank-one Kostant straightening formula in a universal enveloping algebra over ℚ, stated from the three sl₂ Lie-bracket relations.