Documentation

TauCeti.QuantumGroups.UqSl2.LadderModule.Schur

Schur scalars for signed ladder modules #

At a generic parameter q, the signed ladder modules L_m^ε of U_q(sl₂) are simple, pairwise non-isomorphic for distinct (m, ε), and have one-dimensional endomorphism algebras over ℂ. This file packages Schur's lemma into a uniform scalar extraction LadderModule.schurScalar on arbitrary UqSl2 q-linear maps L_m^ε →ₗ[UqSl2 q] L_n^δ as the v₀-coordinate of f v₀.

Every intertwiner f : L_m^ε →ₗ[UqSl2 q] L_n^δ satisfies f (vec q m ε j) = schurScalar f • vec q n δ j for every j : ℤ (apply_vec_eq_schurScalar_smul), so schurScalar is multiplicative under composition (schurScalar_comp) and agrees on endomorphisms with TauCeti.endAlgEquivSelfOfIsSimpleModule (endAlgEquivSelfOfIsSimpleModule_eq_schurScalar).

References #

source
theorem TauCeti.UqSl2.LadderModule.hom_eq_zero_of_ne {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (h : m ≠ n ∨ ε ≠ δ) (f : LadderModule q m ε →ₗ[UqSl2 q] LadderModule q n δ) :
f = 0

At a generic parameter, any UqSl2 q-linear map between signed ladder modules with different highest weights or signs vanishes.

source
noncomputable def TauCeti.UqSl2.LadderModule.schurScalar {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (f : LadderModule q m ε →ₗ[UqSl2 q] LadderModule q n δ) :
ℂ

The scalar attached to a UqSl2 q-linear map L_m^ε → L_n^δ, extracted as the v₀ coordinate of the image of v₀.

Instances For
    source
    @[simp]
    theorem TauCeti.UqSl2.LadderModule.schurScalar_zero {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} :
    schurScalar 0 = 0

    The zero intertwiner has Schur scalar zero.

    source
    @[simp]
    theorem TauCeti.UqSl2.LadderModule.schurScalar_add {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (f g : LadderModule q m ε →ₗ[UqSl2 q] LadderModule q n δ) :
    schurScalar (f + g) = schurScalar f + schurScalar g

    schurScalar is additive.

    source
    @[simp]
    theorem TauCeti.UqSl2.LadderModule.schurScalar_neg {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (f : LadderModule q m ε →ₗ[UqSl2 q] LadderModule q n δ) :
    schurScalar (-f) = -schurScalar f

    schurScalar commutes with negation.

    source
    @[simp]
    theorem TauCeti.UqSl2.LadderModule.schurScalar_sub {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (f g : LadderModule q m ε →ₗ[UqSl2 q] LadderModule q n δ) :
    schurScalar (f - g) = schurScalar f - schurScalar g

    schurScalar commutes with subtraction.

    source
    @[simp]
    theorem TauCeti.UqSl2.LadderModule.schurScalar_smul {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (c : ℂ) (f : LadderModule q m ε →ₗ[UqSl2 q] LadderModule q n δ) :
    schurScalar (c • f) = c * schurScalar f

    schurScalar is ℂ-linear.

    source
    theorem TauCeti.UqSl2.LadderModule.schurScalar_sum {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} {ι : Type u_1} (s : Finset ι) (f : ι → LadderModule q m ε →ₗ[UqSl2 q] LadderModule q n δ) :
    schurScalar (∑ i ∈ s, f i) = ∑ i ∈ s, schurScalar (f i)

    schurScalar commutes with finite sums.

    source
    theorem TauCeti.UqSl2.LadderModule.schurScalar_eq_of_apply_vec_zero {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} {f : LadderModule q m ε →ₗ[UqSl2 q] LadderModule q n δ} {c : ℂ} (hf : f (vec q m ε 0) = c • vec q n δ 0) :
    schurScalar f = c

    If f sends v₀ to c • v₀, then schurScalar f = c.

    source
    @[simp]
    theorem TauCeti.UqSl2.LadderModule.schurScalar_id {q : ℂ} [Fact (q ≠ 0)] {m : ℕ} {ε : ℤˣ} :
    schurScalar LinearMap.id = 1

    The identity endomorphism has Schur scalar 1.

    source
    @[simp]
    theorem TauCeti.UqSl2.LadderModule.endAlgEquivSelfOfIsSimpleModule_eq_schurScalar {q : ℂ} [Fact (q ≠ 0)] {m : ℕ} {ε : ℤˣ} [IsSimpleModule (UqSl2 q) (LadderModule q m ε)] (f : Module.End (UqSl2 q) (LadderModule q m ε)) :
    endAlgEquivSelfOfIsSimpleModule f = schurScalar f

    On a simple signed ladder module, TauCeti.endAlgEquivSelfOfIsSimpleModule evaluates to schurScalar.

    source
    theorem TauCeti.UqSl2.LadderModule.apply_eq_schurScalar_smul {q : ℂ} [Fact (q ≠ 0)] {m : ℕ} {ε : ℤˣ} (hq : IsGenericQuantumParameter q) (f : Module.End (UqSl2 q) (LadderModule q m ε)) (x : LadderModule q m ε) :
    f x = schurScalar f • x

    At a generic parameter, every UqSl2 q-endomorphism of L_m^ε acts as scalar multiplication by its schurScalar.

    source
    theorem TauCeti.UqSl2.LadderModule.schurScalar_eq_zero_of_ne {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (h : m ≠ n ∨ ε ≠ δ) (f : LadderModule q m ε →ₗ[UqSl2 q] LadderModule q n δ) :
    schurScalar f = 0

    At a generic parameter, schurScalar vanishes between inequivalent signed ladder modules.

    source
    theorem TauCeti.UqSl2.LadderModule.apply_vec_eq_schurScalar_smul {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (f : LadderModule q m ε →ₗ[UqSl2 q] LadderModule q n δ) (j : ℤ) :
    f (vec q m ε j) = schurScalar f • vec q n δ j

    At a generic parameter, any UqSl2 q-linear map L_m^ε → L_n^δ sends every ladder vector v_j to schurScalar f • v_j.

    source
    @[simp]
    theorem TauCeti.UqSl2.LadderModule.schurScalar_comp {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) {p : ℕ} {ζ : ℤˣ} (g : LadderModule q n δ →ₗ[UqSl2 q] LadderModule q p ζ) (f : LadderModule q m ε →ₗ[UqSl2 q] LadderModule q n δ) :
    schurScalar (g ∘ₗ f) = schurScalar g * schurScalar f

    schurScalar is multiplicative under composition of UqSl2 q-linear maps between arbitrary signed ladder modules.