The Slodowy slice of an sl₂ triple: contracting action and transversality

Let (h, e, f) be an sl₂ triple in a finite-dimensional Lie algebra L over a field K of characteristic zero. The Slodowy slice at e is the affine subspace S = e + ker (ad f) of L. Its direction is complementary to the tangent space [L, e] of the adjoint orbit of e (IsSl2Triple.isCompl_range_ad_e_ker_ad_f), so S is transverse to that orbit at e at the level of tangent spaces.

Over every characteristic-zero field ad h is diagonalizable with integer eigenvalues, and for a unit c the grading automorphism TauCeti.gradingAut acts on the j-eigenspace L(j) by c ^ j. If L is the Lie algebra of an algebraic group G and λ is a cocharacter of G with differential h, this automorphism is Ad (λ c). The contracting action is

c • x = c ^ 2 • Ad (λ c⁻¹) x,

which acts on L(j) by c ^ (2 - j). It fixes e ∈ L(2), and it preserves S. The point of the construction is that its weights on the direction of S are all at least 2. The kernel of ad f consists of lowest weight vectors for the triple, so it is the direct sum of its intersections with the eigenspaces L(-n) for n : ℕ (IsSl2Triple.ker_toEnd_f_eq_iSup_inf_eigenspace), and the contracting action has weight n + 2 on ker (ad f) ⊓ L(-n). Hence for every x ∈ S the orbit map c ↦ c • x is the restriction to Kˣ of a polynomial map K → S of the form c ↦ e + ∑ₙ c ^ (n + 2) • vₙ. It extends to c = 0 with value e, so the action contracts S to e (IsSl2Triple.exists_contractingAction_eq).

The slice is transverse not only to the orbit of e but to the adjoint orbit of each of its points: for every x ∈ S the tangent space [L, x] of the orbit of x and the direction ker (ad f) of S span L (IsSl2Triple.codisjoint_range_ad_ker_ad_f). If L is the Lie algebra of an algebraic group G, this is the surjectivity of the differential of the action map G × S → L at every point of G × S. The proof grades by the eigenvalues of ad h: the point x is e plus vectors of nonpositive weight, and the graded form of L = [L, e] ⊕ ker (ad f) (IsSl2Triple.eigenspace_add_two_le_map_toEnd_e_sup_ker_toEnd_f) lets one absorb each weight space by induction from the lowest weight. Consequently the two tangent spaces meet in dimension dim ker (ad e) - dim ker (ad x), and no point of the slice has a larger centralizer than e (IsSl2Triple.finrank_ker_ad_le_finrank_ker_ad_e). All three statements hold for the action on any finite-dimensional module.

Main definitions

• TauCeti.slodowySlice K e f: the affine subspace e + ker (ad f) of L.
• IsSl2Triple.contractingAction: the action of Kˣ on L by c ↦ c ^ 2 • gradingAut c⁻¹.

Main results

• IsSl2Triple.contractingAction_apply_of_mem: the contracting action has weight 2 - j on L(j). In particular it fixes e (IsSl2Triple.contractingAction_apply_e).
• IsSl2Triple.exists_contractingAction_eq: the orbit map of a point of the slice is polynomial, with value e at 0.
• IsSl2Triple.contractingAction_apply_mem_slodowySlice: the contracting action preserves the slice.
• IsSl2Triple.codisjoint_range_toEnd_ker_toEnd_f, IsSl2Triple.codisjoint_range_ad_ker_ad_f: the slice is transverse to every orbit it meets.
• IsSl2Triple.finrank_range_toEnd_inf_ker_toEnd_f_add_finrank_ker_toEnd, IsSl2Triple.finrank_range_ad_inf_ker_ad_f_add_finrank_ker_ad: the dimension of the intersection of the two tangent spaces.

References

• P. Slodowy, Simple Singularities and Simple Algebraic Groups, Lecture Notes in Mathematics 815, Springer, 1980, §7.4.
• W. L. Gan and V. Ginzburg, Quantization of Slodowy slices, Int. Math. Res. Not. 2002, no. 5, 243–255, §2.

