Binomial rings

In this file we introduce the binomial property as a mixin, and define the multichoose and choose functions generalizing binomial coefficients.

According to our main reference [elliott2006binomial] (which lists many equivalent conditions), a binomial ring is a torsion-free commutative ring R such that for any x ∈ R and any k ∈ ℕ, the product x(x-1)⋯(x-k+1) is divisible by k!. The torsion-free condition lets us divide by k! unambiguously, so we get uniquely defined binomial coefficients.

The defining condition doesn't require commutativity or associativity, and we get a theory with essentially the same power by replacing subtraction with addition. Thus, we consider any additive commutative monoid with a notion of natural number exponents in which multiplication by positive integers is injective, and demand that the evaluation of the ascending Pochhammer polynomial X(X+1)⋯(X+(k-1)) at any element is divisible by k!. The quotient is called multichoose r k, because for r a natural number, it is the number of multisets of cardinality k taken from a type of cardinality n.

Definitions

• BinomialRing: a mixin class specifying a suitable multichoose function.
• Ring.multichoose: the quotient of an ascending Pochhammer evaluation by a factorial.
• Ring.choose: the quotient of a descending Pochhammer evaluation by a factorial.

Results

• Basic results with choose and multichoose, e.g., choose_zero_right
• Relations between choose and multichoose, negated input.
• Fundamental recursion: choose_succ_succ
• Chu-Vandermonde identity: add_choose_eq
• Pochhammer API

References

• [J. Elliott, Binomial rings, integer-valued polynomials, and λ-rings][elliott2006binomial]

TODO

Further results in Elliot's paper:

• A CommRing is binomial if and only if it admits a λ-ring structure with trivial Adams operations.
• The free commutative binomial ring on a set X is the ring of integer-valued polynomials in the variables X. (also, noncommutative version?)
• Given a commutative binomial ring A and an A-algebra B that is complete with respect to an ideal I, formal exponentiation induces an A-module structure on the multiplicative subgroup 1 + I.

class BinomialRing (R : Type u_1) [AddCommMonoid R] [Pow R ℕ] : Type u_1

A binomial ring is a ring for which ascending Pochhammer evaluations are uniquely divisible by suitable factorials. We define this notion as a mixin for additive commutative monoids with natural number powers, but retain the ring name. We introduce Ring.multichoose as the uniquely defined quotient.

• nsmul_right_injective : ∀ (n : ℕ), n ≠ 0 → Function.Injective fun (x : R) => n • x

  Scalar multiplication by positive integers is injective

• multichoose : R → ℕ → R

  A multichoose function, giving the quotient of Pochhammer evaluations by factorials.

• factorial_nsmul_multichoose : ∀ (r : R) (n : ℕ), n.factorial • BinomialRing.multichoose r n = (ascPochhammer ℕ n).smeval r

  The nth ascending Pochhammer polynomial evaluated at any element is divisible by n!

theorem BinomialRing.nsmul_right_injective {R : Type u_1} [AddCommMonoid R] [Pow R ℕ] [self : BinomialRing R] (n : ℕ) (h : n ≠ 0) : Function.Injective fun (x : R) => n • x

Scalar multiplication by positive integers is injective

theorem BinomialRing.factorial_nsmul_multichoose {R : Type u_1} [AddCommMonoid R] [Pow R ℕ] [self : BinomialRing R] (r : R) (n : ℕ) : n.factorial • BinomialRing.multichoose r n = (ascPochhammer ℕ n).smeval r

The nth ascending Pochhammer polynomial evaluated at any element is divisible by n!

theorem Ring.nsmul_right_injective {R : Type u_1} [AddCommMonoid R] [Pow R ℕ] [BinomialRing R] (n : ℕ) (h : n ≠ 0) : Function.Injective fun (x : R) => n • x

def Ring.multichoose {R : Type u_1} [AddCommMonoid R] [Pow R ℕ] [BinomialRing R] (r : R) (n : ℕ) : R

