Degreewise PBW symmetrization

When n! is a unit in the commutative base ring, averaging the ordered products of Lie generators defines a canonical linear map from the nth symmetric power to the enveloping algebra. Its leading PBW symbol is the product of the symmetric generators. When L is free as an R-module, this gives an injective map on every homogeneous symmetric-algebra component, splitting its PBW symbol.

This is the degreewise filtered comparison used to lift invariant symmetric polynomials to the enveloping algebra without changing their leading terms. Symmetrization intertwines the adjoint action of L on S(L) with the commutator action u ↦ ⁅ι x, u⁆ on U(L): bracketing a symmetrized word with ι x symmetrizes the sum of the words in which one letter y is replaced by ⁅x, y⁆. Hence the symmetrization of a homogeneous Lie invariant p ∈ S(L)^L is central in U(L), and for free L the converse holds as well. These are the central elements whose leading symbols are the given invariants, in the proof of the Harish-Chandra isomorphism by Chevalley's restriction theorem.

The scalar ring lies in Type, as required by Mathlib's Fin n-indexed symmetric power Sym[R]^n L. The Lie algebra module has an independent universe.

Main results

• TauCeti.UniversalEnvelopingAlgebra.lie_ι_pbwSymmetrization_tprod: the commutator of ι x with a symmetrized word.
• TauCeti.UniversalEnvelopingAlgebra.lie_ι_pbwHomogeneousSymmetrization: symmetrization is equivariant for the adjoint actions on S(L) and U(L).
• TauCeti.UniversalEnvelopingAlgebra.pbwHomogeneousSymmetrization_mem_center: the symmetrization of a homogeneous Lie invariant is central.
• TauCeti.UniversalEnvelopingAlgebra.pbwHomogeneousSymmetrization_mem_center_iff and TauCeti.UniversalEnvelopingAlgebra.pbwSymmetrization_mem_center_iff: for free L, a symmetrization is central exactly when the symmetric polynomial is a Lie invariant.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §23.3.
• J. Dixmier, Enveloping Algebras, §2.4.

The Lean code is adapted from the closed Tau Ceti PR https://github.com/TauCetiProject/TauCeti/pull/18162 (feat: construct degreewise PBW symmetrization).

