Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.PBW.AssociatedGraded

The symmetric-algebra map to the associated graded of an enveloping algebra #

For a Lie algebra L over a commutative ring R, the defining relation in its universal enveloping algebra says

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

The right-hand side has PBW filtration degree one, so the degree-one classes of ι(x) and ι(y) commute in the associated graded. Consequently the tensor-algebra map generated by these classes factors through SymmetricAlgebra R L. This file constructs the resulting canonical map

SymmetricAlgebra R L →ₐ[R] gr U(L)

and computes it on products of generators: a product of n symmetric generators is the degree-n class of the corresponding word of Lie generators. That computation is the spanning half of PBW read in the associated graded; it is turned into surjectivity, degree by degree, in TauCeti.Algebra.Lie.UniversalEnveloping.PBW.Homogeneous.

Under the standard hypotheses ensuring PBW over a commutative ring, such as projectivity of L as an R-module, injectivity of this map is the remaining PBW theorem. Once established in the roadmap's general-field setting, the resulting associated-graded isomorphism feeds the triangular decomposition and the construction of Verma modules.

Main definitions and results #

References #

This is the associated-graded-map stage of Layer 3, “PBW, a substantial sub-project”, in the highest-weight roadmap.

source
@[reducible, inline]
abbrev TauCeti.UniversalEnvelopingAlgebra.PBWGradedPiece (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) :
Type (max u v)

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

Equations
Instances For
    source
    @[reducible, inline]
    abbrev TauCeti.UniversalEnvelopingAlgebra.PBWAssociatedGraded (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
    Type (max u v)

    The associated graded of the PBW filtration of U(L).

    Equations
    Instances For
      source
      noncomputable def TauCeti.UniversalEnvelopingAlgebra.pbwGradedGenerator (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
      L →ₗ[R] PBWAssociatedGraded R L

      The degree-one class of the canonical Lie generator in the PBW associated graded.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.UniversalEnvelopingAlgebra.pbwGradedGenerator_apply (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) :
        (pbwGradedGenerator R L) x = (DirectSum.of (PBWGradedPiece R L) 1) (Submodule.Quotient.mk ⟨(UniversalEnvelopingAlgebra.ι R) x, ⋯⟩)

        The PBW graded generator is the degree-one quotient class of ι(x).

        source
        theorem TauCeti.UniversalEnvelopingAlgebra.mul_sub_mul_mem_pbwFiltrationPrevious (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 - y * x ∈ pbwFiltrationPrevious R L (i + j)

        Commutators lower PBW degree. If x and y have PBW filtration degrees at most i and j, respectively, then x * y - y * x has degree strictly below i + j.

        This is the filtered form of the fact that gr U(L) is commutative.

        source
        theorem TauCeti.UniversalEnvelopingAlgebra.pbwGradedMul_comm (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (i j : ℕ) (x : PBWGradedPiece R L i) (y : PBWGradedPiece R L j) :
        cast ⋯ (((Algebra.wordFiltration.gradedMul (↑(UniversalEnvelopingAlgebra.ι R)) i j) x) y) = ((Algebra.wordFiltration.gradedMul (↑(UniversalEnvelopingAlgebra.ι R)) j i) y) x

        Multiplication of PBW homogeneous pieces is commutative after reindexing the degree.

        source
        @[instance_reducible]
        noncomputable instance TauCeti.UniversalEnvelopingAlgebra.pbwGradedGCommRing (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
        DirectSum.GCommRing (PBWGradedPiece R L)

        The homogeneous PBW pieces form a graded commutative ring.

        Equations
        source
        @[instance_reducible]
        noncomputable instance TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedCommRing (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
        CommRing (PBWAssociatedGraded R L)

        The PBW associated graded is commutative.

        Equations
        source
        noncomputable def TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
        SymmetricAlgebra R L →ₐ[R] PBWAssociatedGraded R L

        The canonical algebra map from the symmetric algebra to the PBW associated graded.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) :
          (pbwAssociatedGradedMap R L) ((SymmetricAlgebra.ι R L) x) = (pbwGradedGenerator R L) x

          The canonical map sends a symmetric-algebra generator to its degree-one PBW class.

          source
          @[simp]
          theorem TauCeti.UniversalEnvelopingAlgebra.prod_map_pbwGradedGenerator (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (l : List L) :
          (List.map (⇑(pbwGradedGenerator R L)) l).prod = (DirectSum.of (PBWGradedPiece R L) l.length) (Submodule.Quotient.mk ⟨(List.map (⇑(UniversalEnvelopingAlgebra.ι R)) l).prod, ⋯⟩)

          A product of degree-one PBW classes is the class of the corresponding word of canonical Lie generators, in the degree given by the length of the word.

          source
          @[simp]
          theorem TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap_prod_map_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (l : List L) :
          (pbwAssociatedGradedMap R L) (List.map (⇑(SymmetricAlgebra.ι R L)) l).prod = (DirectSum.of (PBWGradedPiece R L) l.length) (Submodule.Quotient.mk ⟨(List.map (⇑(UniversalEnvelopingAlgebra.ι R)) l).prod, ⋯⟩)

          The canonical map sends a product of symmetric-algebra generators to the class of the corresponding word of Lie generators, in the degree given by the length of the word.