Documentation

TauCeti.Algebra.Lie.Sl2.RangeKer

The range of the raising operator is complementary to the kernel of the lowering operator #

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. This file proves the decomposition

M = e • M ⊕ ker f.

The kernel of f consists of the lowest weight vectors. In the decomposition of M into irreducible V(n)s, each summand contributes one lowest weight line, and the rest of the summand is the image of the raising operator. The proof here does not use that decomposition, a splitting field or the diagonalizability of h. It works over any field of characteristic zero.

For the adjoint module this is the direct sum L = [L, e] ⊕ ker (ad f). The first summand is the image of the differential of the orbit map g ↦ Ad g e of a group with Lie algebra L. The second is the direction of the affine subspace e + ker (ad f), the Slodowy slice at e. So the decomposition is the linear-algebraic content of the transversality of the slice to the adjoint orbit of e. A dimension count also gives dim ker (ad e) = dim ker (ad f): the direction of the slice has the dimension of the centralizer of e.

The argument #

Write E, F, H for the operators by which e, f, h act. Both E and F are nilpotent. Disjointness of range E and ker F is proved by descending induction on k ≥ 1: no nonzero vector of range (E ^ k) is killed by F. For large k the range is zero. For the step, let v = E ^ (n + 1) w with F v = 0. The commutation formula for F past E ^ (n + 1) shows that H v - (n + 2) • v lies in range (E ^ (n + 2)). It is also killed by F, so it vanishes by the induction hypothesis. Then v is a vector of ker F on which H acts by n + 2. The commutation formula gives F (E ^ (j + 1) v) = -(j + 1) (n + 2 + j) • E ^ j v, so E ^ j v = 0 forces v = 0 by induction on j, and E is nilpotent. Hence v = 0.

The same statement for (-h, f, e) gives that range F and ker E are disjoint. In finite dimension the two disjointness statements together with rank-nullity force dim ker E = dim ker F. Hence range E and ker F have complementary dimensions.

Main results #

References #

source
theorem TauCeti.Sl2.disjoint_range_ker {K : Type u_1} {V : Type u_2} [Field K] [CharZero K] [AddCommGroup V] [Module K V] {E F H : Module.End K V} (hE : IsNilpotent E) (hef : E * F - F * E = H) (hhe : H * E - E * H = 2 • E) (hhf : H * F - F * H = -(2 • F)) :
Disjoint (LinearMap.range E) (LinearMap.ker F)

Let E be a nilpotent operator satisfying the sl₂ relations with F and H. Then no nonzero vector in the range of E is killed by F. No finiteness is needed.

source
theorem IsSl2Triple.isNilpotent_toEnd_e {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) :
IsNilpotent ((LieModule.toEnd K L M) e)

The raising element of an sl₂ triple acts nilpotently on a finite-dimensional module over a field of characteristic zero.

source
theorem IsSl2Triple.isNilpotent_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) :
IsNilpotent ((LieModule.toEnd K L M) f)

The lowering element of an sl₂ triple acts nilpotently on a finite-dimensional module over a field of characteristic zero.

source
theorem IsSl2Triple.finrank_ker_toEnd_e_eq_finrank_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) :
Module.finrank K ↥(LinearMap.ker ((LieModule.toEnd K L M) e)) = Module.finrank K ↥(LinearMap.ker ((LieModule.toEnd K L M) f))

The kernels of the raising and lowering operators of an sl₂ triple on a finite-dimensional module have the same dimension. These are the spaces of highest and of lowest weight vectors.

source
theorem IsSl2Triple.isCompl_range_toEnd_e_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) :
IsCompl (LinearMap.range ((LieModule.toEnd K L M) e)) (LinearMap.ker ((LieModule.toEnd K L M) f))

The sl₂ decomposition M = e • M ⊕ ker f. For an sl₂ triple (h, e, f) acting on a finite-dimensional module over a field of characteristic zero, the range of the raising operator and the kernel of the lowering operator are complementary.

source
theorem IsSl2Triple.isCompl_range_ad_e_ker_ad_f {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) :
IsCompl (LinearMap.range ((LieAlgebra.ad K L) e)) (LinearMap.ker ((LieAlgebra.ad K L) f))

The transverse decomposition L = [L, e] ⊕ ker (ad f). For an sl₂ triple (h, e, f) in a finite-dimensional Lie algebra over a field of characteristic zero, the range of ad e and the kernel of ad f are complementary.

source
theorem IsSl2Triple.finrank_ker_ad_e_eq_finrank_ker_ad_f {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) :
Module.finrank K ↥(LinearMap.ker ((LieAlgebra.ad K L) e)) = Module.finrank K ↥(LinearMap.ker ((LieAlgebra.ad K L) f))

The centralizers of the raising and lowering elements of an sl₂ triple in a finite-dimensional Lie algebra over a field of characteristic zero have the same dimension.