Documentation

TauCeti.Algebra.Lie.GeneralLinear.Uniqueness

The highest weight of a gl n-module determines it #

A highest weight vector v of weight μ for the matrix unit positive system (TauCeti.IsGlHighestWeightVector) generates a module in which v is, up to a scalar, the only vector of weight μ: this file proves TauCeti.exists_eq_smul_of_isGlHighestWeightVector_of_mem_lieSpan, and reads off from it that two irreducible gl n K-modules carrying highest weight vectors of the same weight are isomorphic (TauCeti.nonempty_lieModuleEquiv_of_isGlHighestWeightVector), and that an irreducible one has the smallest dimension among the finite-dimensional modules carrying such a vector (TauCeti.finrank_le_of_isGlHighestWeightVector).

The Killing form of gl n K is degenerate as soon as the index type is nonempty, the scalar matrices being central, so none of Mathlib's LieAlgebra.IsKilling machinery applies to it and the corresponding results for a Killing-semisimple Lie algebra (TauCeti.genWeightSpace_eq_span_singleton_of_isHighestWeightVector_of_lieSpan_eq_top and TauCeti.nonempty_lieModuleEquiv_of_isHighestWeightVector) are not available here: their positive system is a RootPairing.Base, and the positive system of gl n K is the matrix unit order. The statements below are the gl n K face of that theory, proved directly from the matrix units.

The argument #

Two ingredients, neither of which needs the module to be finite-dimensional.

The first is that everything a highest weight vector generates under gl n K it already generates under the opposite nilpotent subalgebra 𝔫⁻ of strictly lower triangular matrices (TauCeti.lieSpan_toSubmodule_le_of_isGlHighestWeightVector), which is the statement M = U(𝔫⁻)·v written before the enveloping algebra is available. The proof is the triangular decomposition gl n K = 𝔫⁻ + 𝔟 (TauCeti.exists_mem_strictLowerTriangular_add_mem_upperTriangular): the 𝔫⁻-span of v is stable under the Borel subalgebra 𝔟, by induction over the elements of a Lie span, because moving x ∈ 𝔟 past a bracket with f ∈ 𝔫⁻ costs a term ⁅⁅x, f⁆, -⁆ whose bracket splits again along that decomposition.

The second is a height operator: the diagonal matrix D whose entries are a strictly decreasing integer labelling of the index type. Its adjoint action scales the matrix unit Eᵢⱼ by the integer d i - d j, which is negative exactly for the lowering matrix units, so the span of v together with the eigenspaces of D for the eigenvalues strictly below that of v is stable under 𝔫⁻. By the first ingredient it is therefore everything, and since eigenspaces for distinct eigenvalues are independent, a vector of weight μ — which is automatically a D-eigenvector for the eigenvalue of v — is a multiple of v. The integer labelling is what makes "strictly below" a well-founded notion in a field where the weight entries themselves are arbitrary; characteristic zero enters exactly here, in the injectivity of ℤ → K.

With that, the classical diagonal argument applies verbatim: for highest weight vectors v : M and v' : M' of the same weight, the submodule of M × M' generated by (v, v') contains neither (v, 0) nor (0, v'), because both are vectors of weight μ in it and are not multiples of (v, v'). So the two projections restricted to it are injective, and irreducibility makes them surjective.

Main results #

References #

This supplies "the highest weight determines the irreducible" and the universality substitute of Layer 9 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.

A highest weight vector generates under the lowering operators alone #

source
theorem TauCeti.lieSpan_toSubmodule_le_of_isGlHighestWeightVector {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule (Matrix n n R) M] [LieModule R (Matrix n n R) M] {mu : n → R} {v : M} (hv : IsGlHighestWeightVector mu v) {N : Submodule R M} (hvN : v ∈ N) (hstab : ∀ x ∈ strictLowerTriangular R n, ∀ m ∈ N, ⁅x, m⁆ ∈ N) :
↑(LieSubmodule.lieSpan R (Matrix n n R) {v}) ≤ N

A submodule containing a highest weight vector and stable under 𝔫⁻ contains everything that vector generates under all of gl n R. This is the content of M = U(𝔫⁻) · v, written before the enveloping algebra is available; no hypothesis on the module is needed.

The height operator #

The highest weight line #

source
theorem TauCeti.exists_eq_smul_of_isGlHighestWeightVector_of_mem_lieSpan {K : Type u} [Field K] {n : Type u_1} [Fintype n] [LinearOrder n] [DecidableEq n] {mu : n → K} {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule (Matrix n n K) M] [LieModule K (Matrix n n K) M] {v : M} [CharZero K] (hv : IsGlHighestWeightVector mu v) {w : M} (hw : w ∈ LieSubmodule.lieSpan K (Matrix n n K) {v}) (hweight : ∀ (i : n), ⁅Matrix.single i i 1, w⁆ = mu i • w) :
∃ (c : K), w = c • v

The highest weight line. In the module a highest weight vector v of weight μ generates, every vector on which the diagonal matrix units act by μ is a multiple of v. In particular v really is, up to a scalar, the only highest weight vector of weight μ there.

