Restricting polynomial functions on a Killing Lie algebra to a Cartan subalgebra

Let L be a finite-dimensional Lie algebra over a field K whose Killing form κ is nondegenerate, and H a Cartan subalgebra. The Killing form stays nondegenerate on H, so every x : L has a unique Killing-orthogonal projection π x ∈ H, characterized by κ(π x, h) = κ(x, h) for all h ∈ H. It is the identity on H and, when H splits L, vanishes on every root space of a nonzero root, so it is the projection of L onto H along the sum of the nonzero root spaces (TauCeti.coe_killingCartanProjection).

Through the Killing identifications S(L) ≃ S(L*) (TauCeti.killingSymmetricEquiv) and S(H) ≃ S(H*) (induced by LieAlgebra.IsKilling.cartanEquivDual), the symmetric algebras S(L) and S(H) are the algebras of polynomial functions on L and on H. Restriction of polynomial functions from L to H is then the algebra map S(L) → S(H) induced by π,

TauCeti.lieCartanRestriction H : S(L) →ₐ[K] S(H).

This is the map that Chevalley's restriction theorem is about: restricted to the invariants S(L)^L, it is an isomorphism onto the Weyl invariants S(H)^W (LieSubalgebra.lieChevalleyRestrictionIso), and through the PBW symbols of central elements it is compared with the Harish-Chandra projection.

Read on the dual side, with S(L) as the polynomial functions on L* and S(H) as the polynomial functions on the weights H*, the restriction evaluates a polynomial on L* at the extension TauCeti.killingExtend λ = λ ∘ π of a weight λ to L (TauCeti.lift_lieCartanRestriction).

Main definitions

• TauCeti.killingCartanProjection H: the Killing-orthogonal projection L →ₗ[K] H.
• TauCeti.lieCartanRestriction H: the induced algebra map S(L) →ₐ[K] S(H).

Main results

• TauCeti.killingForm_killingCartanProjection: κ(π x, h) = κ(x, h) for h ∈ H.
• TauCeti.killingCartanProjection_coe and TauCeti.killingCartanProjection_eq_zero_of_mem_rootSpace: the projection is the identity on H and vanishes on the root spaces of nonzero roots.
• TauCeti.killingCartanProjection_eq_zero_of_mem_negativeNilradical and TauCeti.killingCartanProjection_eq_zero_of_mem_positiveNilradical: for a base b of the root system, the projection vanishes on both nilradicals.
• TauCeti.lieCartanRestriction_ι_cartan and TauCeti.lieCartanRestriction_ι_root: the same for the restriction map on generators.
• TauCeti.coe_killingCartanProjection: the projection is the projection TauCeti.genWeightSpaceProjection of the root-space decomposition at the zero weight.
• TauCeti.killingExtend_eq_comp_killingCartanProjection: the extension TauCeti.killingExtend λ of a weight to L is λ ∘ π.
• TauCeti.map_dualMap_killingSymmetricEquiv: the restriction square. Restricting a polynomial function on L to H along the inclusion commutes with the Killing identifications, the restriction on the S(L) side being lieCartanRestriction H.
• TauCeti.lift_lieCartanRestriction: the value of lieCartanRestriction H p at a weight λ is the value of p at TauCeti.killingExtend λ.
• TauCeti.lieCartanRestriction_mem_homogeneousSubmodule: the restriction preserves degrees.
• TauCeti.lieCartanRestriction_surjective: the restriction is onto, split by the map induced by the inclusion H → L.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §23.1, for the restriction of polynomial functions to H and Chevalley's restriction theorem.
• J. Dixmier, Enveloping Algebras, §7.3.

The Killing-orthogonal projection onto a Cartan subalgebra

noncomputable def TauCeti.killingCartanProjection {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] : L →ₗ[K] ↥H

The Killing-orthogonal projection π : L → H onto a Cartan subalgebra: π x is the element of H representing the linear form h ↦ κ(x, h) on H under the restricted Killing form (TauCeti.killingForm_killingCartanProjection). It is the identity on H (TauCeti.killingCartanProjection_coe) and kills the root spaces of nonzero roots (TauCeti.killingCartanProjection_eq_zero_of_mem_rootSpace).

theorem TauCeti.cartanEquivDual_killingCartanProjection {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] (x : L) : (LieAlgebra.IsKilling.cartanEquivDual H) ((killingCartanProjection H) x) = (↑H.incl).dualMap ((killingForm K L) x)

The projection π x represents the restriction of κ(x, ·) to H under LieAlgebra.IsKilling.cartanEquivDual.

@[simp]

theorem TauCeti.killingForm_killingCartanProjection {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] (x : L) (h : ↥H) : ((killingForm K L) ↑((killingCartanProjection H) x)) ↑h = ((killingForm K L) x) ↑h

The characteristic property of the projection: κ(π x, h) = κ(x, h) for every h ∈ H.

theorem TauCeti.eq_killingCartanProjection_iff {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] {x : L} {y : ↥H} : y = (killingCartanProjection H) x ↔ ∀ (h : ↥H), ((killingForm K L) ↑y) ↑h = ((killingForm K L) x) ↑h

The projection π x is the only element of H whose Killing pairings with H are those of x.

@[simp]

theorem TauCeti.killingCartanProjection_coe {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] (h : ↥H) : (killingCartanProjection H) ↑h = h

The projection is the identity on H.

@[simp]

theorem TauCeti.killingCartanProjection_comp_incl {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] : killingCartanProjection H ∘ₗ ↑H.incl = LinearMap.id

The projection is a retraction of the inclusion H → L.

theorem TauCeti.killingCartanProjection_surjective {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] : Function.Surjective ⇑(killingCartanProjection H)

