The Weyl element of a standard sl₂-module

The two ladder operators of TauCeti.Sl2Std K n, raising and lowering, are nilpotent over any characteristic-zero domain K equipped with a ℚ-algebra structure, so they carry a Weyl element

n = exp e · exp (-f) · exp e

in the unit group of Module.End K (Sl2Std K n). This is Chevalley's n_α = x_α(1) x_{-α}(-1) x_α(1) in the rank-one representation V(n). This file computes it.

On the coordinate basis it is the reflection of the weight string, decorated by a sign:

n · vᵢ = (-1) ^ (n - i) · v_{n - i}.

The proof is two steps and uses no representation theory. Conjugation by n sends the raising operator to the negated lowering operator, so n · v₀ is killed by the lowering operator and is therefore a multiple of the lowest weight vector vₙ; its n-th coordinate is read off the exponential series, because the raising operator cannot contribute to that coordinate. That is the case i = 0. Conjugation by n in the other direction, sending the lowering operator to the negated raising operator, turns the string relation f · vᵢ = (n - i) · vᵢ₊₁ into the induction step, the coefficient n - i being invertible exactly while the string continues.

Squaring the formula gives the relation the pinning of a Chevalley group asks for:

n ^ 2 = (-1) ^ n,

the rank-one instance of n_α ^ 2 = h_α(-1), since the torus element h_α(-1) acts on a weight vector of weight μ by (-1) ^ μ(α^∨) and the weights of V(n) are n - 2i ≡ n (mod 2).

Both statements are integral, not merely rational. Over K = ℚ the Weyl element permutes the coordinate basis up to sign, so it preserves the coordinate lattice TauCeti.Sl2Std.integralLattice n. Its restriction is the existing TauCeti.UniversalEnvelopingAlgebra.kostantWeylRestrict, whose square is (-1) ^ n; base changing it along ℤ → A gives the same relation for the existing kostantWeylPoints over every commutative ring A, including characteristics in which the factorials dividing the exponential series need not be invertible. This is the rank-one input the Chevalley--Demazure construction of Layer 9 of the reductive-groups roadmap consumes, in the same form as the rank-one straightening formula and the rank-one admissible lattice.

Main definitions

• TauCeti.Sl2Std.weylUnit: the Weyl element of V(n), a unit of Module.End K (Sl2Std K n). The integral Weyl element is the existing TauCeti.UniversalEnvelopingAlgebra.kostantWeylRestrict, specialized to V(n) over ℚ and its coordinate lattice; its scalar extension is the existing kostantWeylPoints.

Main results

• TauCeti.Sl2Std.weylUnit_apply_basis: n · vᵢ = (-1) ^ (n - i) · v_{n - i}, with the matrix form TauCeti.Sl2Std.weylUnit_apply_apply in coordinates.
• TauCeti.Sl2Std.coe_weylUnit_sq and TauCeti.Sl2Std.weylUnit_weylUnit_apply: n ^ 2 = (-1) ^ n.
• TauCeti.Sl2Std.kostantWeylRestrict_comp_self and TauCeti.Sl2Std.kostantWeylPoints_comp_self: the same relation for the canonical Kostant Weyl element on the coordinate lattice and on its points over an arbitrary commutative ring.

References

• R. W. Carter, Simple Groups of Lie Type, §6.4.
• R. Steinberg, Lectures on Chevalley Groups, §3.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §26.

The Weyl element

noncomputable def TauCeti.Sl2Std.weylUnit (K : Type u_1) [CommRing K] [Algebra ℚ K] (n : ℕ) : (Module.End K (Sl2Std K n))ˣ

The Weyl element of V(n), the unit exp e · exp (-f) · exp e of Module.End K (Sl2Std K n). It is Chevalley's n_α = x_α(1) x_{-α}(-1) x_α(1) in the rank-one representation of highest weight n.

Equations

• TauCeti.Sl2Std.weylUnit K n = TauCeti.weylUnit ⋯ ⋯

theorem TauCeti.Sl2Std.coe_weylUnit (K : Type u_1) [CommRing K] [Algebra ℚ K] (n : ℕ) : ↑(weylUnit K n) = IsNilpotent.exp (raise K n) * IsNilpotent.exp (-lower K n) * IsNilpotent.exp (raise K n)

The Weyl element of V(n) is the threefold product of exponentials.

theorem TauCeti.Sl2Std.weylUnit_mul_raise (K : Type u_1) [CommRing K] [Algebra ℚ K] [CharZero K] (n : ℕ) : ↑(weylUnit K n) * raise K n = -(lower K n * ↑(weylUnit K n))

Conjugating the raising operator by the Weyl element. The relation n e n⁻¹ = -f, written without the inverse.

