The symmetric algebra of a Lie module and its invariants

Let L be a Lie algebra over a commutative ring R and M a Lie module. Each endomorphism m ↦ ⁅x, m⁆ of M extends uniquely to a derivation of the symmetric algebra S(M), and these derivations preserve brackets, so S(M) is again a Lie module over L and the generic Lie-module API applies to it. For M = L this is the adjoint action of L on S(L); for the dual M = L*, with Mathlib's contragredient action ⁅x, φ⁆ = -φ ∘ ad x, it is the coadjoint action on S(L*), the algebra of polynomial functions on L. The action is natural in M, and for the adjoint action also in L.

The elements of S(M) killed by every derivation ⁅x, -⁆ form a subalgebra, the Lie invariants S(M)^L. The derivations preserve each homogeneous degree, so the homogeneous components of an invariant are again invariant. A Lie module equivalence M ≃ N induces an algebra equivalence S(M) ≃ S(N) intertwining the two actions, which therefore carries S(M)^L onto S(N)^L.

For a finite-dimensional semisimple Lie algebra over an algebraically closed field of characteristic zero, the invariants S(L)^L are the leading symbols of the centre of the enveloping algebra, and Chevalley's restriction theorem identifies the invariant polynomial functions S(L*)^L with the Weyl-invariant polynomial functions on a Cartan subalgebra.

Main definitions

• TauCeti.SymmetricAlgebra.lieModuleDerivation: the action of L on S(M) by derivations.
• TauCeti.SymmetricAlgebra.instLieRingModule, TauCeti.SymmetricAlgebra.instLieModule: S(M) is a Lie module over L through these derivations, with TauCeti.SymmetricAlgebra.lie_eq_lieModuleDerivation identifying the bracket.
• TauCeti.SymmetricAlgebra.lieInvariants: the subalgebra S(M)^L of Lie invariants.
• TauCeti.SymmetricAlgebra.homogeneousLieInvariant: the homogeneous invariants S^n(M)^L of degree n.

Main results

• TauCeti.SymmetricAlgebra.lieModuleDerivation_ι: x sends a generator ι m to ι ⁅x, m⁆.
• LieModuleHom.map_apply_lieModuleDerivation: naturality under Lie module maps.
• LieHom.map_apply_lieModuleDerivation: naturality of the adjoint action under Lie algebra maps.
• TauCeti.SymmetricAlgebra.lieModuleDerivation_mem_homogeneousSubmodule: the action preserves each homogeneous degree.
• TauCeti.SymmetricAlgebra.mem_lieInvariants_iff_mem_maxTrivSubmodule: the invariants are the maximal trivial submodule of the Lie module S(M).
• TauCeti.SymmetricAlgebra.decompose_mem_lieInvariants_iff: an element is invariant exactly when all of its homogeneous components are.
• LieModuleEquiv.map_lieInvariants: a Lie module equivalence carries the invariants onto the invariants.
• TauCeti.SymmetricAlgebra.lift_eval_eq_zero_of_mem_homogeneousLieInvariant, TauCeti.SymmetricAlgebra.lift_eval_eq_zero_of_mem_lieInvariants: an invariant polynomial function on M of positive degree, respectively with zero constant term, vanishes at every eigenvector ⁅y, x⁆ = a • x of a nonzero eigenvalue a, by Euler's identity.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §23.1 and §23.3, where L acts on S(L) and on the polynomial functions S(L*) by derivations.
• J. Dixmier, Enveloping Algebras, §2.4.

The action by derivations

