The Gelfand invariants of gl n

Let 𝔼 be the square matrix over the universal enveloping algebra U(gl n) whose (i, j) entry is the canonical generator Eᵢⱼ = ι(Eᵢⱼ) of the matrix unit. The Gelfand invariants are the traces of its powers,

Cᵣ = trace (𝔼 ^ r) = ∑ i₁, …, ∑ iᵣ, Eᵢ₁ᵢ₂ Eᵢ₂ᵢ₃ ⋯ Eᵢᵣᵢ₁ ∈ U(gl n).

They are central in U(gl n) over every commutative ring. The engine is the commutator identity

⁅Eₐb, (𝔼 ^ r)ᵢⱼ⁆ = δ_{b i} (𝔼 ^ r)ₐⱼ - δ_{j a} (𝔼 ^ r)ᵢb,

proved by induction on r from the case r = 1, which is the bracket of two matrix units. Taking i = j and summing over i, the two terms cancel, so Cᵣ commutes with every matrix-unit generator and hence with all of U(gl n). In degree two C₂ is the trace-form Casimir element TauCeti.glCasimir, and in degree one C₁ is the image of the identity matrix.

An injection f : m ↪ n embeds gl m in gl n (TauCeti.glEmbedding), and the induced map of enveloping algebras sends 𝔼 for gl m to the submatrix of 𝔼 for gl n on the range of f. For the chain of upper-left corners gl 1 ⊆ gl 2 ⊆ ⋯ ⊆ gl n the images of the Gelfand invariants of all the corners are the Gelfand-Tsetlin generators of U(gl n). They pairwise commute: the generator of a smaller corner lies in the image of the enveloping algebra of a larger corner, whose Gelfand invariants are central there.

Main definitions

• TauCeti.glGeneratorMatrix: the matrix 𝔼 of matrix-unit generators of U(gl n).
• TauCeti.gelfandInvariant: the Gelfand invariant Cᵣ = trace (𝔼 ^ r).
• TauCeti.gelfandTsetlinGenerator: the image in U(gl (Fin n)) of the Gelfand invariant of the upper-left corner gl (Fin k).

Main results

• TauCeti.lie_ι_single_glGeneratorMatrix_pow_apply: the commutator identity above.
• TauCeti.gelfandInvariant_mem_center: the Gelfand invariants are central in U(gl n).
• TauCeti.gelfandInvariant_zero, TauCeti.gelfandInvariant_one and TauCeti.gelfandInvariant_two: the invariants of degree at most two are the rank, the image of the identity matrix and the trace-form Casimir element.
• TauCeti.map_glEmbedding_gelfandInvariant: the image of a Gelfand invariant along a corner embedding is the trace of a power of the corresponding submatrix of 𝔼.
• TauCeti.commute_map_glEmbedding_gelfandInvariant: images of Gelfand invariants along nested corner embeddings commute.
• TauCeti.map_glEmbedding_castSuccEmb_gelfandTsetlinGenerator: the generators below the top level come from the next smaller corner.
• TauCeti.commute_gelfandTsetlinGenerator_map_glEmbedding: a Gelfand-Tsetlin generator at level k commutes with the image of U(gl (Fin k)).
• TauCeti.commute_gelfandTsetlinGenerator: the Gelfand-Tsetlin generators pairwise commute.

References

• I. M. Gelfand, The center of an infinitesimal group ring, Mat. Sbornik N.S. 26(68) (1950), 103-112.
• A. Molev, Yangians and Classical Lie Algebras, Mathematical Surveys and Monographs 143, American Mathematical Society (2007), Chapter 7.

noncomputable def TauCeti.glGeneratorMatrix (K : Type u_1) [CommRing K] (n : Type u_2) [Fintype n] [DecidableEq n] : Matrix n n (UniversalEnvelopingAlgebra K (Matrix n n K))

The matrix 𝔼 of matrix-unit generators of U(gl n): its (i, j) entry is the canonical generator ι(Eᵢⱼ) of the matrix unit Eᵢⱼ.

@[simp]