theorem TauCeti.Sl2Std.weylUnit_mul_lower (K : Type u_1) [CommRing K] [Algebra ℚ K] [CharZero K] (n : ℕ) : ↑(weylUnit K n) * lower K n = -(raise K n * ↑(weylUnit K n))

Conjugating the lowering operator by the Weyl element. The relation n f n⁻¹ = -e, written without the inverse.

The base case of the string

The Weyl element reverses the string

@[simp]

theorem TauCeti.Sl2Std.weylUnit_apply_basis (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] [CharZero K] (n : ℕ) (i : Fin (n + 1)) : ↑(weylUnit K n) ((basis K n) i) = (-1) ^ (n - ↑i) • (basis K n) i.rev

The Weyl element reverses the weight string with a sign. It carries the coordinate basis vector vᵢ to (-1) ^ (n - i) · v_{n - i}, the reflection s_α of the weight lattice realised inside the group.

The square of the Weyl element

@[simp]

theorem TauCeti.Sl2Std.coe_weylUnit_sq (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] [CharZero K] (n : ℕ) : ↑(weylUnit K n) ^ 2 = (-1) ^ n • 1

The square of the Weyl element is the scalar (-1) ^ n. This is the rank-one instance of Chevalley's relation n_α ^ 2 = h_α(-1): the torus element h_α(-1) acts on a weight vector of weight μ by (-1) ^ μ(α^∨), and every weight of V(n) is congruent to n modulo two.

@[simp]

theorem TauCeti.Sl2Std.coe_inv_weylUnit (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] [CharZero K] (n : ℕ) : ↑(weylUnit K n)⁻¹ = (-1) ^ n • ↑(weylUnit K n)

The inverse Weyl element is the Weyl element itself, up to the scalar (-1) ^ n.

@[simp]

theorem TauCeti.Sl2Std.weylUnit_weylUnit_apply (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] [CharZero K] (n : ℕ) (v : Sl2Std K n) : ↑(weylUnit K n) (↑(weylUnit K n) v) = (-1) ^ n • v

The Weyl element acts on every vector of V(n) by (-1) ^ n after two applications.

The Weyl element in coordinates

@[simp]

theorem TauCeti.Sl2Std.weylUnit_apply_apply (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] [CharZero K] (n : ℕ) (v : Sl2Std K n) (i : Fin (n + 1)) : ↑(weylUnit K n) v i = (-1) ^ ↑i * v i.rev

The matrix of the Weyl element. It sends the i-th coordinate of the image to the reversed coordinate of the source, with the sign (-1) ^ i.

The canonical Kostant Weyl element over ℤ and its points

theorem TauCeti.Sl2Std.coe_kostantWeylRestrict_apply (n : ℕ) (v : ↥(integralLattice n).toAddSubgroup) : ↑((UniversalEnvelopingAlgebra.kostantWeylRestrict ![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] ![(slFinTwoBasis ℚ) 2] (repEnveloping ℚ n) (integralLattice n).toAddSubgroup ⋯ ⋯ ⋯) v) = ↑(weylUnit ℚ n) ↑v

On the standard integral lattice, the existing Kostant Weyl automorphism applies the coordinate Weyl element computed in this file.

theorem TauCeti.Sl2Std.kostantWeylRestrict_comp_self (n : ℕ) : ↑(UniversalEnvelopingAlgebra.kostantWeylRestrict ![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] ![(slFinTwoBasis ℚ) 2] (repEnveloping ℚ n) (integralLattice n).toAddSubgroup ⋯ ⋯ ⋯) ∘ₗ ↑(UniversalEnvelopingAlgebra.kostantWeylRestrict ![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] ![(slFinTwoBasis ℚ) 2] (repEnveloping ℚ n) (integralLattice n).toAddSubgroup ⋯ ⋯ ⋯) = (-1) ^ n • LinearMap.id

The integral form of the relation n ^ 2 = (-1) ^ n. The canonical Kostant Weyl automorphism squares to the integer scalar (-1) ^ n on the standard coordinate lattice.

theorem TauCeti.Sl2Std.kostantWeylPoints_comp_self (n : ℕ) (A : Type u_1) [CommRing A] [Algebra ℤ A] : ↑(UniversalEnvelopingAlgebra.kostantWeylPoints ![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] ![(slFinTwoBasis ℚ) 2] (repEnveloping ℚ n) (integralLattice n).toAddSubgroup ⋯ ⋯ ⋯ A) ∘ₗ ↑(UniversalEnvelopingAlgebra.kostantWeylPoints ![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] ![(slFinTwoBasis ℚ) 2] (repEnveloping ℚ n) (integralLattice n).toAddSubgroup ⋯ ⋯ ⋯ A) = (-1) ^ n • LinearMap.id

The relation over an arbitrary ring of points. The canonical Kostant Weyl element on points squares to (-1) ^ n after base change to every commutative ring, including characteristics in which the factorials dividing the rational exponential need not be invertible.