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 a semiring R in which multiplication by factorials 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, following the convention given for natural numbers.

References

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

TODO

• Replace Nat.multichoose with Ring.multichoose.
• Generalize from Semiring to AddCommMonoid with Pow R ℕ using smeval.

class BinomialRing (R : Type u_1) [Semiring 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 for semirings, 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

  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 : ℕ), Nat.factorial n • BinomialRing.multichoose r n = Polynomial.eval r (ascPochhammer R n)

  ascPochhammer R n evaluated at any r is divisible by n! (witnessed by multichoose)

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

def Ring.multichoose {R : Type u_1} [Semiring 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 group of 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} [Semiring 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} [Semiring R] [BinomialRing R] (r : R) (n : ℕ) : Nat.factorial n • Ring.multichoose r n = Polynomial.eval r (ascPochhammer R n)

instance Nat.instBinomialRing : BinomialRing ℕ

Equations

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

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

The multichoose function for integers.

Equations

• Int.multichoose n k = match n with | Int.ofNat n => ↑(Nat.choose (n + k - 1) k) | Int.negSucc n => (-1) ^ k * ↑(Nat.choose (Nat.succ n) 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 }

def Ring.choose {R : Type u_1} [Ring 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} [Ring R] [BinomialRing R] (r : R) (n : ℕ) : Polynomial.eval r (descPochhammer R n) = Nat.factorial n • Ring.choose r n

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