The PBW symbols of central elements

Restrict the PBW filtration of U(L) to its centre Z(U(L)): the n-th step TauCeti.UniversalEnvelopingAlgebra.centerPBWFiltration R L n consists of the central elements of PBW degree at most n, and TauCeti.UniversalEnvelopingAlgebra.CenterPBWGradedPiece R L n is the quotient by the central elements of degree below n. Taking PBW symbols embeds this quotient in the graded piece gr_n U(L) (TauCeti.UniversalEnvelopingAlgebra.centerPBWGradedToPBWGraded).

This file identifies the image. For L free over R and n! a unit in R, the PBW theorem reads gr_n U(L) as the homogeneous component S^n(L), and the symbols of the central elements of degree n are exactly the homogeneous Lie invariants S^n(L)^L. This gives the linear isomorphism

Z_n / Z_{n-1} ≃ S^n(L)^L

(TauCeti.UniversalEnvelopingAlgebra.centerPBWGradedInvariantIso), compatible with the PBW symbol and inverted by symmetrization. This is the graded comparison between Z(U(L)) and S(L)^L that, combined with Chevalley's restriction theorem, drives the degree induction in the proof of the Harish-Chandra isomorphism.

The two inclusions are proved as follows.

• An invariant p ∈ S^n(L)^L is the symbol of its symmetrization, which is central (TauCeti.UniversalEnvelopingAlgebra.pbwHomogeneousSymmetrization_mem_center).
• Conversely let z be central of degree n with symbol p ∈ S^n(L), so that z and the symmetrization sym p differ by an element of lower degree. Symmetrization intertwines the adjoint actions, so for x ∈ L the symmetrization of x • p is ⁅ι x, sym p⁆ = ⁅ι x, sym p - z⁆, and bracketing with ι x does not raise the degree. Hence sym (x • p) has degree below n, its symbol x • p vanishes, and p is invariant (TauCeti.UniversalEnvelopingAlgebra.mem_lieInvariants_of_pbwHomogeneousComponentMap_eq_mk).

Main definitions

• TauCeti.UniversalEnvelopingAlgebra.centerPBWFiltration and TauCeti.UniversalEnvelopingAlgebra.centerPBWFiltrationPrevious: the PBW filtration restricted to the centre, and its preceding step.
• TauCeti.UniversalEnvelopingAlgebra.CenterPBWGradedPiece: the successive quotients of the restricted filtration.
• TauCeti.UniversalEnvelopingAlgebra.centerPBWGradedToPBWGraded: the PBW symbol of the centre.
• TauCeti.UniversalEnvelopingAlgebra.centerPBWGradedInvariantIso: the isomorphism with the homogeneous Lie invariants S^n(L)^L (TauCeti.SymmetricAlgebra.homogeneousLieInvariant).

Main results

• TauCeti.UniversalEnvelopingAlgebra.centerPBWFiltration_mono and TauCeti.UniversalEnvelopingAlgebra.iSup_centerPBWFiltration_eq_top: the restricted filtration is monotone and exhaustive.
• TauCeti.UniversalEnvelopingAlgebra.centerPBWGradedToPBWGraded_injective: the PBW symbol of the centre is injective.
• TauCeti.UniversalEnvelopingAlgebra.mem_lieInvariants_of_pbwHomogeneousComponentMap_eq_mk: the symbol of a central element is a Lie invariant.
• TauCeti.UniversalEnvelopingAlgebra.centerPBWGradedInvariantIso_symbol and TauCeti.UniversalEnvelopingAlgebra.centerPBWGradedInvariantIso_symm_apply: the isomorphism is the PBW symbol, and its inverse is symmetrization.

References

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

The PBW filtration of the centre

def TauCeti.UniversalEnvelopingAlgebra.centerPBWFiltration (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) : Submodule R ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R L))

The PBW filtration of the centre of U(L): its n-th step consists of the central elements of PBW degree at most n.

def TauCeti.UniversalEnvelopingAlgebra.centerPBWFiltrationPrevious (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) : Submodule R ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R L))

The step preceding degree n in the PBW filtration of the centre: the central elements of PBW degree strictly below n.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mem_centerPBWFiltration {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {n : ℕ} {z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R L))} : z ∈ centerPBWFiltration R L n ↔ ↑z ∈ pbwFiltration R L n

A central element lies in the n-th step of the centre exactly when it has PBW degree at most n in U(L).

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mem_centerPBWFiltrationPrevious {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {n : ℕ} {z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R L))} : z ∈ centerPBWFiltrationPrevious R L n ↔ ↑z ∈ pbwFiltrationPrevious R L n

A central element lies in the step of the centre preceding degree n exactly when it has PBW degree below n in U(L).

theorem TauCeti.UniversalEnvelopingAlgebra.coe_mem_wordFiltration_of_mem_centerPBWFiltration {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {n : ℕ} {z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R L))} (hz : z ∈ centerPBWFiltration R L n) : ↑z ∈ Algebra.wordFiltration (↑(UniversalEnvelopingAlgebra.ι R)) n

A central element of PBW degree at most n lies in the n-th step of the word filtration of U(L).