The projection is onto.

theorem TauCeti.killingExtend_eq_comp_killingCartanProjection {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] (lam : Module.Dual K ↥H) : killingExtend lam = lam ∘ₗ killingCartanProjection H

The extension of a weight factors through the projection: TauCeti.killingExtend λ, the weight λ extended to L by pairing with the vector representing it, is λ ∘ π.

theorem TauCeti.killingCartanProjection_eq_zero_of_mem_rootSpace {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {χ : ↥H → K} (hχ : χ ≠ 0) {x : L} (hx : x ∈ LieAlgebra.rootSpace H χ) : (killingCartanProjection H) x = 0

The projection vanishes on the nonzero root spaces: a vector in the root space of a nonzero χ is Killing-orthogonal to H, the root space of 0.

theorem TauCeti.coe_killingCartanProjection {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] [Nontrivial ↥H] (x : L) : ↑((killingCartanProjection H) x) = (genWeightSpaceProjection K (↥H) L 0) x

The projection is the root-space projection at the zero weight: when H splits L, π is the projection of L onto its zero root space H along the root spaces of the nonzero roots.

The projection on the nilradicals

theorem TauCeti.killingCartanProjection_eq_zero_of_mem_rootSpaceSpan {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] [LieModule.IsTriangularizable K (↥H) L] {S : Set ↥LieSubalgebra.root} {x : L} (hx : x ∈ rootSpaceSpan H S) : (killingCartanProjection H) x = 0

The Killing-orthogonal projection onto H vanishes on the span of any set of root spaces.

theorem TauCeti.killingCartanProjection_eq_zero_of_mem_negativeNilradical {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) {x : L} (hx : x ∈ negativeNilradical H b) : (killingCartanProjection H) x = 0

The Killing-orthogonal projection onto H vanishes on the negative nilradical.

theorem TauCeti.killingCartanProjection_eq_zero_of_mem_positiveNilradical {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) {x : L} (hx : x ∈ positiveNilradical H b) : (killingCartanProjection H) x = 0

The Killing-orthogonal projection onto H vanishes on the positive nilradical.

Restriction of polynomial functions

noncomputable def TauCeti.lieCartanRestriction {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] : SymmetricAlgebra K L →ₐ[K] SymmetricAlgebra K ↥H

Restriction of polynomial functions from L to H: the algebra map S(L) → S(H) induced by the Killing-orthogonal projection π : L → H. Under the Killing identifications of S(L) and S(H) with the polynomial functions on L and on H, it is restriction along H → L (TauCeti.map_dualMap_killingSymmetricEquiv).

@[simp]

theorem TauCeti.lieCartanRestriction_ι {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] (x : L) : (lieCartanRestriction H) ((SymmetricAlgebra.ι K L) x) = (SymmetricAlgebra.ι K ↥H) ((killingCartanProjection H) x)

The restriction sends the generator x to the generator π x.

theorem TauCeti.lieCartanRestriction_ι_cartan {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] (h : ↥H) : (lieCartanRestriction H) ((SymmetricAlgebra.ι K L) ↑h) = (SymmetricAlgebra.ι K ↥H) h

The restriction is the identity on the generators from H.

theorem TauCeti.lieCartanRestriction_ι_root {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {χ : ↥H → K} (hχ : χ ≠ 0) {x : L} (hx : x ∈ LieAlgebra.rootSpace H χ) : (lieCartanRestriction H) ((SymmetricAlgebra.ι K L) x) = 0

The restriction kills the generators from the root spaces of nonzero roots.

@[simp]

theorem TauCeti.lieCartanRestriction_comp_map_incl {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] : (lieCartanRestriction H).comp (SymmetricAlgebra.map K ↑H.incl) = AlgHom.id K (SymmetricAlgebra K ↥H)

The restriction is a retraction of the algebra map S(H) → S(L) induced by the inclusion.

theorem TauCeti.lieCartanRestriction_surjective {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] : Function.Surjective ⇑(lieCartanRestriction H)

The restriction is onto.

theorem TauCeti.lieCartanRestriction_mem_homogeneousSubmodule {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] {n : ℕ} {p : SymmetricAlgebra K L} (hp : p ∈ SymmetricAlgebra.homogeneousSubmodule K L n) : (lieCartanRestriction H) p ∈ SymmetricAlgebra.homogeneousSubmodule K (↥H) n

The restriction preserves degrees: it maps the homogeneous component of degree n of S(L) into that of S(H).

theorem TauCeti.map_dualMap_killingSymmetricEquiv {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] (p : SymmetricAlgebra K L) : (SymmetricAlgebra.map K (↑H.incl).dualMap) ((killingSymmetricEquiv K L) p) = (SymmetricAlgebra.map K ↑(LieAlgebra.IsKilling.cartanEquivDual H)) ((lieCartanRestriction H) p)

The restriction square. Restricting a polynomial function on L, an element of S(L*), along the inclusion H → L commutes with the Killing identifications: transporting p ∈ S(L) to S(L*) and restricting to H is the same as restricting p to S(H) by TauCeti.lieCartanRestriction and transporting along LieAlgebra.IsKilling.cartanEquivDual.

@[simp]

theorem TauCeti.lift_lieCartanRestriction {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] (lam : Module.Dual K ↥H) (p : SymmetricAlgebra K L) : (SymmetricAlgebra.lift lam) ((lieCartanRestriction H) p) = (SymmetricAlgebra.lift (killingExtend lam)) p

The restriction, read on the weights. Viewing S(L) as the polynomial functions on L* and S(H) as the polynomial functions on the weights H*, the value of lieCartanRestriction H p at a weight λ is the value of p at the extension TauCeti.killingExtend λ of λ to L.