The PBW Rees algebra

The PBW Rees algebra consists of polynomials in a central parameter whose coefficient of parameter degree n lies in PBW filtration degree at most n. It retains the filtration inside the polynomial ring over the possibly noncommutative enveloping algebra.

We use TauCeti.coeffSubalgebra, so its grading, homogeneous components, and the linear equivalence between its degree n piece and the n-th filtration step are available directly from TauCeti.coeffSubalgebra.grade, coe_decompose_apply, and gradeEquiv. The coefficientwise membership test is TauCeti.mem_coeffSubalgebra_iff. The shared parameter API is TauCeti.coeffSubalgebra.commute_X, X_mul_injective, and coe_algebraMap; scalar evaluation is TauCeti.coeffSubalgebra.eval. Since reesParameter unfolds to the shared parameter, TauCeti.coeffSubalgebra.span_X_isTwoSided makes the ideal it generates two-sided.

The parameter is central and multiplication by it is injective. The linear generators j(x) = ι(x)t satisfy j(x)j(y) - j(y)j(x) = t j([x,y]). Evaluation at parameter one surjects onto the enveloping algebra. These constructions require neither a basis nor characteristic zero.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §17, for the PBW filtration and the defining enveloping-algebra relation.
• J. Dixmier, Enveloping Algebras, for the Rees construction of a filtered enveloping algebra.

@[reducible, inline]

abbrev TauCeti.UniversalEnvelopingAlgebra.reesAlgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Subalgebra R (Polynomial (UniversalEnvelopingAlgebra R L))

The PBW Rees algebra: the coefficient of tⁿ belongs to PBW filtration degree n.

@[reducible, inline]

noncomputable abbrev TauCeti.UniversalEnvelopingAlgebra.reesParameter (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : ↥(reesAlgebra R L)

The central deformation parameter of the PBW Rees algebra.

@[instance_reducible]

noncomputable instance TauCeti.UniversalEnvelopingAlgebra.instAlgebraPolynomialSubtypeUniversalEnvelopingAlgebraMemSubalgebraReesAlgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Algebra (Polynomial R) ↥(reesAlgebra R L)

The PBW Rees algebra is an algebra over the polynomial parameter ring.

instance TauCeti.UniversalEnvelopingAlgebra.instIsScalarTowerPolynomialSubtypeUniversalEnvelopingAlgebraMemSubalgebraReesAlgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : IsScalarTower R (Polynomial R) ↥(reesAlgebra R L)

The parameter-ring algebra structure extends the original coefficient-ring structure.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.reesGenerator (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : L →ₗ[R] ↥(reesAlgebra R L)

The linear Rees generator j(x) = ι(x)t.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_reesGenerator (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) : ↑((reesGenerator R L) x) = (Polynomial.monomial 1) ((UniversalEnvelopingAlgebra.ι R) x)

theorem TauCeti.UniversalEnvelopingAlgebra.reesGenerator_mul_sub_mul (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x y : L) : (reesGenerator R L) x * (reesGenerator R L) y - (reesGenerator R L) y * (reesGenerator R L) x = reesParameter R L * (reesGenerator R L) ⁅x, y⁆

The commutator of Rees generators has one factor of the deformation parameter.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.eval_reesGenerator (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (r : R) (x : L) : (coeffSubalgebra.eval (pbwFiltration R L) r) ((reesGenerator R L) x) = r • (UniversalEnvelopingAlgebra.ι R) x

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.evalOne_reesGenerator (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) : (coeffSubalgebra.evalOne (pbwFiltration R L)) ((reesGenerator R L) x) = (UniversalEnvelopingAlgebra.ι R) x

theorem TauCeti.UniversalEnvelopingAlgebra.reesAlgebra_evalOne_surjective (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Function.Surjective ⇑(coeffSubalgebra.evalOne (pbwFiltration R L))

Every enveloping-algebra element is the value at parameter one of a Rees polynomial.

theorem TauCeti.UniversalEnvelopingAlgebra.reesParameter_mem_grade_one (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : reesParameter R L ∈ coeffSubalgebra.grade (pbwFiltration R L) 1

The deformation parameter belongs to the degree-one piece.

theorem TauCeti.UniversalEnvelopingAlgebra.reesGenerator_mem_grade_one (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) : (reesGenerator R L) x ∈ coeffSubalgebra.grade (pbwFiltration R L) 1

Each linear Rees generator belongs to the degree-one piece.

theorem TauCeti.UniversalEnvelopingAlgebra.grade_one_eq_span_reesParameter_union_range_reesGenerator (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : coeffSubalgebra.grade (pbwFiltration R L) 1 = Submodule.span R ({reesParameter R L} ∪ Set.range ⇑(reesGenerator R L))

The degree-one piece is spanned by the parameter and the linear Rees generators.

theorem TauCeti.UniversalEnvelopingAlgebra.adjoin_reesParameter_union_range_reesGenerator (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Algebra.adjoin R ({reesParameter R L} ∪ Set.range ⇑(reesGenerator R L)) = ⊤

The parameter and the linear Rees generators generate the PBW Rees algebra over R.

theorem TauCeti.UniversalEnvelopingAlgebra.adjoin_range_reesGenerator (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Algebra.adjoin (Polynomial R) (Set.range ⇑(reesGenerator R L)) = ⊤

Over the parameter ring, the linear Rees generators alone generate the Rees algebra.