The raising and lowering operators between eigenspaces of the Cartan element

Let t : IsSl2Triple h e f be an sl₂ triple in a Lie algebra L over a field K of characteristic zero, and let M be a finite-dimensional L-module. Write M_μ for the μ-eigenspace of h. The raising operator e maps M_μ into M_(μ + 2) (TauCeti.lie_mem_eigenspace_add_two). This file proves that it maps M_μ onto M_(μ + 2) as soon as μ + 2 is not of the form -n with n : ℕ, and that it is injective on M_μ as soon as μ is not a natural number. Dually, the lowering operator f maps M_μ onto M_(μ - 2) when μ - 2 is not a natural number, and is injective on M_μ when μ is not of the form -n.

In a decomposition of M into irreducible modules V(n), with weights n, n - 2, …, -n, these are the familiar statements that e is injective below the middle of each string and surjective above it. The proofs of these statements use no such decomposition and no algebraically closed field. Injectivity is Mathlib's theorem that a primitive vector has a natural-number weight (IsSl2Triple.HasPrimitiveVectorWith.exists_nat). Surjectivity comes from the decomposition M = e • M ⊕ ker f (IsSl2Triple.isCompl_range_toEnd_e_ker_toEnd_f). Both summands are stable under h, so the component in ker f of a vector of M_(μ + 2) also has weight μ + 2, and it vanishes because f is injective on M_(μ + 2). Applying the decomposition inside the sum of the eigenspaces of h, which is a module for the subalgebra generated by the triple (TauCeti.eigenspaceSup), writes the vector as ⁅e, x⁆ with x a sum of eigenvectors. The independence of the eigenspaces then shows that only the μ-component of x contributes. For an arbitrary weight the same argument gives the graded decomposition: every vector of weight μ + 2 is ⁅e, x⁆ + z with x of weight μ and z ∈ ker f of weight μ + 2.

For the adjoint action, h grades L by its eigenspaces L(μ). The case μ = 0 is ⁅e, L(0)⁆ = L(2), IsSl2Triple.map_ad_e_eigenspace_zero. It is the infinitesimal input to the openness of the orbit of e in L(2) under a group with Lie algebra L(0): the differential at the identity of that orbit map is x ↦ ⁅x, e⁆.

In a finite-dimensional module over a field of characteristic zero the eigenspaces of h at the integers span M, and f lowers weights by 2, so the kernel of f is spanned by its homogeneous parts. By the injectivity of f these have weights -n with n : ℕ (IsSl2Triple.ker_toEnd_f_eq_iSup_inf_eigenspace). Dually, the kernel of e is spanned by the vectors it contains of weight n with n : ℕ (IsSl2Triple.ker_toEnd_e_eq_iSup_inf_eigenspace).

Main results

• IsSl2Triple.disjoint_ker_toEnd_e_eigenspace and IsSl2Triple.disjoint_ker_toEnd_f_eigenspace: injectivity of e and f on the eigenspaces.
• IsSl2Triple.f_eq_of_isSl2Triple and IsSl2Triple.e_eq_of_isSl2Triple: in a Noetherian torsion-free Lie algebra over a domain of characteristic zero, two elements of an sl₂ triple including the neutral element determine the third.
• IsSl2Triple.eigenspace_add_two_le_map_toEnd_e_sup_ker_toEnd_f: the graded form of M = e • M ⊕ ker f, namely M_(μ + 2) ≤ e • M_μ + (ker f ⊓ M_(μ + 2)).
• IsSl2Triple.map_toEnd_e_eigenspace: e maps M_μ onto M_(μ + 2) unless μ + 2 = -n.
• IsSl2Triple.map_toEnd_f_eigenspace: f maps M_μ onto M_(μ - 2) unless μ - 2 = n.
• IsSl2Triple.map_ad_e_eigenspace_zero: ⁅e, L(0)⁆ = L(2) in the adjoint grading.
• IsSl2Triple.ker_toEnd_f_eq_iSup_inf_eigenspace: in a finite-dimensional module over a field of characteristic zero, the kernel of f is spanned by the vectors it contains of weight -n, n : ℕ.
• IsSl2Triple.ker_toEnd_e_eq_iSup_inf_eigenspace: dually, the kernel of e is spanned by the vectors it contains of weight n, n : ℕ.

References

• D. H. Collingwood and W. M. McGovern, Nilpotent Orbits in Semisimple Lie Algebras, Van Nostrand Reinhold, 1993, §3.3–3.4, for the grading attached to an sl₂ triple and the surjectivity of ad e from L(0) to L(2).
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 7–9, Chapter VIII, §11, no. 1–2.

Injectivity

