Products of generalized binomial coefficients

This file gives the linearization formula for the product of two generalized binomial coefficients in a binomial ring. The formula reads

(r choose m) (r choose n) =
  ∑ i + j = n, (m choose j) (m + i choose m) (r choose (m + i)).

The coefficients are natural numbers. Consequently the additive subgroup spanned by the coefficients (r choose n) is already a subring. This integral form is the Cartan--Cartan multiplication rule used when normal-ordering the generators of the Kostant integral form: products of the generators (h choose n) remain integral linear combinations of generators of the same kind.

The proof combines Mathlib's Chu--Vandermonde identity Ring.add_choose_eq with its shifted factorization Ring.choose_smul_choose. No polynomial expansion or division by factorials is needed.

Integer translation is controlled by the same basis. Chu--Vandermonde expresses (r + z choose n), for z : ℤ, as an integral combination of the coefficients (r choose k). Applying the formula again with -z proves equality of the two integral spans. This is the integrality input for commuting Cartan binomial coefficients past divided powers of root vectors.

Main results

• TauCeti.ringChoose_mul_ringChoose: the product of two binomial coefficients in r, expanded as a natural-number linear combination of binomial coefficients in r.
• TauCeti.ringChooseSpan: the additive subgroup spanned by the binomial coefficients in one element.
• TauCeti.span_int_range_ringChoose: that span coincides with the ℤ-submodule generated by the coefficients.
• TauCeti.mem_ringChooseSpan_iff_existsUnique: unique integral expansion in the binomial coefficients under ℤ-linear independence.
• TauCeti.mul_mem_ringChooseSpan: that span is closed under multiplication.
• TauCeti.toAddSubgroup_subringClosure_range_ringChoose: the subring generated by the binomial coefficients in r has no additive elements beyond this span.
• TauCeti.Ring.choose_intCast: generalized binomial coefficients commute with integer casts.
• TauCeti.Ring.choose_add_intCast_mem: additive subgroups containing the coefficients of r up to degree n contain the degree-n coefficient of every integer translate of r.
• TauCeti.ringChoose_add_intCast_mem_ringChooseSpan and TauCeti.ringChoose_sub_intCast_mem_ringChooseSpan: integer translates of a coefficient lie in the integral span of the original coefficients.
• TauCeti.ringChooseSpan_add_intCast and TauCeti.ringChooseSpan_sub_intCast: integer translation leaves that integral span unchanged.
• TauCeti.exists_forall_sum_mul_choose_eq: prescribed integer values on an initial segment are attained by an integral combination of binomial coefficients.

References

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

theorem TauCeti.ringChoose_mul_ringChoose {R : Type u_1} [Ring R] [BinomialRing R] (r : R) (m n : ℕ) : Ring.choose r m * Ring.choose r n = ∑ ij ∈ Finset.antidiagonal n, (m.choose ij.2 * (m + ij.1).choose m) • Ring.choose r (m + ij.1)

The product of two generalized binomial coefficients, expanded as an integral linear combination of generalized binomial coefficients in the same element.

The pair (i, j) runs over i + j = n. Thus the summand has binomial degree m + i and coefficient (m choose j) * (m + i choose m). Terms with m < j vanish automatically.

The integral span

def TauCeti.ringChooseSpan {R : Type u_1} [AddCommGroupWithOne R] [Pow R ℕ] [BinomialRing R] (r : R) : AddSubgroup R

The additive subgroup spanned by all generalized binomial coefficients in r.

Equations

• TauCeti.ringChooseSpan r = AddSubgroup.closure (Set.range (Ring.choose r))

theorem TauCeti.ringChooseSpan_def {R : Type u_1} [AddCommGroupWithOne R] [Pow R ℕ] [BinomialRing R] (r : R) : ringChooseSpan r = AddSubgroup.closure (Set.range (Ring.choose r))

The integral span is the additive closure of the generalized binomial coefficients.

@[simp]

theorem TauCeti.ringChoose_mem_ringChooseSpan {R : Type u_1} [AddCommGroupWithOne R] [Pow R ℕ] [BinomialRing R] (r : R) (n : ℕ) : Ring.choose r n ∈ ringChooseSpan r

Every generalized binomial coefficient in r belongs to its integral span.

@[simp]

theorem TauCeti.ringChooseSpan_le_iff {R : Type u_1} [AddCommGroupWithOne R] [Pow R ℕ] [BinomialRing R] {A : AddSubgroup R} {r : R} : ringChooseSpan r ≤ A ↔ ∀ (n : ℕ), Ring.choose r n ∈ A

The integral span of the generalized binomial coefficients in r lies in an additive subgroup exactly when that subgroup contains every such coefficient.

@[simp]

theorem TauCeti.span_int_range_ringChoose {R : Type u_1} [AddCommGroupWithOne R] [Pow R ℕ] [BinomialRing R] (r : R) : Submodule.span ℤ (Set.range (Ring.choose r)) = AddSubgroup.toIntSubmodule (ringChooseSpan r)

