Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.PBW.Decomposition

PBW decomposition relative to a Lie subalgebra #

An ordered basis of a complement of a Lie subalgebra, followed by an ordered basis of the subalgebra, gives a PBW basis whose monomials factor in that order. If the complement is itself a Lie subalgebra, multiplication identifies the tensor product of the two enveloping algebras with the enveloping algebra of the ambient Lie algebra as modules. The subalgebras need not commute, so this is a linear equivalence. This is the algebraic input to triangular decomposition and to induced highest weight modules.

References #

source
noncomputable def LieSubalgebra.relativePBWBasis {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (B : LieSubalgebra R L) {A : Submodule R L} (hA : IsCompl A B.toSubmodule) {ιA : Type w₁} {ιB : Type w₂} (bA : Module.Basis ιA R ↥A) (bB : Module.Basis ιB R ↥B) [LinearOrder ιA] [LinearOrder ιB] :
Module.Basis ((ιA →₀ ℕ) × (ιB →₀ ℕ)) R (UniversalEnvelopingAlgebra R L)

The PBW basis indexed separately by the exponents on a complement and on the subalgebra. Its values are the products described by relativePBWBasis_apply.

Equations
Instances For
    source
    theorem LieSubalgebra.relativePBWBasis_apply {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (B : LieSubalgebra R L) {A : Submodule R L} (hA : IsCompl A B.toSubmodule) {ιA : Type w₁} {ιB : Type w₂} (bA : Module.Basis ιA R ↥A) (bB : Module.Basis ιB R ↥B) [LinearOrder ιA] [LinearOrder ιB] (α : ιA →₀ ℕ) (β : ιB →₀ ℕ) :
    (B.relativePBWBasis hA bA bB) (α, β) = TauCeti.UniversalEnvelopingAlgebra.pbwMonomial R L (fun (i : ιA) => ↑(bA i)) ((Finsupp.toMultiset α).sort fun (x1 x2 : ιA) => x1 ≤ x2) * (TauCeti.UniversalEnvelopingAlgebra.map R B.incl) (bB.pbwBasis β)

    A relative PBW basis vector is an ordered complement monomial times a subalgebra monomial.

    source
    noncomputable def LieSubalgebra.mulMap {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (A B : LieSubalgebra R L) :
    TensorProduct R (UniversalEnvelopingAlgebra R ↥A) (UniversalEnvelopingAlgebra R ↥B) →ₗ[R] UniversalEnvelopingAlgebra R L

    Multiply the images of two enveloping algebras inside the ambient enveloping algebra.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem LieSubalgebra.mulMap_tmul {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (A B : LieSubalgebra R L) (a : UniversalEnvelopingAlgebra R ↥A) (b : UniversalEnvelopingAlgebra R ↥B) :
      (A.mulMap B) (a ⊗ₜ[R] b) = (TauCeti.UniversalEnvelopingAlgebra.map R A.incl) a * (TauCeti.UniversalEnvelopingAlgebra.map R B.incl) b

      On pure tensors the multiplication map is multiplication in the ambient algebra.

      source
      theorem LieSubalgebra.mulMap_bijective {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (A B : LieSubalgebra R L) (h : IsCompl A.toSubmodule B.toSubmodule) [Module.Free R ↥A] [Module.Free R ↥B] :
      Function.Bijective ⇑(A.mulMap B)

      Multiplication is bijective when two free Lie subalgebras complement each other as modules. There are no characteristic or finite-dimensionality assumptions.

      source
      noncomputable def LieSubalgebra.mulEquiv {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (A B : LieSubalgebra R L) (h : IsCompl A.toSubmodule B.toSubmodule) [Module.Free R ↥A] [Module.Free R ↥B] :
      TensorProduct R (UniversalEnvelopingAlgebra R ↥A) (UniversalEnvelopingAlgebra R ↥B) ≃ₗ[R] UniversalEnvelopingAlgebra R L

      The relative PBW decomposition: multiplication identifies the tensor product of the enveloping algebras of complementary free Lie subalgebras with the ambient enveloping algebra.

      Equations
      Instances For
        source
        @[simp]
        theorem LieSubalgebra.mulEquiv_tmul {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (A B : LieSubalgebra R L) (h : IsCompl A.toSubmodule B.toSubmodule) [Module.Free R ↥A] [Module.Free R ↥B] (a : UniversalEnvelopingAlgebra R ↥A) (b : UniversalEnvelopingAlgebra R ↥B) :
        (A.mulEquiv B h) (a ⊗ₜ[R] b) = (TauCeti.UniversalEnvelopingAlgebra.map R A.incl) a * (TauCeti.UniversalEnvelopingAlgebra.map R B.incl) b

        The relative PBW equivalence is normalized by multiplication of the two factors.

        source
        @[simp]
        theorem LieSubalgebra.mulEquiv_symm_mul {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (A B : LieSubalgebra R L) (h : IsCompl A.toSubmodule B.toSubmodule) [Module.Free R ↥A] [Module.Free R ↥B] (a : UniversalEnvelopingAlgebra R ↥A) (b : UniversalEnvelopingAlgebra R ↥B) :
        (A.mulEquiv B h).symm ((TauCeti.UniversalEnvelopingAlgebra.map R A.incl) a * (TauCeti.UniversalEnvelopingAlgebra.map R B.incl) b) = a ⊗ₜ[R] b

        The inverse relative PBW equivalence recovers the tensor factors of a product.