The single-weight isotypy criterion for gl_n

This file packages highest-weight existence and uniqueness into isotypy criteria for modules over the general linear Lie algebra. If every irreducible submodule has the same highest weight, then every pair of irreducible submodules is equivalent. Under complete reducibility, the module is the direct sum of copies of the named irreducible with that weight when the module is nonzero. For the zero module, the result is the empty direct sum and makes no dominance or irreducibility claim about the named carrier.

The foundational LieModule.IsIsotypic assertion is pairwise. The counted direct-sum theorem adds complete reducibility explicitly, since it is not automatic for representations of a reductive Lie algebra unless its centre acts semisimply.

Main results

• isIsotypic_of_forall_irreducible_exists_isGlHighestWeightVector: a criterion using a supplied highest-weight vector in every irreducible submodule.
• isIsotypicOfType_of_forall_irreducible_exists_isGlHighestWeightVector: the supplied-vector criterion identifying an arbitrary irreducible type.
• isIsotypic_of_forall_isGlHighestWeightVector: the finite-dimensional criterion over an algebraically closed field.
• isIsotypicOfType_of_forall_isGlHighestWeightVector: the criterion identifying an arbitrary irreducible type from one highest-weight vector.
• isGlDominantIntegral_of_forall_isGlHighestWeightVector: the dominance consequence of the finite-dimensional single-weight hypothesis for a nonzero module.
• LieSubmodule.exists_isGlHighestWeightVector_of_forall: the highest-weight existence criterion for a nonzero submodule.
• isIsotypicOfType_glIrreducible_of_forall_isGlHighestWeightVector: the fixed-carrier criterion.
• nonempty_lieModuleEquiv_directSum_glIrreducible_of_forall_isGlHighestWeightVector: the counted direct-sum criterion for a completely reducible module.

References

The formal precedent is TauCeti.isIsotypicOfType_of_forall_isHighestWeightVector in TauCeti/Algebra/Lie/HighestWeight/Isotypic.lean.

theorem TauCeti.isIsotypicOfType_of_forall_irreducible_exists_isGlHighestWeightVector {K : Type u} [Field K] [CharZero K] {n : Type u_1} [DecidableEq n] [Fintype n] [LinearOrder n] {M : Type v} [AddCommGroup M] [Module K M] [LieRingModule (Matrix n n K) M] [LieModule K (Matrix n n K) M] {S : Type w} [AddCommGroup S] [Module K S] [LieRingModule (Matrix n n K) S] [LieModule K (Matrix n n K) S] {mu : n → K} [LieModule.IsIrreducible K (Matrix n n K) S] {w : S} (hw : IsGlHighestWeightVector mu w) (h : ∀ (P : LieSubmodule K (Matrix n n K) M) [LieModule.IsIrreducible K (Matrix n n K) ↥P], ∃ (v : ↥P), IsGlHighestWeightVector mu v) : LieModule.IsIsotypicOfType K (Matrix n n K) M S

If every irreducible submodule of a gl_n-module carries a highest-weight vector of weight mu, and an irreducible module S carries one too, then the original module is isotypic of type S.

This supplied-vector form does not require finite-dimensionality or an algebraically closed field.

theorem TauCeti.isIsotypic_of_forall_irreducible_exists_isGlHighestWeightVector {K : Type u} [Field K] [CharZero K] {n : Type u_1} [DecidableEq n] [Fintype n] [LinearOrder n] {M : Type v} [AddCommGroup M] [Module K M] [LieRingModule (Matrix n n K) M] [LieModule K (Matrix n n K) M] {mu : n → K} (h : ∀ (P : LieSubmodule K (Matrix n n K) M) [LieModule.IsIrreducible K (Matrix n n K) ↥P], ∃ (v : ↥P), IsGlHighestWeightVector mu v) : LieModule.IsIsotypic K (Matrix n n K) M

If every irreducible submodule of a gl_n-module carries a highest-weight vector of weight mu, then the module is isotypic.

This form does not require finite-dimensionality or an algebraically closed field: those hypotheses are only needed to produce the highest-weight vectors, which are supplied here.

theorem LieSubmodule.exists_isGlHighestWeightVector_of_forall {K : Type u} [Field K] [CharZero K] {N : ℕ} {M : Type v} [AddCommGroup M] [Module K M] [LieRingModule (Matrix (Fin N) (Fin N) K) M] [LieModule K (Matrix (Fin N) (Fin N) K) M] {mu : Fin N → K} [IsAlgClosed K] (P : LieSubmodule K (Matrix (Fin N) (Fin N) K) M) [FiniteDimensional K ↥P] (hP : P ≠ ⊥) (h : ∀ (nu : Fin N → K) (v : ↥P), TauCeti.IsGlHighestWeightVector nu v → nu = mu) : ∃ (v : ↥P), TauCeti.IsGlHighestWeightVector mu v

Every nonzero finite-dimensional submodule of a gl_N-module over an algebraically closed field contains a highest-weight vector of weight mu, when all highest-weight vectors in that submodule have that weight.