The multichoose function is the quotient of ascending Pochhammer evaluation by the corresponding factorial. When applied to natural numbers, multichoose k n describes choosing a multiset of n items from a type of size k, i.e., choosing with replacement.

Equations

• Ring.multichoose r n = BinomialRing.multichoose r n

@[simp]

theorem Ring.multichoose_eq_multichoose {R : Type u_1} [AddCommMonoid R] [Pow R ℕ] [BinomialRing R] (r : R) (n : ℕ) : BinomialRing.multichoose r n = Ring.multichoose r n

theorem Ring.factorial_nsmul_multichoose_eq_ascPochhammer {R : Type u_1} [AddCommMonoid R] [Pow R ℕ] [BinomialRing R] (r : R) (n : ℕ) : n.factorial • Ring.multichoose r n = (ascPochhammer ℕ n).smeval r

@[simp]

theorem Ring.multichoose_zero_right' {R : Type u_1} [AddCommMonoid R] [Pow R ℕ] [BinomialRing R] (r : R) : Ring.multichoose r 0 = r ^ 0

theorem Ring.multichoose_zero_right {R : Type u_1} [AddCommMonoid R] [Pow R ℕ] [BinomialRing R] [MulOneClass R] [NatPowAssoc R] (r : R) : Ring.multichoose r 0 = 1

@[simp]

theorem Ring.multichoose_one_right' {R : Type u_1} [AddCommMonoid R] [Pow R ℕ] [BinomialRing R] (r : R) : Ring.multichoose r 1 = r ^ 1

theorem Ring.multichoose_one_right {R : Type u_1} [AddCommMonoid R] [Pow R ℕ] [BinomialRing R] [MulOneClass R] [NatPowAssoc R] (r : R) : Ring.multichoose r 1 = r

@[simp]

theorem Ring.multichoose_zero_succ {R : Type u_2} [NonAssocSemiring R] [Pow R ℕ] [NatPowAssoc R] [BinomialRing R] (k : ℕ) : Ring.multichoose 0 (k + 1) = 0

theorem Ring.ascPochhammer_succ_succ {R : Type u_2} [NonAssocSemiring R] [Pow R ℕ] [NatPowAssoc R] [BinomialRing R] (r : R) (k : ℕ) : (ascPochhammer ℕ (k + 1)).smeval (r + 1) = (k + 1).factorial • Ring.multichoose (r + 1) k + (ascPochhammer ℕ (k + 1)).smeval r

theorem Ring.multichoose_succ_succ {R : Type u_2} [NonAssocSemiring R] [Pow R ℕ] [NatPowAssoc R] [BinomialRing R] (r : R) (k : ℕ) : Ring.multichoose (r + 1) (k + 1) = Ring.multichoose r (k + 1) + Ring.multichoose (r + 1) k

@[simp]

theorem Ring.multichoose_one {R : Type u_2} [NonAssocSemiring R] [Pow R ℕ] [NatPowAssoc R] [BinomialRing R] (k : ℕ) : Ring.multichoose 1 k = 1

theorem Ring.multichoose_two {R : Type u_2} [NonAssocSemiring R] [Pow R ℕ] [NatPowAssoc R] [BinomialRing R] (k : ℕ) : Ring.multichoose 2 k = ↑k + 1

@[simp]

theorem Polynomial.ascPochhammer_smeval_cast (R : Type u_1) [Semiring R] {S : Type u_2} [NonAssocSemiring S] [Pow S ℕ] [Module R S] [IsScalarTower R S S] [NatPowAssoc S] (x : S) (n : ℕ) : (ascPochhammer R n).smeval x = (ascPochhammer ℕ n).smeval x

theorem Polynomial.ascPochhammer_smeval_eq_eval {R : Type u_1} [Semiring R] (r : R) (n : ℕ) : (ascPochhammer ℕ n).smeval r = Polynomial.eval r (ascPochhammer R n)

