The PBW filtration of a universal enveloping algebra

This file constructs the first stage of the Poincaré--Birkhoff--Witt development: the increasing filtration of UniversalEnvelopingAlgebra R L by word length in the image of the canonical Lie map UniversalEnvelopingAlgebra.ι R.

The defining relation

ι(x) * ι(y) = ι(y) * ι(x) + ι([x,y])

replaces a degree-two commutator by a degree-one term. Thus word length gives a filtration, not a grading. The associated graded will use this degree drop to make the leading symbols commute; that comparison with SymmetricAlgebra R L is the next PBW stage and is not asserted here.

Nothing in the construction is special to the enveloping algebra: pbwFiltration and pbwFiltrationPrevious are Ado.Algebra.wordFiltration and Ado.Algebra.wordFiltrationPrevious of TauCeti/Algebra/WordFiltration/Basic.lean, specialized to UniversalEnvelopingAlgebra.ι R, exactly as CliffordAlgebra.filtration is that same construction for CliffordAlgebra.ι. What is special to U(L) is the exhaustivity, which comes from the tensor-algebra presentation.

Main definitions and results

• Ado.UniversalEnvelopingAlgebra.pbwFiltration: words of length at most k in the range of UniversalEnvelopingAlgebra.ι R.
• Ado.UniversalEnvelopingAlgebra.pbwFiltration_eq_pow: its defining equation as the power of the scalar-and-generator submodule.
• Ado.UniversalEnvelopingAlgebra.pbwFiltration_mul: multiplication adds degrees.
• Ado.UniversalEnvelopingAlgebra.pbwFiltration_zero and Ado.UniversalEnvelopingAlgebra.pbwFiltration_one: the scalar and generator steps.
• Ado.UniversalEnvelopingAlgebra.adjoin_image_ι_eq_top: the image of any Lie generating set generates U(L) as an R-algebra.
• Ado.UniversalEnvelopingAlgebra.iSup_pbwFiltration_eq_top: the filtration is exhaustive.
• Ado.UniversalEnvelopingAlgebra.exists_mem_pbwFiltration: exhaustivity read elementwise.
• Ado.UniversalEnvelopingAlgebra.instIsRingFiltration: the bundled IsRingFiltration structure on pbwFiltration, with pbwFiltrationPrevious as its preceding-step family.

References

This is the pinned "the PBW filtration" target of Layer 3, "PBW, a substantial sub-project", of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Chapter V, §17.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapter I, §2.7.

