Simultaneous eigenvectors of a subalgebra

Let H be a subalgebra of a Lie algebra L acting on a module M. A vector v on which every element of H acts by a scalar is a simultaneous eigenvector, its eigenvalue being the function chi : H → R that records those scalars. This file collects facts about such a vector. When H is nilpotent, it lies in the generalized weight space of its eigenvalue. And applying to it an eigenvector f of the adjoint action shifts its eigenvalue by that of f, once per application; this second fact is stated both for the whole subalgebra H, as a statement about weight spaces, and for one element of L at a time, where it needs no subalgebra at all.

Both are stated over a commutative ring; only the generalized-weight-space result, TauCeti.mem_genWeightSpace_of_forall_lie_eq_smul, assumes the subalgebra is nilpotent. The Cartan subalgebra of a Lie algebra with non-degenerate Killing form, where the eigenvalue of f is a root, is the case the weight theory uses, and TauCeti.lie_pow_toEnd_eq_smul_of_mem_rootSpace records it.

Dually, a linear functional on which an element acts by a scalar detects weights: over an integral domain it can be nonzero on a generalized weight vector only if that scalar is the value of the weight. This is how a weight is read off a coordinate of a vector in an explicit model.

Main results

• TauCeti.mem_genWeightSpace_of_forall_lie_eq_smul: a simultaneous eigenvector of H lies in the generalized weight space of its eigenvalue, at nilpotency index one.
• TauCeti.lie_mem_weightSpace_of_mem_weightSpace: if H acts on f by psi under the adjoint action, then f carries the weight space of chi into that of psi + chi.
• TauCeti.lie_pow_toEnd_eq_smul: for a single x : L, applying an x-eigenvector f of eigenvalue c to an x-eigenvector of eigenvalue a, k times, gives an x-eigenvector of eigenvalue a + k c.
• TauCeti.apply_eq_of_mem_genWeightSpace: dually, a linear functional on which x acts by the scalar c and which does not vanish on a generalized weight vector of weight chi forces chi x = c.
• TauCeti.lie_pow_toEnd_eq_smul_of_mem_rootSpace: the specialization of the shift to a vector of the root space of psi, which is an adjoint eigenvector of weight psi by LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace.

References

This is elementary weight-space infrastructure for the highest weight modules of Layer 3 and the "integrability relation" milestone of Layer 4 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md: the weight shift is what makes a lowered highest weight vector an eigenvector again.

theorem TauCeti.mem_genWeightSpace_of_forall_lie_eq_smul {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} {M : Type w} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieRing.IsNilpotent ↥H] {chi : ↥H → R} {v : M} (hv : ∀ (x : ↥H), ⁅↑x, v⁆ = chi x • v) : v ∈ LieModule.genWeightSpace M chi

An eigenvector for the whole subalgebra H lies in the generalized weight space of its eigenvalue: an honest simultaneous eigenvector is a generalized one, at nilpotency index one.

theorem TauCeti.lie_mem_weightSpace_of_mem_weightSpace {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} {M : Type w} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {f : L} {psi : ↥H → R} (hf : ∀ (x : ↥H), ⁅↑x, f⁆ = psi x • f) {chi : ↥H → R} {v : M} (hv : v ∈ LieModule.weightSpace M chi) : ⁅f, v⁆ ∈ LieModule.weightSpace M (psi + chi)

Applying an adjoint eigenvector shifts the weight. If H acts on f through psi under the adjoint action and v lies in the weight space of chi, then ⁅f, v⁆ lies in the weight space of psi + chi.

theorem TauCeti.lie_pow_toEnd_eq_smul {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type w} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {x f : L} {a c : R} {v : M} (hv : ⁅x, v⁆ = a • v) (hf : ⁅x, f⁆ = c • f) (k : ℕ) : ⁅x, ((LieModule.toEnd R L M) f ^ k) v⁆ = (a + ↑k * c) • ((LieModule.toEnd R L M) f ^ k) v

Applying an adjoint eigenvector shifts the eigenvalue. If x acts on v by a and f is an eigenvector of ad x of eigenvalue c, then x acts on fᵏ v by a + k c.

Each application of f costs one c by the Leibniz rule, and the statement is the induction on k that accumulates the cost. The vector fᵏ v is allowed to be zero, when the statement is vacuous.

theorem TauCeti.apply_eq_of_mem_genWeightSpace {R : Type u} {L : Type v} [CommRing R] [IsDomain R] [LieRing L] [LieAlgebra R L] [LieRing.IsNilpotent L] {M : Type w} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {chi : L → R} {v : M} (hv : v ∈ LieModule.genWeightSpace M chi) (x : L) (φ : M →ₗ[R] R) {c : R} (hφ : ∀ (m : M), φ ⁅x, m⁆ = c * φ m) (hv0 : φ v ≠ 0) : chi x = c

A linear functional that is an eigenvector of the dual action reads off a generalized weight. If φ ⁅x, m⁆ = c * φ m for every m and v lies in the generalized weight space of chi, then φ v is killed by a power of c - chi x; so chi x = c as soon as φ v ≠ 0.

theorem TauCeti.lie_pow_toEnd_eq_smul_of_mem_rootSpace {K : Type u} {L : Type v} [Field K] [PerfectField K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {chi psi : ↥H → K} {v : M} (hv : ∀ (x : ↥H), ⁅↑x, v⁆ = chi x • v) {f : L} (hf : f ∈ LieAlgebra.rootSpace H psi) (k : ℕ) (x : ↥H) : ⁅↑x, ((LieModule.toEnd K L M) f ^ k) v⁆ = (chi x + ↑k * psi x) • ((LieModule.toEnd K L M) f ^ k) v

Lowering by a root vector shifts the weight. If H acts on v through the linear form chi and f lies in the root space of psi, then H acts on fᵏ v through chi + k psi.