Tensor actions of the rank-one quantum group #
The generic bialgebra tensor product gives an action of UqSl2 q on the algebraic tensor
product of any two native modules. This file records the generator actions for the coproduct
ΔE = E ⊗ 1 + K ⊗ E, ΔF = F ⊗ K⁻¹ + 1 ⊗ F, and ΔK = K ⊗ K.
In particular, the two terms in the root-generator formulas retain their prescribed order.
No finite-dimensionality or generic-parameter hypothesis is needed beyond q ≠ 0.
The coproduct conventions follow A. Virelizier, Quantum groups, Sections 2.3--2.4.
@[simp]
theorem
TauCeti.UqSl2.e_smul_tmul
(q : ℂ)
[Fact (q ≠ 0)]
{M : Type u_1}
{N : Type u_2}
[AddCommMonoid M]
[Module ℂ M]
[Module (UqSl2 q) M]
[IsScalarTower ℂ (UqSl2 q) M]
[AddCommMonoid N]
[Module ℂ N]
[Module (UqSl2 q) N]
[IsScalarTower ℂ (UqSl2 q) N]
(m : M)
(n : N)
:
The raising generator acts through E ⊗ 1 + K ⊗ E.
@[simp]
theorem
TauCeti.UqSl2.f_smul_tmul
(q : ℂ)
[Fact (q ≠ 0)]
{M : Type u_1}
{N : Type u_2}
[AddCommMonoid M]
[Module ℂ M]
[Module (UqSl2 q) M]
[IsScalarTower ℂ (UqSl2 q) M]
[AddCommMonoid N]
[Module ℂ N]
[Module (UqSl2 q) N]
[IsScalarTower ℂ (UqSl2 q) N]
(m : M)
(n : N)
:
The lowering generator acts through F ⊗ K⁻¹ + 1 ⊗ F.
@[simp]
theorem
TauCeti.UqSl2.k_smul_tmul
(q : ℂ)
[Fact (q ≠ 0)]
{M : Type u_1}
{N : Type u_2}
[AddCommMonoid M]
[Module ℂ M]
[Module (UqSl2 q) M]
[IsScalarTower ℂ (UqSl2 q) M]
[AddCommMonoid N]
[Module ℂ N]
[Module (UqSl2 q) N]
[IsScalarTower ℂ (UqSl2 q) N]
(m : M)
(n : N)
:
The weight generator acts on both tensor factors.
@[simp]
theorem
TauCeti.UqSl2.kInv_smul_tmul
(q : ℂ)
[Fact (q ≠ 0)]
{M : Type u_1}
{N : Type u_2}
[AddCommMonoid M]
[Module ℂ M]
[Module (UqSl2 q) M]
[IsScalarTower ℂ (UqSl2 q) M]
[AddCommMonoid N]
[Module ℂ N]
[Module (UqSl2 q) N]
[IsScalarTower ℂ (UqSl2 q) N]
(m : M)
(n : N)
:
The inverse weight generator acts on both tensor factors.