Evaluation of the PBW polynomial representation

The polynomial representation attached to an ordered basis of a Lie algebra gives a linear map from its enveloping algebra to polynomials by applying an operator to 1. An ordered word of basis vectors evaluates to the monomial with exactly those multiplicities. This normalization identifies the ordered PBW basis with the usual polynomial monomials as modules.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Chapter V, §17.4.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapter I, §2.7.

noncomputable def Module.Basis.pbwEval {R : Type u} {L : Type v} {ι : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) : UniversalEnvelopingAlgebra R L →ₗ[R] MvPolynomial ι R

Apply the PBW polynomial representation of the enveloping algebra to the constant 1.

Equations

• b.pbwEval = LinearMap.applyₗ 1 ∘ₗ ((UniversalEnvelopingAlgebra.lift R) b.pbwPolynomialRep).toLinearMap

@[simp]

theorem Module.Basis.pbwEval_one {R : Type u} {L : Type v} {ι : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) : b.pbwEval 1 = 1

theorem Module.Basis.pbwEval_ι_mul {R : Type u} {L : Type v} {ι : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) (x : L) (a : UniversalEnvelopingAlgebra R L) : b.pbwEval ((UniversalEnvelopingAlgebra.ι R) x * a) = (b.pbwPolynomialRep x) (b.pbwEval a)

Left multiplication by a generator becomes its action on polynomials.

theorem Module.Basis.pbwEval_pbwMonomial {R : Type u} {L : Type v} {ι : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) {word : List ι} (hword : List.Pairwise (fun (x1 x2 : ι) => x1 ≤ x2) word) : b.pbwEval (TauCeti.UniversalEnvelopingAlgebra.pbwMonomial R L (⇑b) word) = (MvPolynomial.monomial (Multiset.toFinsupp ↑word)) 1

An ordered word evaluates to the polynomial monomial with the same multiplicities.