Quantum integers at a loop parameter

For an element δ of a commutative ring, the quantum integers [n] at δ are defined by [0] = 0, [1] = 1 and [n + 2] = δ [n + 1] - [n]. When δ = q + q⁻¹ for a unit q they are the symmetric quantum integers [n] = q^(n-1) + q^(n-3) + ⋯ + q^(1-n), but no q is needed to define them: [n] is the value at δ of the rescaled Chebyshev polynomial of the second kind S_(n-1), Mathlib's Polynomial.Chebyshev.S at the integer index n - 1. This is the form in which they enter diagrammatic algebra, where δ is the value of a closed loop: the Jones–Wenzl recursions, the trace of the Jones–Wenzl projections and the Gram determinants of Temperley–Lieb cell modules are all expressed through [n] at the loop value δ.

This file defines TauCeti.qInt R δ n as that Chebyshev evaluation, absorbing the shift of the index by one, and transfers the polynomial identities of TauCeti/RingTheory/Polynomial/Chebyshev/Divisibility.lean to it. Note that [0] = 0 for every δ, so nonvanishing hypotheses on quantum integers concern the indices n ≥ 1 only.

Since Mathlib's polynomials are noncomputable, so is qInt; the evaluator TauCeti.qIntAux computes the same values from the three-term recurrence.

Main definitions

• TauCeti.qInt R δ n: the quantum integer [n] at the loop parameter δ.
• TauCeti.qIntAux δ n: a computable evaluator, equal to qInt R δ n by qIntAux_eq_qInt.

Main results

• TauCeti.qInt_add_two: the recurrence [n + 2] = δ [n + 1] - [n].
• TauCeti.qInt_add_two_mul_inverse: the recurrence divided by a unit [n + 1], the scalar identity behind the Jones–Wenzl recursion.
• TauCeti.qInt_add_add_one: [m + n + 1] = [m + 1] [n + 1] - [m] [n].
• TauCeti.qInt_mul: [mn] at δ is [m] at δ times [n] at Cₘ(δ), where Cₘ is the rescaled Chebyshev polynomial of the first kind, so that Cₘ(q + q⁻¹) = qᵐ + q⁻ᵐ.
• TauCeti.qInt_dvd_qInt: [m] ∣ [n] whenever m ∣ n.
• TauCeti.qInt_two_left, TauCeti.qInt_neg_two_left: at δ = 2 and δ = -2, [n] is n and (-1)^(n+1) n; in characteristic zero these never vanish for n ≥ 1, while in characteristic p they vanish at n = p.
• RingHom.map_qInt: quantum integers commute with ring homomorphisms.
• IsSelfAdjoint.qInt: the quantum integers at a self-adjoint loop parameter are self-adjoint.

References

• L. H. Kauffman and S. L. Lins, Temperley–Lieb Recoupling Theory and Invariants of 3-Manifolds, Annals of Mathematics Studies 134, Princeton University Press, 1994, for the quantum integers as functions of the loop value.

noncomputable def TauCeti.qInt (R : Type u_1) [CommRing R] (δ : R) (n : ℕ) : R

The quantum integer [n] at the loop parameter δ: the value at δ of the rescaled Chebyshev polynomial of the second kind S_(n-1), with the index taken in ℤ so that [0] = S_(-1)(δ) = 0. It satisfies [1] = 1, [2] = δ and [n + 2] = δ [n + 1] - [n] (TauCeti.qInt_add_two), and for a unit q with δ = q + q⁻¹ it is q^(n-1) + q^(n-3) + ⋯ + q^(1-n).

theorem TauCeti.qInt_def {R : Type u_1} [CommRing R] (δ : R) (n : ℕ) : qInt R δ n = Polynomial.eval δ (Polynomial.Chebyshev.S R (↑n - 1))

Unfolding TauCeti.qInt as the value at δ of the Chebyshev polynomial S_(n-1).

@[simp]

theorem TauCeti.qInt_zero {R : Type u_1} [CommRing R] (δ : R) : qInt R δ 0 = 0

[0] = 0 at every loop parameter.

@[simp]

theorem TauCeti.qInt_one {R : Type u_1} [CommRing R] (δ : R) : qInt R δ 1 = 1

