The named irreducible gl N-module of a dominant weight

Let K be a field of characteristic zero. Every dominant integral weight mu : Fin N → K is the highest weight of a finite-dimensional irreducible gl N K-module, and that module is unique up to isomorphism. This file names it: TauCeti.glIrreducible N mu, the L(mu) of the general linear Lie algebra.

The construction

Both halves of the classification are already available, and the carrier is assembled from them. TauCeti.exists_isGlHighestWeightVector_of_isGlDominantIntegral realizes mu as the weight of a highest weight vector v in a finite-dimensional module, namely a trace twist of an exterior power of a standard module; TauCeti.nonempty_lieModuleEquiv_of_isGlHighestWeightVector says that an irreducible module carrying such a vector is determined by mu. What is missing between the two is that an irreducible one exists at all. The complete-reducibility API currently available in Tau Ceti applies to Killing-semisimple Lie algebras over algebraically closed fields, not directly to gl N K; this file instead uses a quotient construction available at the stated generality. The Lie submodule v generates is finite-dimensional, so its lattice of Lie submodules has a coatom, and TauCeti.isIrreducible_quotient_iff_isCoatom makes the quotient by that coatom irreducible, with the class of v a highest weight vector of weight mu still.

This quotient route avoids requiring a separate complete-reducibility transfer from sl N K to the particular trace-twisted exterior-power module. Such a transfer can recover a submodule realization because the identity acts by one scalar there, but that result is not part of the available API used by this construction.

Two choices go into the carrier, the decomposition of mu as an antitone tuple of natural numbers translated along the central direction and the coatom, and the construction singles out neither: both are made with Classical.choice, and nothing is claimed about which. The carrier is therefore characterized not by its construction but by TauCeti.nonempty_lieModuleEquiv_glIrreducible, which identifies it with any irreducible module carrying a highest weight vector of weight mu. Off the dominant weights the carrier is junk — still a finite-dimensional gl N K-module, but with no claim about it — as with the other total-by-convention constructions of the roadmap.

Main definitions

• TauCeti.glIrreducible N mu: the named carrier L(mu), with its K-module and gl N K-module structures and its finite-dimensionality.
• TauCeti.glIrreducibleGenerator N mu: its distinguished generator, the class of the chosen highest weight vector. Like the carrier itself it depends on the two choices above, so what is known of it is what the results below say.

The construction itself — the chosen decomposition of mu, the chosen highest weight vector, the Lie submodule it generates, the chosen coatom, and the lemmas about them — is private to this file and is no part of the interface. The data-carrying module instances transported from the quotient are marked @[no_expose], which is what lets their bodies name those private constants.

Main results

• TauCeti.isIrreducible_glIrreducible: L(mu) is irreducible for dominant integral mu.
• TauCeti.isGlHighestWeightVector_glIrreducibleGenerator, with its existential form TauCeti.exists_isGlHighestWeightVector_glIrreducible: its distinguished generator is a highest weight vector of weight mu and generates the carrier, which is what ties the carrier to its name; TauCeti.lieSpan_glIrreducibleGenerator_eq_top states the generating property explicitly.
• TauCeti.weightSpace_glIrreducible_eq_span_singleton and TauCeti.finrank_weightSpace_glIrreducible: the top weight space of L(mu) is its distinguished generator line, and therefore has dimension one.
• TauCeti.nonempty_lieModuleEquiv_glIrreducible: L(mu) is the irreducible of highest weight mu: every irreducible gl N K-module carrying a highest weight vector of weight mu is isomorphic to it, and TauCeti.finrank_glIrreducible_le bounds its dimension by that of any finite-dimensional module carrying such a vector.
• TauCeti.isIrreducible_glIrreducible_restrict_sl: L(mu) stays irreducible on restriction to sl N K, over any characteristic-zero field: by TauCeti.one_lie_glIrreducible_eq_smul the identity matrix acts by the explicit scalar ∑ i, mu i, so no algebraic closedness is needed to know that the centre acts by scalars.

References

This is the named carrier glIrreducible of Layer 9 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, with the structural pins isIrreducible_glIrreducible, finiteDimensional_glIrreducible, exists_isGlHighestWeightVector_glIrreducible and isIrreducible_glIrreducible_restrict_sl of its Suggested.lean.

• R. Goodman, N. R. Wallach, Symmetry, Representations, and Invariants, GTM 255, §5.5.

The realizing module and its highest weight vector

The coatom and the carrier

