The enveloping algebra of an abelian Lie algebra is its symmetric algebra

Let L be an abelian Lie algebra over a commutative ring R, that is, one whose bracket vanishes identically (IsLieAbelian L). This file proves that the canonical map ι : L → UniversalEnvelopingAlgebra R L exhibits U(L) as the symmetric algebra of the R-module L, and reads off the resulting basis of U(L).

What this says

The defining relation of U(L) is ι x * ι y - ι y * ι x = ι ⁅x, y⁆, so for an abelian L it is the commutativity relation and nothing else: U(L) is commutative (TauCeti.UniversalEnvelopingAlgebra.instCommRing), and it is the universal commutative R-algebra containing L, which is the symmetric algebra. Both algebras are therefore built by the same universal property, and the comparison is the pair of lifts in either direction; nothing finer, and in particular no Poincaré--Birkhoff--Witt input, is used.

The consequence that is not visible in the universal property is the basis. The symmetric algebra of a free module is a polynomial algebra (Mathlib's SymmetricAlgebra.equivMvPolynomial), so for a basis b of L the algebra U(L) is the polynomial algebra on the b i (TauCeti.UniversalEnvelopingAlgebra.mvPolynomialEquiv) and the monomials ∏ᵢ ι(b i) ^ nᵢ are an R-basis of it (TauCeti.UniversalEnvelopingAlgebra.basisMonomials). That is the Poincaré--Birkhoff--Witt ordered-monomial theorem for an abelian Lie algebra: the ordering of a monomial carries no information here, since the generators commute, so a monomial is recorded by its exponent function n : κ →₀ ℕ rather than by a sorted word.

The comparison also makes ι injective on any abelian L (TauCeti.UniversalEnvelopingAlgebra.ι_injective_of_isLieAbelian), with no hypothesis on L as a module: it identifies ι with the canonical map L → S(L), which the square-zero extension R ⊕ L retracts. For a general Lie algebra injectivity is instead a corollary of Poincaré--Birkhoff--Witt, which over a commutative ring needs L to be free (or at least projective) as an R-module, and is unconditional only over a field.

Where it is used

A Cartan subalgebra H of a Lie algebra L with non-degenerate Killing form is abelian, by Mathlib's LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra; that instance also asks that L be free and finite as an R-module, that R be an integral domain and a principal ideal ring, and that L be Artinian, all of which hold for a finite-dimensional Lie algebra over a field. TauCeti.UniversalEnvelopingAlgebra.symmetricAlgebraEquiv then applies to H with no hypotheses of its own beyond that abelianness, and identifies U(H) with S(H). This identification is used in the Harish-Chandra projection from the center of U(L) to S(H).

Main definitions and results

• TauCeti.UniversalEnvelopingAlgebra.instCommRing: the enveloping algebra of an abelian Lie algebra is commutative.
• TauCeti.UniversalEnvelopingAlgebra.isSymmetricAlgebra_ι and TauCeti.UniversalEnvelopingAlgebra.symmetricAlgebraEquiv: ι : L → U(L) exhibits U(L) as the symmetric algebra of L, with the resulting algebra isomorphism S(L) ≃ₐ[R] U(L).
• TauCeti.UniversalEnvelopingAlgebra.mvPolynomialEquiv: for a basis of L, the identification of U(L) with a polynomial algebra.
• TauCeti.UniversalEnvelopingAlgebra.ι_injective_of_isLieAbelian: ι is injective, with no hypothesis on L as an R-module.
• TauCeti.UniversalEnvelopingAlgebra.basisMonomials: the monomial basis of U(L).

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Chapter V, §17 (the Poincaré--Birkhoff--Witt theorem; §17.2 is the abelian case).
• N. Bourbaki, Lie Groups and Lie Algebras, Chapter I, §2.7.

Commutativity

@[instance_reducible]

instance TauCeti.UniversalEnvelopingAlgebra.instCommRing (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] : CommRing (UniversalEnvelopingAlgebra R L)

The enveloping algebra of an abelian Lie algebra is commutative. The defining relation ι x * ι y - ι y * ι x = ι ⁅x, y⁆ of U(L) reads ι x * ι y = ι y * ι x when the bracket vanishes, and U(L) is generated by the scalars and those generators.

Equations

• TauCeti.UniversalEnvelopingAlgebra.instCommRing R L = { toRing := inferInstance, mul_comm := ⋯ }

The comparison with the symmetric algebra

theorem TauCeti.UniversalEnvelopingAlgebra.isSymmetricAlgebra_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] : IsSymmetricAlgebra ↑(UniversalEnvelopingAlgebra.ι R)

The canonical map of an abelian Lie algebra into its enveloping algebra exhibits the enveloping algebra as the symmetric algebra. The two universal properties describe the same object: an R-linear map out of L into a commutative R-algebra is the same thing as a Lie algebra homomorphism, because the bracket on L and the commutator on the target both vanish.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.symmetricAlgebraEquiv (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] : SymmetricAlgebra R L ≃ₐ[R] UniversalEnvelopingAlgebra R L

The symmetric algebra of an abelian Lie algebra is its enveloping algebra, as an algebra isomorphism S(L) ≃ₐ[R] U(L) carrying the canonical generators to the canonical generators.

Equations

• TauCeti.UniversalEnvelopingAlgebra.symmetricAlgebraEquiv R L = ⋯.equiv

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.symmetricAlgebraEquiv_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] (x : L) : (symmetricAlgebraEquiv R L) ((SymmetricAlgebra.ι R L) x) = (UniversalEnvelopingAlgebra.ι R) x

The comparison isomorphism sends the canonical generator SymmetricAlgebra.ι R L x of S(L) to the canonical generator UniversalEnvelopingAlgebra.ι R x of U(L).

