Verma modules

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field K of characteristic zero, let H be a splitting Cartan subalgebra and let b be a base of the root system LieAlgebra.IsKilling.rootSystem H, so that the Borel subalgebra 𝔟 = H + n⁺ of TauCeti/Algebra/Lie/Weights/Borel.lean is available. For a linear form lam on H this file builds the Verma module M(lam), the universal module generated by a vector on which H acts through lam and which the positive nilradical annihilates.

The presentation

M(lam) is classically written U(L) ⊗_{U(𝔟)} K_lam, where K_lam is the one-dimensional 𝔟-module on which x = h + n acts by lam h. Since U(L) is a free right U(𝔟)-module only after Poincaré--Birkhoff--Witt, and since Mathlib's tensor product is taken over a commutative base, this file instead uses a quotient presentation:

TauCeti.vermaIdeal b lam is the left ideal generated by the elements ι x - lam x for x : H together with ι x for x in the positive nilradical, and TauCeti.VermaModule b lam := U(L) ⧸ vermaIdeal b lam.

For a decomposition x = h + n of an element of 𝔟, the associated degree-one relation satisfies ι x - lam h = (ι h - lam h) + ι n and hence belongs to this ideal. This containment is the content of TauCeti.exists_ι_sub_algebraMap_mem_vermaIdeal_of_mem_borelSubalgebra below.

Reading the quotient as a Lie module is what TauCeti/Algebra/Lie/UniversalEnveloping/Module.lean was built for: a left ideal is exactly a U(L)-submodule of U(L), so the quotient is a U(L)-module, and TauCeti.UniversalEnvelopingAlgebra.asLieRingModule turns that into an L-module. The same file supplies the two dictionary results the universal property runs on: Lie module homomorphisms out of M(lam) are U(L)-linear maps, and the Lie submodule generated by the canonical vector is its U(L)-span.

The universal property, and nonvanishing

The universal property TauCeti.existsUnique_lieModuleHom_apply_vermaGenerator is proved in the form that does not presuppose M(lam) ≠ 0: for any vector v of any L-module on which H acts through lam and which n⁺ annihilates — v = 0 allowed — there is a unique Lie module homomorphism M(lam) → N sending the canonical generator to v. Everything below is a consequence of it.

That M(lam) is nonzero is exactly the statement that the left ideal vermaIdeal b lam is proper (TauCeti.vermaGenerator_eq_zero_iff). The Verma relations are the elements ι x - χ x for x in the Borel subalgebra, where χ = TauCeti.borelCharacter H b lam is the character h + n ↦ lam h of 𝔟, and the left ideal these generate is proper by the freeness of U(L) as a right U(𝔟)-module, a consequence of Poincaré--Birkhoff--Witt (TauCeti.UniversalEnvelopingAlgebra.span_range_ι_sub_algebraMap_ne_top). This is TauCeti.vermaIdeal_ne_top, so the canonical generator is a highest weight vector of weight lam for every lam (TauCeti.isHighestWeightVector_vermaGenerator) and L(lam) is irreducible for every lam.

Freeness over U(n⁻)

The same relative Poincaré--Birkhoff--Witt input gives more than nonvanishing. Since L = n⁻ ⊕ 𝔟 (TauCeti.isCompl_negativeNilradical_borelSubalgebra), U(L) is a free right U(𝔟)-module on the ordered monomials in a basis of n⁻, and the induced module M(lam) is therefore a free U(n⁻)-module of rank one on v_lam: the map U(n⁻) → M(lam), y ↦ y · v_lam, is a linear equivalence (TauCeti.universalEnvelopingEquivVermaModule). Through the PBW basis of U(n⁻) this is the input for computing the weight multiplicities of M(lam).

Main definitions