The ℤ-linear span of the generalized binomial coefficients in r is the integral submodule associated to ringChooseSpan r.

theorem TauCeti.mem_ringChooseSpan_iff_existsUnique {R : Type u_1} [AddCommGroupWithOne R] [Pow R ℕ] [BinomialRing R] {r : R} (h : LinearIndependent ℤ fun (n : ℕ) => Ring.choose r n) (x : R) : x ∈ ringChooseSpan r ↔ ∃! a : ℕ →₀ ℤ, (a.sum fun (n : ℕ) (z : ℤ) => z • Ring.choose r n) = x

An element lies in the integral span of the generalized binomial coefficients in r exactly when it has a unique finite integral expansion in those coefficients, provided the sequence of coefficients is ℤ-linearly independent.

@[simp]

theorem TauCeti.one_mem_ringChooseSpan {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] [BinomialRing R] (r : R) : 1 ∈ ringChooseSpan r

The integral span of the generalized binomial coefficients contains one.

theorem TauCeti.mul_mem_ringChooseSpan {R : Type u_1} [Ring R] [BinomialRing R] (r : R) {x y : R} (hx : x ∈ ringChooseSpan r) (hy : y ∈ ringChooseSpan r) : x * y ∈ ringChooseSpan r

The integral span of the generalized binomial coefficients is closed under multiplication.

This is the algebraic content of ringChoose_mul_ringChoose: its natural-number coefficients act by repeated addition, so every product of spanning generators remains in the same additive span.

@[simp]

theorem TauCeti.toAddSubgroup_subringClosure_range_ringChoose {R : Type u_1} [Ring R] [BinomialRing R] (r : R) : (Subring.closure (Set.range (Ring.choose r))).toAddSubgroup = ringChooseSpan r

The subring generated by the generalized binomial coefficients in one element r is, as an additive subgroup, exactly their integral span: no products or powers of these coefficients escape the span they already generate additively.

@[simp]

theorem TauCeti.mem_subringClosure_range_ringChoose_iff {R : Type u_1} [Ring R] [BinomialRing R] {r x : R} : x ∈ Subring.closure (Set.range (Ring.choose r)) ↔ x ∈ ringChooseSpan r

Membership in the subring generated by the generalized binomial coefficients in r is membership in their integral additive span.

Integer translation

@[simp]

theorem TauCeti.Ring.choose_intCast {R : Type u_1} [Ring R] [BinomialRing R] (z : ℤ) (n : ℕ) : Ring.choose (↑z) n = ↑(Ring.choose z n)

Generalized binomial coefficients commute with the canonical map from the integers.

theorem TauCeti.Ring.choose_add_intCast_mem {R : Type u_1} [Ring R] [BinomialRing R] {G : Type u_2} [SetLike G R] [AddSubgroupClass G R] {A : G} {r : R} {n : ℕ} (hr : ∀ k ≤ n, Ring.choose r k ∈ A) (z : ℤ) : Ring.choose (r + ↑z) n ∈ A

An additive subgroup-like set containing the generalized binomial coefficients of r up to degree n contains the degree-n coefficient after translating r by an integer.

@[simp]

theorem TauCeti.ringChoose_add_intCast_mem_ringChooseSpan {R : Type u_1} [Ring R] [BinomialRing R] (r : R) (z : ℤ) (n : ℕ) : Ring.choose (r + ↑z) n ∈ ringChooseSpan r

Translating the argument of a generalized binomial coefficient by an integer keeps it in the integral span of the coefficients in the original argument.

Chu--Vandermonde expands (r + z choose n) as products of (r choose i) with integer-valued coefficients (z choose j).

@[simp]

theorem TauCeti.ringChoose_sub_intCast_mem_ringChooseSpan {R : Type u_1} [Ring R] [BinomialRing R] (r : R) (z : ℤ) (n : ℕ) : Ring.choose (r - ↑z) n ∈ ringChooseSpan r

Subtracting an integer from the argument of a generalized binomial coefficient keeps it in the integral span of the coefficients in the original argument.

@[simp]

theorem TauCeti.ringChooseSpan_add_intCast {R : Type u_1} [Ring R] [BinomialRing R] (r : R) (z : ℤ) : ringChooseSpan (r + ↑z) = ringChooseSpan r

Integer translation leaves the integral span of the generalized binomial coefficients unchanged.

@[simp]

theorem TauCeti.ringChooseSpan_sub_intCast {R : Type u_1} [Ring R] [BinomialRing R] (r : R) (z : ℤ) : ringChooseSpan (r - ↑z) = ringChooseSpan r

Subtracting an integer from the argument leaves the integral span of the generalized binomial coefficients unchanged.

Identities and negation for generalized binomial coefficients