theorem IsSl2Triple.disjoint_ker_toEnd_e_eigenspace {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [IsDomain K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [IsNoetherian K M] [Module.IsTorsionFree K M] {h e f : L} {μ : K} (t : IsSl2Triple h e f) (hμ : ∀ (n : ℕ), μ ≠ ↑n) : Disjoint (LinearMap.ker ((LieModule.toEnd K L M) e)) (((LieModule.toEnd K L M) h).eigenspace μ)

The raising operator is injective on the eigenspaces at weights outside ℕ. A nonzero vector of weight μ killed by e is a primitive vector, and the weight of a primitive vector is a natural number.

theorem IsSl2Triple.disjoint_ker_toEnd_f_eigenspace {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [IsDomain K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [IsNoetherian K M] [Module.IsTorsionFree K M] {h e f : L} {μ : K} (t : IsSl2Triple h e f) (hμ : ∀ (n : ℕ), μ ≠ -↑n) : Disjoint (LinearMap.ker ((LieModule.toEnd K L M) f)) (((LieModule.toEnd K L M) h).eigenspace μ)

The lowering operator is injective on the eigenspaces at weights outside -ℕ. This is IsSl2Triple.disjoint_ker_toEnd_e_eigenspace for the triple (-h, f, e).

theorem IsSl2Triple.f_eq_of_isSl2Triple (K : Type u_1) [CommRing K] [IsDomain K] [CharZero K] {L : Type u_2} [LieRing L] [LieAlgebra K L] [IsNoetherian K L] [Module.IsTorsionFree K L] {h e f f' : L} (t : IsSl2Triple h e f) (t' : IsSl2Triple h e f') : f = f'

The neutral and raising elements of an sl₂ triple determine the lowering element. In a Noetherian torsion-free Lie algebra over a domain K of characteristic zero, any two sl₂ triples (h, e, f) and (h, e, f') sharing h and e satisfy f = f'.

theorem IsSl2Triple.e_eq_of_isSl2Triple (K : Type u_1) [CommRing K] [IsDomain K] [CharZero K] {L : Type u_2} [LieRing L] [LieAlgebra K L] [IsNoetherian K L] [Module.IsTorsionFree K L] {h e e' f : L} (t : IsSl2Triple h e f) (t' : IsSl2Triple h e' f) : e = e'

The neutral and lowering elements of an sl₂ triple determine the raising element. In a Noetherian torsion-free Lie algebra over a domain K of characteristic zero, any two sl₂ triples (h, e, f) and (h, e', f) sharing h and f satisfy e = e'.

Surjectivity

theorem IsSl2Triple.eigenspace_add_two_le_map_toEnd_e_sup_ker_toEnd_f {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] {h e f : L} (t : IsSl2Triple h e f) (μ : K) : ((LieModule.toEnd K L M) h).eigenspace (μ + 2) ≤ Submodule.map ((LieModule.toEnd K L M) e) (((LieModule.toEnd K L M) h).eigenspace μ) ⊔ LinearMap.ker ((LieModule.toEnd K L M) f) ⊓ ((LieModule.toEnd K L M) h).eigenspace (μ + 2)

The graded form of the decomposition M = e • M ⊕ ker f. Every vector of weight μ + 2 is ⁅e, x⁆ + z with x of weight μ and z a vector of weight μ + 2 killed by f.

theorem IsSl2Triple.map_toEnd_e_eigenspace {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] {h e f : L} {μ : K} (t : IsSl2Triple h e f) (hμ : ∀ (n : ℕ), μ + 2 ≠ -↑n) : Submodule.map ((LieModule.toEnd K L M) e) (((LieModule.toEnd K L M) h).eigenspace μ) = ((LieModule.toEnd K L M) h).eigenspace (μ + 2)

The raising operator maps M_μ onto M_(μ + 2) unless μ + 2 is of the form -n with n : ℕ. In particular e maps M_μ onto M_(μ + 2) for every integer μ ≥ -1.

theorem IsSl2Triple.map_toEnd_f_eigenspace {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] {h e f : L} {μ : K} (t : IsSl2Triple h e f) (hμ : ∀ (n : ℕ), μ - 2 ≠ ↑n) : Submodule.map ((LieModule.toEnd K L M) f) (((LieModule.toEnd K L M) h).eigenspace μ) = ((LieModule.toEnd K L M) h).eigenspace (μ - 2)

The lowering operator maps M_μ onto M_(μ - 2) unless μ - 2 is a natural number. This is IsSl2Triple.map_toEnd_e_eigenspace for the triple (-h, f, e).

theorem IsSl2Triple.map_ad_e_eigenspace_zero {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] {h e f : L} [FiniteDimensional K L] (t : IsSl2Triple h e f) : Submodule.map ((LieAlgebra.ad K L) e) (((LieAlgebra.ad K L) h).eigenspace 0) = ((LieAlgebra.ad K L) h).eigenspace 2

⁅e, L(0)⁆ = L(2). For an sl₂ triple (h, e, f) in a finite-dimensional Lie algebra over a field of characteristic zero, ad e maps the 0-eigenspace of ad h onto its 2-eigenspace.

The weights of h on the kernels of the lowering and raising operators

theorem IsSl2Triple.ker_toEnd_f_eq_iSup_inf_eigenspace {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] {h e f : L} (t : IsSl2Triple h e f) : LinearMap.ker ((LieModule.toEnd K L M) f) = ⨆ (n : ℕ), LinearMap.ker ((LieModule.toEnd K L M) f) ⊓ ((LieModule.toEnd K L M) h).eigenspace (-↑n)

The kernel of the lowering operator is graded by -ℕ. In a finite-dimensional module over a field of characteristic zero, the kernel of f is spanned by the vectors it contains of weight -n for h, n : ℕ.

theorem IsSl2Triple.ker_toEnd_e_eq_iSup_inf_eigenspace {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] {h e f : L} (t : IsSl2Triple h e f) : LinearMap.ker ((LieModule.toEnd K L M) e) = ⨆ (n : ℕ), LinearMap.ker ((LieModule.toEnd K L M) e) ⊓ ((LieModule.toEnd K L M) h).eigenspace ↑n

The kernel of the raising operator is graded by ℕ. In a finite-dimensional module over a field of characteristic zero, the kernel of e is spanned by the vectors it contains of weight n for h, n : ℕ. This is IsSl2Triple.ker_toEnd_f_eq_iSup_inf_eigenspace for the triple (-h, f, e).