theorem TauCeti.glGeneratorMatrix_apply (K : Type u_1) [CommRing K] (n : Type u_2) [Fintype n] [DecidableEq n] (i j : n) : glGeneratorMatrix K n i j = (UniversalEnvelopingAlgebra.ι K) (Matrix.single i j 1)

noncomputable def TauCeti.gelfandInvariant (K : Type u_1) [CommRing K] (n : Type u_2) [Fintype n] [DecidableEq n] (r : ℕ) : UniversalEnvelopingAlgebra K (Matrix n n K)

The Gelfand invariant Cᵣ = trace (𝔼 ^ r) = ∑ Eᵢ₁ᵢ₂ Eᵢ₂ᵢ₃ ⋯ Eᵢᵣᵢ₁ of degree r in the universal enveloping algebra of gl n.

theorem TauCeti.gelfandInvariant_def (K : Type u_1) [CommRing K] (n : Type u_2) [Fintype n] [DecidableEq n] (r : ℕ) : gelfandInvariant K n r = (glGeneratorMatrix K n ^ r).trace

@[simp]

theorem TauCeti.gelfandInvariant_zero (K : Type u_1) [CommRing K] (n : Type u_2) [Fintype n] [DecidableEq n] : gelfandInvariant K n 0 = ↑(Fintype.card n)

The Gelfand invariant of degree zero is the rank.

@[simp]

theorem TauCeti.gelfandInvariant_one (K : Type u_1) [CommRing K] (n : Type u_2) [Fintype n] [DecidableEq n] : gelfandInvariant K n 1 = (UniversalEnvelopingAlgebra.ι K) 1

The Gelfand invariant of degree one is the image of the identity matrix.

theorem TauCeti.gelfandInvariant_two (K : Type u_1) [CommRing K] (n : Type u_2) [Fintype n] [DecidableEq n] : gelfandInvariant K n 2 = glCasimir K n

The Gelfand invariant of degree two is the trace-form Casimir element.

theorem TauCeti.lie_ι_single_glGeneratorMatrix_pow_apply (K : Type u_1) [CommRing K] (n : Type u_2) [Fintype n] [DecidableEq n] (a b i j : n) (r : ℕ) : ⁅(UniversalEnvelopingAlgebra.ι K) (Matrix.single a b 1), (glGeneratorMatrix K n ^ r) i j⁆ = (if b = i then (glGeneratorMatrix K n ^ r) a j else 0) - if j = a then (glGeneratorMatrix K n ^ r) i b else 0

The bracket of a matrix-unit generator with an entry of 𝔼 ^ r: ⁅Eₐb, (𝔼 ^ r)ᵢⱼ⁆ = δ_{b i} (𝔼 ^ r)ₐⱼ - δ_{j a} (𝔼 ^ r)ᵢb.

theorem TauCeti.gelfandInvariant_mem_center (K : Type u_1) [CommRing K] (n : Type u_2) [Fintype n] [DecidableEq n] (r : ℕ) : gelfandInvariant K n r ∈ Subalgebra.center K (UniversalEnvelopingAlgebra K (Matrix n n K))

The Gelfand invariants are central in the universal enveloping algebra of gl n.

theorem TauCeti.commute_gelfandInvariant (K : Type u_1) [CommRing K] (n : Type u_2) [Fintype n] [DecidableEq n] (r s : ℕ) : Commute (gelfandInvariant K n r) (gelfandInvariant K n s)

Any two Gelfand invariants commute.

theorem TauCeti.map_glEmbedding_glGeneratorMatrix {K : Type u_1} [CommRing K] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (f : m ↪ n) : (glGeneratorMatrix K m).map ⇑(UniversalEnvelopingAlgebra.map K (glEmbedding K f)) = (glGeneratorMatrix K n).submatrix ⇑f ⇑f

The enveloping-algebra map of a corner embedding sends the generator matrix of gl m to the submatrix of the generator matrix of gl n on the range of the embedding.

theorem TauCeti.map_glEmbedding_gelfandInvariant {K : Type u_1} [CommRing K] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (f : m ↪ n) (r : ℕ) : (UniversalEnvelopingAlgebra.map K (glEmbedding K f)) (gelfandInvariant K m r) = ((glGeneratorMatrix K n).submatrix ⇑f ⇑f ^ r).trace