theorem TauCeti.UniversalEnvelopingAlgebra.centerPBWFiltration_mono (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Monotone (centerPBWFiltration R L)

The PBW filtration of the centre is monotone.

theorem TauCeti.UniversalEnvelopingAlgebra.exists_mem_centerPBWFiltration (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R L))) : ∃ (n : ℕ), z ∈ centerPBWFiltration R L n

Every central element has finite PBW degree: it lies in some step of the PBW filtration of the centre.

theorem TauCeti.UniversalEnvelopingAlgebra.iSup_centerPBWFiltration_eq_top (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : ⨆ (n : ℕ), centerPBWFiltration R L n = ⊤

The PBW filtration of the centre is exhaustive.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.centerPBWFiltrationPrevious_zero (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : centerPBWFiltrationPrevious R L 0 = ⊥

The step of the centre preceding degree zero is trivial.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.centerPBWFiltrationPrevious_succ (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) : centerPBWFiltrationPrevious R L (n + 1) = centerPBWFiltration R L n

In successor degree, the preceding step of the centre is the previous filtration step.

@[reducible, inline]

abbrev TauCeti.UniversalEnvelopingAlgebra.CenterPBWGradedPiece (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) : Type (max u v)

The degree-n successive quotient of the PBW filtration of the centre of U(L).

noncomputable def TauCeti.UniversalEnvelopingAlgebra.centerPBWGradedToPBWGraded (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) : CenterPBWGradedPiece R L n →ₗ[R] PBWGradedPiece R L n

The PBW symbol of the centre: the class of a central element of degree at most n in the degree-n graded piece of U(L).

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.centerPBWGradedToPBWGraded_mk (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {n : ℕ} (z : ↥(centerPBWFiltration R L n)) : (centerPBWGradedToPBWGraded R L n) (Submodule.Quotient.mk z) = Submodule.Quotient.mk ⟨↑↑z, ⋯⟩

The PBW symbol of the class of a central element is the class of that element.

theorem TauCeti.UniversalEnvelopingAlgebra.centerPBWGradedToPBWGraded_injective (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) : Function.Injective ⇑(centerPBWGradedToPBWGraded R L n)

The PBW symbol of the centre is injective: a central element of degree at most n whose degree-n symbol vanishes has degree below n.

The symbols of central elements are Lie invariants

theorem TauCeti.UniversalEnvelopingAlgebra.mem_lieInvariants_of_pbwHomogeneousComponentMap_eq_mk {R : Type} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] {n : ℕ} (hn : IsUnit ↑n.factorial) {z : UniversalEnvelopingAlgebra R L} (hz : z ∈ Subalgebra.center R (UniversalEnvelopingAlgebra R L)) (hzn : z ∈ Algebra.wordFiltration (↑(UniversalEnvelopingAlgebra.ι R)) n) {p : ↥(SymmetricAlgebra.homogeneousSubmodule R L n)} (hp : (pbwHomogeneousComponentMap R L n) p = Submodule.Quotient.mk ⟨z, hzn⟩) : ↑p ∈ SymmetricAlgebra.lieInvariants R L L

The PBW symbol of a central element is a Lie invariant. If z is central of PBW degree at most n and the homogeneous polynomial p ∈ S^n(L) has the degree-n class of z as its PBW image, then p is killed by the adjoint action of L. This needs L free, so that S^n(L) embeds in gr_n U(L), and n! a unit, to symmetrize.

The centre symbols are the homogeneous invariants

noncomputable def TauCeti.UniversalEnvelopingAlgebra.centerPBWGradedInvariantIso (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] (n : ℕ) (hn : IsUnit ↑n.factorial) : CenterPBWGradedPiece R L n ≃ₗ[R] ↥(SymmetricAlgebra.homogeneousLieInvariant R L L n)

The central elements of degree n, modulo those of lower degree, are the homogeneous Lie invariants of degree n, for L free over R and n! a unit in R: the isomorphism Z_n / Z_{n-1} ≃ S^n(L)^L taking a central element to its PBW symbol.

theorem TauCeti.UniversalEnvelopingAlgebra.centerPBWGradedInvariantIso_symbol (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] (n : ℕ) (hn : IsUnit ↑n.factorial) (z : CenterPBWGradedPiece R L n) : (centerPBWGradedToPBWGraded R L n) z = (pbwHomogeneousComponentMap R L n) ⟨↑((centerPBWGradedInvariantIso R L n hn) z), ⋯⟩

The isomorphism Z_n / Z_{n-1} ≃ S^n(L)^L is the PBW symbol: the PBW image of the invariant attached to a class of central elements is the degree-n class of those elements.

theorem TauCeti.UniversalEnvelopingAlgebra.centerPBWGradedInvariantIso_symm_apply (R : Type) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] (n : ℕ) (hn : IsUnit ↑n.factorial) (p : ↥(SymmetricAlgebra.homogeneousLieInvariant R L L n)) : (centerPBWGradedInvariantIso R L n hn).symm p = Submodule.Quotient.mk ⟨⟨(pbwHomogeneousSymmetrization R L n hn) ⟨↑p, ⋯⟩, ⋯⟩, ⋯⟩

The inverse of Z_n / Z_{n-1} ≃ S^n(L)^L is symmetrization: a homogeneous invariant corresponds to the class of its symmetrization, which is central.