def TauCeti.glIrreducible {K : Type u} [Field K] [CharZero K] (N : ℕ) (mu : Fin N → K) : Type u

The irreducible gl N K-module L(mu) of highest weight mu, the quotient of the module generated by the chosen highest weight vector by the chosen maximal proper submodule of it.

For a dominant integral mu this is irreducible (TauCeti.isIrreducible_glIrreducible), carries a highest weight vector of weight mu (TauCeti.isGlHighestWeightVector_glIrreducibleGenerator), and is thereby determined up to isomorphism (TauCeti.nonempty_lieModuleEquiv_glIrreducible). Off the dominant weights nothing is claimed of it; it is total in mu only so that statements about it need not carry dominance in their types.

Equations

• TauCeti.glIrreducible N mu = (↥(TauCeti.glCarrierSpan✝ K mu) ⧸ TauCeti.glCarrierCoatom✝ K mu)

@[instance_reducible]

noncomputable instance TauCeti.instAddCommGroupGlIrreducible {K : Type u} [Field K] [CharZero K] {N : ℕ} {mu : Fin N → K} : AddCommGroup (glIrreducible N mu)

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.instModuleGlIrreducible {K : Type u} [Field K] [CharZero K] {N : ℕ} {mu : Fin N → K} : Module K (glIrreducible N mu)

Equations

