The trace-form Casimir element of gl n

For the general linear Lie algebra gl n R = Matrix n n R, the invariant nondegenerate form used by highest-weight theory is the trace form

B(X, Y) = trace (X * Y).

The matrix units Eᵢⱼ and Eⱼᵢ are dual for this form. The corresponding Casimir element is

Ω = ∑ i, ∑ j, ι(Eᵢⱼ) ι(Eⱼᵢ) ∈ U(gl n).

This file constructs TauCeti.glCasimir and proves that it is central. Centrality is proved directly on matrix units: the four terms in the commutator with Eₐb cancel in pairs. Since the matrix units span gl n and the canonical generators span its universal enveloping algebra as an algebra, this proves commutation with every element of U(gl n).

On a module generated by a gl n highest-weight vector of weight μ, this element acts as ∑ i, μ i * (μ i + n - 1 - 2 * i).

Main definitions and results

• TauCeti.glCasimir: the trace-form Casimir element of gl n.
• TauCeti.glCasimir_def: its defining matrix-unit sum.
• TauCeti.ι_mul_glCasimir: every canonical Lie generator commutes with glCasimir.
• TauCeti.glCasimir_mem_center: glCasimir is central in U(gl n).
• TauCeti.representation_glCasimir_apply: its action on any Lie module is the double-action sum ∑ i, ∑ j, ⁅Eᵢⱼ, ⁅Eⱼᵢ, m⁆⁆.
• TauCeti.glCasimir_smul_of_isGlHighestWeightVector: its scalar action on a highest-weight vector.
• TauCeti.glCasimir_smul_of_isGlHighestWeightVector_of_lieSpan_eq_top: its scalar action on a cyclic highest-weight module.
• TauCeti.glCasimir_eigenvalue_glHalfStaircase: the Casimir polynomial at the half-shifted staircase over any field in which two is invertible.
• TauCeti.glCasimir_eigenvalue_glStaircase: the Casimir polynomial at the rational staircase.

References

• R. Goodman and N. R. Wallach, Symmetry, Representations, and Invariants, Springer GTM 255 (2009), Chapter 4.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Springer GTM 9 (1972), Section 6.

noncomputable def TauCeti.glCasimir (K : Type u) [CommRing K] (n : Type v) [Fintype n] [DecidableEq n] : UniversalEnvelopingAlgebra K (Matrix n n K)

The trace-form Casimir element of gl n K, ∑ i, ∑ j, ι(Eᵢⱼ) * ι(Eⱼᵢ) ∈ U(gl n K).

The two matrix units in each summand are dual for TauCeti.traceBilinForm K n, since trace (Eᵢⱼ Eₖₗ) is 1 exactly when j = k and l = i.

Equations

• TauCeti.glCasimir K n = ∑ i : n, ∑ j : n, (UniversalEnvelopingAlgebra.ι K) (Matrix.single i j 1) * (UniversalEnvelopingAlgebra.ι K) (Matrix.single j i 1)

theorem TauCeti.glCasimir_def (K : Type u) [CommRing K] (n : Type v) [Fintype n] [DecidableEq n] : glCasimir K n = ∑ i : n, ∑ j : n, (UniversalEnvelopingAlgebra.ι K) (Matrix.single i j 1) * (UniversalEnvelopingAlgebra.ι K) (Matrix.single j i 1)

The trace-form Casimir element is its defining sum over pairs of matrix units.

theorem TauCeti.ι_mul_glCasimir (K : Type u) [CommRing K] (n : Type v) [Fintype n] [DecidableEq n] (X : Matrix n n K) : (UniversalEnvelopingAlgebra.ι K) X * glCasimir K n = glCasimir K n * (UniversalEnvelopingAlgebra.ι K) X

Every canonical Lie generator commutes with the trace-form Casimir element of gl n.

theorem TauCeti.glCasimir_mem_center (K : Type u) [CommRing K] (n : Type v) [Fintype n] [DecidableEq n] : glCasimir K n ∈ Subalgebra.center K (UniversalEnvelopingAlgebra K (Matrix n n K))

The trace-form Casimir element of gl n is central in its universal enveloping algebra.

theorem TauCeti.representation_glCasimir_apply (K : Type u) [CommRing K] (n : Type v) [Fintype n] [DecidableEq n] {M : Type u_1} [AddCommGroup M] [Module K M] [LieRingModule (Matrix n n K) M] [LieModule K (Matrix n n K) M] (m : M) : ((UniversalEnvelopingAlgebra.representation K (Matrix n n K) M) (glCasimir K n)) m = ∑ i : n, ∑ j : n, ⁅Matrix.single i j 1, ⁅Matrix.single j i 1, m⁆⁆

The trace-form Casimir acts on a gl n-module by the double-action sum ∑ i, ∑ j, ⁅Eᵢⱼ, ⁅Eⱼᵢ, m⁆⁆.

