Quantum integers as Laurent polynomials

The symmetric quantum integer [r]_q = (q^r - q^(-r)) / (q - q⁻¹) of TauCeti/QuantumGroups/QuantumInteger/Basic.lean is the value at v = q of a Laurent polynomial with integer coefficients,

[n]_v = v^(n-1) + v^(n-3) + ⋯ + v^(1-n) for n ≥ 0, and [-n]_v = -[n]_v.

This file defines that Laurent polynomial TauCeti.laurentQuantumInteger r in ℤ[v, v⁻¹] as S_(r-1)(v + v⁻¹), where S is Mathlib's rescaled Chebyshev polynomial of the second kind Polynomial.Chebyshev.S. It is characterized, without a denominator, by (v - v⁻¹) [r]_v = v^r - v^(-r). Evaluating it at a unit q of a field with q - q⁻¹ ≠ 0 gives the field quantum integer [r]_q, while evaluating it at v = 1, where the quotient formula degenerates, gives the ordinary integer r. Writing matrix coefficients with these Laurent polynomials therefore describes a family of representations at a generic parameter and its classical specialization at v = 1 at the same time.

Main definitions

• TauCeti.laurentQuantumInteger r: the quantum integer [r]_v in ℤ[v, v⁻¹].

Main results

• TauCeti.laurentQuantumInteger_neg: [-r]_v = -[r]_v.
• TauCeti.T_sub_T_neg_mul_laurentQuantumInteger: (v - v⁻¹) [r]_v = v^r - v^(-r).
• TauCeti.laurentEval_laurentQuantumInteger: the value at a unit q of a field with q - q⁻¹ ≠ 0 is the quantum integer [r]_q.
• TauCeti.laurentEval_one_laurentQuantumInteger: the value at v = 1 is r.
• TauCeti.laurentQuantumInteger_add: the addition formula [a + b]_v = v^a [b]_v + v^(-b) [a]_v.
• TauCeti.qInt_add_inv_eq_laurentEval: the value of [n]_v at a unit u of a commutative ring is the quantum integer TauCeti.qInt at the loop parameter u + u⁻¹.
• TauCeti.sub_inv_mul_qInt_add_inv: (u - u⁻¹) [n] = uⁿ - u⁻ⁿ at δ = u + u⁻¹.
• TauCeti.qInt_add_inv_eq_quantumInteger: at q in a field with q - q⁻¹ ≠ 0, the quantum integer at δ = q + q⁻¹ is the field quantum integer TauCeti.quantumInteger q n.

References

• J. C. Jantzen, Lectures on Quantum Groups, Graduate Studies in Mathematics 6, Chapter 0, for the symmetric quantum integers as Laurent polynomials.

noncomputable def TauCeti.laurentQuantumInteger (r : ℤ) : LaurentPolynomial ℤ

The symmetric quantum integer [r]_v as a Laurent polynomial with integer coefficients, [r]_v = S_(r-1)(v + v⁻¹) for the rescaled Chebyshev polynomial S of the second kind. Thus [n]_v = v^(n-1) + v^(n-3) + ⋯ + v^(1-n) for n ≥ 0, and [-n]_v = -[n]_v.

@[simp]

theorem TauCeti.laurentQuantumInteger_zero : laurentQuantumInteger 0 = 0

[0]_v = 0.

@[simp]

theorem TauCeti.laurentQuantumInteger_one : laurentQuantumInteger 1 = 1

[1]_v = 1.

@[simp]

theorem TauCeti.laurentQuantumInteger_neg (r : ℤ) : laurentQuantumInteger (-r) = -laurentQuantumInteger r

Negating the index negates the quantum integer: [-r]_v = -[r]_v.

theorem TauCeti.T_sub_T_neg_mul_laurentQuantumInteger (r : ℤ) : (LaurentPolynomial.T 1 - LaurentPolynomial.T (-1)) * laurentQuantumInteger r = LaurentPolynomial.T r - LaurentPolynomial.T (-r)

The quantum integer [r]_v is characterized by (v - v⁻¹) [r]_v = v^r - v^(-r).

@[simp]

theorem TauCeti.laurentEval_one_laurentQuantumInteger {A : Type u_1} [Ring A] (r : ℤ) : (laurentEval 1) (laurentQuantumInteger r) = ↑r

At v = 1 the quantum integer [r]_v is the integer r.

theorem TauCeti.sub_inv_mul_laurentEval_laurentQuantumInteger {S : Type u_1} [Ring S] (u : Sˣ) (r : ℤ) : (↑u - ↑u⁻¹) * (laurentEval u) (laurentQuantumInteger r) = ↑(u ^ r) - ↑(u ^ (-r))

The value of [r]_v at a unit q of a ring satisfies (q - q⁻¹) [r]_q = q^r - q^(-r).

theorem TauCeti.laurentEval_laurentQuantumInteger {K : Type u_1} [Field K] {u : Kˣ} (hu : ↑u - (↑u)⁻¹ ≠ 0) (r : ℤ) : (laurentEval u) (laurentQuantumInteger r) = quantumInteger (↑u) r

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

theorem TauCeti.qInt_add_inv_eq_laurentEval {R : Type u_1} [CommRing R] (u : Rˣ) (n : ℕ) : qInt R (↑u + ↑u⁻¹) n = (laurentEval u) (laurentQuantumInteger ↑n)

At δ = u + u⁻¹ for a unit u, the quantum integer [n] is the value at u of the Laurent quantum integer [n]_v.

theorem TauCeti.sub_inv_mul_qInt_add_inv {R : Type u_1} [CommRing R] (u : Rˣ) (n : ℕ) : (↑u - ↑u⁻¹) * qInt R (↑u + ↑u⁻¹) n = ↑u ^ n - ↑u⁻¹ ^ n

The q-side characterization of the quantum integers: at δ = u + u⁻¹ for a unit u, (u - u⁻¹) [n] = uⁿ - u⁻ⁿ.

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

At a parameter q of a field with q - q⁻¹ ≠ 0, the quantum integer at δ = q + q⁻¹ is the field quantum integer [n]_q = (qⁿ - q⁻ⁿ) / (q - q⁻¹).

theorem TauCeti.laurentQuantumInteger_add (a b : ℤ) : laurentQuantumInteger (a + b) = LaurentPolynomial.T a * laurentQuantumInteger b + LaurentPolynomial.T (-b) * laurentQuantumInteger a

The addition formula [a + b]_v = v^a [b]_v + v^(-b) [a]_v.