Commuting powers in U_q(sl₂)

This file gives the closed formula for commuting the raising generator E past a power of the lowering generator F. It is the calculation that detects the highest weight of a finite lowering string, and is also used in the finite-dimensional complete-reducibility argument. We also record a parameter-free form, valid even at q = ±1, that only remembers that the correction term is F ^ n times a combination of K and K⁻¹.

The convention follows A. Virelizier, Quantum groups, Section 2.4.

theorem TauCeti.UqSl2.k_mul_f_pow {q : ℂ} (r : ℕ) : k q * f q ^ r = (q⁻¹ ^ 2) ^ r • (f q ^ r * k q)

Commuting K past a natural power of F.

theorem TauCeti.UqSl2.kInv_mul_f_pow {q : ℂ} (r : ℕ) : kInv q * f q ^ r = (q ^ 2) ^ r • (f q ^ r * kInv q)

Commuting K⁻¹ past a natural power of F.

theorem TauCeti.UqSl2.e_mul_f_pow {q : ℂ} (hq : q - q⁻¹ ≠ 0) (r : ℕ) : e q * f q ^ r = f q ^ r * e q + (quantumInteger q ↑r * (q - q⁻¹)⁻¹) • (f q ^ (r - 1) * (q⁻¹ ^ (r - 1) • k q - q ^ (r - 1) • kInv q))

The commutator formula for E and a natural power of F: E F^r = F^r E + [r]_q F^(r-1) (q^(1-r) K - q^(r-1) K⁻¹) / (q-q⁻¹).

theorem TauCeti.UqSl2.exists_e_mul_f_pow_succ {q : ℂ} (n : ℕ) : ∃ (α : ℂ) (β : ℂ), e q * f q ^ (n + 1) = f q ^ (n + 1) * e q + f q ^ n * (α • k q + β • kInv q)

Commuting E past a positive power of F leaves a correction F ^ n (α K + β K⁻¹). Unlike e_mul_f_pow, this holds for every q, including q = ±1.