• TauCeti.instModuleGlIrreducible = { smul := TauCeti.instModuleGlIrreducible._aux_1✝, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[instance_reducible]

noncomputable instance TauCeti.instLieRingModuleMatrixFinGlIrreducible {K : Type u} [Field K] [CharZero K] {N : ℕ} {mu : Fin N → K} : LieRingModule (Matrix (Fin N) (Fin N) K) (glIrreducible N mu)

Equations

• TauCeti.instLieRingModuleMatrixFinGlIrreducible = { bracket := TauCeti.instLieRingModuleMatrixFinGlIrreducible._aux_1✝, add_lie := ⋯, lie_add := ⋯, leibniz_lie := ⋯ }

instance TauCeti.instLieModuleMatrixFinGlIrreducible {K : Type u} [Field K] [CharZero K] {N : ℕ} {mu : Fin N → K} : LieModule K (Matrix (Fin N) (Fin N) K) (glIrreducible N mu)

instance TauCeti.finiteDimensional_glIrreducible {K : Type u} [Field K] [CharZero K] {N : ℕ} {mu : Fin N → K} : FiniteDimensional K (glIrreducible N mu)

L(mu) is finite-dimensional, for every mu: it is a quotient of a submodule of an exterior power of a finite-dimensional standard module. Dominance is needed only to know that it is not the zero module.

noncomputable def TauCeti.glIrreducibleGenerator {K : Type u} [Field K] [CharZero K] (N : ℕ) (mu : Fin N → K) : glIrreducible N mu

The distinguished generator of L(mu), the class of the chosen highest weight vector. It inherits the two choices the carrier is built from and is not canonical; what is known of it is TauCeti.isGlHighestWeightVector_glIrreducibleGenerator.

Equations

• TauCeti.glIrreducibleGenerator N mu = (LieSubmodule.Quotient.mk' (TauCeti.glCarrierCoatom✝ K mu)) ⟨TauCeti.glCarrierVector✝ K mu, ⋯⟩

The structure of the carrier

theorem TauCeti.isIrreducible_glIrreducible {K : Type u} [Field K] [CharZero K] {N : ℕ} {mu : Fin N → K} (hmu : IsGlDominantIntegral mu) : LieModule.IsIrreducible K (Matrix (Fin N) (Fin N) K) (glIrreducible N mu)

L(mu) is irreducible, for a dominant integral mu: it is the quotient of a Lie module by a coatom of its lattice of Lie submodules.

theorem TauCeti.isGlHighestWeightVector_glIrreducibleGenerator {K : Type u} [Field K] [CharZero K] {N : ℕ} {mu : Fin N → K} (hmu : IsGlDominantIntegral mu) : IsGlHighestWeightVector mu (glIrreducibleGenerator N mu)

The distinguished generator of L(mu) is a highest weight vector of weight mu, the statement that ties the carrier to its name. It is nonzero because the chosen vector generates the module being divided, so a proper submodule cannot contain it.

theorem TauCeti.lieSpan_glIrreducibleGenerator_eq_top {K : Type u} [Field K] [CharZero K] {N : ℕ} {mu : Fin N → K} (hmu : IsGlDominantIntegral mu) : LieSubmodule.lieSpan K (Matrix (Fin N) (Fin N) K) {glIrreducibleGenerator N mu} = ⊤

The distinguished highest weight vector generates L(mu).

theorem TauCeti.weightSpace_glIrreducible_eq_span_singleton {K : Type u} [Field K] [CharZero K] {N : ℕ} {mu : Fin N → K} (hmu : IsGlDominantIntegral mu) : ↑(LieModule.weightSpace (glIrreducible N mu) ⇑((glWeightEquiv K (Fin N)) mu)) = K ∙ glIrreducibleGenerator N mu

The top weight space of L(mu) is its distinguished generator line.

@[simp]

theorem TauCeti.finrank_weightSpace_glIrreducible {K : Type u} [Field K] [CharZero K] {N : ℕ} {mu : Fin N → K} (hmu : IsGlDominantIntegral mu) : Module.finrank K ↥(LieModule.weightSpace (glIrreducible N mu) ⇑((glWeightEquiv K (Fin N)) mu)) = 1

The top weight has multiplicity one in L(mu).

theorem TauCeti.exists_isGlHighestWeightVector_glIrreducible {K : Type u} [Field K] [CharZero K] {N : ℕ} {mu : Fin N → K} (hmu : IsGlDominantIntegral mu) : ∃ (v : glIrreducible N mu), IsGlHighestWeightVector mu v

L(mu) carries a highest weight vector of weight mu, the existential form of TauCeti.isGlHighestWeightVector_glIrreducibleGenerator pinned by the roadmap.

theorem TauCeti.nonempty_lieModuleEquiv_glIrreducible {K : Type u} [Field K] [CharZero K] {N : ℕ} {mu : Fin N → K} {M : Type u_1} [AddCommGroup M] [Module K M] [LieRingModule (Matrix (Fin N) (Fin N) K) M] [LieModule K (Matrix (Fin N) (Fin N) K) M] [LieModule.IsIrreducible K (Matrix (Fin N) (Fin N) K) M] {v : M} (hmu : IsGlDominantIntegral mu) (hv : IsGlHighestWeightVector mu v) : Nonempty (M ≃ₗ⁅K,Matrix (Fin N) (Fin N) K⁆ glIrreducible N mu)

L(mu) is the irreducible of highest weight mu. Any irreducible gl N K-module carrying a highest weight vector of weight mu is isomorphic to the carrier, so nothing is lost by naming one of them. M is not assumed finite-dimensional, the classification TauCeti.nonempty_lieModuleEquiv_of_isGlHighestWeightVector needing no finiteness; that M then is finite-dimensional is a consequence rather than a hypothesis.

theorem TauCeti.finrank_glIrreducible_le {K : Type u} [Field K] [CharZero K] {N : ℕ} {mu : Fin N → K} {M : Type u_1} [AddCommGroup M] [Module K M] [LieRingModule (Matrix (Fin N) (Fin N) K) M] [LieModule K (Matrix (Fin N) (Fin N) K) M] [FiniteDimensional K M] {v : M} (hmu : IsGlDominantIntegral mu) (hv : IsGlHighestWeightVector mu v) : Module.finrank K (glIrreducible N mu) ≤ Module.finrank K M

L(mu) has the smallest dimension of the modules of highest weight mu: any finite-dimensional gl N K-module carrying a highest weight vector of weight mu has at least the dimension of the carrier.

theorem TauCeti.one_lie_glIrreducible_eq_smul {K : Type u} [Field K] [CharZero K] {N : ℕ} {mu : Fin N → K} (hmu : IsGlDominantIntegral mu) (m : glIrreducible N mu) : ⁅1, m⁆ = (∑ i : Fin N, mu i) • m

The identity matrix acts on L(mu) by the scalar ∑ i, mu i.

theorem TauCeti.isIrreducible_glIrreducible_restrict_sl {K : Type u} [Field K] [CharZero K] {N : ℕ} {mu : Fin N → K} (hmu : IsGlDominantIntegral mu) : LieModule.IsIrreducible K (↥(LieAlgebra.SpecialLinear.sl (Fin N) K)) (glIrreducible N mu)

L(mu) stays irreducible on restriction to sl N K: the identity matrix acts on it by the scalar ∑ i, mu i (TauCeti.one_lie_glIrreducible_eq_smul), so the centre of gl N K acts by scalars and the sl N K-submodules are already gl N K-submodules. The explicit scalar is what lets the statement hold over any characteristic-zero field, algebraic closedness being needed only where the scalar has to be produced by Schur's lemma.