noncomputable def TauCeti.UniversalEnvelopingAlgebra.pbwSymmetrization (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (hn : IsUnit ↑n.factorial) : SymmetricPower R (Fin n) L →ₗ[R] UniversalEnvelopingAlgebra R L

The average of all ordered products of a symmetric tensor's Lie generators.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.pbwSymmetrization_tprod (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (hn : IsUnit ↑n.factorial) (m : Fin n → L) : (pbwSymmetrization R L n hn) (⨂ₛ[R] (i : Fin n), m i) = ↑hn.unit⁻¹ • ∑ σ : Equiv.Perm (Fin n), (List.ofFn fun (i : Fin n) => (UniversalEnvelopingAlgebra.ι R) (m (σ i))).prod

On pure symmetric tensors, symmetrization averages the products over all permutations.

theorem TauCeti.UniversalEnvelopingAlgebra.pbwSymmetrization_tprod_rat (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Algebra ℚ R] (n : ℕ) (hn : IsUnit ↑n.factorial) (m : Fin n → L) : (pbwSymmetrization R L n hn) (⨂ₛ[R] (i : Fin n), m i) = (algebraMap ℚ R) (↑n.factorial)⁻¹ • ∑ σ : Equiv.Perm (Fin n), (List.ofFn fun (i : Fin n) => (UniversalEnvelopingAlgebra.ι R) (m (σ i))).prod

Over a rational algebra, the unit-normalized average is the usual rational average.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.pbwSymmetrization_tprod_const (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (hn : IsUnit ↑n.factorial) (x : L) : (pbwSymmetrization R L n hn) (⨂ₛ[R] (x_1 : Fin n), x) = (UniversalEnvelopingAlgebra.ι R) x ^ n

Symmetrization sends a pure power to the corresponding power of a Lie generator.

theorem TauCeti.UniversalEnvelopingAlgebra.pbwSymmetrization_mem_pbwFiltration (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (hn : IsUnit ↑n.factorial) (x : SymmetricPower R (Fin n) L) : (pbwSymmetrization R L n hn) x ∈ pbwFiltration R L n

Symmetrization has PBW filtration degree at most its symmetric degree.

theorem TauCeti.UniversalEnvelopingAlgebra.pbwSymmetrization_tprod_sub_mem_pbwFiltrationPrevious (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (hn : IsUnit ↑n.factorial) (m : Fin n → L) : (pbwSymmetrization R L n hn) (⨂ₛ[R] (i : Fin n), m i) - (List.ofFn fun (i : Fin n) => (UniversalEnvelopingAlgebra.ι R) (m i)).prod ∈ pbwFiltrationPrevious R L n

Symmetrizing a word changes it only in strictly smaller PBW filtration degree.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mk_pbwSymmetrization (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (hn : IsUnit ↑n.factorial) (x : SymmetricPower R (Fin n) L) : Submodule.Quotient.mk ⟨(pbwSymmetrization R L n hn) x, ⋯⟩ = (pbwHomogeneousComponentMap R L n) ((SymmetricPower.toHomogeneous R L n) x)

The leading symbol of tensor symmetrization is its canonical PBW image, without any freeness assumption on the Lie algebra module.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.pbwHomogeneousSymmetrization (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (hn : IsUnit ↑n.factorial) : ↥(SymmetricAlgebra.homogeneousSubmodule R L n) →ₗ[R] UniversalEnvelopingAlgebra R L

Degreewise symmetrization, expressed on homogeneous symmetric polynomials.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.pbwHomogeneousSymmetrization_apply (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (hn : IsUnit ↑n.factorial) (p : ↥(SymmetricAlgebra.homogeneousSubmodule R L n)) : (pbwHomogeneousSymmetrization R L n hn) p = (pbwSymmetrization R L n hn) ((SymmetricPower.equivHomogeneous n).symm p)

Homogeneous symmetrization is tensor symmetrization after the inverse comparison.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.pbwHomogeneousSymmetrization_equivHomogeneous (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (hn : IsUnit ↑n.factorial) (x : SymmetricPower R (Fin n) L) : (pbwHomogeneousSymmetrization R L n hn) ((SymmetricPower.equivHomogeneous n) x) = (pbwSymmetrization R L n hn) x

The homogeneous map agrees with tensor symmetrization under the canonical comparison.

theorem TauCeti.UniversalEnvelopingAlgebra.pbwHomogeneousSymmetrization_mem_pbwFiltration (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (hn : IsUnit ↑n.factorial) (p : ↥(SymmetricAlgebra.homogeneousSubmodule R L n)) : (pbwHomogeneousSymmetrization R L n hn) p ∈ pbwFiltration R L n

Homogeneous symmetrization lands in the corresponding PBW filtration step.

theorem TauCeti.UniversalEnvelopingAlgebra.pbwHomogeneousSymmetrization_mem_wordFiltration (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (hn : IsUnit ↑n.factorial) (p : ↥(SymmetricAlgebra.homogeneousSubmodule R L n)) : (pbwHomogeneousSymmetrization R L n hn) p ∈ Algebra.wordFiltration (↑(UniversalEnvelopingAlgebra.ι R)) n

Homogeneous symmetrization lands in the word filtration used for the PBW graded piece.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mk_pbwHomogeneousSymmetrization (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (hn : IsUnit ↑n.factorial) (p : ↥(SymmetricAlgebra.homogeneousSubmodule R L n)) : Submodule.Quotient.mk ⟨(pbwHomogeneousSymmetrization R L n hn) p, ⋯⟩ = (pbwHomogeneousComponentMap R L n) p

Taking the leading PBW symbol of symmetrization recovers the canonical PBW image.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.pbwHomogeneousSymmetrization_ι_pow (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (hn : IsUnit ↑n.factorial) (x : L) (h : (SymmetricAlgebra.ι R L) x ^ n ∈ SymmetricAlgebra.homogeneousSubmodule R L n) : (pbwHomogeneousSymmetrization R L n hn) ⟨(SymmetricAlgebra.ι R L) x ^ n, h⟩ = (UniversalEnvelopingAlgebra.ι R) x ^ n

Homogeneous symmetrization sends the n-th power of a generator of S(L) to the n-th power of the corresponding generator of U(L).

theorem TauCeti.UniversalEnvelopingAlgebra.range_pbwHomogeneousSymmetrization (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (hn : IsUnit ↑n.factorial) : (pbwHomogeneousSymmetrization R L n hn).range = (pbwSymmetrization R L n hn).range

Homogeneous and tensor symmetrization in degree n have the same range.

theorem TauCeti.UniversalEnvelopingAlgebra.iSup_range_pbwSymmetrization_eq_top (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (hn : ∀ (n : ℕ), IsUnit ↑n.factorial) : ⨆ (n : ℕ), (pbwSymmetrization R L n ⋯).range = ⊤

Symmetrization is onto. When every factorial is a unit of R, the enveloping algebra is spanned by the symmetrizations of all degrees. A word of length n in the generators is its own symmetrization up to an element of PBW filtration degree n - 1, so this follows by induction on the length of words. No freeness of L is needed.

Equivariance and central elements

theorem TauCeti.UniversalEnvelopingAlgebra.lie_ι_pbwSymmetrization_tprod (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (hn : IsUnit ↑n.factorial) (x : L) (m : Fin n → L) : ⁅(UniversalEnvelopingAlgebra.ι R) x, (pbwSymmetrization R L n hn) (⨂ₛ[R] (i : Fin n), m i)⁆ = ∑ k : Fin n, (pbwSymmetrization R L n hn) (⨂ₛ[R] (i : Fin n), Function.update m k ⁅x, m k⁆ i)

The commutator with a Lie generator, on a symmetrized word. Bracketing the symmetrization of m 0, …, m (n - 1) with ι x gives the sum of the symmetrizations of the words in which one letter m k is replaced by ⁅x, m k⁆.

theorem TauCeti.UniversalEnvelopingAlgebra.lie_ι_pbwHomogeneousSymmetrization (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (hn : IsUnit ↑n.factorial) (x : L) {p q : ↥(SymmetricAlgebra.homogeneousSubmodule R L n)} (hpq : ((SymmetricAlgebra.lieModuleDerivation R L L) x) ↑p = ↑q) : ⁅(UniversalEnvelopingAlgebra.ι R) x, (pbwHomogeneousSymmetrization R L n hn) p⁆ = (pbwHomogeneousSymmetrization R L n hn) q

Symmetrization is equivariant for the adjoint actions. If q is the image of the homogeneous symmetric polynomial p under the adjoint action of x on S(L), then the symmetrization of q is the commutator of ι x with the symmetrization of p.

theorem TauCeti.UniversalEnvelopingAlgebra.pbwHomogeneousSymmetrization_mem_center (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (hn : IsUnit ↑n.factorial) {p : ↥(SymmetricAlgebra.homogeneousSubmodule R L n)} (hp : ↑p ∈ SymmetricAlgebra.lieInvariants R L L) : (pbwHomogeneousSymmetrization R L n hn) p ∈ Subalgebra.center R (UniversalEnvelopingAlgebra R L)

Symmetrizing a Lie invariant gives a central element. The symmetrization of a homogeneous element of S(L)^L commutes with every element of U(L).

theorem TauCeti.UniversalEnvelopingAlgebra.pbwSymmetrization_mem_center (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (hn : IsUnit ↑n.factorial) {t : SymmetricPower R (Fin n) L} (ht : (SymmetricPower.toSymmetricAlgebra R L n) t ∈ SymmetricAlgebra.lieInvariants R L L) : (pbwSymmetrization R L n hn) t ∈ Subalgebra.center R (UniversalEnvelopingAlgebra R L)

Symmetrizing a Lie-invariant symmetric tensor gives a central element.

theorem TauCeti.UniversalEnvelopingAlgebra.pbwHomogeneousSymmetrization_injective (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] (n : ℕ) (hn : IsUnit ↑n.factorial) : Function.Injective ⇑(pbwHomogeneousSymmetrization R L n hn)

Symmetrization of homogeneous symmetric polynomials is injective.

theorem TauCeti.UniversalEnvelopingAlgebra.pbwSymmetrization_injective (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] (n : ℕ) (hn : IsUnit ↑n.factorial) : Function.Injective ⇑(pbwSymmetrization R L n hn)

Degreewise tensor symmetrization is injective when the Lie algebra module is free.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.pbwHomogeneousSymmetrization_mem_center_iff (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] (n : ℕ) (hn : IsUnit ↑n.factorial) {p : ↥(SymmetricAlgebra.homogeneousSubmodule R L n)} : (pbwHomogeneousSymmetrization R L n hn) p ∈ Subalgebra.center R (UniversalEnvelopingAlgebra R L) ↔ ↑p ∈ SymmetricAlgebra.lieInvariants R L L

The symmetrization of a homogeneous polynomial is central exactly when the polynomial is a Lie invariant, for L free over R. Symmetrization intertwines the adjoint actions on S(L) and on U(L), and it is injective on each homogeneous component.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.pbwSymmetrization_mem_center_iff (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] (n : ℕ) (hn : IsUnit ↑n.factorial) {t : SymmetricPower R (Fin n) L} : (pbwSymmetrization R L n hn) t ∈ Subalgebra.center R (UniversalEnvelopingAlgebra R L) ↔ (SymmetricPower.toSymmetricAlgebra R L n) t ∈ SymmetricAlgebra.lieInvariants R L L

The symmetrization of a symmetric tensor is central exactly when the tensor is a Lie invariant, read in S(L), for L free over R.