noncomputable def TauCeti.SymmetricAlgebra.lieModuleDerivation (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : L →ₗ⁅R⁆ Derivation R (SymmetricAlgebra R M) (SymmetricAlgebra R M)

The action of L on the symmetric algebra of a Lie module M, by derivations: x acts by the derivation extending the endomorphism m ↦ ⁅x, m⁆ of M. For M = L this is the adjoint action of L on S(L), by the derivations extending LieAlgebra.ad.

theorem TauCeti.SymmetricAlgebra.lieModuleDerivation_apply (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) : (lieModuleDerivation R L M) x = (SymmetricAlgebra.derivationOfEnd R M) ((LieModule.toEnd R L M) x)

The derivation by which x acts is the derivation induced by the endomorphism ⁅x, -⁆.

@[simp]

theorem TauCeti.SymmetricAlgebra.lieModuleDerivation_ι (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (m : M) : ((lieModuleDerivation R L M) x) ((SymmetricAlgebra.ι R M) m) = (SymmetricAlgebra.ι R M) ⁅x, m⁆

The action of x sends a symmetric generator ι m to ι ⁅x, m⁆.

@[instance_reducible]

noncomputable instance TauCeti.SymmetricAlgebra.instLieRingModule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : LieRingModule L (SymmetricAlgebra R M)

The symmetric algebra of M is a Lie ring module over L through the derivations lieModuleDerivation.

instance TauCeti.SymmetricAlgebra.instLieModule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : LieModule R L (SymmetricAlgebra R M)

The symmetric algebra of M is a Lie module over L through the derivations lieModuleDerivation.

@[simp]

theorem TauCeti.SymmetricAlgebra.lie_eq_lieModuleDerivation (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (p : SymmetricAlgebra R M) : ⁅x, p⁆ = ((lieModuleDerivation R L M) x) p

The bracket of x : L with p ∈ S(M) is the derivation by which x acts, applied to p.

theorem TauCeti.SymmetricAlgebra.lieModuleDerivation_mem_homogeneousSubmodule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) {n : ℕ} {p : SymmetricAlgebra R M} (hp : p ∈ homogeneousSubmodule R M n) : ((lieModuleDerivation R L M) x) p ∈ homogeneousSubmodule R M n

The action of L preserves each homogeneous submodule of the symmetric algebra.

theorem TauCeti.SymmetricAlgebra.lieModuleDerivation_decompose (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (p : SymmetricAlgebra R M) (n : ℕ) : ((lieModuleDerivation R L M) x) ↑(((DirectSum.decompose (homogeneousSubmodule R M)) p) n) = ↑(((DirectSum.decompose (homogeneousSubmodule R M)) (((lieModuleDerivation R L M) x) p)) n)

The action of L commutes with the projections onto the homogeneous components.

theorem LieModuleHom.map_apply_lieModuleDerivation {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N : Type w'} [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : M →ₗ⁅R,L⁆ N) (x : L) (p : SymmetricAlgebra R M) : (SymmetricAlgebra.map R ↑f) (((TauCeti.SymmetricAlgebra.lieModuleDerivation R L M) x) p) = ((TauCeti.SymmetricAlgebra.lieModuleDerivation R L N) x) ((SymmetricAlgebra.map R ↑f) p)

The symmetric-algebra map induced by a morphism of Lie modules intertwines the actions.

theorem LieHom.map_apply_lieModuleDerivation {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L' : Type w'} [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (x : L) (p : SymmetricAlgebra R L) : (SymmetricAlgebra.map R ↑f) (((TauCeti.SymmetricAlgebra.lieModuleDerivation R L L) x) p) = ((TauCeti.SymmetricAlgebra.lieModuleDerivation R L' L') (f x)) ((SymmetricAlgebra.map R ↑f) p)

The symmetric-algebra map induced by a Lie algebra homomorphism intertwines the adjoint actions.

The invariants

noncomputable def TauCeti.SymmetricAlgebra.lieInvariants (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : Subalgebra R (SymmetricAlgebra R M)

The Lie invariants S(M)^L: the elements of the symmetric algebra killed by the action of every element of L.

theorem TauCeti.SymmetricAlgebra.mem_lieInvariants {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {p : SymmetricAlgebra R M} : p ∈ lieInvariants R L M ↔ ∀ (x : L), ((lieModuleDerivation R L M) x) p = 0

Membership in the invariants: p is killed by the action of every element of L.

theorem TauCeti.SymmetricAlgebra.mem_lieInvariants_iff_mem_maxTrivSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {p : SymmetricAlgebra R M} : p ∈ lieInvariants R L M ↔ p ∈ LieModule.maxTrivSubmodule R L (SymmetricAlgebra R M)

The invariants of S(M) are the vectors of the Lie module S(M) killed by L.

theorem TauCeti.SymmetricAlgebra.ι_mem_lieInvariants {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {m : M} (hm : ∀ (x : L), ⁅x, m⁆ = 0) : (SymmetricAlgebra.ι R M) m ∈ lieInvariants R L M

The generator ι m of a vector m killed by L is invariant.

theorem TauCeti.SymmetricAlgebra.decompose_mem_lieInvariants_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {p : SymmetricAlgebra R M} : (∀ (n : ℕ), ↑(((DirectSum.decompose (homogeneousSubmodule R M)) p) n) ∈ lieInvariants R L M) ↔ p ∈ lieInvariants R L M

The invariants are graded: an element of the symmetric algebra is invariant exactly when each of its homogeneous components is.

theorem TauCeti.SymmetricAlgebra.decompose_mem_lieInvariants {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {p : SymmetricAlgebra R M} (hp : p ∈ lieInvariants R L M) (n : ℕ) : ↑(((DirectSum.decompose (homogeneousSubmodule R M)) p) n) ∈ lieInvariants R L M

A homogeneous component of an invariant is invariant.

noncomputable def TauCeti.SymmetricAlgebra.homogeneousLieInvariant (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (n : ℕ) : Submodule R (SymmetricAlgebra R M)

The homogeneous Lie invariants S^n(M)^L of degree n: the invariants that are homogeneous of degree n.

@[simp]

theorem TauCeti.SymmetricAlgebra.mem_homogeneousLieInvariant {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {n : ℕ} {p : SymmetricAlgebra R M} : p ∈ homogeneousLieInvariant R L M n ↔ p ∈ lieInvariants R L M ∧ p ∈ homogeneousSubmodule R M n

Membership in the homogeneous Lie invariants of degree n: p is invariant and homogeneous of degree n.

theorem LieModuleEquiv.map_apply_lieModuleDerivation {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N : Type w'} [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (e : M ≃ₗ⁅R,L⁆ N) (x : L) (p : SymmetricAlgebra R M) : (SymmetricAlgebra.map R ↑e.toLinearEquiv) (((TauCeti.SymmetricAlgebra.lieModuleDerivation R L M) x) p) = ((TauCeti.SymmetricAlgebra.lieModuleDerivation R L N) x) ((SymmetricAlgebra.map R ↑e.toLinearEquiv) p)

The symmetric-algebra map induced by a Lie module equivalence intertwines the actions.

@[simp]

theorem LieModuleEquiv.map_mem_lieInvariants_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N : Type w'} [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (e : M ≃ₗ⁅R,L⁆ N) {p : SymmetricAlgebra R M} : (SymmetricAlgebra.map R ↑e.toLinearEquiv) p ∈ TauCeti.SymmetricAlgebra.lieInvariants R L N ↔ p ∈ TauCeti.SymmetricAlgebra.lieInvariants R L M

An element is invariant exactly when its image under the symmetric-algebra map of a Lie module equivalence is.

theorem LieModuleEquiv.map_lieInvariants {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N : Type w'} [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (e : M ≃ₗ⁅R,L⁆ N) : Subalgebra.map (SymmetricAlgebra.map R ↑e.toLinearEquiv) (TauCeti.SymmetricAlgebra.lieInvariants R L M) = TauCeti.SymmetricAlgebra.lieInvariants R L N

Transport of invariants: the symmetric-algebra map of a Lie module equivalence carries the invariants onto the invariants.

Vanishing at eigenvectors

theorem TauCeti.SymmetricAlgebra.lift_eval_eq_zero_of_mem_homogeneousLieInvariant {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [NoZeroDivisors R] [CharZero R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {n : ℕ} (hn : n ≠ 0) {p : SymmetricAlgebra R (Module.Dual R M)} (hp : p ∈ homogeneousLieInvariant R L (Module.Dual R M) n) {y : L} {x : M} {a : R} (hyx : ⁅y, x⁆ = a • x) (ha : a ≠ 0) : (SymmetricAlgebra.lift ((Module.Dual.eval R M) x)) p = 0

A homogeneous invariant polynomial function of positive degree vanishes at every eigenvector of a nonzero eigenvalue. If p on the Lie module M is invariant and homogeneous of degree n ≠ 0, and ⁅y, x⁆ = a • x with a ≠ 0, then p (x) = 0.

theorem TauCeti.SymmetricAlgebra.lift_eval_eq_zero_of_mem_lieInvariants {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [NoZeroDivisors R] [CharZero R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {p : SymmetricAlgebra R (Module.Dual R M)} (hp : p ∈ lieInvariants R L (Module.Dual R M)) (hp₀ : SymmetricAlgebra.algebraMapInv p = 0) {y : L} {x : M} {a : R} (hyx : ⁅y, x⁆ = a • x) (ha : a ≠ 0) : (SymmetricAlgebra.lift ((Module.Dual.eval R M) x)) p = 0

An invariant polynomial function with zero constant term vanishes at every eigenvector of a nonzero eigenvalue. If p on the Lie module M is invariant with algebraMapInv p = 0, and ⁅y, x⁆ = a • x with a ≠ 0, then p (x) = 0.