theorem TauCeti.isIsotypic_of_forall_isGlHighestWeightVector {K : Type u} [Field K] [CharZero K] {N : ℕ} {M : Type v} [AddCommGroup M] [Module K M] [LieRingModule (Matrix (Fin N) (Fin N) K) M] [LieModule K (Matrix (Fin N) (Fin N) K) M] {mu : Fin N → K} [IsAlgClosed K] [FiniteDimensional K M] (h : ∀ (nu : Fin N → K) (v : M), IsGlHighestWeightVector nu v → nu = mu) : LieModule.IsIsotypic K (Matrix (Fin N) (Fin N) K) M

The single-weight isotypy criterion for gl_N. If every highest-weight vector in a finite-dimensional gl_N-module over an algebraically closed field has weight mu, then every pair of irreducible submodules is equivalent.

theorem TauCeti.isIsotypicOfType_of_forall_isGlHighestWeightVector {K : Type u} [Field K] [CharZero K] {N : ℕ} {M : Type v} [AddCommGroup M] [Module K M] [LieRingModule (Matrix (Fin N) (Fin N) K) M] [LieModule K (Matrix (Fin N) (Fin N) K) M] {S : Type w} [AddCommGroup S] [Module K S] [LieRingModule (Matrix (Fin N) (Fin N) K) S] [LieModule K (Matrix (Fin N) (Fin N) K) S] {mu : Fin N → K} [IsAlgClosed K] [FiniteDimensional K M] [LieModule.IsIrreducible K (Matrix (Fin N) (Fin N) K) S] {w : S} (hw : IsGlHighestWeightVector mu w) (h : ∀ (nu : Fin N → K) (v : M), IsGlHighestWeightVector nu v → nu = mu) : LieModule.IsIsotypicOfType K (Matrix (Fin N) (Fin N) K) M S

If an irreducible gl_N-module S carries a highest-weight vector of weight mu, then a finite-dimensional module over an algebraically closed field whose highest-weight vectors all have weight mu is isotypic of type S.

theorem TauCeti.isGlDominantIntegral_of_forall_isGlHighestWeightVector {K : Type u} [Field K] [CharZero K] {N : ℕ} {M : Type v} [AddCommGroup M] [Module K M] [LieRingModule (Matrix (Fin N) (Fin N) K) M] [LieModule K (Matrix (Fin N) (Fin N) K) M] {mu : Fin N → K} [IsAlgClosed K] [FiniteDimensional K M] [Nontrivial M] (h : ∀ (nu : Fin N → K) (v : M), IsGlHighestWeightVector nu v → nu = mu) : IsGlDominantIntegral mu

If all highest-weight vectors in a nonzero finite-dimensional gl_N-module over an algebraically closed field have weight mu, then mu is dominant integral.

theorem TauCeti.isIsotypicOfType_glIrreducible_of_forall_isGlHighestWeightVector {K : Type u} [Field K] [CharZero K] {N : ℕ} {M : Type v} [AddCommGroup M] [Module K M] [LieRingModule (Matrix (Fin N) (Fin N) K) M] [LieModule K (Matrix (Fin N) (Fin N) K) M] {mu : Fin N → K} [IsAlgClosed K] [FiniteDimensional K M] (h : ∀ (nu : Fin N → K) (v : M), IsGlHighestWeightVector nu v → nu = mu) : LieModule.IsIsotypicOfType K (Matrix (Fin N) (Fin N) K) M (glIrreducible N mu)

The single-weight fixed-carrier criterion for gl_N. A finite-dimensional module over an algebraically closed field whose highest-weight vectors all have weight mu is isotypic of type glIrreducible N mu. For the zero module this holds vacuously.

theorem TauCeti.nonempty_lieModuleEquiv_directSum_glIrreducible_of_forall_isGlHighestWeightVector {K : Type u} [Field K] [CharZero K] {N : ℕ} {M : Type v} [AddCommGroup M] [Module K M] [LieRingModule (Matrix (Fin N) (Fin N) K) M] [LieModule K (Matrix (Fin N) (Fin N) K) M] {mu : Fin N → K} [IsAlgClosed K] [FiniteDimensional K M] [ComplementedLattice (LieSubmodule K (Matrix (Fin N) (Fin N) K) M)] (h : ∀ (nu : Fin N → K) (v : M), IsGlHighestWeightVector nu v → nu = mu) : Nonempty (M ≃ₗ⁅K,Matrix (Fin N) (Fin N) K⁆ DirectSum (Fin (LieModule.isotypicMultiplicity K (Matrix (Fin N) (Fin N) K) M (glIrreducible N mu))) fun (x : Fin (LieModule.isotypicMultiplicity K (Matrix (Fin N) (Fin N) K) M (glIrreducible N mu))) => glIrreducible N mu)

The single-weight direct-sum criterion for gl_N. A finite-dimensional completely reducible gl_N-module over an algebraically closed field whose highest-weight vectors all have weight mu is the direct sum of LieModule.isotypicMultiplicity copies of the named irreducible glIrreducible N mu.

Complete reducibility is an explicit hypothesis: it is not automatic for a reductive Lie algebra, whose centre may act non-semisimply. For a nonzero module the weight is dominant integral, so the named carrier is irreducible. For the zero module the multiplicity is zero, and the theorem only identifies the empty direct sum without making a claim about the carrier.