• TauCeti.vermaRelations b lam and TauCeti.vermaIdeal b lam: the defining relations of weight lam and the left ideal of U(L) they generate.
• TauCeti.VermaModule b lam: the Verma module M(lam), with its K-module, U(L)-module and L-module structures.
• TauCeti.vermaMk b lam: the canonical projection U(L) → M(lam), as a U(L)-linear map.
• TauCeti.vermaGenerator b lam: the canonical generator v_lam, the class of 1.
• TauCeti.irreducibleQuotient b lam: the irreducible quotient L(lam), the quotient of M(lam) by its maximal submodule, with its K-module and L-module structures.
• TauCeti.irreducibleQuotientMk b lam: the canonical projection M(lam) → L(lam), as a Lie module homomorphism.
• TauCeti.irreducibleQuotientGenerator b lam: the canonical generator of L(lam), the class of the canonical generator of M(lam).

Main results

• TauCeti.lie_vermaGenerator_eq_smul and TauCeti.lie_vermaGenerator_eq_zero_of_mem_positiveNilradical: the Cartan subalgebra acts on the canonical generator through lam, and the positive nilradical annihilates it.
• TauCeti.lieSpan_vermaGenerator_eq_top: the canonical generator generates M(lam), so M(lam) is a highest weight module of weight lam as soon as the generator is nonzero.
• TauCeti.existsUnique_lieModuleHom_apply_vermaGenerator: the universal property.
• TauCeti.exists_surjective_lieModuleHom_of_isHighestWeightVector: every highest weight module of weight lam is a quotient of M(lam), which is what makes M(lam) universal in the sense the classification uses.
• TauCeti.isHighestWeightVector_vermaGenerator_iff, TauCeti.vermaGenerator_eq_zero_iff and TauCeti.subsingleton_vermaModule_iff: the nonvanishing of M(lam) is the properness of TauCeti.vermaIdeal.
• TauCeti.vermaIdeal_eq_span_range_ι_sub_algebraMap: the Verma ideal is the left ideal generated by the elements ι x - χ x for x in 𝔟, χ the Borel character of weight lam, so that M(lam) is induced from the one-dimensional 𝔟-module K_lam.
• TauCeti.vermaIdeal_ne_top, TauCeti.vermaGenerator_ne_zero and TauCeti.isHighestWeightVector_vermaGenerator: M(lam) ≠ 0 for every lam, and its canonical generator is a highest weight vector of weight lam.
• TauCeti.universalEnvelopingEquivVermaModule, with TauCeti.universalEnvelopingEquivVermaModule_apply and TauCeti.universalEnvelopingEquivVermaModule_mul: M(lam) is a free U(n⁻)-module of rank one on v_lam, the map y ↦ y · v_lam being a U(n⁻)-linear equivalence U(n⁻) ≃ M(lam).
• TauCeti.pow_toEnd_vermaGenerator_ne_zero: lowering v_lam by a nonzero element of n⁻, any number of times, never gives zero.
• TauCeti.irreducibleQuotientMk_surjective and TauCeti.lieSpan_irreducibleQuotientGenerator_eq_top: every vector of L(lam) is the class of one of M(lam), and the canonical generator generates L(lam).
• TauCeti.isIrreducible_irreducibleQuotient and TauCeti.isHighestWeightVector_irreducibleQuotientGenerator: L(lam) is irreducible and its canonical generator is a highest weight vector of weight lam, for every lam.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §20.3.
• J. E. Humphreys, Representations of Semisimple Lie Algebras in the BGG Category O, §1.3.

The defining left ideal

def TauCeti.vermaRelations {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) (lam : Module.Dual K ↥H) : Set (UniversalEnvelopingAlgebra K L)

The Verma relations of weight lam: the elements ι x - lam x of U(L) for x in the Cartan subalgebra, together with the elements ι x for x in the positive nilradical. Their image in M(lam) is what forces the Cartan subalgebra to act on the class of 1 through lam and the positive nilradical to annihilate it. Those are two of the three conditions defining a highest weight vector, so that class is a highest weight vector of weight lam exactly when it is nonzero; see TauCeti.isHighestWeightVector_vermaGenerator_iff.

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.vermaIdeal {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) (lam : Module.Dual K ↥H) : Submodule (UniversalEnvelopingAlgebra K L) (UniversalEnvelopingAlgebra K L)

The Verma ideal of weight lam: the left ideal of U(L) generated by the Verma relations.

Equations

• TauCeti.vermaIdeal b lam = Submodule.span (UniversalEnvelopingAlgebra K L) (TauCeti.vermaRelations b lam)

