Modules induced from a character of a Lie subalgebra

Let B be a Lie subalgebra of a Lie algebra L over a commutative ring R, and let χ : B → R be a character of B. The elements ι x - χ x of U(L), for x : B, generate a left ideal of U(L), and the quotient of U(L) by it is the induced module U(L) ⊗_{U(B)} R_χ, presented without a tensor product over the noncommutative ring U(B). This file proves that the left ideal is proper as soon as B has a complement in L and both B and the complement are free; over a field this holds for every Lie subalgebra. In other words, the induced module is nonzero.

When the complement is itself a Lie subalgebra A, the induced module is moreover a free U(A)-module of rank one on the class of 1: every element of U(L) is congruent to an element of U(A) modulo the left ideal, and an element of U(A) lying in the left ideal is zero. For a semisimple Lie algebra, its Borel subalgebra 𝔟 and the opposite nilradical n⁻, this is the freeness of the Verma module over U(n⁻).

The input is the freeness half of the Poincaré--Birkhoff--Witt theorem relative to a subalgebra: U(L) is a free right U(B)-module on the ordered monomials in a basis of a complement of B. For a semisimple Lie algebra and its Borel subalgebra this is what makes Verma modules nonzero. The spanning half needs no basis: it only uses that U(L) = U(A) · U(B) when A and B span L, and that every element r of U(B) is congruent to the scalar χ r.

Main results

• TauCeti.UniversalEnvelopingAlgebra.span_range_ι_sub_algebraMap_ne_top_of_isCompl: over a nontrivial commutative ring, if B has a complement and both are free, the left ideal generated by ι x - χ x is proper.
• TauCeti.UniversalEnvelopingAlgebra.span_range_ι_sub_algebraMap_ne_top: over a field, the same holds for every Lie subalgebra.
• UniversalEnvelopingAlgebra.map_sub_algebraMap_lift_mem_span_range_ι_sub_algebraMap: every r in U(B) is congruent to χ r modulo the left ideal.
• TauCeti.UniversalEnvelopingAlgebra.exists_sub_map_mem_span_range_ι_sub_algebraMap: if the Lie subalgebras A and B span L, every element of U(L) is congruent to one of U(A).
• TauCeti.UniversalEnvelopingAlgebra.map_mem_span_range_ι_sub_algebraMap_iff_of_isCompl: if the Lie subalgebra A is a complement of B and both are free, an element of U(A) lies in the left ideal only if it is zero.

Implementation notes

Choose an ordered basis of L that lists a basis of the complement A before a basis of B. By PBW its ordered monomials form a basis of U(L), and each of them factors as an ordered monomial in the basis of A times the image of an ordered monomial of U(B). The linear form on U(L) that reads off the coefficient of a fixed A-monomial and applies χ to it is then right U(B)-semilinear along χ, so it kills the left ideal. The form attached to the empty monomial sends 1 to 1, which gives properness; when A is a Lie subalgebra, the forms attached to all monomials restrict on U(A) to its PBW coordinates, which gives freeness. Rather than building the right U(B)-module structure, the file defines these linear forms directly on the PBW basis.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §17.4 and §20.3.

