The classification of the finite-dimensional irreducible sl₂-modules

TauCeti/Algebra/Lie/Sl2/WeightString.lean shows that a module carrying a primitive vector of weight n : ℕ and irreducible over the subalgebra of an sl₂ triple is determined by n, and TauCeti/Algebra/Lie/Sl2/Standard.lean exhibits such a module, Ado.Sl2Std K n = V(n), for every n. What neither file supplies is the remaining half of the classification: that a finite-dimensional irreducible module has a primitive vector at all. This file supplies it and draws the classification.

The argument is the standard one, and Mathlib runs it: over a triangularizable module the Cartan element h has an eigenvector which the raising operator pushes up the h-spectrum by 2 at a time until it dies, leaving a primitive vector (IsSl2Triple.exists_hasPrimitiveVectorWith). All that is added here is that IsSl2Triple.HasPrimitiveVectorWith.exists_nat makes the weight a natural number.

Triangularizability is carried as a hypothesis rather than bought with an algebraically closed field: over such a field a finite-dimensional module is triangularizable by Mathlib's LieModule.instIsTriangularizableOfIsAlgClosed, so the algebraically closed case is these statements with that instance supplied by inference, and needs no separate form.

Note that no irreducibility is needed for the existence of a primitive vector: a nonzero triangularizable Noetherian module suffices. Irreducibility enters only when the weight string of that vector is asked to be the whole module.

Both halves are stated for an arbitrary Lie algebra L generated by an sl₂ triple, and then specialized to sl (Fin 2) K with its standard triple, where they say that every finite-dimensional triangularizable irreducible module is V(n) for exactly one n.

Main results

• Ado.exists_hasPrimitiveVectorWith: every nonzero triangularizable module over an sl₂ triple has a primitive vector, of weight a natural number.
• Ado.existsUnique_nat_hasPrimitiveVectorWith: the classification by highest weight. A triangularizable irreducible module over a Lie algebra generated by an sl₂ triple has exactly one highest weight n : ℕ, and Ado.finrank_eq_of_hasPrimitiveVectorWith_of_eq_top computes its dimension as n + 1.
• Ado.nonempty_lieModuleEquiv_of_hasPrimitiveVectorWith: the highest weight determines the module, now as an equivalence over the whole of L rather than over the subalgebra of the triple.
• Ado.Sl2Std.existsUnique_nonempty_lieModuleEquiv: the classification for sl (Fin 2) K. A finite-dimensional triangularizable irreducible sl (Fin 2) K-module is equivalent to V(n) for exactly one n : ℕ.
• Ado.Sl2Std.exists_eq_sub_two_mul_of_hasEigenvalue: every weight of such a module is among n, n - 2, …, -n. That its weights are in particular integers holds for an arbitrary finite-dimensional module, irreducible or not, and is Ado.exists_int_of_hasEigenvalue_slFinTwo in TauCeti/Algebra/Lie/Sl2/Spectrum.lean.

References

This is Layer 0 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, whose exists_hasPrimitiveVectorWith is Ado.exists_hasPrimitiveVectorWith.

• [J. E. Humphreys, Introduction to Lie Algebras and Representation Theory][humphreys1972], §7.2.

Existence of a primitive vector

theorem Ado.exists_hasPrimitiveVectorWith {K : Type u_1} [CommRing K] [IsDomain K] [CharZero K] {L : Type u_2} [LieRing L] [LieAlgebra K L] (M : Type u_3) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [Module.IsTorsionFree K M] [IsNoetherian K M] {h e f : L} [Nontrivial M] [LieModule.IsTriangularizable K L M] (t : IsSl2Triple h e f) : ∃ (w : M) (n : ℕ), t.HasPrimitiveVectorWith w ↑n

Existence of a primitive vector. Every nonzero triangularizable module over an sl₂ triple carries a primitive vector, and its weight is a natural number.

This is the half of the classification of the finite-dimensional irreducible sl₂-modules that Ado.exists_isIrreducible_hasPrimitiveVectorWith leaves open. Irreducibility is not needed: the eigenvector triangularizability supplies can be raised in any module at all. It refines Mathlib's IsSl2Triple.exists_hasPrimitiveVectorWith, which produces a primitive vector of some weight in K, by pinning that weight down to a natural number.

Over an algebraically closed field a finite-dimensional module is triangularizable, so there the LieModule.IsTriangularizable hypothesis is discharged by instance inference.

The classification over a Lie algebra generated by a triple

