Symmetric quantum binomial coefficients

This file defines the symmetric quantum binomial coefficient [n choose k]_q in a field by the Pascal recursion [n+1 choose k+1]_q = q^(n-k) [n choose k]_q + q^(-(k+1)) [n choose k+1]_q, with [n choose 0]_q = 1 and [0 choose k+1]_q = 0, and proves the noncommutative q-binomial theorem: if q ≠ 0 and two elements of an algebra satisfy y x = q² x y, then (x + y)^n = ∑_k q^(k(n-k)) [n choose k]_q x^k y^(n-k).

The symmetric normalization makes [n choose k]_q invariant under q ↦ q⁻¹, and under k ↦ n - k for k ≤ n. It gives [n choose 1]_q = [n]_q whenever q - q⁻¹ ≠ 0, so that the quantum integer [n]_q is defined by a nonzero denominator, and it specializes to Nat.choose at q = 1. The q-binomial theorem computes the coproducts of the powers of the root generators of U_q(sl₂).

Negating the parameter gives [n choose k]_{-q} = (-1)^{k(n-k)} [n choose k]_q. This identity uses no division by quantum integers, so it includes roots of unity and q = ±1; at q = -1 it gives a signed ordinary binomial coefficient. These signs enter comparisons of quantum divided-power relations at opposite parameters.

Main definitions

• TauCeti.quantumBinomial q n k: the symmetric quantum binomial coefficient [n choose k]_q.

Main results

• TauCeti.quantumBinomial_succ_succ and TauCeti.quantumBinomial_succ_succ': the two Pascal rules, obtained from each other by q ↦ q⁻¹.
• TauCeti.quantumBinomial_succ_right_eq: the absorption identity [n choose k + 1]_q [k + 1]_q = [n choose k]_q [n - k]_q.
• TauCeti.quantumBinomial_inv and TauCeti.quantumBinomial_symm: invariance under q ↦ q⁻¹, and under k ↦ n - k for k ≤ n.
• TauCeti.quantumBinomial_neg_left: the sign change [n choose k]_{-q} = (-1)^{k(n-k)} [n choose k]_q.
• TauCeti.quantumBinomial_one_right: [n choose 1]_q = [n]_q when q - q⁻¹ ≠ 0.
• TauCeti.quantumBinomial_one: the classical specialization [n choose k]_1 = n.choose k.
• TauCeti.add_pow_of_mul_eq_smul_mul: the q-binomial theorem for y x = q² x y with q ≠ 0.
• TauCeti.coeff_prod_range_one_add_C_mul_X: Cauchy's binomial theorem in coefficient form, the coefficient of X ^ k in ∏_{j < n} (1 + q^(2j) X) is q^(k(n-1)) [n choose k]_q.

References

• C. Kassel, Quantum Groups, Graduate Texts in Mathematics 155, Section IV.2, for Gaussian binomial coefficients and the q-binomial formula for y x = q x y.
• J. C. Jantzen, Lectures on Quantum Groups, Graduate Studies in Mathematics 6, Chapter 0, for the symmetric normalization.
• G. Lusztig, Introduction to Quantum Groups, Sections 1.3 and 33.2, for the symmetric normalization and sign comparisons.
• V. Kac and P. Cheung, Quantum Calculus, Universitext, Chapter 5, for Gauss's (Cauchy's) binomial formula.

def TauCeti.quantumBinomial {K : Type u_1} [CommSemiring K] [Inv K] (q : K) : ℕ → ℕ → K

The symmetric quantum binomial coefficient [n choose k]_q, defined by [n choose 0]_q = 1, [0 choose k+1]_q = 0 and the Pascal rule [n+1 choose k+1]_q = q^(n-k) [n choose k]_q + q^(-(k+1)) [n choose k+1]_q.

@[simp]

theorem TauCeti.quantumBinomial_zero_right {K : Type u_1} [CommSemiring K] [Inv K] (q : K) (n : ℕ) : quantumBinomial q n 0 = 1

[n choose 0]_q = 1.

theorem TauCeti.quantumBinomial_zero_succ {K : Type u_1} [CommSemiring K] [Inv K] (q : K) (k : ℕ) : quantumBinomial q 0 (k + 1) = 0

[0 choose k + 1]_q = 0.

theorem TauCeti.quantumBinomial_succ_succ {K : Type u_1} [CommSemiring K] [Inv K] (q : K) (n k : ℕ) : quantumBinomial q (n + 1) (k + 1) = q ^ (n - k) * quantumBinomial q n k + q⁻¹ ^ (k + 1) * quantumBinomial q n (k + 1)

The defining Pascal rule [n+1 choose k+1]_q = q^(n-k) [n choose k]_q + q^(-(k+1)) [n choose k+1]_q.

@[simp]

