Documentation

LeanPool.Ado.Algebra.Lie.UniversalEnveloping.PBW.Ordered

Ordered monomials span the PBW filtration #

Let e : ι → L be a linearly ordered spanning family of a Lie algebra. This file proves that the degree-k Poincaré--Birkhoff--Witt filtration of UniversalEnvelopingAlgebra R L is spanned by the monomials

ι(e(i₁)) ⋯ ι(e(iₙ)),    i₁ ≤ ⋯ ≤ iₙ,    n ≤ k.

There are two steps. First, span_prod_map_eq_wordFiltration expands arbitrary Lie-algebra words in the spanning family. Second, sorting a word in that family changes it only by a term in the preceding filtration step, by pbwMonomial_sub_insertionSort_mem_pbwFiltrationPrevious. Induction on the filtration degree then absorbs this error into shorter ordered monomials.

For an arbitrary Lie homomorphism, the induced enveloping-algebra map sends the ordered monomials in a family, and their span, exactly onto those for the image family.

This is the spanning half of the ordered-monomial basis target in Layer 3 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md. Linear independence, and hence the full PBW basis, still requires the symmetric-algebra comparison.

Main definitions and results #

References #

source
def Ado.UniversalEnvelopingAlgebra.orderedPBWMonomials (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {ι : Type w} [LE ι] (e : ι → L) (k : ℕ) :
Set (UniversalEnvelopingAlgebra R L)

Ordered PBW monomials in a family indexed by an ordered type, of word length at most k.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Ado.UniversalEnvelopingAlgebra.mem_orderedPBWMonomials_iff (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {ι : Type w} [LE ι] (e : ι → L) {k : ℕ} {a : UniversalEnvelopingAlgebra R L} :
    a ∈ orderedPBWMonomials R L e k ↔ ∃ (word : List ι), List.Pairwise (fun (x1 x2 : ι) => x1 ≤ x2) word ∧ word.length ≤ k ∧ pbwMonomial R L e word = a

    Membership in orderedPBWMonomials, in terms of an ordered word of family indices.

    source
    theorem Ado.UniversalEnvelopingAlgebra.pbwMonomial_mem_orderedPBWMonomials (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {ι : Type w} [LE ι] (e : ι → L) {k : ℕ} {word : List ι} (hsorted : List.Pairwise (fun (x1 x2 : ι) => x1 ≤ x2) word) (hword : word.length ≤ k) :
    pbwMonomial R L e word ∈ orderedPBWMonomials R L e k

    An ordered family word of length at most k gives an ordered PBW monomial of degree at most k.

    source
    theorem Ado.UniversalEnvelopingAlgebra.orderedPBWMonomials_mono (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {ι : Type w} [LE ι] (e : ι → L) :
    Monotone (orderedPBWMonomials R L e)

    Increasing the degree bound enlarges the set of ordered PBW monomials.

    source
    theorem Ado.UniversalEnvelopingAlgebra.orderedPBWMonomials_subset_pbwFiltration (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {ι : Type w} [LE ι] (e : ι → L) (k : ℕ) :
    orderedPBWMonomials R L e k ⊆ ↑(pbwFiltration R L k)

    Every ordered PBW monomial of degree at most k lies in the k-th PBW filtration step.

    source
    @[simp]
    theorem Ado.UniversalEnvelopingAlgebra.orderedPBWMonomials_zero (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {ι : Type w} [LE ι] (e : ι → L) :
    orderedPBWMonomials R L e 0 = {1}

    The only ordered PBW monomial of degree zero is the empty monomial 1.

    source
    @[simp]
    theorem Ado.UniversalEnvelopingAlgebra.image_orderedPBWMonomials (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type x} [LieRing M] [LieAlgebra R M] {ι : Type w} [LE ι] (f : L →ₗ⁅R⁆ M) (e : ι → L) (k : ℕ) :
    ⇑(map R f) '' orderedPBWMonomials R L e k = orderedPBWMonomials R M (fun (i : ι) => f (e i)) k

    An induced enveloping-algebra map sends the ordered monomials in a family exactly to the ordered monomials in its image family. This statement does not require the Lie map or the family to be surjective.

    source
    @[simp]
    theorem Ado.UniversalEnvelopingAlgebra.map_span_orderedPBWMonomials (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type x} [LieRing M] [LieAlgebra R M] {ι : Type w} [LE ι] (f : L →ₗ⁅R⁆ M) (e : ι → L) (k : ℕ) :
    Submodule.map (map R f).toLinearMap (Submodule.span R (orderedPBWMonomials R L e k)) = Submodule.span R (orderedPBWMonomials R M (fun (i : ι) => f (e i)) k)

    The induced enveloping-algebra map carries the span of the ordered monomials in a family onto the span of the corresponding ordered monomials in its image family.

    source
    theorem Ado.UniversalEnvelopingAlgebra.span_orderedPBWMonomials_eq_pbwFiltration (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {ι : Type w} [LinearOrder ι] (e : ι → L) (he : Submodule.span R (Set.range e) = ⊤) (k : ℕ) :
    Submodule.span R (orderedPBWMonomials R L e k) = pbwFiltration R L k

    Ordered PBW monomials span the PBW filtration. For a linearly ordered spanning family e in L, the monomials in nondecreasing family elements of length at most k span precisely filtration degree k of UniversalEnvelopingAlgebra R L.

    This is the spanning half of PBW. The reverse information needed for a basis is linear independence, which comes from identifying the associated graded algebra with SymmetricAlgebra R L.

    source
    theorem Ado.UniversalEnvelopingAlgebra.span_iUnion_orderedPBWMonomials_eq_top (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {ι : Type w} [LinearOrder ι] (e : ι → L) (he : Submodule.span R (Set.range e) = ⊤) :
    Submodule.span R (⋃ (k : ℕ), orderedPBWMonomials R L e k) = ⊤

    The ordered PBW monomials in a linearly ordered spanning family span the whole universal enveloping algebra.