theorem TauCeti.ι_sub_algebraMap_mem_vermaIdeal {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) (lam : Module.Dual K ↥H) (x : ↥H) : (UniversalEnvelopingAlgebra.ι K) ↑x - (algebraMap K (UniversalEnvelopingAlgebra K L)) (lam x) ∈ vermaIdeal b lam

The relation ι x - lam x lies in the Verma ideal, for x in the Cartan subalgebra.

theorem TauCeti.ι_mem_vermaIdeal_of_mem_positiveNilradical {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) (lam : Module.Dual K ↥H) {x : L} (hx : x ∈ positiveNilradical H b) : (UniversalEnvelopingAlgebra.ι K) x ∈ vermaIdeal b lam

The relation ι x lies in the Verma ideal, for x in the positive nilradical.

theorem TauCeti.exists_ι_sub_algebraMap_mem_vermaIdeal_of_mem_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) (lam : Module.Dual K ↥H) {x : L} (hx : x ∈ borelSubalgebra H b) : ∃ (h : ↥H), (UniversalEnvelopingAlgebra.ι K) x - (algebraMap K (UniversalEnvelopingAlgebra K L)) (lam h) ∈ vermaIdeal b lam

For an element x = h + n of the Borel subalgebra, the degree-one relation ι x - lam h belongs to the Verma ideal, since it is the sum of the two kinds of generator.

The Verma module and its structures

def TauCeti.VermaModule {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) (lam : Module.Dual K ↥H) : Type (max u v)

The Verma module M(lam), defined here as the quotient of U(L) by the left ideal TauCeti.vermaIdeal of Verma relations.

Equations

• TauCeti.VermaModule b lam = (UniversalEnvelopingAlgebra K L ⧸ TauCeti.vermaIdeal b lam)

@[instance_reducible]

instance TauCeti.instAddCommGroupVermaModule {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) (lam : Module.Dual K ↥H) : AddCommGroup (VermaModule b lam)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TauCeti.instModuleUniversalEnvelopingAlgebraVermaModule {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) (lam : Module.Dual K ↥H) : Module (UniversalEnvelopingAlgebra K L) (VermaModule b lam)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TauCeti.instModuleVermaModule {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) (lam : Module.Dual K ↥H) : Module K (VermaModule b lam)

Equations