In a binomial ring, Mathlib's Ring.choose_neg writes (-r choose n) as a sign times the multichoose coefficient of r, which is (r + n - 1 choose n). This file takes the last step and expands that coefficient by the Chu--Vandermonde identity, so that (-r choose n) becomes an integer combination of the coefficients (r choose k) for k ≤ n, with the ordinary binomial coefficients of n - 1 as its weights.

The consequence, TauCeti.Ring.choose_neg_mem, is the form a consumer uses: an additive subgroup containing (r choose k) for every k ≤ n contains (-r choose n) as well. That is what makes the Cartan generators of a Kostant integral form stable under the antipode of an enveloping algebra, since the antipode negates each Cartan vector.

The file also records a weighted form of Pascal's identity. Its two terms are exactly the adjacent coefficients that arise when one more raising operator is moved through a rank-one Kostant normal-ordering sum: the first keeps the summation index and the second increments it. The identity combines them without division, which is the integral step needed in the induction.

Main results

• TauCeti.Ring.choose_neg_succ_eq_sum: the expansion of (-r choose (n + 1)) as a signed Chu--Vandermonde sum of the coefficients (r choose k).
• TauCeti.Ring.choose_neg_mem: an additive subgroup containing the coefficients of r up to degree n contains the degree-n coefficient of -r.
• TauCeti.ringChooseSpan_neg: negation leaves the integral span unchanged.
• TauCeti.Ring.mul_weighted_choose_add_mul_choose: a scalar-weighted Pascal identity.

References

• J. Elliott, Binomial rings, integer-valued polynomials, and λ-rings, J. Pure Appl. Algebra 207 (2006), 165–185.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §26.2, for the rank-one Kostant normal-ordering formula that consumes the weighted identity.

Weighted Pascal identities

@[simp]

theorem TauCeti.Ring.mul_weighted_choose_add_mul_choose {R : Type u_2} [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] [BinomialRing R] (r c : R) (k : ℕ) : c * Ring.choose (r - 1) (k + 1) + (r + c) * Ring.choose (r - 1) k = c * Ring.choose r (k + 1) + (k + 1) • Ring.choose r (k + 1)

A scalar-weighted form of Pascal's identity:

c (r - 1 choose k + 1) + (r + c) (r - 1 choose k)
  = c (r choose k + 1) + (k + 1) (r choose k + 1).

No commutativity between c and r is needed: every occurrence of c is on the left.

Negating the argument

theorem TauCeti.Ring.choose_neg_succ_eq_sum {R : Type u_2} [Ring R] [BinomialRing R] (r : R) (n : ℕ) : Ring.choose (-r) (n + 1) = (↑n + 1).negOnePow • ∑ ij ∈ Finset.antidiagonal (n + 1), Ring.choose r ij.1 * ↑(n.choose ij.2)

Negating the argument of a generalized binomial coefficient of positive degree expands, by Chu--Vandermonde, into a signed sum of the coefficients of the original argument weighted by ordinary binomial coefficients of n.

The degree is written as n + 1 because the multichoose shift r + n - 1 of Ring.choose_neg is a natural-number translate of r only in positive degree. Degree zero is Ring.choose_zero_right on both sides.

theorem TauCeti.Ring.choose_neg_mem {R : Type u_2} [Ring R] [BinomialRing R] {G : Type u_3} [SetLike G R] [AddSubgroupClass G R] {A : G} {r : R} {n : ℕ} (hr : ∀ k ≤ n, Ring.choose r k ∈ A) : Ring.choose (-r) n ∈ A

An additive subgroup-like set containing the generalized binomial coefficients of r up to degree n contains the degree-n coefficient of -r.

@[simp]

theorem TauCeti.ringChooseSpan_neg {R : Type u_1} [Ring R] [BinomialRing R] (r : R) : ringChooseSpan (-r) = ringChooseSpan r

Negation leaves the integral span of the generalized binomial coefficients unchanged.

Integral interpolation on an initial segment

The generalized binomial coefficients are the integrally interpolating family: prescribing arbitrary integer values on 0, 1, …, N is always solvable in integer coefficients, even though the interpolating polynomial itself has non-integral coefficients. This is Newton's forward-difference formula, and it is what lets integral combinations of the binomial coefficients (h choose k) of a Cartan vector separate the integer weights of a representation, one weight at a time.

theorem TauCeti.exists_forall_sum_mul_choose_eq (N : ℕ) (g : ℕ → ℤ) : ∃ (c : ℕ → ℤ), ∀ j ≤ N, ∑ k ∈ Finset.range (N + 1), c k * ↑(j.choose k) = g j

Integral interpolation by binomial coefficients. Arbitrary integer values on the initial segment 0, 1, …, N are attained by an integral combination of the binomial coefficients (· choose k) for k ≤ N.

The matrix (j choose k) is lower unitriangular, so the coefficients are read off one at a time: the induction step solves for c (N + 1) using (N + 1 choose N + 1) = 1, and the added term does not disturb the smaller values because (j choose N + 1) = 0 for j ≤ N.