Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.Triangular

Factorizations of the universal enveloping algebra #

Let L be a finite-dimensional Killing-semisimple Lie algebra in characteristic zero, with a splitting Cartan subalgebra H and a base of its root system. The spanning statements identify U(n⁻) Β· U(π”Ÿ) and U(n⁻) Β· U(H) Β· U(n⁺) with U(L), where each factor is viewed as a subalgebra of U(L).

For the Borel algebra, the sharper tensor decomposition is available: borelMulEquiv is the linear equivalence U(H) βŠ— U(n⁺) ≃ U(π”Ÿ) given by multiplication. It has forward and inverse computation rules on products. This factorization separates the Cartan part from the positive root operators in triangular decomposition and highest weight constructions.

Combined with the decomposition L = n⁻ βŠ• π”Ÿ, it gives the triangular decomposition triangularMulEquiv : U(n⁻) βŠ— (U(H) βŠ— U(n⁺)) ≃ U(L), f βŠ— h βŠ— e ↦ f h e: every element of U(L) is uniquely a sum of such ordered products, up to the relations of the tensor product. Its inverse is what the Harish-Chandra projection U(L) β†’ U(H) is built from.

References #

source
theorem TauCeti.UniversalEnvelopingAlgebra.negativeNilradical_mul_borelSubalgebra_eq_top {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (β†₯H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) :
Subalgebra.toSubmodule (envelopingSubalgebra K (negativeNilradical H b)) * Subalgebra.toSubmodule (envelopingSubalgebra K (borelSubalgebra H b)) = ⊀

U(n⁻) Β· U(π”Ÿ) = U(L): the enveloping algebra of L is spanned by the products of the enveloping subalgebra of the negative nilradical with that of the Borel subalgebra.

This is the enveloping-algebra form of the spanning statement L = n⁻ + π”Ÿ (TauCeti.negativeNilradical_sup_borelSubalgebra_eq_top); it does not assert that the factors of a product are determined by it.

source
theorem TauCeti.UniversalEnvelopingAlgebra.cartan_mul_positiveNilradical_eq_envelopingSubalgebra_borelSubalgebra {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (β†₯H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) :
Subalgebra.toSubmodule (envelopingSubalgebra K H) * Subalgebra.toSubmodule (envelopingSubalgebra K (positiveNilradical H b)) = Subalgebra.toSubmodule (envelopingSubalgebra K (borelSubalgebra H b))

U(H) Β· U(n⁺) = U(π”Ÿ): the enveloping subalgebra of the Borel subalgebra is spanned by the products of the enveloping subalgebra of the Cartan subalgebra with that of the positive nilradical.

source
theorem TauCeti.UniversalEnvelopingAlgebra.negativeNilradical_mul_cartan_mul_positiveNilradical_eq_top {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (β†₯H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) :
Subalgebra.toSubmodule (envelopingSubalgebra K (negativeNilradical H b)) * Subalgebra.toSubmodule (envelopingSubalgebra K H) * Subalgebra.toSubmodule (envelopingSubalgebra K (positiveNilradical H b)) = ⊀

The triangular decomposition of U(L), in its spanning form: U(n⁻) · U(H) · U(n⁺) = U(L).

Every element of U(L) is a sum of products f Β· h Β· e with f in the subalgebra generated by the negative root vectors, h in the subalgebra generated by the Cartan subalgebra, and e in the subalgebra generated by the positive root vectors. Uniqueness of such an expression is the PoincarΓ©--Birkhoff--Witt half and is not claimed.

source
noncomputable def TauCeti.UniversalEnvelopingAlgebra.borelMulEquiv {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (β†₯H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) :
TensorProduct K (UniversalEnvelopingAlgebra K β†₯H) (UniversalEnvelopingAlgebra K β†₯(positiveNilradical H b)) ≃ₗ[K] UniversalEnvelopingAlgebra K β†₯(borelSubalgebra H b)

Multiplication identifies the Cartan and positive enveloping factors with the Borel enveloping algebra.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.borelMulEquiv_tmul {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (β†₯H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (h : UniversalEnvelopingAlgebra K β†₯H) (n : UniversalEnvelopingAlgebra K β†₯(positiveNilradical H b)) :
    (borelMulEquiv H b) (h βŠ—β‚œ[K] n) = (map K (LieSubalgebra.inclusion β‹―)) h * (map K (LieSubalgebra.inclusion β‹―)) n

    The Borel decomposition sends a pure tensor to the ordered product of its two images.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.borelMulEquiv_symm_mul {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (β†₯H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (h : UniversalEnvelopingAlgebra K β†₯H) (n : UniversalEnvelopingAlgebra K β†₯(positiveNilradical H b)) :
    (borelMulEquiv H b).symm ((map K (LieSubalgebra.inclusion β‹―)) h * (map K (LieSubalgebra.inclusion β‹―)) n) = h βŠ—β‚œ[K] n

    The inverse Borel decomposition recovers the Cartan and positive factors of a product.

    source
    noncomputable def TauCeti.UniversalEnvelopingAlgebra.triangularMulEquiv {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (β†₯H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) :
    TensorProduct K (UniversalEnvelopingAlgebra K β†₯(negativeNilradical H b)) (TensorProduct K (UniversalEnvelopingAlgebra K β†₯H) (UniversalEnvelopingAlgebra K β†₯(positiveNilradical H b))) ≃ₗ[K] UniversalEnvelopingAlgebra K L

    The triangular decomposition of U(L): multiplication identifies U(n⁻) βŠ— (U(H) βŠ— U(n⁺)) with U(L), sending f βŠ— h βŠ— e to the ordered product f h e of the images of the three factors (TauCeti.UniversalEnvelopingAlgebra.triangularMulEquiv_tmul). It is the Borel decomposition TauCeti.UniversalEnvelopingAlgebra.borelMulEquiv followed by the decomposition of U(L) along L = n⁻ βŠ• π”Ÿ.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.UniversalEnvelopingAlgebra.triangularMulEquiv_tmul {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (β†₯H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (f : UniversalEnvelopingAlgebra K β†₯(negativeNilradical H b)) (h : UniversalEnvelopingAlgebra K β†₯H) (e : UniversalEnvelopingAlgebra K β†₯(positiveNilradical H b)) :
      (triangularMulEquiv H b) (f βŠ—β‚œ[K] (h βŠ—β‚œ[K] e)) = (map K (negativeNilradical H b).incl) f * (map K H.incl) h * (map K (positiveNilradical H b).incl) e

      The triangular decomposition sends a pure tensor to the ordered product of its three images.

      source
      @[simp]
      theorem TauCeti.UniversalEnvelopingAlgebra.triangularMulEquiv_symm_mul_mul {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (β†₯H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (f : UniversalEnvelopingAlgebra K β†₯(negativeNilradical H b)) (h : UniversalEnvelopingAlgebra K β†₯H) (e : UniversalEnvelopingAlgebra K β†₯(positiveNilradical H b)) :
      (triangularMulEquiv H b).symm ((map K (negativeNilradical H b).incl) f * (map K H.incl) h * (map K (positiveNilradical H b).incl) e) = f βŠ—β‚œ[K] (h βŠ—β‚œ[K] e)

      The inverse triangular decomposition recovers the three factors of an ordered product.