Simultaneous eigenspaces of the centre of the enveloping algebra

Let M be a module over a Lie algebra L over a commutative ring R, and let Z(U(L)) = Subalgebra.center R (UniversalEnvelopingAlgebra R L) be the centre of the universal enveloping algebra. For a candidate eigenvalue function χ : Z(U(L)) → R, the centre eigenspace

M_χ = {m ∈ M | z • m = χ z • m for every z ∈ Z(U(L))}

is a Lie submodule of M, because a central element acts by a map commuting with the Lie action (TauCeti.UniversalEnvelopingAlgebra.representation_lie_of_mem_center). It is the simultaneous eigenspace of the commuting family of operators by which the centre acts, in the same way that Mathlib's LieModule.genWeightSpace is the simultaneous generalized eigenspace of a nilpotent Lie algebra. The eigenvalue function is an arbitrary function, as for weight spaces; the central characters of highest weight modules (TauCeti.vermaCentralCharacter) are the functions it is used with.

Over a domain, and for a torsion-free module, centre eigenspaces for distinct eigenvalue functions are independent (TauCeti.UniversalEnvelopingAlgebra.iSupIndep_centerEigenspace): this is Mathlib's independence of simultaneous generalized eigenspaces of a commuting family, Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo, restricted to genuine eigenspaces. A homomorphism of Lie modules intertwines the actions of the centre, so it carries each centre eigenspace into the corresponding one (LieModuleHom.map_centerEigenspace_le).

Main definitions

• TauCeti.UniversalEnvelopingAlgebra.centerEigenspace: the simultaneous eigenspace of the centre of U(L) for an eigenvalue function, as a Lie submodule.

Main results

• TauCeti.UniversalEnvelopingAlgebra.mem_centerEigenspace: membership is the eigenvector equation for every central element.
• LieModuleHom.map_centerEigenspace_le: Lie module homomorphisms preserve centre eigenspaces.
• TauCeti.UniversalEnvelopingAlgebra.centerEigenspace_eq_top_iff: the centre acts on the whole module through χ exactly when the centre eigenspace is everything.
• TauCeti.UniversalEnvelopingAlgebra.iSupIndep_centerEigenspace: centre eigenspaces for distinct eigenvalue functions are independent.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §23.2.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.centerEigenspace (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.center R (UniversalEnvelopingAlgebra R L)) → R) : LieSubmodule R L M

The centre eigenspace of a Lie module for an eigenvalue function χ on the centre of the universal enveloping algebra: the Lie submodule of vectors on which every central element z of U(L) acts as multiplication by χ z. It is a Lie submodule because central elements act by maps commuting with the Lie action.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mem_centerEigenspace {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.center R (UniversalEnvelopingAlgebra R L)) → R} {m : M} : m ∈ centerEigenspace R L M χ ↔ ∀ (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R L))), ((representation R L M) ↑z) m = χ z • m

A vector lies in the centre eigenspace for χ exactly when every central element z of U(L) acts on it as multiplication by χ z.

theorem TauCeti.UniversalEnvelopingAlgebra.centerEigenspace_toSubmodule {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.center R (UniversalEnvelopingAlgebra R L)) → R) : ↑(centerEigenspace R L M χ) = ⨅ (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R L))), ((representation R L M) ↑z).eigenspace (χ z)

The underlying submodule of a centre eigenspace is the intersection of the eigenspaces of the operators by which the central elements act.

theorem TauCeti.UniversalEnvelopingAlgebra.centerEigenspace_eq_top_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] {χ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R L)) → R} : centerEigenspace R L M χ = ⊤ ↔ ∀ (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R L))) (m : M), ((representation R L M) ↑z) m = χ z • m

The centre acts on a Lie module through χ exactly when the centre eigenspace for χ is the whole module.

theorem LieModuleHom.map_centerEigenspace_le {R : Type u} {L : Type v} {M : Type w} {N : Type x} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : M →ₗ⁅R,L⁆ N) (χ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R L)) → R) : LieSubmodule.map f (TauCeti.UniversalEnvelopingAlgebra.centerEigenspace R L M χ) ≤ TauCeti.UniversalEnvelopingAlgebra.centerEigenspace R L N χ

A homomorphism of Lie modules carries a centre eigenspace into the centre eigenspace of the same eigenvalue function, since it intertwines the actions of U(L).

theorem TauCeti.UniversalEnvelopingAlgebra.lieSpan_le_centerEigenspace_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] {χ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R L)) → R} {S : Set M} : LieSubmodule.lieSpan R L S ≤ centerEigenspace R L M χ ↔ ∀ v ∈ S, ∀ (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R L))), ((representation R L M) ↑z) v = χ z • v

A Lie submodule is contained in a centre eigenspace exactly when a Lie-generating set of it is: centrality propagates the eigenvector equation from generators.

theorem TauCeti.UniversalEnvelopingAlgebra.iSupIndep_centerEigenspace {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] [IsDomain R] [Module.IsTorsionFree R M] : iSupIndep fun (χ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R L)) → R) => centerEigenspace R L M χ

Centre eigenspaces for distinct eigenvalue functions are independent: they form an independent family of Lie submodules. The operators by which the central elements act commute with each other, so this is the independence of simultaneous generalized eigenspaces of a commuting family, restricted to genuine eigenspaces.

theorem TauCeti.UniversalEnvelopingAlgebra.disjoint_centerEigenspace {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] [IsDomain R] [Module.IsTorsionFree R M] {χ₁ χ₂ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R L)) → R} (h : χ₁ ≠ χ₂) : Disjoint (centerEigenspace R L M χ₁) (centerEigenspace R L M χ₂)

Centre eigenspaces for distinct eigenvalue functions meet only in zero.