Quantum integers

This file develops the symmetric quantum integers associated to a generic nonzero parameter in a field. Besides the quotient definition, it provides a denominator-free Laurent sum, the sign and three-term recurrence identities, and the nonvanishing result needed for the ladder coefficients of generic rank-one quantum-group representations.

def TauCeti.IsGenericQuantumParameter {K : Type u_1} [Field K] (q : K) : Prop

An element of a field is a generic quantum parameter if it is nonzero and none of its positive natural powers is one.

theorem TauCeti.isGenericQuantumParameter_iff {K : Type u_1} [Field K] {q : K} : IsGenericQuantumParameter q ↔ q ≠ 0 ∧ ∀ (n : ℕ), 0 < n → q ^ n ≠ 1

Characterization of generic quantum parameters: nonzero, with no positive natural power equal to one.

theorem TauCeti.IsGenericQuantumParameter.ne_zero {K : Type u_1} [Field K] {q : K} (hq : IsGenericQuantumParameter q) : q ≠ 0

A generic quantum parameter is nonzero.

theorem TauCeti.IsGenericQuantumParameter.pow_ne_one {K : Type u_1} [Field K] {q : K} (hq : IsGenericQuantumParameter q) {n : ℕ} (hn : 0 < n) : q ^ n ≠ 1

No positive natural power of a generic quantum parameter is one.

theorem TauCeti.IsGenericQuantumParameter.pow_injective {K : Type u_1} [Field K] {q : K} (hq : IsGenericQuantumParameter q) : Function.Injective fun (x : ℕ) => q ^ x

The natural powers of a generic quantum parameter are pairwise distinct.

theorem TauCeti.IsGenericQuantumParameter.zpow_injective {K : Type u_1} [Field K] {q : K} (hq : IsGenericQuantumParameter q) : Function.Injective fun (x : ℤ) => q ^ x

The integer powers of a generic quantum parameter are pairwise distinct.

theorem TauCeti.IsGenericQuantumParameter.eq_one_of_units_mul_zpow_eq_zpow {K : Type u_1} [Field K] [NeZero 2] {q : K} (hq : IsGenericQuantumParameter q) {ε : ℤˣ} {m n : ℤ} (h : ↑↑ε * q ^ m = q ^ n) : ε = 1

At a generic parameter in a field of characteristic not two, a signed power ε q ^ m is an integral power of q only for the positive sign.

theorem TauCeti.IsGenericQuantumParameter.units_mul_zpow_inj {K : Type u_1} [Field K] [NeZero 2] {q : K} (hq : IsGenericQuantumParameter q) {ε δ : ℤˣ} {m n : ℤ} : ↑↑ε * q ^ m = ↑↑δ * q ^ n ↔ ε = δ ∧ m = n

At a generic parameter in a field of characteristic not two, a signed power ε q ^ m determines both the sign ε and the exponent m.

theorem TauCeti.IsGenericQuantumParameter.ne_inv {K : Type u_1} [Field K] {q : K} (hq : IsGenericQuantumParameter q) : q ≠ q⁻¹

A generic quantum parameter is not equal to its inverse.

theorem TauCeti.IsGenericQuantumParameter.sub_inv_ne_zero {K : Type u_1} [Field K] {q : K} (hq : IsGenericQuantumParameter q) : q - q⁻¹ ≠ 0

The denominator in the symmetric quantum-integer formula is nonzero at a generic parameter.

theorem TauCeti.IsGenericQuantumParameter.inv {K : Type u_1} [Field K] {q : K} (hq : IsGenericQuantumParameter q) : IsGenericQuantumParameter q⁻¹

The inverse of a generic quantum parameter is generic.

theorem TauCeti.IsGenericQuantumParameter.pow {K : Type u_1} [Field K] {q : K} (hq : IsGenericQuantumParameter q) {k : ℕ} (hk : 0 < k) : IsGenericQuantumParameter (q ^ k)

A positive natural power of a generic quantum parameter is generic.

theorem TauCeti.IsGenericQuantumParameter.pow_mul_injective {K : Type u_1} [Field K] {q c : K} (hq : IsGenericQuantumParameter q) (hc : c ≠ 0) : Function.Injective fun (n : ℕ) => q ^ n * c

For nonzero c, the multiples q ^ n * c of a generic quantum parameter q are pairwise distinct.