theorem Polynomial.descPochhammer_smeval_eq_ascPochhammer {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] (r : R) (n : ℕ) : (descPochhammer ℤ n).smeval r = (ascPochhammer ℕ n).smeval (r - ↑n + 1)

theorem Polynomial.descPochhammer_smeval_eq_descFactorial {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] (n : ℕ) (k : ℕ) : (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)

theorem Polynomial.ascPochhammer_smeval_neg_eq_descPochhammer {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] (r : R) (k : ℕ) : (ascPochhammer ℕ k).smeval (-r) = (-1) ^ k * (descPochhammer ℤ k).smeval r

instance Nat.instBinomialRing : BinomialRing ℕ

Equations

• One or more equations did not get rendered due to their size.

def Int.multichoose (n : ℤ) (k : ℕ) : ℤ

The multichoose function for integers.

Equations

• n.multichoose k = match n with | Int.ofNat n => ↑((n + k - 1).choose k) | Int.negSucc n => (-1) ^ k * ↑((n + 1).choose k)

instance Int.instBinomialRing : BinomialRing ℤ

Equations

• Int.instBinomialRing = { nsmul_right_injective := Int.instBinomialRing.proof_1, multichoose := Int.multichoose, factorial_nsmul_multichoose := Int.instBinomialRing.proof_2 }

noncomputable instance instBinomialRingOfModuleNNRat {R : Type u_1} [AddCommMonoid R] [Module ℚ≥0 R] [Pow R ℕ] : BinomialRing R

Equations

• instBinomialRingOfModuleNNRat = { nsmul_right_injective := ⋯, multichoose := fun (r : R) (n : ℕ) => (↑n.factorial)⁻¹ • (ascPochhammer ℕ n).smeval r, factorial_nsmul_multichoose := ⋯ }

@[simp]

theorem Ring.smeval_ascPochhammer_self_neg (n : ℕ) : (ascPochhammer ℕ n).smeval (-↑n) = (-1) ^ n * ↑n.factorial

@[simp]

theorem Ring.smeval_ascPochhammer_succ_neg (n : ℕ) : (ascPochhammer ℕ (n + 1)).smeval (-↑n) = 0

theorem Ring.smeval_ascPochhammer_neg_add (n : ℕ) (k : ℕ) : (ascPochhammer ℕ (n + k + 1)).smeval (-↑n) = 0

@[simp]

theorem Ring.smeval_ascPochhammer_neg_of_lt {n : ℕ} {k : ℕ} (h : n < k) : (ascPochhammer ℕ k).smeval (-↑n) = 0

theorem Ring.smeval_ascPochhammer_nat_cast {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] (n : ℕ) (k : ℕ) : (ascPochhammer ℕ k).smeval ↑n = ↑((ascPochhammer ℕ k).smeval n)

theorem Ring.multichoose_neg_self (n : ℕ) : Ring.multichoose (-↑n) n = (-1) ^ n

@[simp]

theorem Ring.multichoose_neg_succ (n : ℕ) : Ring.multichoose (-↑n) (n + 1) = 0

theorem Ring.multichoose_neg_add (n : ℕ) (k : ℕ) : Ring.multichoose (-↑n) (n + k + 1) = 0

@[simp]

theorem Ring.multichoose_neg_of_lt (n : ℕ) (k : ℕ) (h : n < k) : Ring.multichoose (-↑n) k = 0