• TauCeti.instModuleVermaModule b lam = { smul := TauCeti.instModuleVermaModule._aux_1 b lam, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

instance TauCeti.instIsScalarTowerUniversalEnvelopingAlgebraVermaModule {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) (lam : Module.Dual K ↥H) : IsScalarTower K (UniversalEnvelopingAlgebra K L) (VermaModule b lam)

@[instance_reducible]

noncomputable instance TauCeti.instLieRingModuleVermaModule {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) (lam : Module.Dual K ↥H) : LieRingModule L (VermaModule b lam)

Equations

• TauCeti.instLieRingModuleVermaModule b lam = TauCeti.UniversalEnvelopingAlgebra.asLieRingModule K L (TauCeti.VermaModule b lam)

instance TauCeti.instLieModuleVermaModule {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) (lam : Module.Dual K ↥H) : LieModule K L (VermaModule b lam)

theorem TauCeti.vermaModule_ι_smul {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) (lam : Module.Dual K ↥H) (x : L) (m : VermaModule b lam) : (UniversalEnvelopingAlgebra.ι K) x • m = ⁅x, m⁆

The L-action on the Verma module is the action of the canonical Lie generators of U(L). This is the compatibility hypothesis the enveloping-algebra dictionary consumes.

theorem TauCeti.representation_vermaModule_apply {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) (lam : Module.Dual K ↥H) (u : UniversalEnvelopingAlgebra K L) (m : VermaModule b lam) : ((UniversalEnvelopingAlgebra.representation K L (VermaModule b lam)) u) m = u • m

The enveloping representation of the Verma module is its U(L)-module structure: the action of U(L) induced by the L-action, TauCeti.UniversalEnvelopingAlgebra.representation, is the scalar action of U(L) on the quotient U(L) ⧸ vermaIdeal b lam.

def TauCeti.vermaMk {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) (lam : Module.Dual K ↥H) : UniversalEnvelopingAlgebra K L →ₗ[UniversalEnvelopingAlgebra K L] VermaModule b lam

The canonical projection U(L) → M(lam), bundled as a U(L)-linear map so that its algebraic behaviour — map_zero, map_add, map_smul — is available from the LinearMap API without unfolding the quotient.

Equations

• TauCeti.vermaMk b lam = (TauCeti.vermaIdeal b lam).mkQ

theorem TauCeti.vermaMk_surjective {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) (lam : Module.Dual K ↥H) : Function.Surjective ⇑(vermaMk b lam)

theorem TauCeti.vermaMk_eq_iff {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) (lam : Module.Dual K ↥H) {u w : UniversalEnvelopingAlgebra K L} : (vermaMk b lam) u = (vermaMk b lam) w ↔ u - w ∈ vermaIdeal b lam

@[simp]

theorem TauCeti.vermaMk_eq_zero_iff {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) (lam : Module.Dual K ↥H) {u : UniversalEnvelopingAlgebra K L} : (vermaMk b lam) u = 0 ↔ u ∈ vermaIdeal b lam

@[simp]

theorem TauCeti.smul_vermaMk {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) (lam : Module.Dual K ↥H) (u w : UniversalEnvelopingAlgebra K L) : u • (vermaMk b lam) w = (vermaMk b lam) (u * w)

def TauCeti.vermaGenerator {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) (lam : Module.Dual K ↥H) : VermaModule b lam

The canonical generator v_lam of the Verma module, the class of 1. It is a highest weight vector of weight lam exactly when it is nonzero, which is TauCeti.isHighestWeightVector_vermaGenerator_iff.

Equations

• TauCeti.vermaGenerator b lam = (TauCeti.vermaMk b lam) 1

@[simp]

theorem TauCeti.smul_vermaGenerator {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) (lam : Module.Dual K ↥H) (u : UniversalEnvelopingAlgebra K L) : u • vermaGenerator b lam = (vermaMk b lam) u

@[simp]

theorem TauCeti.lie_vermaGenerator_eq_smul {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) (lam : Module.Dual K ↥H) (x : ↥H) : ⁅↑x, vermaGenerator b lam⁆ = lam x • vermaGenerator b lam

The Cartan subalgebra acts on the canonical generator through lam.

theorem TauCeti.lie_vermaGenerator_eq_zero_of_mem_positiveNilradical {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) (lam : Module.Dual K ↥H) {x : L} (hx : x ∈ positiveNilradical H b) : ⁅x, vermaGenerator b lam⁆ = 0

The positive nilradical annihilates the canonical generator.

theorem TauCeti.span_vermaGenerator_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) (lam : Module.Dual K ↥H) : UniversalEnvelopingAlgebra K L ∙ vermaGenerator b lam = ⊤

The canonical generator spans the Verma module over U(L).

theorem TauCeti.lieSpan_vermaGenerator_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) (lam : Module.Dual K ↥H) : LieSubmodule.lieSpan K L {vermaGenerator b lam} = ⊤

The canonical generator generates the Verma module as a Lie module, by the dictionary carrying generated Lie submodules to U(L)-spans. Together with TauCeti.isHighestWeightVector_vermaGenerator_iff this exhibits M(lam) as a highest weight module of weight lam whenever it is nonzero.

The universal property

theorem TauCeti.existsUnique_lieModuleHom_apply_vermaGenerator {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) (lam : Module.Dual K ↥H) {N : Type w} [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] (v : N) (hcartan : ∀ (x : ↥H), ⁅↑x, v⁆ = lam x • v) (hpos : ∀ x ∈ positiveNilradical H b, ⁅x, v⁆ = 0) : ∃! φ : VermaModule b lam →ₗ⁅K,L⁆ N, φ (vermaGenerator b lam) = v

The universal property of the Verma module. If H acts on a vector v of an L-module N through lam and the positive nilradical annihilates v, then there is a unique homomorphism of L-modules M(lam) → N carrying the canonical generator to v.

The vector v is not assumed nonzero, so this does not presuppose that M(lam) is nonzero.

Highest weight vectors and nonvanishing

