BinomialNotes.txt

Part I, Goal:

Introduce binomial rings, following J. Elliot's paper.

Binomial rings are torsion-free commutative rings R such that for any x ∈ R and any k ∈ ℕ, we have k! | x(x-1)⋯(x-k+1).
The torsion-free condition implies multiplication by k! is injective, so we define `choose x k` to be the unique y such that y*k! = x(x-1)⋯(x-k+1).

We can generalize this to the following condition: multiplication by positive integers is injective, and k! | x(x+1)⋯(x+k-1) for all x and k.
Then, the defining conditions don't need a commutative ring - we just need a way to evaluate polynomials with natural number coefficients.
We define multichoose x k to be the unique function satisfying k! | x(x+1)⋯(x+k-1).

Part II, Theorems about binomial coefficients we need for vertex algebras:

0. Z is a binomial ring.  If ℚ ⊂ R, then k! is invertible, so R is binomial.
1. When x ∈ ℕ, Ring.choose agrees with nat.choose.
2. nat.choose_mul : n.choose k * k.choose s = n.choose s * (n-s).choose (k-s) when k \geq s
   An alternative form is x.choose (n+k) * (n+k).choose k = x.choose n * (x-n).choose k
   so we know which terms need to be non-negative.
3. (-1)^k x.choose k = (k-x-1).choose k
4. Vandermonde convolution: (x+y).choose k = \sum ij \in antidiagonal k, x.choose ij.1 * y.choose ij.2

Theorems about series we need:
1. Expansions of (x-y)^(-N) when |x| < |y| and |y| < |x| - A good treatment of Hahn series in two variables should make this work.
2. Difference of expansions is annihilated by (x-y)^N - I may more API for variables.
3. Formal taylor expansion of (1+x)^r - need divided-power derivatives (which is done).
4. If we define (x-y)^r = x^r(1-y/x)^r ∈ x^r R[x^(-1)][[y]]
   when |x|>|y|, show ((x-y)^r)^s = (x-y)^{rs} in the same region.

Part III, Implementation plan:

All theorems are finished and merged into Mathlib4.

Part IV, To do:

Consider proving some of Elliott's other results (#7 may be relevant):
1. The integer-valued polynomial rings (generated by Ring.choose x_i n) are free (commutative) binomial rings.  That is, we get a left adjoint to the forgetful functor to sets.
2. A commutative ring is binomial if and only if it is a \lambda-ring whose Adams operations are all identity.
3. There is a right-adjoint to the forgetful functor from commutative binomial rings to commutative rings, and the universal \lambda ring is a module.
4. There is a right-adjoint to the inclusion of binomial rings to \lambda-rings, namely the functor that takes a \lambda-ring to the largest subring on which Adams operations are identity.
4. A presentation of the ring of integer-valued polynomials.
5. In order that a commutative ring A be binomial, it is necessary and sufficient that for all primes p and a \in A, a^p \equiv a mod pA.
6. Smallest enveloping binomial ring of a torsion-free ring.
7. Let B be a binomial ring, and let A be a commutative B-algebra that is complete with respect to an ideal I.  Then, the multiplicative abelian group 1+I has a B-module structure given by (1+a)^b = \sum_{n \geq 0} \binom{b}{n} a^n.  Note that the axioms for module structure are equivalent to certain binomial identities, and the one for (1+a)^{bb'} is not yet covered here.