The Poincaré--Birkhoff--Witt theorem

For a Lie algebra L over a commutative ring R that is free as an R-module, the canonical algebra map

Sym(L) → gr U(L)

from the symmetric algebra to the associated graded of the PBW filtration is an isomorphism. It is surjective for every L (TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap_surjective); this file proves injectivity, the linear-independence half of the theorem.

The argument

Choose a basis b of L indexed by a linearly ordered type, and let U(L) act on the polynomial algebra S through the PBW representation Module.Basis.pbwPolynomialRep of TauCeti/Algebra/Lie/UniversalEnveloping/PBW/PolynomialRep.lean. Evaluating that action at 1 sends the PBW filtration step Uₙ into the polynomials of total degree at most n, and sends a word ι(x₁) ⋯ ι(xₙ) to the product of the linear forms zₓ₁ ⋯ zₓₙ up to terms of lower degree. Taking the degree-n homogeneous component therefore kills Uₙ₋₁ and descends to a linear map on the n-th graded piece, which composed with the degree-n component of Sym(L) → gr U(L) is the polynomial algebra isomorphism Sym(L) ≃ S attached to b. A map with an injective composite is injective.

Main results

• TauCeti.UniversalEnvelopingAlgebra.pbwHomogeneousComponentMap_injective: every degreewise component of the canonical map is injective.
• TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap_injective: the canonical map Sym(L) → gr U(L) is injective.
• TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedEquiv: the Poincaré--Birkhoff--Witt theorem, the algebra isomorphism Sym(L) ≃ₐ[R] gr U(L) for free L.

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.

theorem TauCeti.UniversalEnvelopingAlgebra.pbwHomogeneousComponentMap_injective (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] (n : ℕ) : Function.Injective ⇑(pbwHomogeneousComponentMap R L n)

Every degreewise component of the canonical map Sym(L) → gr U(L) is injective when L is a free module.

theorem TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap_injective (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] : Function.Injective ⇑(pbwAssociatedGradedMap R L)

The linear-independence half of the Poincaré--Birkhoff--Witt theorem. The canonical map Sym(L) → gr U(L) is injective when L is a free module.

theorem TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap_bijective (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] : Function.Bijective ⇑(pbwAssociatedGradedMap R L)

The canonical map Sym(L) → gr U(L) is bijective when L is a free module.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedEquiv (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] : SymmetricAlgebra R L ≃ₐ[R] PBWAssociatedGraded R L

The Poincaré--Birkhoff--Witt theorem. For a Lie algebra that is free as a module, the symmetric algebra is isomorphic to the associated graded of the PBW filtration of the enveloping algebra, by the algebra map sending x ∈ L to the degree-one class of ι(x).

Equations

• TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedEquiv R L = AlgEquiv.ofBijective (TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap R L) ⋯

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_pbwAssociatedGradedEquiv (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] : ⇑(pbwAssociatedGradedEquiv R L) = ⇑(pbwAssociatedGradedMap R L)