[1] = 1 at every loop parameter.

@[simp]

theorem TauCeti.qInt_two {R : Type u_1} [CommRing R] (δ : R) : qInt R δ 2 = δ

[2] = δ.

theorem TauCeti.qInt_add_two {R : Type u_1} [CommRing R] (δ : R) (n : ℕ) : qInt R δ (n + 2) = δ * qInt R δ (n + 1) - qInt R δ n

The defining recurrence of the quantum integers: [n + 2] = δ [n + 1] - [n].

theorem TauCeti.qInt_add_two_mul_inverse {R : Type u_1} [CommRing R] (δ : R) (n : ℕ) (h : IsUnit (qInt R δ (n + 1))) : qInt R δ (n + 2) * Ring.inverse (qInt R δ (n + 1)) = δ - qInt R δ n * Ring.inverse (qInt R δ (n + 1))

The recurrence divided by [n + 1]: [n + 2] / [n + 1] = δ - [n] / [n + 1] when [n + 1] is a unit, with division Ring.inverse.

theorem TauCeti.qInt_add_add_one {R : Type u_1} [CommRing R] (δ : R) (m n : ℕ) : qInt R δ (m + n + 1) = qInt R δ (m + 1) * qInt R δ (n + 1) - qInt R δ m * qInt R δ n

The addition formula for quantum integers: [m + n + 1] = [m + 1] [n + 1] - [m] [n].

theorem TauCeti.qInt_mul {R : Type u_1} [CommRing R] (δ : R) (m n : ℕ) : qInt R δ (m * n) = qInt R δ m * qInt R (Polynomial.eval δ (Polynomial.Chebyshev.C R ↑m)) n

The multiplication formula for quantum integers: [mn] at δ is [m] at δ times [n] at Cₘ(δ), where Cₘ is the rescaled Chebyshev polynomial of the first kind. For a unit q with δ = q + q⁻¹ this is [mn]_q = [m]_q [n]_{qᵐ}, since Cₘ(q + q⁻¹) = qᵐ + q⁻ᵐ.

theorem TauCeti.qInt_dvd_qInt {R : Type u_1} [CommRing R] (δ : R) {m n : ℕ} (h : m ∣ n) : qInt R δ m ∣ qInt R δ n

Divisibility of quantum integers: [m] ∣ [n] whenever m ∣ n.

@[simp]

theorem TauCeti.qInt_two_left {R : Type u_1} [CommRing R] (n : ℕ) : qInt R 2 n = ↑n

At the loop parameter δ = 2 the quantum integer [n] is the integer n.

@[simp]

theorem TauCeti.qInt_neg_two_left {R : Type u_1} [CommRing R] (n : ℕ) : qInt R (-2) n = (-1) ^ (n + 1) * ↑n

At the loop parameter δ = -2 the quantum integer [n] is (-1)^(n+1) n.

@[simp]

theorem RingHom.map_qInt {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] (f : R →+* R') (δ : R) (n : ℕ) : f (TauCeti.qInt R δ n) = TauCeti.qInt R' (f δ) n

Quantum integers commute with ring homomorphisms: f [n]_δ = [n]_{f δ}.

theorem IsSelfAdjoint.qInt {R : Type u_1} [CommRing R] [StarRing R] {δ : R} (hδ : IsSelfAdjoint δ) (n : ℕ) : IsSelfAdjoint (TauCeti.qInt R δ n)

The quantum integers at a self-adjoint loop parameter are self-adjoint.

A computable evaluator

def TauCeti.qIntAux {R : Type u_1} [CommRing R] (δ : R) (n : ℕ) : R

A computable evaluator for the quantum integers: qIntAux δ n iterates ([k], [k + 1]) ↦ ([k + 1], δ [k + 1] - [k]) starting from ([0], [1]) = (0, 1), and so agrees with the noncomputable qInt R δ n (qIntAux_eq_qInt). The body is exposed so that values can be computed by evaluation or by decide in other modules.

@[simp]

theorem TauCeti.qIntAux_eq_qInt {R : Type u_1} [CommRing R] (δ : R) (n : ℕ) : qIntAux δ n = qInt R δ n

The computable evaluator qIntAux computes the quantum integers.