theorem Ring.multichoose_succ_neg_natCast {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [BinomialRing R] [NatPowAssoc R] (n : ℕ) : Ring.multichoose (-↑n) (n + 1) = 0

theorem Ring.smeval_ascPochhammer_int_ofNat {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] (r : R) (n : ℕ) : (ascPochhammer ℤ n).smeval r = (ascPochhammer ℕ n).smeval r

def Ring.choose {R : Type u_1} [AddCommGroupWithOne R] [Pow R ℕ] [BinomialRing R] (r : R) (n : ℕ) : R

The binomial coefficient choose r n generalizes the natural number choose function, interpreted in terms of choosing without replacement.

Equations

• Ring.choose r n = Ring.multichoose (r - ↑n + 1) n

theorem Ring.descPochhammer_eq_factorial_smul_choose {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [BinomialRing R] [NatPowAssoc R] (r : R) (n : ℕ) : (descPochhammer ℤ n).smeval r = n.factorial • Ring.choose r n

theorem Ring.choose_natCast {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [BinomialRing R] [NatPowAssoc R] (n : ℕ) (k : ℕ) : Ring.choose (↑n) k = ↑(n.choose k)

@[deprecated Ring.choose_natCast]

theorem Ring.choose_nat_cast {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [BinomialRing R] [NatPowAssoc R] (n : ℕ) (k : ℕ) : Ring.choose (↑n) k = ↑(n.choose k)

Alias of Ring.choose_natCast.

@[simp]

theorem Ring.choose_zero_right' {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [BinomialRing R] (r : R) : Ring.choose r 0 = (r + 1) ^ 0

theorem Ring.choose_zero_right {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [BinomialRing R] [NatPowAssoc R] (r : R) : Ring.choose r 0 = 1

@[simp]

theorem Ring.choose_zero_succ (R : Type u_2) [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] [BinomialRing R] (n : ℕ) : Ring.choose 0 (n + 1) = 0

theorem Ring.choose_zero_pos (R : Type u_2) [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] [BinomialRing R] {k : ℕ} (h_pos : 0 < k) : Ring.choose 0 k = 0

theorem Ring.choose_zero_ite (R : Type u_2) [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] [BinomialRing R] (k : ℕ) : Ring.choose 0 k = if k = 0 then 1 else 0

@[simp]

theorem Ring.choose_one_right' {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [BinomialRing R] (r : R) : Ring.choose r 1 = r ^ 1

theorem Ring.choose_one_right {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [BinomialRing R] [NatPowAssoc R] (r : R) : Ring.choose r 1 = r

theorem Ring.descPochhammer_succ_succ_smeval {R : Type u_2} [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] (r : R) (k : ℕ) : (descPochhammer ℤ (k + 1)).smeval (r + 1) = (k + 1) • (descPochhammer ℤ k).smeval r + (descPochhammer ℤ (k + 1)).smeval r

theorem Ring.choose_succ_succ {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [BinomialRing R] [NatPowAssoc R] (r : R) (k : ℕ) : Ring.choose (r + 1) (k + 1) = Ring.choose r k + Ring.choose r (k + 1)

theorem Ring.choose_eq_nat_choose {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [BinomialRing R] [NatPowAssoc R] (n : ℕ) (k : ℕ) : Ring.choose (↑n) k = ↑(n.choose k)

theorem Ring.choose_smul_choose {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [BinomialRing R] [NatPowAssoc R] (r : R) (n : ℕ) (k : ℕ) (hkn : k ≤ n) : n.choose k • Ring.choose r n = Ring.choose r k * Ring.choose (r - ↑k) (n - k)

theorem Ring.choose_add_smul_choose {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [BinomialRing R] [NatPowAssoc R] (r : R) (n : ℕ) (k : ℕ) : (n + k).choose k • Ring.choose (r + ↑k) (n + k) = Ring.choose (r + ↑k) k * Ring.choose r n

theorem Ring.descPochhammer_smeval_add {R : Type u_1} [Ring R] {r : R} {s : R} (k : ℕ) (h : Commute r s) : (descPochhammer ℤ k).smeval (r + s) = ∑ ij ∈ Finset.antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)

Pochhammer version of Chu-Vandermonde identity

theorem Ring.add_choose_eq {R : Type u_1} [Ring R] [BinomialRing R] {r : R} {s : R} (k : ℕ) (h : Commute r s) : Ring.choose (r + s) k = ∑ ij ∈ Finset.antidiagonal k, Ring.choose r ij.1 * Ring.choose s ij.2

The Chu-Vandermonde identity for binomial rings