The Killing identification of S(L) with the polynomial functions on L

Let L be a finite-dimensional Lie algebra over a field K whose Killing form κ is nondegenerate. The Killing form is invariant, κ ⁅x, y⁆ z = -κ y ⁅x, z⁆, so x ↦ κ x is an equivalence of Lie modules from the adjoint module L to the coadjoint module L*. It induces an algebra equivalence from the symmetric algebra S(L) to the algebra S(L*) of polynomial functions on L, sending a generator x to the linear function κ x, and this equivalence intertwines the adjoint action of L on S(L) with the coadjoint action on S(L*). Hence it carries the adjoint invariants S(L)^L onto the invariant polynomial functions S(L*)^L.

This is the identification under which polynomial functions on L, such as the trace polynomials x ↦ tr (ρ(x) ^ m) of a representation ρ, are compared with the leading symbols of central elements of the enveloping algebra, which live in S(L)^L, in the proof of the Harish-Chandra isomorphism by Chevalley's restriction theorem.

Main definitions

• TauCeti.killingSymmetricEquiv: the algebra equivalence S(L) ≃ S(L*) induced by the Killing duality TauCeti.killingDuality : L ≃ L* of TauCeti/Algebra/Lie/Killing/Duality.lean.

Main results

• TauCeti.killingSymmetricEquiv_ι: a generator x goes to the linear function κ x.
• TauCeti.killingSymmetricEquiv_symm_ι: conversely, a linear function f goes back to the generator x with κ x = f.
• TauCeti.killingSymmetricEquiv_lieModuleDerivation: the equivalence intertwines the adjoint action on S(L) with the coadjoint action on S(L*).
• TauCeti.map_killingSymmetricEquiv_lieInvariants: it carries the invariants S(L)^L onto the invariant polynomial functions S(L*)^L.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §23.1 and §23.3.
• J. Dixmier, Enveloping Algebras, §7.3.

noncomputable def TauCeti.killingSymmetricEquiv (K : Type u_1) (L : Type u_2) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] : SymmetricAlgebra K L ≃ₐ[K] SymmetricAlgebra K (Module.Dual K L)

The algebra equivalence of the symmetric algebra S(L) with the algebra S(L*) of polynomial functions on L induced by the Killing duality.

theorem TauCeti.killingSymmetricEquiv_apply (K : Type u_1) (L : Type u_2) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (p : SymmetricAlgebra K L) : (killingSymmetricEquiv K L) p = (SymmetricAlgebra.map K (killingForm K L)) p

The Killing equivalence S(L) ≃ S(L*) is the symmetric-algebra map of the Killing form, read as a linear map L → L*.

@[simp]

theorem TauCeti.killingSymmetricEquiv_ι (K : Type u_1) (L : Type u_2) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (x : L) : (killingSymmetricEquiv K L) ((SymmetricAlgebra.ι K L) x) = (SymmetricAlgebra.ι K (Module.Dual K L)) ((killingForm K L) x)

The Killing equivalence S(L) ≃ S(L*) sends a generator x to the linear function κ x.

theorem TauCeti.killingSymmetricEquiv_symm (K : Type u_1) (L : Type u_2) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] : (killingSymmetricEquiv K L).symm = SymmetricAlgebra.mapEquiv K (killingDuality K L).symm.toLinearEquiv

The inverse of the Killing equivalence S(L) ≃ S(L*) is the symmetric-algebra equivalence induced by the inverse of the Killing duality.

@[simp]

theorem TauCeti.killingSymmetricEquiv_symm_ι (K : Type u_1) (L : Type u_2) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (f : Module.Dual K L) : (killingSymmetricEquiv K L).symm ((SymmetricAlgebra.ι K (Module.Dual K L)) f) = (SymmetricAlgebra.ι K L) ((killingDuality K L).symm f)

The inverse of the Killing equivalence S(L) ≃ S(L*) sends a linear function f to the generator x with κ x = f.

theorem TauCeti.killingSymmetricEquiv_lieModuleDerivation (K : Type u_1) (L : Type u_2) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (x : L) (p : SymmetricAlgebra K L) : (killingSymmetricEquiv K L) (((SymmetricAlgebra.lieModuleDerivation K L L) x) p) = ((SymmetricAlgebra.lieModuleDerivation K L (Module.Dual K L)) x) ((killingSymmetricEquiv K L) p)

The Killing equivalence intertwines the adjoint and coadjoint actions: it carries the adjoint derivation of x on S(L) to the coadjoint derivation of x on S(L*).

@[simp]

theorem TauCeti.killingSymmetricEquiv_mem_lieInvariants_iff (K : Type u_1) (L : Type u_2) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {p : SymmetricAlgebra K L} : (killingSymmetricEquiv K L) p ∈ SymmetricAlgebra.lieInvariants K L (Module.Dual K L) ↔ p ∈ SymmetricAlgebra.lieInvariants K L L

An element of S(L) is invariant exactly when its image in S(L*) under the Killing equivalence is an invariant polynomial function.

theorem TauCeti.map_killingSymmetricEquiv_lieInvariants (K : Type u_1) (L : Type u_2) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] : Subalgebra.map (↑(killingSymmetricEquiv K L)) (SymmetricAlgebra.lieInvariants K L L) = SymmetricAlgebra.lieInvariants K L (Module.Dual K L)

The Killing equivalence identifies the invariants: it carries S(L)^L onto the invariant polynomial functions S(L*)^L.