Documentation

TauCeti.QuantumGroups.UqSl2.PBW

A PBW basis of U_q(sl₂) #

For a nonzero parameter q, the monomials

F ^ a * K ^ b * E ^ c, with a c : ℕ and b : ℤ,

form a complex basis of UqSl2 q. The construction transports the nested left-monomial bases of the iterated Ore presentation. Those bases initially put the Laurent monomial first, in the order K ^ b * F ^ a * E ^ c; commuting F ^ a past K ^ b gives the displayed normalization. Thus the coordinates supplied by pbwBasis.repr are the unique PBW coefficients of an element.

The second half of the file reads off how the generators act on PBW coordinates, which is the input to leading-coefficient arguments such as the computation of the center.

The basis and its normalization follow C. Kassel, Quantum Groups, Graduate Texts in Mathematics 155, Section VI.1.

source
theorem TauCeti.UqSl2.f_mul_kUnit_zpow (q : ℂ) [Fact (q ≠ 0)] (b : ℤ) :
f q * ↑(kUnit q ^ b) = q ^ (2 * b) • (↑(kUnit q ^ b) * f q)

Moving F past an arbitrary integer power of K multiplies by q ^ (2b).

source
theorem TauCeti.UqSl2.f_pow_mul_kUnit_zpow (q : ℂ) [Fact (q ≠ 0)] (a : ℕ) (b : ℤ) :
f q ^ a * ↑(kUnit q ^ b) = q ^ (2 * b * ↑a) • (↑(kUnit q ^ b) * f q ^ a)

Moving a natural power of F past an integer power of K.

source
noncomputable def TauCeti.UqSl2.pbwBasis (q : ℂ) [Fact (q ≠ 0)] :
Module.Basis (ℕ × ℤ × ℕ) ℂ (UqSl2 q)

The Poincaré--Birkhoff--Witt basis of UqSl2 q, indexed by the exponents (a, b, c) of the ordered monomial F ^ a * K ^ b * E ^ c.

Instances For
    source
    @[simp]
    theorem TauCeti.UqSl2.pbwBasis_apply (q : ℂ) [Fact (q ≠ 0)] (a : ℕ) (b : ℤ) (c : ℕ) :
    (pbwBasis q) (a, b, c) = f q ^ a * ↑(kUnit q ^ b) * e q ^ c

    A vector of the PBW basis is the corresponding ordered monomial.

    Commuting with K #

    source
    theorem TauCeti.UqSl2.pbwBasis_repr_eq_zero_of_commute_k {q : ℂ} [Fact (q ≠ 0)] (hq : IsGenericQuantumParameter q) {z : UqSl2 q} (hz : Commute (k q) z) {a : ℕ} {b : ℤ} {c : ℕ} (hac : a ≠ c) :
    ((pbwBasis q).repr z) (a, b, c) = 0

    Weight-zero reduction. At a generic parameter, an element commuting with K has no PBW monomial F ^ a * K ^ b * E ^ c with a ≠ c.

    Raising the E-exponent #

    source
    theorem TauCeti.UqSl2.e_mul_pbwBasis_sub_mem {q : ℂ} [Fact (q ≠ 0)] (a : ℕ) (b : ℤ) (c : ℕ) :
    e q * (pbwBasis q) (a, b, c) - q ^ (-2 * b) • (pbwBasis q) (a, b, c + 1) ∈ Submodule.span ℂ (⇑(pbwBasis q) '' {i : ℕ × ℤ × ℕ | i.2.2 = c})

    Left multiplication by E raises the E-exponent of a PBW monomial by one, with leading coefficient q ^ (-2b), up to monomials with the same E-exponent.

    source
    theorem TauCeti.UqSl2.f_mul_pbwBasis {q : ℂ} [Fact (q ≠ 0)] (a : ℕ) (b : ℤ) (c : ℕ) :
    f q * (pbwBasis q) (a, b, c) = (pbwBasis q) (a + 1, b, c)

    Left multiplication by F raises the F-exponent of a PBW monomial by one.

    source
    theorem TauCeti.UqSl2.k_mul_pbwBasis {q : ℂ} [Fact (q ≠ 0)] (a : ℕ) (b : ℤ) (c : ℕ) :
    k q * (pbwBasis q) (a, b, c) = (q⁻¹ ^ 2) ^ a • (pbwBasis q) (a, b + 1, c)

    Left multiplication by K raises the K-exponent of a PBW monomial by one, with coefficient q ^ (-2a).

    source
    theorem TauCeti.UqSl2.kInv_mul_pbwBasis {q : ℂ} [Fact (q ≠ 0)] (a : ℕ) (b : ℤ) (c : ℕ) :
    kInv q * (pbwBasis q) (a, b, c) = (q ^ 2) ^ a • (pbwBasis q) (a, b - 1, c)

    Left multiplication by K⁻¹ lowers the K-exponent of a PBW monomial by one, with coefficient q ^ (2a).

    source
    theorem TauCeti.UqSl2.f_mul_mem_span_pbwBasis {q : ℂ} [Fact (q ≠ 0)] {c : ℕ} {x : UqSl2 q} (hx : x ∈ Submodule.span ℂ (⇑(pbwBasis q) '' {i : ℕ × ℤ × ℕ | i.2.2 = c})) :
    f q * x ∈ Submodule.span ℂ (⇑(pbwBasis q) '' {i : ℕ × ℤ × ℕ | i.2.2 = c})

    Left multiplication by F preserves the span of the PBW monomials with a given E-exponent c.

    source
    theorem TauCeti.UqSl2.pbwBasis_repr_of_raise {q : ℂ} [Fact (q ≠ 0)] {ψ : UqSl2 q →ₗ[ℂ] UqSl2 q} {d : ℕ} {s : ℤ → ℂ} (hψ : ∀ (a : ℕ) (b : ℤ) (c : ℕ), ψ ((pbwBasis q) (a, b, c)) - s b • (pbwBasis q) (a + d, b, c + 1) ∈ Submodule.span ℂ (⇑(pbwBasis q) '' {i : ℕ × ℤ × ℕ | i.2.2 = c})) {x : UqSl2 q} {n : ℕ} (hx : ∀ i ∈ ((pbwBasis q).repr x).support, i.2.2 ≤ n) :
    (∀ i ∈ ((pbwBasis q).repr (ψ x)).support, i.2.2 ≤ n + 1) ∧ ∀ (a : ℕ) (b : ℤ), ((pbwBasis q).repr (ψ x)) (a + d, b, n + 1) = s b * ((pbwBasis q).repr x) (a, b, n)

    Let ψ be a linear endomorphism sending each PBW monomial F ^ a * K ^ b * E ^ c to s b • F ^ (a + d) * K ^ b * E ^ (c + 1) modulo monomials with E-exponent c. If the E-exponents of x are at most n, then those of ψ x are at most n + 1, and the coordinates of ψ x with E-exponent n + 1 are read off from those of x with E-exponent n.

    Commuting with E #

    source
    theorem TauCeti.UqSl2.pbwBasis_repr_eq_zero_of_commute_e {q : ℂ} [Fact (q ≠ 0)] (hq : IsGenericQuantumParameter q) {z : UqSl2 q} (hz : Commute (e q) z) {n : ℕ} (hn : ∀ i ∈ ((pbwBasis q).repr z).support, i.2.2 ≤ n) (a : ℕ) {b : ℤ} (hb : b ≠ 0) :
    ((pbwBasis q).repr z) (a, b, n) = 0

    At a generic parameter, an element commuting with E whose PBW monomials all have E-exponent at most n has no monomial F ^ a * K ^ b * E ^ n with b ≠ 0.