theorem TauCeti.UniversalEnvelopingAlgebra.symmetricAlgebraEquiv_symm_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] (x : L) : (symmetricAlgebraEquiv R L).symm ((UniversalEnvelopingAlgebra.ι R) x) = (SymmetricAlgebra.ι R L) x

The inverse of the comparison isomorphism sends the canonical generator UniversalEnvelopingAlgebra.ι R x of U(L) back to SymmetricAlgebra.ι R L x. This is the form to quote by hand; the simp-normal form is TauCeti.UniversalEnvelopingAlgebra.symmetricAlgebraEquiv_symm_ι', because simp rewrites ι to mkAlgHom by UniversalEnvelopingAlgebra.ι_apply.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.symmetricAlgebraEquiv_symm_ι' (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] (x : L) : (symmetricAlgebraEquiv R L).symm ((UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) x)) = (SymmetricAlgebra.ι R L) x

TauCeti.UniversalEnvelopingAlgebra.symmetricAlgebraEquiv_symm_ι with its left-hand side in simp-normal form: the simp lemma UniversalEnvelopingAlgebra.ι_apply unfolds ι R x to mkAlgHom R L (TensorAlgebra.ι R x), so this is the shape simp actually meets.

theorem TauCeti.UniversalEnvelopingAlgebra.ι_injective_of_isLieAbelian (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] : Function.Injective ⇑(UniversalEnvelopingAlgebra.ι R)

The canonical map of an abelian Lie algebra into its enveloping algebra is injective. Under the comparison it is the canonical map L → S(L), which is injective for every module. For a general Lie algebra injectivity is instead a corollary of the Poincaré--Birkhoff--Witt theorem, which over a commutative ring needs L to be free (or at least projective) as an R-module.

instance TauCeti.UniversalEnvelopingAlgebra.instModuleFree (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] [Module.Free R L] : Module.Free R (UniversalEnvelopingAlgebra R L)

The enveloping algebra of an abelian Lie algebra which is free as a module is free as a module.

The monomial basis

noncomputable def TauCeti.UniversalEnvelopingAlgebra.mvPolynomialEquiv (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] {κ : Type w} (b : Module.Basis κ R L) : MvPolynomial κ R ≃ₐ[R] UniversalEnvelopingAlgebra R L

The enveloping algebra of an abelian Lie algebra with a basis is a polynomial algebra on that basis.

Equations

• TauCeti.UniversalEnvelopingAlgebra.mvPolynomialEquiv R L b = (SymmetricAlgebra.equivMvPolynomial b).symm.trans (TauCeti.UniversalEnvelopingAlgebra.symmetricAlgebraEquiv R L)

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mvPolynomialEquiv_X (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] {κ : Type w} (b : Module.Basis κ R L) (i : κ) : (mvPolynomialEquiv R L b) (MvPolynomial.X i) = (UniversalEnvelopingAlgebra.ι R) (b i)

The polynomial identification sends the variable X i to the canonical generator ι R (b i) of U(L).

theorem TauCeti.UniversalEnvelopingAlgebra.mvPolynomialEquiv_symm_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] {κ : Type w} (b : Module.Basis κ R L) (i : κ) : (mvPolynomialEquiv R L b).symm ((UniversalEnvelopingAlgebra.ι R) (b i)) = MvPolynomial.X i

The inverse of the polynomial identification sends the canonical generator ι R (b i) of U(L) back to the variable X i. This is the form to quote by hand; the simp-normal form is TauCeti.UniversalEnvelopingAlgebra.mvPolynomialEquiv_symm_ι', because simp rewrites ι to mkAlgHom by UniversalEnvelopingAlgebra.ι_apply.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mvPolynomialEquiv_symm_ι' (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] {κ : Type w} (b : Module.Basis κ R L) (i : κ) : (mvPolynomialEquiv R L b).symm ((UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) (b i))) = MvPolynomial.X i

TauCeti.UniversalEnvelopingAlgebra.mvPolynomialEquiv_symm_ι with its left-hand side in simp-normal form: the simp lemma UniversalEnvelopingAlgebra.ι_apply unfolds ι R (b i) to mkAlgHom R L (TensorAlgebra.ι R (b i)), so this is the shape simp actually meets.

theorem TauCeti.UniversalEnvelopingAlgebra.mvPolynomialEquiv_toAlgHom (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] {κ : Type w} (b : Module.Basis κ R L) : ↑(mvPolynomialEquiv R L b) = MvPolynomial.aeval fun (i : κ) => (UniversalEnvelopingAlgebra.ι R) (b i)

The polynomial identification is evaluation of a polynomial at the canonical generators.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.basisMonomials (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] {κ : Type w} (b : Module.Basis κ R L) : Module.Basis (κ →₀ ℕ) R (UniversalEnvelopingAlgebra R L)

The monomials in a basis of an abelian Lie algebra are a basis of its enveloping algebra. This is the Poincaré--Birkhoff--Witt ordered-monomial theorem in the abelian case, where a monomial is determined by its exponent function because the generators commute.

Equations

• TauCeti.UniversalEnvelopingAlgebra.basisMonomials R L b = b.symmetricAlgebra.map ↑(TauCeti.UniversalEnvelopingAlgebra.symmetricAlgebraEquiv R L)

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.basisMonomials_apply (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] {κ : Type w} (b : Module.Basis κ R L) (n : κ →₀ ℕ) : (basisMonomials R L b) n = n.prod fun (i : κ) (k : ℕ) => (UniversalEnvelopingAlgebra.ι R) (b i) ^ k

The monomial basis vector at an exponent function n is the monomial ∏ᵢ ι (b i) ^ nᵢ in the canonical generators.