theorem TauCeti.isHighestWeightVector_vermaGenerator_iff {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) (lam : Module.Dual K ↥H) : IsHighestWeightVector b lam (vermaGenerator b lam) ↔ vermaGenerator b lam ≠ 0

The canonical generator is a highest weight vector exactly when it is nonzero. The other two conditions hold unconditionally, by TauCeti.lie_vermaGenerator_eq_smul and TauCeti.lie_vermaGenerator_eq_zero_of_mem_positiveNilradical.

theorem TauCeti.exists_surjective_lieModuleHom_of_isHighestWeightVector {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) (lam : Module.Dual K ↥H) {N : Type w} [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] {v : N} (hv : IsHighestWeightVector b lam v) (hgen : LieSubmodule.lieSpan K L {v} = ⊤) : ∃ (φ : VermaModule b lam →ₗ⁅K,L⁆ N), Function.Surjective ⇑φ ∧ φ (vermaGenerator b lam) = v

Every highest weight module of weight lam is a quotient of the Verma module. This is the sense in which M(lam) is the universal highest weight module of weight lam, and the form in which the classification of the irreducible highest weight modules consumes it.

theorem TauCeti.vermaGenerator_eq_zero_iff {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) (lam : Module.Dual K ↥H) : vermaGenerator b lam = 0 ↔ vermaIdeal b lam = ⊤

The canonical generator vanishes exactly when the Verma ideal is improper. So M(lam) ≠ 0 says that the left ideal generated by the Verma relations is proper, which follows from the freeness of U(L) as a right U(𝔟)-module (TauCeti.vermaIdeal_ne_top).

theorem TauCeti.subsingleton_vermaModule_iff {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) (lam : Module.Dual K ↥H) : Subsingleton (VermaModule b lam) ↔ vermaGenerator b lam = 0

The Verma module vanishes exactly when its canonical generator does, the generator spanning it.

The Verma module is induced from the Borel character

theorem TauCeti.vermaIdeal_eq_span_range_ι_sub_algebraMap {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) (lam : Module.Dual K ↥H) : vermaIdeal b lam = Submodule.span (UniversalEnvelopingAlgebra K L) (Set.range fun (x : ↥(borelSubalgebra H b)) => (UniversalEnvelopingAlgebra.ι K) ↑x - (algebraMap K (UniversalEnvelopingAlgebra K L)) ((borelCharacter H b lam) x))

The Verma ideal is the left ideal induced by the Borel character: it is generated by the elements ι x - χ x for x in the Borel subalgebra, where χ = TauCeti.borelCharacter H b lam is the character h + n ↦ lam h of 𝔟 = H + n⁺. So M(lam) is the module U(L) ⊗_{U(𝔟)} K_lam induced from the one-dimensional 𝔟-module of weight lam, presented as a quotient of U(L).

The Verma module is nonzero

@[simp]

theorem TauCeti.vermaIdeal_ne_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) (lam : Module.Dual K ↥H) : vermaIdeal b lam ≠ ⊤

The Verma ideal is proper. Its generators ι x - lam x for x in the Cartan subalgebra and ι x for x in the positive nilradical are all of the form ι x - χ x for x in the Borel subalgebra, where χ = TauCeti.borelCharacter H b lam is the character h + n ↦ lam h. The left ideal generated by those is proper, by the freeness of U(L) as a right U(𝔟)-module (TauCeti.UniversalEnvelopingAlgebra.span_range_ι_sub_algebraMap_ne_top).

@[simp]

theorem TauCeti.vermaGenerator_ne_zero {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) (lam : Module.Dual K ↥H) : vermaGenerator b lam ≠ 0

The Verma module is nonzero: its canonical generator does not vanish, for every weight lam.

theorem TauCeti.isHighestWeightVector_vermaGenerator {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) (lam : Module.Dual K ↥H) : IsHighestWeightVector b lam (vermaGenerator b lam)

The canonical generator of the Verma module is a highest weight vector of weight lam, for every weight lam.

instance TauCeti.instNontrivialVermaModule {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) (lam : Module.Dual K ↥H) : Nontrivial (VermaModule b lam)

The Verma module is free of rank one over U(n⁻)