The image of the Gelfand invariant of gl m along a corner embedding f : m ↪ n is the trace of the r-th power of the submatrix of 𝔼 on the range of f.

theorem TauCeti.commute_map_glEmbedding_gelfandInvariant {K : Type u_1} [CommRing K] {l : Type u_2} {m : Type u_3} {n : Type u_4} [Fintype l] [DecidableEq l] [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (f : l ↪ m) (g : m ↪ n) (r s : ℕ) : Commute ((UniversalEnvelopingAlgebra.map K (glEmbedding K (f.trans g))) (gelfandInvariant K l r)) ((UniversalEnvelopingAlgebra.map K (glEmbedding K g)) (gelfandInvariant K m s))

Images of Gelfand invariants along nested corner embeddings l ↪ m ↪ n commute: the image of an invariant of gl l lies in the image of U(gl m), where the invariants of gl m are central.

noncomputable def TauCeti.gelfandTsetlinGenerator (K : Type u_1) [CommRing K] {n k : ℕ} (hk : k ≤ n) (r : ℕ) : UniversalEnvelopingAlgebra K (Matrix (Fin n) (Fin n) K)

The Gelfand-Tsetlin generator of degree r at level k ≤ n: the image in U(gl (Fin n)) of the Gelfand invariant Cᵣ of the upper-left corner gl (Fin k).

theorem TauCeti.gelfandTsetlinGenerator_def (K : Type u_1) [CommRing K] {n k : ℕ} (hk : k ≤ n) (r : ℕ) : gelfandTsetlinGenerator K hk r = (UniversalEnvelopingAlgebra.map K (glEmbedding K (Fin.castLEEmb hk))) (gelfandInvariant K (Fin k) r)

theorem TauCeti.gelfandTsetlinGenerator_eq_trace (K : Type u_1) [CommRing K] {n k : ℕ} (hk : k ≤ n) (r : ℕ) : gelfandTsetlinGenerator K hk r = ((glGeneratorMatrix K (Fin n)).submatrix (Fin.castLE hk) (Fin.castLE hk) ^ r).trace

The Gelfand-Tsetlin generator of degree r at level k is the trace of the r-th power of the upper-left k × k corner of the generator matrix.

@[simp]

theorem TauCeti.gelfandTsetlinGenerator_self (K : Type u_1) [CommRing K] {n : ℕ} (r : ℕ) : gelfandTsetlinGenerator K ⋯ r = gelfandInvariant K (Fin n) r

At the top level the Gelfand-Tsetlin generators are the Gelfand invariants of gl (Fin n).

theorem TauCeti.map_glEmbedding_castSuccEmb_gelfandTsetlinGenerator (K : Type u_1) [CommRing K] {n k : ℕ} (hk : k ≤ n) (r : ℕ) : (UniversalEnvelopingAlgebra.map K (glEmbedding K Fin.castSuccEmb)) (gelfandTsetlinGenerator K hk r) = gelfandTsetlinGenerator K ⋯ r

The Gelfand-Tsetlin generators of U(gl (Fin (n + 1))) below the top level are the images of those of U(gl (Fin n)) along the corner embedding.

theorem TauCeti.commute_gelfandTsetlinGenerator_map_glEmbedding (K : Type u_1) [CommRing K] {n k : ℕ} (hk : k ≤ n) (r : ℕ) (u : UniversalEnvelopingAlgebra K (Matrix (Fin k) (Fin k) K)) : Commute (gelfandTsetlinGenerator K hk r) ((UniversalEnvelopingAlgebra.map K (glEmbedding K (Fin.castLEEmb hk))) u)

A Gelfand-Tsetlin generator at level k commutes with the image of U(gl (Fin k)).

theorem TauCeti.commute_gelfandTsetlinGenerator (K : Type u_1) [CommRing K] {n k k' : ℕ} (hk : k ≤ n) (hk' : k' ≤ n) (r s : ℕ) : Commute (gelfandTsetlinGenerator K hk r) (gelfandTsetlinGenerator K hk' s)

The Gelfand-Tsetlin generators pairwise commute, across all levels and degrees.