theorem TauCeti.quantumBinomial_eq_zero_of_lt {K : Type u_1} [CommSemiring K] [Inv K] (q : K) {n k : ℕ} (h : n < k) : quantumBinomial q n k = 0

[n choose k]_q = 0 for n < k.

@[simp]

theorem TauCeti.quantumBinomial_self {K : Type u_1} [CommSemiring K] [Inv K] (q : K) (n : ℕ) : quantumBinomial q n n = 1

[n choose n]_q = 1.

theorem TauCeti.quantumBinomial_succ_succ_zpow {K : Type u_1} [Semifield K] (q : K) (n k : ℕ) : quantumBinomial q (n + 1) (k + 1) = q ^ (↑n - ↑k) * quantumBinomial q n k + q ^ (-(↑k + 1)) * quantumBinomial q n (k + 1)

The defining Pascal rule with integer exponents. This form holds for all indices, including k > n, because the corresponding quantum binomial coefficients vanish.

@[simp]

theorem TauCeti.quantumBinomial_one {K : Type u_1} [Semifield K] (n k : ℕ) : quantumBinomial 1 n k = ↑(n.choose k)

Over a semifield, the quantum binomial coefficients at q = 1 are the ordinary binomial coefficients.

theorem TauCeti.coeff_prod_range_one_add_C_mul_X {K : Type u_1} [Semifield K] {q : K} (hq : q ≠ 0) (n k : ℕ) : (∏ j ∈ Finset.range n, (1 + Polynomial.C ((q ^ 2) ^ j) * Polynomial.X)).coeff k = q ^ (↑k * (↑n - 1)) * quantumBinomial q n k

Cauchy's binomial theorem, in coefficient form: for q ≠ 0, the coefficient of X ^ k in ∏_{j < n} (1 + q^(2j) X) is q^(k(n-1)) [n choose k]_q.

theorem TauCeti.quantumBinomial_one_right {K : Type u_1} [Field K] {q : K} (hq : q - q⁻¹ ≠ 0) (n : ℕ) : quantumBinomial q n 1 = quantumInteger q ↑n

[n choose 1]_q = [n]_q whenever the quantum integers are defined by a nonzero denominator.

theorem TauCeti.quantumBinomial_succ_right_eq {K : Type u_1} [Field K] (q : K) (n k : ℕ) : quantumBinomial q n (k + 1) * quantumInteger q (↑k + 1) = quantumBinomial q n k * quantumInteger q (↑n - ↑k)

The absorption identity [n choose k + 1]_q [k + 1]_q = [n choose k]_q [n - k]_q. At a generic parameter it determines [n choose k]_q from [n choose 0]_q = 1.

theorem TauCeti.quantumBinomial_succ_succ' {K : Type u_1} [Field K] (q : K) (n k : ℕ) : quantumBinomial q (n + 1) (k + 1) = q⁻¹ ^ (n - k) * quantumBinomial q n k + q ^ (k + 1) * quantumBinomial q n (k + 1)

The second Pascal rule [n+1 choose k+1]_q = q^(-(n-k)) [n choose k]_q + q^(k+1) [n choose k+1]_q, the image of the defining rule under q ↦ q⁻¹.

@[simp]

theorem TauCeti.quantumBinomial_inv {K : Type u_1} [Field K] (q : K) (n k : ℕ) : quantumBinomial q⁻¹ n k = quantumBinomial q n k

The quantum binomial coefficients are invariant under q ↦ q⁻¹.

@[simp]

theorem TauCeti.quantumBinomial_neg_left {K : Type u_1} [Field K] (q : K) (n k : ℕ) : quantumBinomial (-q) n k = (-1) ^ (k * (n - k)) * quantumBinomial q n k

Negating the parameter multiplies the symmetric quantum binomial by (-1)^(k * (n - k)). This includes zero parameters and indices above the diagonal.

theorem TauCeti.quantumBinomial_symm {K : Type u_1} [Field K] (q : K) {n k : ℕ} (h : k ≤ n) : quantumBinomial q n (n - k) = quantumBinomial q n k

The symmetry [n choose n - k]_q = [n choose k]_q for k ≤ n.

theorem TauCeti.add_pow_of_mul_eq_smul_mul {K : Type u_1} [Field K] {A : Type u_2} [Semiring A] [Algebra K A] {q : K} (hq : q ≠ 0) {x y : A} (h : y * x = q ^ 2 • (x * y)) (n : ℕ) : (x + y) ^ n = ∑ k ∈ Finset.range (n + 1), (q ^ (k * (n - k)) * quantumBinomial q n k) • (x ^ k * y ^ (n - k))

The q-binomial theorem: if y x = q² x y for a nonzero scalar q, then (x + y)^n = ∑_k q^(k(n-k)) [n choose k]_q x^k y^(n-k).