theorem UniversalEnvelopingAlgebra.map_sub_algebraMap_lift_mem_span_range_ι_sub_algebraMap {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (B : LieSubalgebra R L) (χ : LieAlgebra.LieCharacter R ↥B) (r : UniversalEnvelopingAlgebra R ↥B) : (TauCeti.UniversalEnvelopingAlgebra.map R B.incl) r - (algebraMap R (UniversalEnvelopingAlgebra R L)) (((lift R) χ) r) ∈ Submodule.span (UniversalEnvelopingAlgebra R L) (Set.range fun (x : ↥B) => (ι R) ↑x - (algebraMap R (UniversalEnvelopingAlgebra R L)) (χ x))

U(B) acts on the canonical generator through the character. For every r in U(B), the image of r in U(L) is congruent to the scalar χ r modulo the left ideal generated by the elements ι x - χ x, for x : B. In the induced module U(L) ⊗_{U(B)} R_χ this says that r acts on the canonical generator by χ r.

theorem TauCeti.UniversalEnvelopingAlgebra.exists_sub_map_mem_span_range_ι_sub_algebraMap {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {B : LieSubalgebra R L} (χ : LieAlgebra.LieCharacter R ↥B) {A : LieSubalgebra R L} (hAB : A.toSubmodule ⊔ B.toSubmodule = ⊤) (u : UniversalEnvelopingAlgebra R L) : ∃ (y : UniversalEnvelopingAlgebra R ↥A), u - (map R A.incl) y ∈ Submodule.span (UniversalEnvelopingAlgebra R L) (Set.range fun (x : ↥B) => (UniversalEnvelopingAlgebra.ι R) ↑x - (algebraMap R (UniversalEnvelopingAlgebra R L)) (χ x))

The induced module is spanned by the image of U(A) when the Lie subalgebras A and B together span L: every element of U(L) is congruent to an element of U(A) modulo the left ideal generated by the elements ι x - χ x, for x : B. In the induced module U(L) ⊗_{U(B)} R_χ this says that the canonical generator generates it over U(A).

theorem TauCeti.UniversalEnvelopingAlgebra.map_mem_span_range_ι_sub_algebraMap_iff_of_isCompl {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {B : LieSubalgebra R L} (χ : LieAlgebra.LieCharacter R ↥B) {A : LieSubalgebra R L} (hAB : IsCompl A.toSubmodule B.toSubmodule) [Module.Free R ↥A] [Module.Free R ↥B] {y : UniversalEnvelopingAlgebra R ↥A} : (map R A.incl) y ∈ Submodule.span (UniversalEnvelopingAlgebra R L) (Set.range fun (x : ↥B) => (UniversalEnvelopingAlgebra.ι R) ↑x - (algebraMap R (UniversalEnvelopingAlgebra R L)) (χ x)) ↔ y = 0

The image of U(A) meets the induced relations only in zero when the Lie subalgebra A is a complement of B and both are free: an element of U(A) whose image lies in the left ideal generated by the elements ι x - χ x, for x : B, is zero. Together with TauCeti.UniversalEnvelopingAlgebra.exists_sub_map_mem_span_range_ι_sub_algebraMap this says that the induced module U(L) ⊗_{U(B)} R_χ is a free U(A)-module of rank one on its canonical generator.

theorem TauCeti.UniversalEnvelopingAlgebra.span_range_ι_sub_algebraMap_ne_top_of_isCompl {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (B : LieSubalgebra R L) (χ : LieAlgebra.LieCharacter R ↥B) [Nontrivial R] {A : Submodule R L} (hA : IsCompl A B.toSubmodule) [Module.Free R ↥A] [Module.Free R ↥B] : Submodule.span (UniversalEnvelopingAlgebra R L) (Set.range fun (x : ↥B) => (UniversalEnvelopingAlgebra.ι R) ↑x - (algebraMap R (UniversalEnvelopingAlgebra R L)) (χ x)) ≠ ⊤

A character of a Lie subalgebra generates a proper left ideal. If the Lie subalgebra B of L has a complement A and both are free, then for every character χ of B the elements ι x - χ x of U(L), for x : B, generate a proper left ideal of U(L). Equivalently, the induced module U(L) ⊗_{U(B)} R_χ is nonzero.

theorem TauCeti.UniversalEnvelopingAlgebra.span_range_ι_sub_algebraMap_ne_top {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] (B : LieSubalgebra K L) (χ : LieAlgebra.LieCharacter K ↥B) : Submodule.span (UniversalEnvelopingAlgebra K L) (Set.range fun (x : ↥B) => (UniversalEnvelopingAlgebra.ι K) ↑x - (algebraMap K (UniversalEnvelopingAlgebra K L)) (χ x)) ≠ ⊤

A character of a Lie subalgebra generates a proper left ideal, over a field. For every Lie subalgebra B of a Lie algebra L over a field and every character χ of B, the elements ι x - χ x of U(L), for x : B, generate a proper left ideal of U(L).