This is the computational interface used by the highest-weight eigenvalue calculation: it exposes the matrix-unit expression while keeping TauCeti.glCasimir itself opaque.

theorem TauCeti.glCasimir_smul_of_isGlHighestWeightVector (K : Type u) [CommRing K] {N : ℕ} {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] {mu : Fin N → K} {v : M} (hv : IsGlHighestWeightVector mu v) : ((UniversalEnvelopingAlgebra.representation K (Matrix (Fin N) (Fin N) K) M) (glCasimir K (Fin N))) v = (∑ i : Fin N, mu i * (mu i + ↑N - 1 - 2 * ↑↑i)) • v

On a highest-weight vector of weight mu, the trace-form Casimir acts by the scalar ∑ i, mu i * (mu i + N - 1 - 2 * i).

theorem TauCeti.glCasimir_smul_of_isGlHighestWeightVector_of_lieSpan_eq_top (K : Type u) [CommRing K] {N : ℕ} {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] {mu : Fin N → K} {v : M} (hv : IsGlHighestWeightVector mu v) (hgen : LieSubmodule.lieSpan K (Matrix (Fin N) (Fin N) K) {v} = ⊤) (m : M) : ((UniversalEnvelopingAlgebra.representation K (Matrix (Fin N) (Fin N) K) M) (glCasimir K (Fin N))) m = (∑ i : Fin N, mu i * (mu i + ↑N - 1 - 2 * ↑↑i)) • m

On a cyclic gl N-module generated by a highest-weight vector of weight mu, the trace-form Casimir acts by the scalar ∑ i, mu i * (mu i + N - 1 - 2 * i).

theorem TauCeti.glCasimir_eigenvalue_glHalfStaircase {F : Type u_1} [Field F] [Invertible 2] (N : ℕ) : ∑ i : Fin N, glHalfStaircase F N i * (glHalfStaircase F N i + ↑N - 1 - 2 * ↑↑i) = ↑N * (2 * ↑N ^ 2 - 1) / 4

The trace-form gl_N Casimir polynomial at the half-shifted staircase over a field in which two is invertible is N (2 N² - 1) / 4.

theorem TauCeti.glCasimir_eigenvalue_glHalfStaircase_sub_single {F : Type u_1} [Field F] [Invertible 2] (N : ℕ) (t : Fin N) : ∑ i : Fin N, (glHalfStaircase F N - Pi.single t 1) i * ((glHalfStaircase F N - Pi.single t 1) i + ↑N - 1 - 2 * ↑↑i) = ↑N * (2 * ↑N ^ 2 - 1) / 4 - 3 * ↑N + 3 + 4 * ↑↑t

Lowering the t-th entry of the half-shifted staircase changes the Casimir scalar by -3 N + 3 + 4 t.

theorem TauCeti.glCasimir_eigenvalue_glHalfStaircase_sub_single_diff {F : Type u_1} [Field F] [Invertible 2] (N : ℕ) (s t : Fin N) : ∑ i : Fin N, (glHalfStaircase F N - Pi.single t 1) i * ((glHalfStaircase F N - Pi.single t 1) i + ↑N - 1 - 2 * ↑↑i) - ∑ i : Fin N, (glHalfStaircase F N - Pi.single s 1) i * ((glHalfStaircase F N - Pi.single s 1) i + ↑N - 1 - 2 * ↑↑i) = 4 * (↑↑t - ↑↑s)

The difference of the lowered half-shifted staircase Casimir scalars is 4 (t - s).

theorem TauCeti.glCasimir_eigenvalue_glHalfStaircase_sub_single_ne {F : Type u_1} [Field F] [CharZero F] (N : ℕ) (s t : Fin N) (hst : s ≠ t) : ∑ i : Fin N, (glHalfStaircase F N - Pi.single t 1) i * ((glHalfStaircase F N - Pi.single t 1) i + ↑N - 1 - 2 * ↑↑i) ≠ ∑ i : Fin N, (glHalfStaircase F N - Pi.single s 1) i * ((glHalfStaircase F N - Pi.single s 1) i + ↑N - 1 - 2 * ↑↑i)

The lowered half-shifted staircase Casimir scalars are distinct at distinct indices.

theorem TauCeti.glCasimir_eigenvalue_glStaircase {F : Type u_1} [Field F] [CharZero F] (N : ℕ) : ∑ i : Fin N, (algebraMap ℚ F) (glStaircase N i) * ((algebraMap ℚ F) (glStaircase N i) + ↑N - 1 - 2 * ↑↑i) = ↑N * (2 * ↑N ^ 2 - 1) / 4

The trace-form gl_N Casimir polynomial at the rational staircase weight is N (2 N² - 1) / 4.