Chevalley's restriction theorem

Let L be a finite-dimensional Lie algebra over a field K of characteristic zero whose Killing form is nondegenerate, and H a splitting Cartan subalgebra. Restricting polynomial functions from L to H is, through the Killing identifications, the algebra map TauCeti.lieCartanRestriction H : S(L) →ₐ[K] S(H). Chevalley's restriction theorem says that it restricts to an isomorphism from the invariants S(L)^L onto the Weyl invariants S(H)^W (TauCeti.linearInvariants H). It has three parts.

• Weyl invariance. The restriction of an invariant is fixed by the coreflection of every root (TauCeti.map_coreflection_lieCartanRestriction), and the coreflections generate the Weyl group.
• Injectivity on S(L)^L is LieSubalgebra.lieCartanRestriction_injOn_lieInvariants: it rests on the density of the conjugates of H under the inner automorphisms.
• Surjectivity. The Weyl invariants form a graded subalgebra, and in each degree m they are spanned by the power sums ∑_μ dim L(λ)_μ · t_μ ^ m of the weights of the irreducible modules L(λ), λ dominant integral (TauCeti.span_highestWeightTracePowerRestriction_eq_linearInvariants_inf_homogeneousSubmodule). Each such power sum is the restriction of the invariant polynomial function x ↦ tr (ρ_λ(x) ^ m) on L. This part uses that K is algebraically closed.

Main definitions

• LieSubalgebra.lieChevalleyRestrictionIso H: the isomorphism S(L)^L ≃ₐ[K] S(H)^W given by restriction to H.

Main results

• TauCeti.lieCartanRestriction_mem_linearInvariants: the restriction of an invariant is a Weyl invariant.
• LieSubalgebra.linearInvariants_inf_homogeneousSubmodule_le_map_lieInvariants: a homogeneous Weyl invariant of degree m is the restriction of an invariant of degree m.
• LieSubalgebra.map_lieInvariants_lieCartanRestriction: the image of S(L)^L is S(H)^W.
• LieSubalgebra.lieChevalleyRestrictionIso_mem_homogeneousSubmodule_iff: the isomorphism preserves degrees in both directions.

References

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

Weyl invariance of the restriction

theorem TauCeti.lieCartanRestriction_mem_linearInvariants {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {p : SymmetricAlgebra K L} (hp : p ∈ SymmetricAlgebra.lieInvariants K L L) : (lieCartanRestriction H) p ∈ linearInvariants H

The restriction of an invariant is a Weyl invariant: for p ∈ S(L)^L, the restriction TauCeti.lieCartanRestriction H p lies in S(H)^W.

Surjectivity onto the Weyl invariants

theorem LieSubalgebra.linearInvariants_inf_homogeneousSubmodule_le_map_lieInvariants {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [IsAlgClosed K] (m : ℕ) : Subalgebra.toSubmodule (TauCeti.linearInvariants H) ⊓ TauCeti.SymmetricAlgebra.homogeneousSubmodule K (↥H) m ≤ Submodule.map (TauCeti.lieCartanRestriction H).toLinearMap (Subalgebra.toSubmodule (TauCeti.SymmetricAlgebra.lieInvariants K L L) ⊓ TauCeti.SymmetricAlgebra.homogeneousSubmodule K L m)

A homogeneous Weyl invariant is the restriction of a homogeneous invariant. Every Weyl invariant q ∈ S(H)^W homogeneous of degree m is TauCeti.lieCartanRestriction H p for some invariant p ∈ S(L)^L homogeneous of degree m.

theorem LieSubalgebra.map_lieInvariants_lieCartanRestriction {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [IsAlgClosed K] : Subalgebra.map (TauCeti.lieCartanRestriction H) (TauCeti.SymmetricAlgebra.lieInvariants K L L) = TauCeti.linearInvariants H

Chevalley's restriction theorem, image form. Restriction to H maps the invariants S(L)^L onto the Weyl invariants S(H)^W.

noncomputable def LieSubalgebra.lieChevalleyRestrictionIso {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [IsAlgClosed K] : ↥(TauCeti.SymmetricAlgebra.lieInvariants K L L) ≃ₐ[K] ↥(TauCeti.linearInvariants H)

Chevalley's restriction theorem. Restriction of polynomial functions from L to H, TauCeti.lieCartanRestriction H, is an isomorphism from the invariants S(L)^L onto the Weyl invariants S(H)^W.

@[simp]

theorem LieSubalgebra.coe_lieChevalleyRestrictionIso_apply {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [IsAlgClosed K] (p : ↥(TauCeti.SymmetricAlgebra.lieInvariants K L L)) : ↑(H.lieChevalleyRestrictionIso p) = (TauCeti.lieCartanRestriction H) ↑p

The Chevalley isomorphism is restriction to H.

@[simp]

theorem LieSubalgebra.lieCartanRestriction_lieChevalleyRestrictionIso_symm_apply {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [IsAlgClosed K] (q : ↥(TauCeti.linearInvariants H)) : (TauCeti.lieCartanRestriction H) ↑(H.lieChevalleyRestrictionIso.symm q) = ↑q

The inverse of the Chevalley isomorphism sends a Weyl invariant to the invariant restricting to it.

theorem LieSubalgebra.lieChevalleyRestrictionIso_mem_homogeneousSubmodule_iff {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [IsAlgClosed K] {p : ↥(TauCeti.SymmetricAlgebra.lieInvariants K L L)} {m : ℕ} : ↑(H.lieChevalleyRestrictionIso p) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule K (↥H) m ↔ ↑p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule K L m

The Chevalley isomorphism preserves degrees: an invariant is homogeneous of degree m exactly when its restriction to H is.