noncomputable def TauCeti.universalEnvelopingEquivVermaModule {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) (lam : Module.Dual K ↥H) : UniversalEnvelopingAlgebra K ↥(negativeNilradical H b) ≃ₗ[K] VermaModule b lam

The Verma module is a free U(n⁻)-module of rank one on its canonical generator: the map U(n⁻) → M(lam), y ↦ y · v_lam, is a linear equivalence, where U(n⁻) acts on M(lam) through the map U(n⁻) → U(L) induced by the inclusion of the negative nilradical. Its value is TauCeti.universalEnvelopingEquivVermaModule_apply, and it intertwines left multiplication on U(n⁻) with the action on M(lam) (TauCeti.universalEnvelopingEquivVermaModule_mul).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.universalEnvelopingEquivVermaModule_apply {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) (lam : Module.Dual K ↥H) (y : UniversalEnvelopingAlgebra K ↥(negativeNilradical H b)) : (universalEnvelopingEquivVermaModule b lam) y = (UniversalEnvelopingAlgebra.map K (negativeNilradical H b).incl) y • vermaGenerator b lam

The equivalence U(n⁻) ≃ M(lam) sends y to y · v_lam.

theorem TauCeti.universalEnvelopingEquivVermaModule_one {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) (lam : Module.Dual K ↥H) : (universalEnvelopingEquivVermaModule b lam) 1 = vermaGenerator b lam

The equivalence U(n⁻) ≃ M(lam) sends 1 to the canonical generator v_lam.

theorem TauCeti.universalEnvelopingEquivVermaModule_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) (lam : Module.Dual K ↥H) (y z : UniversalEnvelopingAlgebra K ↥(negativeNilradical H b)) : (universalEnvelopingEquivVermaModule b lam) (y * z) = (UniversalEnvelopingAlgebra.map K (negativeNilradical H b).incl) y • (universalEnvelopingEquivVermaModule b lam) z

The equivalence U(n⁻) ≃ M(lam) is U(n⁻)-linear: it carries left multiplication by y on U(n⁻) to the action of y on M(lam).

theorem TauCeti.pow_toEnd_vermaGenerator_ne_zero {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) (lam : Module.Dual K ↥H) {f : L} (hf : f ∈ negativeNilradical H b) (hf0 : f ≠ 0) (k : ℕ) : ((LieModule.toEnd K L (VermaModule b lam)) f ^ k) (vermaGenerator b lam) ≠ 0

Lowering the canonical generator never gives zero: for a nonzero f in the negative nilradical, f^k · v_lam ≠ 0 in M(lam) for every k. Through the freeness U(n⁻) ≃ M(lam) the vector is the image of (ι f)^k, which is nonzero because U(n⁻) is a domain containing n⁻, by Poincaré--Birkhoff--Witt.

def TauCeti.irreducibleQuotient {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) (lam : Module.Dual K ↥H) : Type (max u v)

The irreducible quotient L(lam): the quotient of the Verma module by the maximal submodule of TauCeti/Algebra/Lie/HighestWeight/Maximal.lean. As with TauCeti.VermaModule, the carrier is a definition with its module structures declared one by one, so that statements about L(lam) are made against this name rather than against the quotient it is built from.

Nothing about it is irreducible by fiat: irreducibility is TauCeti.isIrreducible_irreducibleQuotient, which rests on M(lam) ≠ 0. Naming the carrier is what lets a statement about L(lam) be phrased at one fixed module instead of at an arbitrary irreducible module carrying a highest weight vector of weight lam.

Equations

• TauCeti.irreducibleQuotient b lam = (TauCeti.VermaModule b lam ⧸ TauCeti.maximalSubmodule H (TauCeti.VermaModule b lam) lam)

@[instance_reducible]

noncomputable instance TauCeti.instAddCommGroupIrreducibleQuotient {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) (lam : Module.Dual K ↥H) : AddCommGroup (irreducibleQuotient b lam)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance TauCeti.instModuleIrreducibleQuotient {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) (lam : Module.Dual K ↥H) : Module K (irreducibleQuotient b lam)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance TauCeti.instLieRingModuleIrreducibleQuotient {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) (lam : Module.Dual K ↥H) : LieRingModule L (irreducibleQuotient b lam)