def Ado.UniversalEnvelopingAlgebra.pbwFiltration (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : Submodule R (UniversalEnvelopingAlgebra R L)

The PBW filtration on U(L): its k-th step is spanned by products of at most k canonical Lie generators.

This is Ado.Algebra.wordFiltration specialized to UniversalEnvelopingAlgebra.ι R; the shared API is in TauCeti/Algebra/WordFiltration/Basic.lean.

Equations

• Ado.UniversalEnvelopingAlgebra.pbwFiltration R L k = Ado.Algebra.wordFiltration (↑(UniversalEnvelopingAlgebra.ι R)) k

theorem Ado.UniversalEnvelopingAlgebra.pbwFiltration_def (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : pbwFiltration R L k = Algebra.wordFiltration (↑(UniversalEnvelopingAlgebra.ι R)) k

The PBW filtration is the word filtration generated by the canonical Lie map.

theorem Ado.UniversalEnvelopingAlgebra.pbwFiltration_eq_pow (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : pbwFiltration R L k = (1 ⊔ (↑(UniversalEnvelopingAlgebra.ι R)).range) ^ k

PBW filtration degree k is the k-th power of the scalars and canonical Lie generators.

def Ado.UniversalEnvelopingAlgebra.pbwFiltrationPrevious (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : ℕ → Submodule R (UniversalEnvelopingAlgebra R L)

The step preceding degree k in the PBW filtration, that is Ado.Algebra.wordFiltrationPrevious specialized to UniversalEnvelopingAlgebra.ι R, with bottom in degree zero.

Equations

• Ado.UniversalEnvelopingAlgebra.pbwFiltrationPrevious R L = Ado.Algebra.wordFiltrationPrevious ↑(UniversalEnvelopingAlgebra.ι R)

theorem Ado.UniversalEnvelopingAlgebra.pbwFiltrationPrevious_def (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : pbwFiltrationPrevious R L k = Algebra.wordFiltrationPrevious (↑(UniversalEnvelopingAlgebra.ι R)) k

The preceding PBW filtration is the preceding word filtration of the canonical Lie map.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.pbwFiltrationPrevious_zero (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : pbwFiltrationPrevious R L 0 = ⊥

The preceding PBW filtration is trivial in degree zero.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.pbwFiltrationPrevious_succ (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : pbwFiltrationPrevious R L (k + 1) = pbwFiltration R L k

In successor degree, the preceding PBW filtration is the previous filtration step.

theorem Ado.UniversalEnvelopingAlgebra.prod_map_ι_mem_pbwFiltration (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {k : ℕ} {l : List L} (hl : l.length ≤ k) : (List.map (⇑(UniversalEnvelopingAlgebra.ι R)) l).prod ∈ pbwFiltration R L k

A word of at most k canonical Lie generators lies in PBW filtration degree k.

theorem Ado.UniversalEnvelopingAlgebra.pbwFiltration_le_iff (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {k : ℕ} {p : Submodule R (UniversalEnvelopingAlgebra R L)} : pbwFiltration R L k ≤ p ↔ ∀ (l : List L), l.length ≤ k → (List.map (⇑(UniversalEnvelopingAlgebra.ι R)) l).prod ∈ p

A submodule contains the k-th PBW filtration step exactly when it contains every word of length at most k in the canonical Lie generators.

theorem Ado.UniversalEnvelopingAlgebra.pbwFiltration_mono (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Monotone (pbwFiltration R L)

The PBW filtration is increasing.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.pbwFiltration_zero (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : pbwFiltration R L 0 = 1

PBW filtration degree zero consists of scalars.

theorem Ado.UniversalEnvelopingAlgebra.one_mem_pbwFiltration (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : 1 ∈ pbwFiltration R L k

The empty word puts 1 in every PBW filtration step.

theorem Ado.UniversalEnvelopingAlgebra.algebraMap_mem_pbwFiltration (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (r : R) (k : ℕ) : (algebraMap R (UniversalEnvelopingAlgebra R L)) r ∈ pbwFiltration R L k

Scalars belong to every PBW filtration step.

theorem Ado.UniversalEnvelopingAlgebra.ι_mem_pbwFiltration_one (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) : (UniversalEnvelopingAlgebra.ι R) x ∈ pbwFiltration R L 1

A canonical Lie generator has PBW filtration degree at most one.

theorem Ado.UniversalEnvelopingAlgebra.ι_range_le_pbwFiltration_one (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : (↑(UniversalEnvelopingAlgebra.ι R)).range ≤ pbwFiltration R L 1

The range of the canonical Lie map lies in the first PBW filtration step.

theorem Ado.UniversalEnvelopingAlgebra.pbwFiltration_mul (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (i j : ℕ) : pbwFiltration R L i * pbwFiltration R L j = pbwFiltration R L (i + j)

Multiplication adds PBW filtration degrees.

theorem Ado.UniversalEnvelopingAlgebra.mul_mem_pbwFiltration (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {i j : ℕ} {x y : UniversalEnvelopingAlgebra R L} (hx : x ∈ pbwFiltration R L i) (hy : y ∈ pbwFiltration R L j) : x * y ∈ pbwFiltration R L (i + j)

The elementwise multiplicativity of the PBW filtration.

theorem Ado.UniversalEnvelopingAlgebra.mul_mem_pbwFiltrationPrevious_left (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {i j : ℕ} {x y : UniversalEnvelopingAlgebra R L} (hx : x ∈ pbwFiltrationPrevious R L i) (hy : y ∈ pbwFiltration R L j) : x * y ∈ pbwFiltrationPrevious R L (i + j)

Multiplication preserves a strict degree drop in the left factor of the PBW filtration.

theorem Ado.UniversalEnvelopingAlgebra.mul_mem_pbwFiltrationPrevious_right (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {i j : ℕ} {x y : UniversalEnvelopingAlgebra R L} (hx : x ∈ pbwFiltration R L i) (hy : y ∈ pbwFiltrationPrevious R L j) : x * y ∈ pbwFiltrationPrevious R L (i + j)

Multiplication preserves a strict degree drop in the right factor of the PBW filtration.

theorem Ado.UniversalEnvelopingAlgebra.pbwFiltration_pow (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (i n : ℕ) : pbwFiltration R L i ^ n = pbwFiltration R L (i * n)

Iterating pbwFiltration_mul: the n-th submodule power of the i-th step is the i * n-th step.

theorem Ado.UniversalEnvelopingAlgebra.pbwFiltration_eq_iSup_pow (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : pbwFiltration R L k = ⨆ (i : { i : ℕ // i ≤ k }), (↑(UniversalEnvelopingAlgebra.ι R)).range ^ ↑i

The k-th PBW filtration step is the supremum of the powers of the canonical generator range of degree at most k.

theorem Ado.UniversalEnvelopingAlgebra.pbwFiltration_succ_eq_sup (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : pbwFiltration R L (k + 1) = pbwFiltration R L k ⊔ (↑(UniversalEnvelopingAlgebra.ι R)).range ^ (k + 1)

The successor PBW step adjoins words of exactly the new degree.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.pbwFiltration_one (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : pbwFiltration R L 1 = 1 ⊔ (↑(UniversalEnvelopingAlgebra.ι R)).range

PBW filtration degree one consists of the scalars and the canonical Lie generators.

theorem Ado.UniversalEnvelopingAlgebra.adjoin_image_ι_eq_top (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {S : Set L} (hS : LieSubalgebra.lieSpan R L S = ⊤) : Algebra.adjoin R (⇑(UniversalEnvelopingAlgebra.ι R) '' S) = ⊤

A Lie generating set generates the enveloping algebra. If S generates L as a Lie algebra, then the image of S under the canonical map generates U(L) as an R-algebra.

Only the associative subalgebra generated by the image is involved, so no linear independence or finiteness of S is needed.

theorem Ado.UniversalEnvelopingAlgebra.iSup_pbwFiltration_eq_top (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : ⨆ (k : ℕ), pbwFiltration R L k = ⊤

The PBW filtration is exhaustive. The canonical generators generate U(L) as an algebra, so every element is a combination of words of some finite length.

theorem Ado.UniversalEnvelopingAlgebra.exists_mem_pbwFiltration (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (a : UniversalEnvelopingAlgebra R L) : ∃ (k : ℕ), a ∈ pbwFiltration R L k

Every element of the enveloping algebra lies in some PBW filtration step, the elementwise form of Ado.UniversalEnvelopingAlgebra.iSup_pbwFiltration_eq_top.

instance Ado.UniversalEnvelopingAlgebra.instIsRingFiltration (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : IsRingFiltration (pbwFiltration R L) (pbwFiltrationPrevious R L)

The PBW filtration carries Mathlib's bundled ring-filtration structure.