Quantum factorials

This file defines the quantum factorial [n]_q! = [1]_q [2]_q ⋯ [n]_q of the symmetric quantum integers [r]_q = (q^r - q^(-r)) / (q - q⁻¹) in a field, and the corresponding Laurent polynomial [n]_v! ∈ ℤ[v, v⁻¹].

Quantum factorials are the denominators of the divided powers x^(n) = x^n / [n]_q! of the Chevalley generators of a quantized enveloping algebra. Their nonvanishing is the genericity hypothesis under which those divided powers exist: [n]_q! ≠ 0 for every n exactly when q is nonzero and not a root of unity. At a root of unity, with q² of order ℓ, the quantum factorial [n]_q! is nonzero exactly for n < ℓ. The field convention makes every quantum integer vanish when q - q⁻¹ = 0, so [n]_(±1)! = 0 for n ≥ 1; the Laurent quantum factorial instead specializes to n! at v = 1.

Main definitions

• TauCeti.quantumFactorial q n: the quantum factorial [n]_q! in a field.
• TauCeti.laurentQuantumFactorial n: the quantum factorial [n]_v! in ℤ[v, v⁻¹].

Main results

• TauCeti.quantumInteger_eq_zero_iff_dvd: if q ≠ 0 and q² is a primitive ℓ-th root of unity, then [r]_q = 0 iff ℓ ∣ r.
• TauCeti.forall_quantumFactorial_ne_zero_iff: [n]_q! ≠ 0 for all n iff q is a generic quantum parameter, that is, nonzero and not a root of unity.
• TauCeti.quantumFactorial_ne_zero_iff_lt: if q² is a primitive ℓ-th root of unity with ℓ > 0, then [n]_q! ≠ 0 iff n < ℓ.
• TauCeti.quantumBinomial_mul_quantumFactorial_mul_quantumFactorial: for k ≤ n, [n choose k]_q [k]_q! [n - k]_q! = [n]_q!, with no hypothesis on q.
• TauCeti.inv_quantumFactorial_smul_add_pow: the divided-power form of the q-binomial theorem, (x + y)^(n) = ∑_k q^(k(n-k)) x^(k) y^(n-k) when y x = q² x y and [n]_q! ≠ 0.
• TauCeti.laurentEval_laurentQuantumFactorial and TauCeti.laurentEval_one_laurentQuantumFactorial: [n]_v! specializes to [n]_q! at v = q when q - q⁻¹ ≠ 0, and to n! at v = 1; in particular [n]_v! ≠ 0 (TauCeti.laurentQuantumFactorial_ne_zero).

References

• J. C. Jantzen, Lectures on Quantum Groups, Graduate Studies in Mathematics 6, Chapter 0, for quantum factorials and the symmetric normalization.
• G. Lusztig, Introduction to Quantum Groups, Progress in Mathematics 110, Section 1.3, for quantum factorials and divided powers.

Vanishing of quantum integers at roots of unity

theorem TauCeti.quantumInteger_eq_zero_iff_dvd {K : Type u_1} [Field K] {q : K} (hq : q ≠ 0) {ℓ : ℕ} (h : IsPrimitiveRoot (q ^ 2) ℓ) (r : ℤ) : quantumInteger q r = 0 ↔ ↑ℓ ∣ r

If q ≠ 0 and q² is a primitive ℓ-th root of unity, then the quantum integer [r]_q vanishes exactly when ℓ ∣ r. For ℓ = 1, that is q = ±1, every quantum integer vanishes by the field convention.

Quantum factorials in a field

noncomputable def TauCeti.quantumFactorial {K : Type u_1} [Field K] (q : K) (n : ℕ) : K

The quantum factorial [n]_q! = [1]_q [2]_q ⋯ [n]_q of the symmetric quantum integers.

theorem TauCeti.quantumFactorial_def {K : Type u_1} [Field K] (q : K) (n : ℕ) : quantumFactorial q n = ∏ j ∈ Finset.range n, quantumInteger q (↑j + 1)

The defining product formula for the quantum factorial.

@[simp]

theorem TauCeti.quantumFactorial_zero {K : Type u_1} [Field K] (q : K) : quantumFactorial q 0 = 1

[0]_q! = 1.

theorem TauCeti.quantumFactorial_succ {K : Type u_1} [Field K] (q : K) (n : ℕ) : quantumFactorial q (n + 1) = quantumFactorial q n * quantumInteger q (↑n + 1)

[n + 1]_q! = [n]_q! [n + 1]_q.

@[simp]

theorem TauCeti.quantumFactorial_one {K : Type u_1} [Field K] (q : K) : quantumFactorial q 1 = quantumInteger q 1

[1]_q! = [1]_q, which is 1 when q - q⁻¹ ≠ 0.

@[simp]

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

Replacing the parameter by its inverse leaves every quantum factorial unchanged.

theorem TauCeti.quantumFactorial_eq_zero_iff {K : Type u_1} [Field K] {q : K} {n : ℕ} : quantumFactorial q n = 0 ↔ ∃ j < n, quantumInteger q (↑j + 1) = 0

The quantum factorial [n]_q! vanishes exactly when one of its factors [j + 1]_q, j < n, does.

theorem TauCeti.quantumFactorial_ne_zero_of_le {K : Type u_1} [Field K] {q : K} {m n : ℕ} (hmn : m ≤ n) (hn : quantumFactorial q n ≠ 0) : quantumFactorial q m ≠ 0

