The enveloping algebra of a line is a polynomial ring

For an abelian Lie algebra L over a commutative ring R with a basis b, the enveloping algebra U(L) is the polynomial algebra on the b i (TauCeti.UniversalEnvelopingAlgebra.mvPolynomialEquiv). This file reads off the one-variable case, where a single basis vector makes U(L) the polynomial ring R[X] in the image of that vector.

The one-variable case is where the Poincaré--Birkhoff--Witt theorem is first visible: its content is that the powers ι(b default) ^ n are linearly independent, and here they are the ordinary monomials of a polynomial ring, TauCeti.UniversalEnvelopingAlgebra.basisPow. Both the algebra identification and the basis are stated for a basis indexed by an arbitrary Unique type rather than by PUnit, since that is what MvPolynomial.uniqueAlgEquiv provides and a consumer holding a Basis (Fin 1) R L should not have to reindex it.

Main definitions

• TauCeti.UniversalEnvelopingAlgebra.polynomialEquiv: for a basis of an abelian L indexed by a Unique type, the identification R[X] ≃ₐ[R] U(L).
• TauCeti.UniversalEnvelopingAlgebra.basisPow: the powers of the image of the basis vector, as an R-basis of U(L) indexed by ℕ.

Main results

• TauCeti.UniversalEnvelopingAlgebra.polynomialEquiv_X and TauCeti.UniversalEnvelopingAlgebra.polynomialEquiv_X_pow: the variable goes to the canonical generator, and its powers to the powers of that generator -- the normalization without which the identification says nothing about the Poincaré--Birkhoff--Witt monomials.
• TauCeti.UniversalEnvelopingAlgebra.polynomialEquiv_toAlgHom: the identification is evaluation at the canonical generator.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Chapter V, §17.2 (the abelian case of the Poincaré--Birkhoff--Witt theorem).

The one-variable polynomial identification

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

The enveloping algebra of an abelian Lie algebra with a one-element basis is a polynomial ring in one variable, the variable going to the image of the basis vector (TauCeti.UniversalEnvelopingAlgebra.polynomialEquiv_X).

This is the one-variable case of TauCeti.UniversalEnvelopingAlgebra.mvPolynomialEquiv, composed with Mathlib's MvPolynomial.uniqueAlgEquiv.

Equations

• TauCeti.UniversalEnvelopingAlgebra.polynomialEquiv R L b = (MvPolynomial.uniqueAlgEquiv R κ).symm.trans (TauCeti.UniversalEnvelopingAlgebra.mvPolynomialEquiv R L b)

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.polynomialEquiv_X (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] {κ : Type w} [Unique κ] (b : Module.Basis κ R L) : (polynomialEquiv R L b) Polynomial.X = (UniversalEnvelopingAlgebra.ι R) (b default)

The polynomial identification sends the variable to the canonical generator ι R (b default) of U(L). Together with TauCeti.UniversalEnvelopingAlgebra.polynomialEquiv_C this pins polynomialEquiv down, an algebra map out of R[X] being determined by the image of X.

theorem TauCeti.UniversalEnvelopingAlgebra.polynomialEquiv_C (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] {κ : Type w} [Unique κ] (b : Module.Basis κ R L) (r : R) : (polynomialEquiv R L b) (Polynomial.C r) = (algebraMap R (UniversalEnvelopingAlgebra R L)) r

The polynomial identification is the algebra map on scalars. This is not a simp lemma: its left-hand side is not in simp-normal form, Polynomial.C_eq_algebraMap rewriting C r to algebraMap R _ r, which AlgEquiv.commutes then carries across.

theorem TauCeti.UniversalEnvelopingAlgebra.polynomialEquiv_X_pow (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] {κ : Type w} [Unique κ] (b : Module.Basis κ R L) (n : ℕ) : (polynomialEquiv R L b) (Polynomial.X ^ n) = (UniversalEnvelopingAlgebra.ι R) (b default) ^ n

The n-th power of the variable goes to the n-th power of the canonical generator. This is the normalization the Poincaré--Birkhoff--Witt monomials of a one-dimensional Lie algebra are asked for: the monomial basis of R[X] is carried to the powers of ι R (b default), and not to any other scaling of them. It is not a simp lemma: its left-hand side is not in simp-normal form, map_pow distributing the identification over the power first.

theorem TauCeti.UniversalEnvelopingAlgebra.polynomialEquiv_monomial (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] {κ : Type w} [Unique κ] (b : Module.Basis κ R L) (n : ℕ) (r : R) : (polynomialEquiv R L b) ((Polynomial.monomial n) r) = r • (UniversalEnvelopingAlgebra.ι R) (b default) ^ n

The polynomial identification sends a monomial to a scaled power of the canonical generator.

theorem TauCeti.UniversalEnvelopingAlgebra.polynomialEquiv_toAlgHom (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] {κ : Type w} [Unique κ] (b : Module.Basis κ R L) : ↑(polynomialEquiv R L b) = Polynomial.aeval ((UniversalEnvelopingAlgebra.ι R) (b default))

The polynomial identification is evaluation at the canonical generator.

theorem TauCeti.UniversalEnvelopingAlgebra.polynomialEquiv_symm_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] {κ : Type w} [Unique κ] (b : Module.Basis κ R L) : (polynomialEquiv R L b).symm ((UniversalEnvelopingAlgebra.ι R) (b default)) = Polynomial.X

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.polynomialEquiv_symm_ι' (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] {κ : Type w} [Unique κ] (b : Module.Basis κ R L) : (polynomialEquiv R L b).symm ((UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) (b default))) = Polynomial.X

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

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

The powers of the image of a one-element basis are a basis of the enveloping algebra. This is the Poincaré--Birkhoff--Witt ordered-monomial theorem for a Lie algebra of rank one: a monomial in a single generator is recorded by its exponent, and the powers are linearly independent.

This is TauCeti.UniversalEnvelopingAlgebra.basisMonomials with its index changed from the exponent functions κ →₀ ℕ to the exponent itself: a consumer of a rank-one enveloping algebra reads off degrees, and would otherwise have to transport every statement along Finsupp.uniqueEquiv.

Equations

• TauCeti.UniversalEnvelopingAlgebra.basisPow R L b = (TauCeti.UniversalEnvelopingAlgebra.basisMonomials R L b).reindex (Finsupp.uniqueEquiv default)

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.basisPow_apply (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsLieAbelian L] {κ : Type w} [Unique κ] (b : Module.Basis κ R L) (n : ℕ) : (basisPow R L b) n = (UniversalEnvelopingAlgebra.ι R) (b default) ^ n

The n-th vector of TauCeti.UniversalEnvelopingAlgebra.basisPow is the n-th power of the canonical generator.