source
theorem TauCeti.weightSpace_eq_span_singleton_of_isGlHighestWeightVector_of_lieSpan_eq_top {K : Type u} [Field K] {n : Type u_1} [Fintype n] [LinearOrder n] [DecidableEq n] {mu : n → K} {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule (Matrix n n K) M] [LieModule K (Matrix n n K) M] {v : M} [CharZero K] (hv : IsGlHighestWeightVector mu v) (hspan : LieSubmodule.lieSpan K (Matrix n n K) {v} = ⊤) :
↑(LieModule.weightSpace M ⇑((glWeightEquiv K n) mu)) = K ∙ v

The top weight space is the highest weight line. If a highest weight vector v generates its gl n K-module, then the honest weight space of its weight is exactly K · v.

source
theorem TauCeti.finrank_weightSpace_eq_one_of_isGlHighestWeightVector_of_lieSpan_eq_top {K : Type u} [Field K] {n : Type u_1} [Fintype n] [LinearOrder n] [DecidableEq n] {mu : n → K} {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule (Matrix n n K) M] [LieModule K (Matrix n n K) M] {v : M} [CharZero K] (hv : IsGlHighestWeightVector mu v) (hspan : LieSubmodule.lieSpan K (Matrix n n K) {v} = ⊤) :
Module.finrank K ↥(LieModule.weightSpace M ⇑((glWeightEquiv K n) mu)) = 1

The top weight has multiplicity one in a cyclic highest weight module.

The diagonal argument #

The classification #

source
noncomputable def TauCeti.lieModuleEquivOfIsGlHighestWeightVector {K : Type u} [Field K] {n : Type u_1} [DecidableEq n] [Fintype n] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule (Matrix n n K) M] {v : M} {M' : Type w₁} [AddCommGroup M'] [Module K M'] [LieRingModule (Matrix n n K) M'] {v' : M'} [LinearOrder n] {mu : n → K} [CharZero K] [LieModule K (Matrix n n K) M] [LieModule K (Matrix n n K) M'] [LieModule.IsIrreducible K (Matrix n n K) M] [LieModule.IsIrreducible K (Matrix n n K) M'] (hv : IsGlHighestWeightVector mu v) (hv' : IsGlHighestWeightVector mu v') :
M ≃ₗ⁅K,Matrix n n K⁆ M'

The equivalence between two irreducible gl n K-modules of the same highest weight, obtained by identifying both with the submodule of their product generated by the diagonal vector.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.lieModuleEquivOfIsGlHighestWeightVector_apply {K : Type u} [Field K] {n : Type u_1} [DecidableEq n] [Fintype n] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule (Matrix n n K) M] {v : M} {M' : Type w₁} [AddCommGroup M'] [Module K M'] [LieRingModule (Matrix n n K) M'] {v' : M'} [LinearOrder n] {mu : n → K} [CharZero K] [LieModule K (Matrix n n K) M] [LieModule K (Matrix n n K) M'] [LieModule.IsIrreducible K (Matrix n n K) M] [LieModule.IsIrreducible K (Matrix n n K) M'] (hv : IsGlHighestWeightVector mu v) (hv' : IsGlHighestWeightVector mu v') :
    (lieModuleEquivOfIsGlHighestWeightVector hv hv') v = v'
    source
    theorem TauCeti.nonempty_lieModuleEquiv_of_isGlHighestWeightVector {K : Type u} [Field K] {n : Type u_1} [DecidableEq n] [Fintype n] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule (Matrix n n K) M] {v : M} {M' : Type w₁} [AddCommGroup M'] [Module K M'] [LieRingModule (Matrix n n K) M'] {v' : M'} [LinearOrder n] {mu : n → K} [CharZero K] [LieModule K (Matrix n n K) M] [LieModule K (Matrix n n K) M'] [LieModule.IsIrreducible K (Matrix n n K) M] [LieModule.IsIrreducible K (Matrix n n K) M'] (hv : IsGlHighestWeightVector mu v) (hv' : IsGlHighestWeightVector mu v') :
    Nonempty (M ≃ₗ⁅K,Matrix n n K⁆ M')

    The highest weight determines the irreducible gl n K-module. Two irreducible gl n K-modules carrying highest weight vectors of the same weight μ are isomorphic. Neither is assumed finite-dimensional, and K is not assumed algebraically closed: the highest weight vectors are the data that would otherwise have to be produced.

    source
    theorem TauCeti.finrank_le_of_isGlHighestWeightVector {K : Type u} [Field K] {n : Type u_1} [DecidableEq n] [Fintype n] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule (Matrix n n K) M] {v : M} {M' : Type w₁} [AddCommGroup M'] [Module K M'] [LieRingModule (Matrix n n K) M'] {v' : M'} [LinearOrder n] {mu : n → K} [CharZero K] [LieModule K (Matrix n n K) M] [LieModule K (Matrix n n K) M'] [LieModule.IsIrreducible K (Matrix n n K) M] [FiniteDimensional K M'] (hv : IsGlHighestWeightVector mu v) (hv' : IsGlHighestWeightVector mu v') :
    Module.finrank K M ≤ Module.finrank K M'

    An irreducible highest weight module is the smallest one of its weight. If M is an irreducible gl n K-module with a highest weight vector of weight μ, then every finite-dimensional module carrying a highest weight vector of weight μ has at least the dimension of M. Cyclicity of the second vector is not needed: the submodule it generates already has dimension at least that of M.