The PBW representation of a Lie algebra on a polynomial algebra

Let L be a Lie algebra over a commutative ring R, free with a basis b indexed by a linearly ordered type ι, and let S = R[zᵢ | i ∈ ι] be the polynomial algebra on the same index set. This file constructs the representation of L on S that proves the linear-independence half of the Poincaré--Birkhoff--Witt theorem: a Lie algebra homomorphism

b.pbwPolynomialRep : L →ₗ⁅R⁆ Module.End R S

such that

• bᵢ acts on a monomial z^σ all of whose variables are at least i by multiplication by zᵢ;
• every x : L acts on a polynomial of total degree at most d as multiplication by the linear form zₓ = ∑ᵢ (b.repr x i) zᵢ, up to an error of total degree at most d.

Given a word x₁ ⋯ xₙ in L, the induced action of U(L) therefore sends 1 to zₓ₁ ⋯ zₓₙ up to lower-degree terms, and sends an ordered monomial bᵢ₁ ⋯ bᵢₙ (i₁ ≤ ⋯ ≤ iₙ) to the monomial zᵢ₁ ⋯ zᵢₙ exactly. This is what separates the graded pieces of the PBW filtration from each other.

The construction

The action of bₗ on a monomial z^σ is defined by induction on the degree of σ. If every variable of σ is at least l, it is multiplication by zₗ. Otherwise σ = eμ + τ where μ is the least variable of σ and μ < l, and the value is forced by the commutator relation that the representation must satisfy:

bₗ · z^σ = zμ zₗ z^τ + bμ · (bₗ · z^τ - zₗ z^τ) + ⁅bₗ, bμ⁆ · z^τ,

where all actions on the right are on polynomials of degree less than that of σ. The induction is carried out by iterating a single step on bilinear maps L → S → S; the iterates agree on polynomials of degree at most n from the n-th one onwards, and their limit is the action. Verifying that the result is a Lie algebra homomorphism is again an induction on degree, whose only nontrivial case uses the Jacobi identity. The recursive construction and its degree estimates use only a module with a bracket; the Lie identities enter when proving the representation law.

Main definitions and results

• Module.Basis.pbwPolynomialRep: the representation.
• Module.Basis.pbwPolynomialRep_basis_monomial_of_le: the action of bₗ on a monomial in variables at least l is multiplication by zₗ.
• Module.Basis.pbwPolynomialRep_sub_mul_mem_restrictTotalDegree: up to terms of total degree at most d, the action on a polynomial of total degree at most d is multiplication by the corresponding linear form.
• Module.Basis.pbwPolynomialRep_mem_restrictTotalDegree: the action raises total degree by at most one.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Chapter V, §17.4, Lemma A, whose proof this file follows.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapter I, §2.7.

Monomial bookkeeping

The inductive step

The limit action

The commutator relation

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

The PBW representation. For a Lie algebra L with a basis b indexed by a linearly ordered type ι, the representation of L on the polynomial algebra R[zᵢ | i ∈ ι] in which bₗ acts on a monomial in variables at least l by multiplication by zₗ (Module.Basis.pbwPolynomialRep_basis_monomial_of_le), and every element acts as multiplication by its linear form up to lower-degree terms (Module.Basis.pbwPolynomialRep_sub_mul_mem_restrictTotalDegree).

Equations

• b.pbwPolynomialRep = { toLinearMap := Module.Basis.PBWPolynomialRep.act✝ b, map_lie' := ⋯ }

@[simp]

theorem Module.Basis.pbwPolynomialRep_basis_monomial_of_le {R : Type u} {L : Type v} {ι : Type w} [CommRing R] [LinearOrder ι] [LieRing L] [LieAlgebra R L] (b : Basis ι R L) {l : ι} {σ : ι →₀ ℕ} (r : R) (h : ∀ i ∈ σ.support, l ≤ i) : (b.pbwPolynomialRep (b l)) ((MvPolynomial.monomial σ) r) = MvPolynomial.X l * (MvPolynomial.monomial σ) r

A basis vector bₗ acts on a monomial with any coefficient, all of whose variables are at least l, as multiplication by the variable zₗ.

theorem Module.Basis.pbwPolynomialRep_sub_mul_mem_restrictTotalDegree {R : Type u} {L : Type v} {ι : Type w} [CommRing R] [LinearOrder ι] [LieRing L] [LieAlgebra R L] (b : Basis ι R L) {d : ℕ} (x : L) {p : MvPolynomial ι R} (hp : p ∈ MvPolynomial.restrictTotalDegree ι R d) : (b.pbwPolynomialRep x) p - ((b.constr R) MvPolynomial.X) x * p ∈ MvPolynomial.restrictTotalDegree ι R d

On polynomials of total degree at most d, the action of x is multiplication by the linear form zₓ = b.constr R X x, up to an error of total degree at most d.

theorem Module.Basis.pbwPolynomialRep_mem_restrictTotalDegree {R : Type u} {L : Type v} {ι : Type w} [CommRing R] [LinearOrder ι] [LieRing L] [LieAlgebra R L] (b : Basis ι R L) {d : ℕ} (x : L) {p : MvPolynomial ι R} (hp : p ∈ MvPolynomial.restrictTotalDegree ι R d) : (b.pbwPolynomialRep x) p ∈ MvPolynomial.restrictTotalDegree ι R (d + 1)

The action raises total degree by at most one.