Documentation

TauCeti.QuantumGroups.UqSl2.Rescale

Rescaling automorphisms of U_q(sl₂) #

The assignments E ↦ t E, F ↦ t⁻¹ F, K ↦ K, K⁻¹ ↦ K⁻¹ preserve the rank-one presentation. They give a multiplicative family of algebra automorphisms UqSl2.rescale, parametrized by complex units. No restriction on q is needed.

These automorphisms record the freedom to normalize raising and lowering operators without changing the weight operator. On an ordered monomial F^a K^b E^c, the rescaling factor is t⁻ᵃ tᶜ; the integer power of K is unchanged.

For nonzero q, conjugation by K is the rescaling automorphism with parameter q², so conjugation by K ^ b multiplies E by q ^ (2b).

source
def TauCeti.UqSl2.rescale (q : ℂ) :
ℂˣ →* UqSl2 q ≃ₐ[ℂ] UqSl2 q

Rescale E by a complex unit and F by its inverse, fixing K and K⁻¹. Multiplication of parameters corresponds to composition of algebra automorphisms.

Instances For
    source
    @[simp]
    theorem TauCeti.UqSl2.rescale_e {q : ℂ} (t : ℂˣ) :
    ((rescale q) t) (e q) = ↑t • e q

    The rescaling automorphism multiplies the raising generator by its parameter.

    source
    @[simp]
    theorem TauCeti.UqSl2.rescale_f {q : ℂ} (t : ℂˣ) :
    ((rescale q) t) (f q) = ↑t⁻¹ • f q

    The rescaling automorphism multiplies the lowering generator by the inverse parameter.

    source
    @[simp]
    theorem TauCeti.UqSl2.rescale_k {q : ℂ} (t : ℂˣ) :
    ((rescale q) t) (k q) = k q

    Rescaling fixes the weight generator.

    source
    @[simp]
    theorem TauCeti.UqSl2.rescale_kInv {q : ℂ} (t : ℂˣ) :
    ((rescale q) t) (kInv q) = kInv q

    Rescaling fixes the inverse weight generator.

    source
    @[simp]
    theorem TauCeti.UqSl2.rescale_kUnit_zpow {q : ℂ} (t : ℂˣ) (b : ℤ) :
    ((rescale q) t) ↑(kUnit q ^ b) = ↑(kUnit q ^ b)

    Rescaling fixes every integer power of the distinguished weight unit.

    source
    theorem TauCeti.UqSl2.rescale_orderedMonomial {q : ℂ} (t : ℂˣ) (a c : ℕ) (b : ℤ) :
    ((rescale q) t) (f q ^ a * ↑(kUnit q ^ b) * e q ^ c) = (↑t⁻¹ ^ a * ↑t ^ c) • (f q ^ a * ↑(kUnit q ^ b) * e q ^ c)

    An ordered monomial has rescaling weight c - a, independently of its K exponent. This formula does not assume linear independence of the ordered monomials.

    source
    theorem TauCeti.UqSl2.toAlgEquiv_conjAct_kUnit {q : ℂ} [Fact (q ≠ 0)] :
    MulSemiringAction.toAlgEquiv ℂ (UqSl2 q) (ConjAct.toConjAct (kUnit q)) = (rescale q) (Units.mk0 q ⋯ ^ 2)

    Conjugation by K is the rescaling automorphism with parameter q².

    source
    theorem TauCeti.UqSl2.kUnit_zpow_mul_e_mul_inv {q : ℂ} [Fact (q ≠ 0)] (b : ℤ) :
    ↑(kUnit q ^ b) * e q * ↑(kUnit q ^ b)⁻¹ = q ^ (2 * b) • e q

    Conjugation by an integer power of K rescales E.

    source
    theorem TauCeti.UqSl2.e_mul_kUnit_zpow {q : ℂ} [Fact (q ≠ 0)] (b : ℤ) :
    e q * ↑(kUnit q ^ b) = q ^ (-2 * b) • (↑(kUnit q ^ b) * e q)

    Commuting E past an integer power of K multiplies by q ^ (-2b).