theorem TauCeti.ne_zero_of_sub_inv_ne_zero {K : Type u_1} [Field K] {q : K} (hq : q - q⁻¹ ≠ 0) : q ≠ 0

If q - q⁻¹ is nonzero, then so is q.

noncomputable def TauCeti.quantumInteger {K : Type u_1} [Field K] (q : K) (r : ℤ) : K

The symmetric quantum integer [r]_q = (q^r - q⁻ʳ) / (q - q⁻¹).

theorem TauCeti.quantumInteger_def {K : Type u_1} [Field K] (q : K) (r : ℤ) : quantumInteger q r = (q ^ r - q ^ (-r)) / (q - q⁻¹)

The defining quotient formula for the symmetric quantum integer.

theorem TauCeti.sub_inv_mul_quantumInteger_natCast {K : Type u_1} [Field K] (q : K) (n : ℕ) : (q - q⁻¹) * quantumInteger q ↑n = q ^ n - q⁻¹ ^ n

(q - q⁻¹) [n]_q = q^n - q^(-n) for natural n.

@[simp]

theorem TauCeti.quantumInteger_zero {K : Type u_1} [Field K] (q : K) : quantumInteger q 0 = 0

The zeroth quantum integer is zero.

@[simp]

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

The first quantum integer is one whenever its defining denominator is nonzero.

@[simp]

theorem TauCeti.quantumInteger_neg {K : Type u_1} [Field K] (q : K) (r : ℤ) : quantumInteger q (-r) = -quantumInteger q r

Negating the index negates the quantum integer.

@[simp]

theorem TauCeti.quantumInteger_inv {K : Type u_1} [Field K] (q : K) (r : ℤ) : quantumInteger q⁻¹ r = quantumInteger q r

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

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

The first-order recurrence used to obtain the Laurent expansion of positive quantum integers.

theorem TauCeti.quantumInteger_natCast_eq_sum {K : Type u_1} [Field K] {q : K} (hq : q - q⁻¹ ≠ 0) (n : ℕ) : quantumInteger q ↑n = ∑ j ∈ Finset.range n, q ^ (2 * ↑j + 1 - ↑n)

For a positive index, the quantum integer is a Laurent polynomial with coefficients one: [n]_q = q^(1-n) + q^(3-n) + ⋯ + q^(n-1).

theorem TauCeti.quantumInteger_add_one {K : Type u_1} [Field K] (q : K) (r : ℤ) : quantumInteger q (r + 1) = (q + q⁻¹) * quantumInteger q r - quantumInteger q (r - 1)

The symmetric quantum integers satisfy the usual three-term recurrence.

theorem TauCeti.quantumInteger_add {K : Type u_1} [Field K] (q : K) (a b : ℤ) : quantumInteger q (a + b) = q ^ a * quantumInteger q b + q ^ (-b) * quantumInteger q a

The addition formula [a + b]_q = q^a [b]_q + q^(-b) [a]_q.

theorem TauCeti.quantumInteger_sub {K : Type u_1} [Field K] (q : K) (a b : ℤ) : quantumInteger q (a - b) = quantumInteger q a * quantumInteger q (b + 1) - quantumInteger q (a + 1) * quantumInteger q b

The difference of two quantum integers as a determinant of neighbouring quantum integers: [a - b]_q = [a]_q [b + 1]_q - [a + 1]_q [b]_q.

theorem TauCeti.quantumInteger_ne_zero {K : Type u_1} [Field K] {q : K} (hq : IsGenericQuantumParameter q) {r : ℤ} (hr : r ≠ 0) : quantumInteger q r ≠ 0

Every nonzero-index quantum integer is nonzero at a generic parameter.

theorem TauCeti.quantumInteger_eq_zero_iff {K : Type u_1} [Field K] {q : K} (hq : q ≠ 0) (r : ℤ) : quantumInteger q r = 0 ↔ q ^ (2 * r) = 1

For q ≠ 0, the quantum integer [r]_q vanishes exactly when q^(2r) = 1. When q - q⁻¹ = 0, that is q = ±1, both sides hold: [r]_q = 0 by the field convention.

@[simp]

theorem RingHom.map_quantumInteger {K : Type u_1} {L : Type u_2} [Field K] [Field L] (φ : K →+* L) (q : K) (r : ℤ) : φ (TauCeti.quantumInteger q r) = TauCeti.quantumInteger (φ q) r

Ring homomorphisms between fields commute with the quantum integers.