theorem Ado.finrank_eq_of_hasPrimitiveVectorWith_of_eq_top {K : Type u_1} [CommRing K] [IsDomain K] [CharZero K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [Module.IsTorsionFree K M] [IsNoetherian K M] {h e f : L} {t : IsSl2Triple h e f} {m : M} {n : ℕ} (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) [LieModule.IsIrreducible K L M] (P : t.HasPrimitiveVectorWith m ↑n) : Module.finrank K M = n + 1

The rank of an irreducible with a given highest weight. A module irreducible over a Lie algebra generated by an sl₂ triple, carrying a primitive vector of weight n, has rank n + 1. This is Ado.finrank_eq_of_hasPrimitiveVectorWith with the irreducibility hypothesis moved from the subalgebra of the triple to the whole algebra, which generates it.

theorem Ado.nonempty_lieModuleEquiv_of_hasPrimitiveVectorWith {K : Type u_1} [CommRing K] [IsDomain K] [CharZero K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [Module.IsTorsionFree K M] [IsNoetherian K M] {h e f : L} {t : IsSl2Triple h e f} {m : M} {n : ℕ} {M' : Type u_4} [AddCommGroup M'] [Module K M'] [LieRingModule L M'] [LieModule K L M'] [Module.IsTorsionFree K M'] [IsNoetherian K M'] {m' : M'} (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) [LieModule.IsIrreducible K L M] [LieModule.IsIrreducible K L M'] (P : t.HasPrimitiveVectorWith m ↑n) (P' : t.HasPrimitiveVectorWith m' ↑n) : Nonempty (M ≃ₗ⁅K,L⁆ M')

The highest weight determines the irreducible, over the whole algebra. Two modules irreducible over a Lie algebra generated by an sl₂ triple, carrying primitive vectors of the same weight n, are equivalent as L-modules.

Ado.lieModuleEquivOfHasPrimitiveVectorWith proves this over the subalgebra generated by the triple, which is the correct hypothesis in general; when that subalgebra is everything, Ado.lieModuleEquivOfEqTop upgrades the conclusion to the ambient algebra.

theorem Ado.existsUnique_nat_hasPrimitiveVectorWith {K : Type u_1} [CommRing K] [IsDomain K] [CharZero K] {L : Type u_2} [LieRing L] [LieAlgebra K L] (M : Type u_3) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [Module.IsTorsionFree K M] [IsNoetherian K M] {h e f : L} {t : IsSl2Triple h e f} (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) [LieModule.IsTriangularizable K L M] [LieModule.IsIrreducible K L M] : ∃! n : ℕ, ∃ (w : M), t.HasPrimitiveVectorWith w ↑n

The classification by highest weight. A triangularizable irreducible module over a Lie algebra generated by an sl₂ triple has exactly one highest weight, a natural number: one exists by Ado.exists_hasPrimitiveVectorWith, and two would force two values on the dimension of M.

Together with Ado.finrank_eq_of_hasPrimitiveVectorWith_of_eq_top, Ado.nonempty_lieModuleEquiv_of_hasPrimitiveVectorWith and Ado.exists_isIrreducible_hasPrimitiveVectorWith this is the classification: a triangularizable irreducible has a highest weight n : ℕ, which determines it and gives it dimension n + 1, and every natural number occurs as such a weight.

The classification for sl (Fin 2) K

theorem Ado.Sl2Std.eq_of_linearEquiv {K : Type u_1} [Field K] {m n : ℕ} (φ : Sl2Std K m ≃ₗ[K] Sl2Std K n) : m = n

V(m) and V(n) are not even linearly isomorphic unless m = n, their dimensions being m + 1 and n + 1.

theorem Ado.Sl2Std.exists_eq_sub_two_mul_of_hasEigenvalue {K : Type u_1} [Field K] {M : Type u_2} [AddCommGroup M] [Module K M] [LieRingModule (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M] [LieModule K (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M] {n : ℕ} (φ : M ≃ₗ⁅K,↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)⁆ Sl2Std K n) {μ : K} (hμ : ((LieModule.toEnd K (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M) ((slFinTwoBasis K) 2)).HasEigenvalue μ) : ∃ (i : Fin (n + 1)), μ = ↑n - 2 * ↑↑i

The weights of a module equivalent to V(n). An eigenvalue of the Cartan element h = E₀₀ - E₁₁ on such a module is one of n, n - 2, …, -n: the equivalence carries an eigenvector to an eigenvector, and Ado.Sl2Std.eigenspace_diag_eq_bot says V(n) has no other weights.

theorem Ado.Sl2Std.existsUnique_nonempty_lieModuleEquiv {K : Type u_1} [Field K] (M : Type u_2) [AddCommGroup M] [Module K M] [LieRingModule (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M] [LieModule K (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M] [CharZero K] [FiniteDimensional K M] [LieModule.IsTriangularizable K (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M] [LieModule.IsIrreducible K (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M] : ∃! n : ℕ, Nonempty (M ≃ₗ⁅K,↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)⁆ Sl2Std K n)

The classification of the finite-dimensional irreducible sl₂-modules. Over a field of characteristic zero, a finite-dimensional triangularizable irreducible sl (Fin 2) K-module is equivalent to the standard module V(n) for exactly one n : ℕ. Over an algebraically closed field triangularizability is automatic, so this reads as the classification of all the finite-dimensional irreducibles.

The proof is the two halves meeting: Ado.exists_hasPrimitiveVectorWith produces a primitive vector of weight n, and Ado.Sl2Std.lieModuleEquiv matches its weight string with that of V(n). Uniqueness of n is Ado.Sl2Std.eq_of_linearEquiv.