Polynomial evaluation across a semiconjugacy relation

If a * x = x * (a + c) and c commutes with x, then moving a polynomial in a past x ^ n shifts its argument by n • c:

p(a) xⁿ = xⁿ p(a + n c).

The reverse reordering shifts by -n c. The main application is to the generalized binomial coefficients Ring.choose a m: these are the Cartan generators of a Kostant integral form, while the powers are the numerators of its root-vector divided powers.

The first result, SemiconjBy.smeval_right, is the general mechanism. It says that polynomial evaluation preserves both right-hand entries of SemiconjBy. The remaining results specialize it to an additive shift and then to Ring.choose.

Main results

• SemiconjBy.smeval_right: simultaneous polynomial evaluation preserves semiconjugacy.
• Polynomial.smeval_mul_pow_eq_pow_mul_smeval and Polynomial.pow_mul_smeval_eq_smeval_mul_pow: the corresponding polynomial reordering identities.
• TauCeti.ringChoose_mul_pow and TauCeti.pow_mul_ringChoose: their two binomial-coefficient forms.

References

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

theorem SemiconjBy.smeval_right {R : Type u} {A : Type v} [Semiring R] [Semiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {a x y : A} (h : SemiconjBy a x y) (p : Polynomial R) : SemiconjBy a (p.smeval x) (p.smeval y)

Polynomial evaluation preserves the two right-hand entries of a semiconjugacy relation.

This generalizes Mathlib's Polynomial.smeval_commute_left from Commute to SemiconjBy, following its proof.

theorem Polynomial.smeval_mul_pow_eq_pow_mul_smeval {A : Type u} [Semiring A] {R : Type v} [Semiring R] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (p : Polynomial R) {a x c : A} (h : a * x = x * (a + c)) (hc : Commute c x) (n : ℕ) : p.smeval a * x ^ n = x ^ n * p.smeval (a + n • c)

A polynomial in a can be moved to the right across x ^ n by shifting its argument by n • c.

theorem Polynomial.pow_mul_smeval_eq_smeval_mul_pow {A : Type u} [Ring A] {R : Type v} [Semiring R] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (p : Polynomial R) {a x c : A} (h : a * x = x * (a + c)) (hc : Commute c x) (n : ℕ) : x ^ n * p.smeval a = p.smeval (a - n • c) * x ^ n

A polynomial in a can be moved to the left across x ^ n by shifting its argument by -n • c.

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

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

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

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