Equations

• TauCeti.instLieRingModuleIrreducibleQuotient b lam = { bracket := TauCeti.instLieRingModuleIrreducibleQuotient._aux_1 b lam, add_lie := ⋯, lie_add := ⋯, leibniz_lie := ⋯ }

instance TauCeti.instLieModuleIrreducibleQuotient {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) (lam : Module.Dual K ↥H) : LieModule K L (irreducibleQuotient b lam)

noncomputable def TauCeti.irreducibleQuotientMk {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) (lam : Module.Dual K ↥H) : VermaModule b lam →ₗ⁅K,L⁆ irreducibleQuotient b lam

The canonical projection M(lam) → L(lam), bundled as a Lie module homomorphism, so that its algebraic behaviour — map_zero, map_add, map_smul, map_lie — is available from the LieModuleHom API without unfolding the quotient. It is the analogue for L(lam) of TauCeti.vermaMk, and together with TauCeti.irreducibleQuotientMk_surjective it is how every vector of L(lam) is reached.

Equations

• TauCeti.irreducibleQuotientMk b lam = LieSubmodule.Quotient.mk' (TauCeti.maximalSubmodule H (TauCeti.VermaModule b lam) lam)

theorem TauCeti.irreducibleQuotientMk_surjective {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) (lam : Module.Dual K ↥H) : Function.Surjective ⇑(irreducibleQuotientMk b lam)

The canonical projection onto L(lam) is surjective: every vector of L(lam) is the class of one of M(lam). This is the elimination rule matching TauCeti.irreducibleQuotientMk, and it is what lets a statement about L(lam) be checked on representatives without unfolding the quotient.

noncomputable def TauCeti.irreducibleQuotientGenerator {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) (lam : Module.Dual K ↥H) : irreducibleQuotient b lam

The canonical generator of L(lam), the class of the canonical generator of M(lam). It is a highest weight vector of weight lam (TauCeti.isHighestWeightVector_irreducibleQuotientGenerator), and it is the introduction rule through which L(lam) is populated without unfolding the quotient. The body is not exposed: the public equation is TauCeti.irreducibleQuotientMk_vermaGenerator.

Equations

• TauCeti.irreducibleQuotientGenerator b lam = (TauCeti.irreducibleQuotientMk b lam) (TauCeti.vermaGenerator b lam)

@[simp]

theorem TauCeti.irreducibleQuotientMk_vermaGenerator {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) (lam : Module.Dual K ↥H) : (irreducibleQuotientMk b lam) (vermaGenerator b lam) = irreducibleQuotientGenerator b lam

theorem TauCeti.lieSpan_irreducibleQuotientGenerator_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) (lam : Module.Dual K ↥H) : LieSubmodule.lieSpan K L {irreducibleQuotientGenerator b lam} = ⊤

The canonical generator generates L(lam), the canonical generator of M(lam) generating M(lam) and the projection being surjective. So L(lam) is a highest weight module of weight lam.

theorem TauCeti.isIrreducible_irreducibleQuotient {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) (lam : Module.Dual K ↥H) : LieModule.IsIrreducible K L (irreducibleQuotient b lam)

L(lam) is irreducible, for every weight lam. The Verma module is nonzero, so it is a highest weight module of weight lam, and its quotient by the maximal submodule is irreducible. By TauCeti.quotientMaximalSubmoduleEquivOfSurjectiveOfIsIrreducible it is then the only irreducible highest weight module of weight lam, up to isomorphism.

instance TauCeti.instIsIrreducibleIrreducibleQuotient {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) (lam : Module.Dual K ↥H) : LieModule.IsIrreducible K L (irreducibleQuotient b lam)

theorem TauCeti.isHighestWeightVector_irreducibleQuotientGenerator {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) (lam : Module.Dual K ↥H) : IsHighestWeightVector b lam (irreducibleQuotientGenerator b lam)

L(lam) carries a highest weight vector of weight lam, its canonical generator; the anti-vacuity companion of TauCeti.isIrreducible_irreducibleQuotient, without which any family of pairwise non-isomorphic irreducibles would do.