Commuting binomial coefficients with divided powers

Suppose that a * x = x * (a + c) in an associative algebra over ℚ, with c commuting with x. This file combines polynomial semiconjugacy with normalized powers to prove

(a choose m) x⁽ⁿ⁾ = x⁽ⁿ⁾ (a + n c choose m),
x⁽ⁿ⁾ (a choose m) = (a - n c choose m) x⁽ⁿ⁾.

These identities are the Cartan/root-vector reordering rules used in a PBW basis of the Kostant integral form. Their significance is integral: although x⁽ⁿ⁾ contains the denominator n!, moving it past a Cartan binomial coefficient introduces no new rational coefficient.

Main results

• TauCeti.Associative.ringChoose_mul_dividedPower: move a binomial coefficient to the right.
• TauCeti.Associative.dividedPower_mul_ringChoose: move a binomial coefficient to the left.

References

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

theorem TauCeti.Associative.ringChoose_mul_dividedPower {A : Type u} [Ring A] [Algebra ℚ A] [BinomialRing A] (m : ℕ) {a x c : A} (h : a * x = x * (a + c)) (hc : Commute c x) (n : ℕ) : Ring.choose a m * dividedPower n x = dividedPower n x * Ring.choose (a + n • c) m

A generalized binomial coefficient can be moved to the right across a divided power by shifting its argument by n • c.

theorem TauCeti.Associative.dividedPower_mul_ringChoose {A : Type u} [Ring A] [Algebra ℚ A] [BinomialRing A] (m : ℕ) {a x c : A} (h : a * x = x * (a + c)) (hc : Commute c x) (n : ℕ) : dividedPower n x * Ring.choose a m = Ring.choose (a - n • c) m * dividedPower n x

A generalized binomial coefficient can be moved to the left across a divided power by shifting its argument by -n • c.