The ordered Poincaré--Birkhoff--Witt basis

For any ordered basis b of a Lie algebra over a commutative ring, the products of its canonical generators in increasing order form a basis of the enveloping algebra. The indices are finitely supported natural exponents. The value at an exponent is the corresponding ordered product, with coefficient 1, including the empty product 1.

The evaluation of the polynomial representation gives a linear equivalence with multivariate polynomials carrying these basis vectors to the usual monomials. This is an equivalence of modules; the enveloping algebra need not be commutative.

Main results

• Module.Basis.pbwBasis: the ordered monomial basis of the enveloping algebra.
• Module.Basis.pbwBasis_eq_prod_pow: its value as the increasing product of generator powers.
• Module.Basis.pbwEquiv: the linear equivalence with multivariate polynomials.

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.pbwBasis {R : Type u} {L : Type v} {ι : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) : Basis (ι →₀ ℕ) R (UniversalEnvelopingAlgebra R L)

The Poincaré--Birkhoff--Witt basis: ordered monomials in a chosen basis of the Lie algebra, over an arbitrary commutative ring.

Equations

• b.pbwBasis = Module.Basis.mk ⋯ ⋯

theorem Module.Basis.pbwBasis_apply {R : Type u} {L : Type v} {ι : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) (n : ι →₀ ℕ) : b.pbwBasis n = TauCeti.UniversalEnvelopingAlgebra.pbwMonomial R L (⇑b) ((Finsupp.toMultiset n).sort fun (x1 x2 : ι) => x1 ≤ x2)

The basis vector at n is the word containing n i copies of each generator, sorted in increasing order.

@[simp]

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

@[simp]

theorem Module.Basis.pbwEval_pbwBasis {R : Type u} {L : Type v} {ι : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) (n : ι →₀ ℕ) : b.pbwEval (b.pbwBasis n) = (MvPolynomial.monomial n) 1

PBW evaluation sends each ordered basis vector to the corresponding polynomial monomial.

theorem Module.Basis.pbwEval_bijective {R : Type u} {L : Type v} {ι : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) : Function.Bijective ⇑b.pbwEval

The PBW evaluation is bijective: it carries the ordered basis to the polynomial basis.

noncomputable def Module.Basis.pbwEquiv {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

The linear PBW equivalence with polynomials, normalized by the ordered monomial basis.

Equations

• b.pbwEquiv = LinearEquiv.ofBijective b.pbwEval ⋯

@[simp]

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

@[simp]

theorem Module.Basis.pbwEquiv_symm_monomial {R : Type u} {L : Type v} {ι : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) (n : ι →₀ ℕ) : b.pbwEquiv.symm ((MvPolynomial.monomial n) 1) = b.pbwBasis n

theorem Module.Basis.pbwBasis_eq_prod_pow {R : Type u} {L : Type v} {ι : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) (n : ι →₀ ℕ) : b.pbwBasis n = (List.map (fun (i : ι) => (UniversalEnvelopingAlgebra.ι R) (b i) ^ n i) (n.support.sort fun (x1 x2 : ι) => x1 ≤ x2)).prod

The basis vector at n is the product of ι(b i) ^ n i, with the support traversed in increasing order. No commutativity of the enveloping algebra is assumed.

@[simp]

theorem Module.Basis.pbwBasis_single {R : Type u} {L : Type v} {ι : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) (i : ι) (k : ℕ) : b.pbwBasis (Finsupp.single i k) = (UniversalEnvelopingAlgebra.ι R) (b i) ^ k