Generalized binomial coefficients of an endomorphism at an eigenvector

An endomorphism f of a rational vector space is an element of the ℚ-algebra Module.End ℚ V, which is a binomial ring, so the generalized binomial coefficients Ring.choose f n = f (f - 1) ⋯ (f - n + 1) / n ! are again endomorphisms. This file records that they are computed on eigenvectors by the same expression in the eigenvalue:

f v = μ • v   →   (f choose n) v = (μ choose n) • v.

The mechanism is Mathlib's characterization of Ring.choose by Ring.descPochhammer_eq_factorial_smul_choose: the descending Pochhammer polynomial has integer coefficients, so it is evaluated on an eigenvector by evaluating it at the eigenvalue, and the factorial is then cancelled because a rational vector space is torsion-free.

Integer eigenvalues are the case of interest: the coefficient is then an ordinary natural-number binomial coefficient, which is what makes the Cartan generators (h choose n) of a Kostant integral form act integrally on weight vectors. TauCeti.Sl2Std.ringChoose_diag_apply is the coordinate form of the same computation for the standard sl₂-modules, where the endomorphism is diagonal in a fixed basis rather than merely applied to one eigenvector.

Main results

• TauCeti.ringChoose_end_apply_of_apply_eq_smul: the binomial coefficient of an endomorphism scales an eigenvector by the binomial coefficient of its eigenvalue.
• TauCeti.ringChoose_end_apply_of_apply_eq_natCast_smul: the specialization to a natural-number eigenvalue, where the scalar is Nat.choose.
• TauCeti.ringChoose_end_apply_mem_span_of_apply_eq_intCast_smul: binomial coefficients of an endomorphism preserve the integral span of integer-eigenvalue generators.

References

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

theorem TauCeti.ringChoose_end_apply_of_apply_eq_smul {V : Type u_1} [AddCommGroup V] [Module ℚ V] {f : Module.End ℚ V} {v : V} {μ : ℚ} (h : f v = μ • v) (n : ℕ) : (Ring.choose f n) v = Ring.choose μ n • v

A binomial coefficient of an endomorphism acts on an eigenvector through its eigenvalue. If f v = μ • v then (f choose n) v = (μ choose n) • v.

Both sides are n !-th multiples of the descending Pochhammer expression, which is a polynomial with integer coefficients and hence is evaluated on v by evaluating it at μ.

theorem TauCeti.ringChoose_end_apply_of_apply_eq_natCast_smul {V : Type u_1} [AddCommGroup V] [Module ℚ V] {f : Module.End ℚ V} {v : V} {j : ℕ} (h : f v = ↑j • v) (n : ℕ) : (Ring.choose f n) v = ↑(j.choose n) • v

The binomial coefficients of an endomorphism act on an eigenvector with natural-number eigenvalue j by the ordinary binomial coefficients (j choose n); in particular they act integrally.

theorem TauCeti.ringChoose_end_apply_mem_span_of_apply_eq_intCast_smul {V : Type u_1} [AddCommGroup V] [Module ℚ V] {I : Type u_2} {f : Module.End ℚ V} {e : I → V} {weight : I → ℤ} (heigen : ∀ (i : I), f (e i) = ↑(weight i) • e i) (n : ℕ) {v : V} (hv : v ∈ Submodule.span ℤ (Set.range e)) : (Ring.choose f n) v ∈ Submodule.span ℤ (Set.range e)

Binomial coefficients of an endomorphism preserve the integral span of any family of eigenvectors whose eigenvalues are integers.