Permuting PBW words modulo lower filtration

This file proves the first consequence of the defining relation of a universal enveloping algebra for its associated graded. If two words in the canonical generators differ only by a permutation, then their difference has filtration degree strictly below their common word length. In particular, the leading term of a word is unchanged when the word is sorted.

An adjacent exchange is the mathematical heart of the proof:

ι(x) * ι(y) - ι(y) * ι(x) = ι([x,y]).

The left side has word length two while the right side has word length one. Multiplying by the unchanged suffix preserves this one-degree drop. Induction on List.Perm then gives the result for an arbitrary permutation.

Main definitions and results

• Ado.UniversalEnvelopingAlgebra.pbwMonomial: the product of a word in a chosen family of Lie-algebra elements.
• Ado.UniversalEnvelopingAlgebra.map_pbwMonomial: induced maps act factorwise on PBW monomials.
• Ado.UniversalEnvelopingAlgebra.prod_map_ι_sub_prod_map_ι_mem_pbwFiltrationPrevious_of_perm: permuted words in canonical generators differ by a lower-filtration term.
• pbwMonomial_sub_pbwMonomial_mem_pbwFiltrationPrevious_of_perm: the same statement for words in an indexed family.
• Ado.UniversalEnvelopingAlgebra.pbwMonomial_sub_insertionSort_mem_pbwFiltrationPrevious: every word has the same leading term as its ordered version.

This is the first part of the associated-graded-map target in Layer 3, "PBW, a substantial sub-project", of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md. The next stage uses these permutation-invariant leading terms to define the map from SymmetricAlgebra R L to the associated graded of U(L).

References

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

theorem Ado.UniversalEnvelopingAlgebra.prod_map_ι_sub_prod_map_ι_mem_pbwFiltrationPrevious_of_perm (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {l₁ l₂ : List L} (h : l₁.Perm l₂) : (List.map (⇑(UniversalEnvelopingAlgebra.ι R)) l₁).prod - (List.map (⇑(UniversalEnvelopingAlgebra.ι R)) l₂).prod ∈ pbwFiltrationPrevious R L l₁.length

Permuting a word does not change its leading PBW term. The products of two permuted lists of canonical generators differ by an element of degree strictly below their common length.

def Ado.UniversalEnvelopingAlgebra.pbwMonomial (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {ιIndex : Type w} (e : ιIndex → L) (word : List ιIndex) : UniversalEnvelopingAlgebra R L

The PBW monomial attached to a word of indices in a family e : ιIndex → L. No ordering or linear-independence hypothesis on the family is needed.

Equations

• Ado.UniversalEnvelopingAlgebra.pbwMonomial R L e word = (List.map (⇑(UniversalEnvelopingAlgebra.ι R)) (List.map e word)).prod

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.pbwMonomial_nil (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {ιIndex : Type w} (e : ιIndex → L) : pbwMonomial R L e [] = 1

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.pbwMonomial_cons (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {ιIndex : Type w} (e : ιIndex → L) (i : ιIndex) (word : List ιIndex) : pbwMonomial R L e (i :: word) = (UniversalEnvelopingAlgebra.ι R) (e i) * pbwMonomial R L e word

theorem Ado.UniversalEnvelopingAlgebra.pbwMonomial_def (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {ιIndex : Type w} (e : ιIndex → L) (word : List ιIndex) : pbwMonomial R L e word = (List.map (⇑(UniversalEnvelopingAlgebra.ι R)) (List.map e word)).prod

A PBW monomial is the product of the corresponding canonical Lie generators.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.map_pbwMonomial {ιIndex : Type w} (S : Type u) [CommRing S] {A : Type v} {B : Type x} [LieRing A] [LieAlgebra S A] [LieRing B] [LieAlgebra S B] (f : A →ₗ⁅S⁆ B) (e : ιIndex → A) (word : List ιIndex) : (map S f) (pbwMonomial S A e word) = pbwMonomial S B (fun (i : ιIndex) => f (e i)) word

An induced enveloping-algebra map applies the Lie homomorphism to every factor of a PBW monomial.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.pbwMonomial_append (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {ιIndex : Type w} (e : ιIndex → L) (word₁ word₂ : List ιIndex) : pbwMonomial R L e (word₁ ++ word₂) = pbwMonomial R L e word₁ * pbwMonomial R L e word₂

theorem Ado.UniversalEnvelopingAlgebra.pbwMonomial_mem_pbwFiltration (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {ιIndex : Type w} (e : ιIndex → L) (word : List ιIndex) : pbwMonomial R L e word ∈ pbwFiltration R L word.length

A PBW monomial belongs to the filtration step given by the length of its word.

theorem Ado.UniversalEnvelopingAlgebra.pbwMonomial_sub_pbwMonomial_mem_pbwFiltrationPrevious_of_perm (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {ιIndex : Type w} (e : ιIndex → L) {word₁ word₂ : List ιIndex} (h : word₁.Perm word₂) : pbwMonomial R L e word₁ - pbwMonomial R L e word₂ ∈ pbwFiltrationPrevious R L word₁.length

Permuted words in any indexed family give PBW monomials with the same leading term.

theorem Ado.UniversalEnvelopingAlgebra.pbwMonomial_sub_insertionSort_mem_pbwFiltrationPrevious (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {ιIndex : Type w} (r : ιIndex → ιIndex → Prop) [DecidableRel r] (e : ιIndex → L) (word : List ιIndex) : pbwMonomial R L e word - pbwMonomial R L e (List.insertionSort r word) ∈ pbwFiltrationPrevious R L word.length

Sorting the indices of a PBW monomial by a decidable relation preserves its leading term. This is the form used to span the associated graded by ordered monomials.