def TauCeti.slodowySlice (R : Type u_1) {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (e f : L) : AffineSubspace R L

The Slodowy slice e + ker (ad f), as an affine subspace of L. When (h, e, f) is an sl₂ triple in a finite-dimensional Lie algebra over a field of characteristic zero, its direction ker (ad f) is complementary to [L, e] (IsSl2Triple.isCompl_range_ad_e_ker_ad_f). For f = 0, in particular in the degenerate case e = f = 0, it is all of L (TauCeti.slodowySlice_zero_right).

@[simp]

theorem TauCeti.mem_slodowySlice {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {e f x : L} : x ∈ slodowySlice R e f ↔ ⁅f, x - e⁆ = 0

A point x lies in the Slodowy slice e + ker (ad f) exactly when ⁅f, x - e⁆ = 0.

theorem TauCeti.self_mem_slodowySlice {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {e f : L} : e ∈ slodowySlice R e f

The Slodowy slice e + ker (ad f) passes through e.

@[simp]

theorem TauCeti.direction_slodowySlice {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {e f : L} : (slodowySlice R e f).direction = LinearMap.ker ((LieAlgebra.ad R L) f)

The direction of the Slodowy slice e + ker (ad f) is the centralizer ker (ad f) of f.

@[simp]

theorem TauCeti.slodowySlice_zero_right {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {e : L} : slodowySlice R e 0 = ⊤

For f = 0 the Slodowy slice is all of L.

The contracting action on the slice

noncomputable def IsSl2Triple.contractingAction {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {h e f : L} (t : IsSl2Triple h e f) : Kˣ →* Module.End K L

The contracting action of Kˣ on L attached to an sl₂ triple (h, e, f): c acts by c ^ 2 • gradingAut c⁻¹, that is, by c ^ (2 - j) on the j-eigenspace of ad h (IsSl2Triple.contractingAction_apply_of_mem). For an algebraic group with Lie algebra L and a cocharacter λ with differential h this is c ↦ c ^ 2 • Ad (λ c⁻¹). It fixes e and preserves the Slodowy slice e + ker (ad f), on which it extends to c = 0 (IsSl2Triple.exists_contractingAction_eq).

theorem IsSl2Triple.contractingAction_apply {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {h e f : L} (t : IsSl2Triple h e f) (hh : DirectSum.IsInternal fun (j : ℤ) => ((LieAlgebra.ad K L) h).eigenspace ↑j) (c : Kˣ) (x : L) : (t.contractingAction c) x = ↑c ^ 2 • (TauCeti.gradingAut hh c⁻¹) x

The contracting action at c is c ^ 2 times the grading automorphism at c⁻¹.

theorem IsSl2Triple.contractingAction_apply_of_mem {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {h e f : L} (t : IsSl2Triple h e f) (c : Kˣ) {j : ℤ} {x : L} (hx : x ∈ ((LieAlgebra.ad K L) h).eigenspace ↑j) : (t.contractingAction c) x = ↑c ^ (2 - j) • x

The weights of the contracting action. The unit c acts on the j-eigenspace of ad h by c ^ (2 - j).

@[simp]

theorem IsSl2Triple.contractingAction_apply_e {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {h e f : L} (t : IsSl2Triple h e f) (c : Kˣ) : (t.contractingAction c) e = e

The contracting action fixes e, which has weight 2 for ad h.

theorem IsSl2Triple.exists_contractingAction_eq {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {h e f : L} (t : IsSl2Triple h e f) {x : L} (hx : x ∈ TauCeti.slodowySlice K e f) : ∃ (v : ℕ →₀ L), (∀ (n : ℕ), v n ∈ LinearMap.ker ((LieAlgebra.ad K L) f) ⊓ ((LieAlgebra.ad K L) h).eigenspace (-↑n)) ∧ (x = e + v.sum fun (x : ℕ) (w : L) => w) ∧ ∀ (c : Kˣ), (t.contractingAction c) x = e + v.sum fun (n : ℕ) (w : L) => ↑c ^ (n + 2) • w

The contracting action extends to c = 0 on the slice. A point x of the Slodowy slice is e + ∑ₙ vₙ with vₙ ∈ ker (ad f) of weight -n for ad h, and the unit c moves it to e + ∑ₙ c ^ (n + 2) • vₙ. So the orbit map c ↦ c • x is the restriction of a polynomial map taking the value e at c = 0.

theorem IsSl2Triple.contractingAction_apply_mem_slodowySlice {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {h e f : L} (t : IsSl2Triple h e f) (c : Kˣ) {x : L} (hx : x ∈ TauCeti.slodowySlice K e f) : (t.contractingAction c) x ∈ TauCeti.slodowySlice K e f

The contracting action preserves the Slodowy slice.

Transversality of the slice to every orbit it meets

theorem IsSl2Triple.codisjoint_range_toEnd_ker_toEnd_f {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] {h e f x : L} (t : IsSl2Triple h e f) (hx : x ∈ TauCeti.slodowySlice K e f) : Codisjoint (LinearMap.range ((LieModule.toEnd K L M) x)) (LinearMap.ker ((LieModule.toEnd K L M) f))

The Slodowy slice is transverse to every orbit it meets. For an sl₂ triple (h, e, f) and every point x of the slice e + ker (ad f), the range of x and the kernel of f acting on a finite-dimensional module span the module. At x = e this is the codisjointness half of IsSl2Triple.isCompl_range_toEnd_e_ker_toEnd_f.

theorem IsSl2Triple.finrank_range_toEnd_inf_ker_toEnd_f_add_finrank_ker_toEnd {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] {h e f x : L} (t : IsSl2Triple h e f) (hx : x ∈ TauCeti.slodowySlice K e f) : Module.finrank K ↥(LinearMap.range ((LieModule.toEnd K L M) x) ⊓ LinearMap.ker ((LieModule.toEnd K L M) f)) + Module.finrank K ↥(LinearMap.ker ((LieModule.toEnd K L M) x)) = Module.finrank K ↥(LinearMap.ker ((LieModule.toEnd K L M) e))

The dimension of the transverse intersection. For every point x of the Slodowy slice e + ker (ad f), the intersection of the range of x with the kernel of f acting on a finite-dimensional module has dimension dim ker e - dim ker x.

theorem IsSl2Triple.finrank_ker_toEnd_le_finrank_ker_toEnd_e {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] {h e f x : L} (t : IsSl2Triple h e f) (hx : x ∈ TauCeti.slodowySlice K e f) : Module.finrank K ↥(LinearMap.ker ((LieModule.toEnd K L M) x)) ≤ Module.finrank K ↥(LinearMap.ker ((LieModule.toEnd K L M) e))

The kernel of e has the largest dimension among the kernels of the points of the Slodowy slice e + ker (ad f) acting on a finite-dimensional module.

theorem IsSl2Triple.codisjoint_range_ad_ker_ad_f {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {h e f x : L} (t : IsSl2Triple h e f) (hx : x ∈ TauCeti.slodowySlice K e f) : Codisjoint (LinearMap.range ((LieAlgebra.ad K L) x)) (LinearMap.ker ((LieAlgebra.ad K L) f))

The Slodowy slice is transverse to every adjoint orbit it meets. For every point x of the slice e + ker (ad f), the tangent space [L, x] of the adjoint orbit of x and the direction ker (ad f) of the slice span L.

theorem IsSl2Triple.finrank_range_ad_inf_ker_ad_f_add_finrank_ker_ad {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {h e f x : L} (t : IsSl2Triple h e f) (hx : x ∈ TauCeti.slodowySlice K e f) : Module.finrank K ↥(LinearMap.range ((LieAlgebra.ad K L) x) ⊓ LinearMap.ker ((LieAlgebra.ad K L) f)) + Module.finrank K ↥(LinearMap.ker ((LieAlgebra.ad K L) x)) = Module.finrank K ↥(LinearMap.ker ((LieAlgebra.ad K L) e))

The dimension of the transverse intersection. For every point x of the Slodowy slice e + ker (ad f), the intersection of the tangent space [L, x] of the adjoint orbit of x with the direction ker (ad f) of the slice has dimension dim ker (ad e) - dim ker (ad x), the difference of the dimensions of the orbits of x and of e.

theorem IsSl2Triple.finrank_ker_ad_le_finrank_ker_ad_e {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {h e f x : L} (t : IsSl2Triple h e f) (hx : x ∈ TauCeti.slodowySlice K e f) : Module.finrank K ↥(LinearMap.ker ((LieAlgebra.ad K L) x)) ≤ Module.finrank K ↥(LinearMap.ker ((LieAlgebra.ad K L) e))

The centralizer of e has the largest dimension among the centralizers of the points of the Slodowy slice e + ker (ad f).