Nonvanishing of quantum factorials passes to smaller indices: if [n]_q! ≠ 0 and m ≤ n, then [m]_q! ≠ 0.

theorem TauCeti.sub_inv_ne_zero_of_quantumFactorial_ne_zero {K : Type u_1} [Field K] {q : K} {n : ℕ} (hn₀ : n ≠ 0) (hn : quantumFactorial q n ≠ 0) : q - q⁻¹ ≠ 0

A nonzero quantum factorial [n]_q! with n ≥ 1 forces the defining denominator q - q⁻¹ of the quantum integers to be nonzero.

theorem TauCeti.quantumFactorial_ne_zero {K : Type u_1} [Field K] {q : K} (hq : IsGenericQuantumParameter q) (n : ℕ) : quantumFactorial q n ≠ 0

Quantum factorials do not vanish at a generic quantum parameter.

theorem TauCeti.forall_quantumFactorial_ne_zero_iff {K : Type u_1} [Field K] {q : K} : (∀ (n : ℕ), quantumFactorial q n ≠ 0) ↔ IsGenericQuantumParameter q

Genericity through quantum factorials: all quantum factorials [n]_q! are nonzero exactly when q is a generic quantum parameter, that is, nonzero and not a root of unity.

theorem TauCeti.quantumFactorial_ne_zero_iff_lt {K : Type u_1} [Field K] {q : K} {ℓ : ℕ} (h : IsPrimitiveRoot (q ^ 2) ℓ) (hℓ : 0 < ℓ) {n : ℕ} : quantumFactorial q n ≠ 0 ↔ n < ℓ

Quantum factorials at a root of unity: if q² is a primitive ℓ-th root of unity with ℓ > 0, then [n]_q! ≠ 0 exactly when n < ℓ.

@[simp]

theorem RingHom.map_quantumFactorial {K : Type u_1} [Field K] {L : Type u_2} [Field L] (φ : K →+* L) (q : K) (n : ℕ) : φ (TauCeti.quantumFactorial q n) = TauCeti.quantumFactorial (φ q) n

Ring homomorphisms between fields commute with the quantum factorials.

Quantum binomial coefficients as quotients of quantum factorials

theorem TauCeti.quantumBinomial_mul_quantumFactorial_mul_quantumFactorial {K : Type u_1} [Field K] (q : K) {n k : ℕ} (hk : k ≤ n) : quantumBinomial q n k * quantumFactorial q k * quantumFactorial q (n - k) = quantumFactorial q n

The quantum binomial coefficient times the two complementary quantum factorials is the quantum factorial: [n choose k]_q [k]_q! [n - k]_q! = [n]_q! for k ≤ n. This holds for every parameter q, including those at which quantum factorials vanish.

theorem TauCeti.quantumBinomial_eq_div {K : Type u_1} [Field K] {q : K} {n k : ℕ} (hn : quantumFactorial q n ≠ 0) (hk : k ≤ n) : quantumBinomial q n k = quantumFactorial q n / (quantumFactorial q k * quantumFactorial q (n - k))

When [n]_q! ≠ 0, the quantum binomial coefficient is the quotient of quantum factorials [n choose k]_q = [n]_q! / ([k]_q! [n - k]_q!) for k ≤ n.

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

The divided-power q-binomial theorem: if y x = q² x y and [n]_q! ≠ 0, then the divided power (x + y)^(n) = (x + y)^n / [n]_q! expands as ∑_k q^(k(n-k)) x^(k) y^(n-k), with x^(k) = x^k / [k]_q!.

The Laurent quantum factorial

noncomputable def TauCeti.laurentQuantumFactorial (n : ℕ) : LaurentPolynomial ℤ

The quantum factorial [n]_v! = [1]_v [2]_v ⋯ [n]_v of the Laurent quantum integers in ℤ[v, v⁻¹].

theorem TauCeti.laurentQuantumFactorial_def (n : ℕ) : laurentQuantumFactorial n = ∏ j ∈ Finset.range n, laurentQuantumInteger (↑j + 1)

The defining product formula for the Laurent quantum factorial.

@[simp]

theorem TauCeti.laurentQuantumFactorial_zero : laurentQuantumFactorial 0 = 1

[0]_v! = 1.

theorem TauCeti.laurentQuantumFactorial_succ (n : ℕ) : laurentQuantumFactorial (n + 1) = laurentQuantumFactorial n * laurentQuantumInteger (↑n + 1)

[n + 1]_v! = [n]_v! [n + 1]_v.

theorem TauCeti.laurentEval_laurentQuantumFactorial {K : Type u_1} [Field K] {u : Kˣ} (hu : ↑u - (↑u)⁻¹ ≠ 0) (n : ℕ) : (laurentEval u) (laurentQuantumFactorial n) = quantumFactorial (↑u) n

At a unit q of a field with q - q⁻¹ ≠ 0, the Laurent quantum factorial [n]_v! takes the value [n]_q!.

@[simp]

theorem TauCeti.laurentEval_one_laurentQuantumFactorial {A : Type u_1} [CommRing A] (n : ℕ) : (laurentEval 1) (laurentQuantumFactorial n) = ↑n.factorial

At v = 1 the Laurent quantum factorial [n]_v! is the factorial n!.

theorem TauCeti.laurentQuantumFactorial_ne_zero (n : ℕ) : laurentQuantumFactorial n ≠ 0

The Laurent quantum factorial [n]_v! is nonzero, since its value at v = 1 is n!.