The Weyl group of the diagonal torus of the special linear group #

The Weyl group of the diagonal root datum of SL_{r+1} is the symmetric group on the r + 1 coordinate lines. Reflections act on ordered root indices by transpositions, and faithfulness follows because the coroots span the cocharacter lattice. This realizes the identification integrally, including rank zero.

Over a field whose determinant-one diagonal torus separates coordinates, composing with the matrix normalizer computation identifies the normalizer quotient with this Weyl group. The root-index and character-lattice formulas specify the identification; in particular a normalizer class with a transposition as its coordinate permutation gives the corresponding reflection. The separation assumption concerns the group of rational points and is essential over small finite fields. No scheme-theoretic normalizer assertion is made here.

References #

J. S. Milne, Algebraic Groups (2017), Example 21.2 and Section 21.1.
J. E. Humphreys, Linear Algebraic Groups (1975), Section 26.3.

The normalizer comparison follows the general-linear comparison in TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Root.WeylGroup. The root-datum computation uses Mathlib's RootPairing.range_weylGroupToPerm and the existing coordinate-index action.

source

noncomputable def TauCeti.SpecialLinear.diagonalPermMulEquivWeylGroup (r : ℕ) :

Equiv.Perm (Fin (r + 1)) ≃* ↥(RootPairing.weylGroup (diagonalRootDatum r))

The Weyl group of the diagonal root datum of SL_{r+1} is the permutation group of the coordinate lines. A permutation acts simultaneously on both entries of a root index.

Equations

TauCeti.SpecialLinear.diagonalPermMulEquivWeylGroup r = (MonoidHom.ofInjective ⋯).trans ((MulEquiv.subgroupCongr ⋯).trans (MonoidHom.ofInjective ⋯).symm)

Instances For

source

@[simp]

theorem TauCeti.SpecialLinear.diagonalPermMulEquivWeylGroup_indexEquiv_apply {r : ℕ} (e : Equiv.Perm (Fin (r + 1))) (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) :

(↑↑((diagonalPermMulEquivWeylGroup r) e)).indexEquiv p = (SplitTorus.coordinatePermRootIndex e) p

The Weyl element attached to a coordinate permutation acts componentwise on root indices.

source

@[simp]

theorem TauCeti.SpecialLinear.diagonalPermMulEquivWeylGroup_swap {r : ℕ} (i j : Fin (r + 1)) (hij : i ≠ j) :

(diagonalPermMulEquivWeylGroup r) (Equiv.swap i j) = RootPairing.weylGroup.ofIdx (diagonalRootDatum r) ⟨(i, j), hij⟩

A transposition of coordinate lines is the reflection in their difference root.

source

@[simp]

theorem TauCeti.SpecialLinear.diagonalPermMulEquivWeylGroup_symm_ofIdx {r : ℕ} (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) :

(diagonalPermMulEquivWeylGroup r).symm (RootPairing.weylGroup.ofIdx (diagonalRootDatum r) p) = Equiv.swap (↑p).1 (↑p).2

A root reflection corresponds to the transposition of its two coordinate indices.

source

@[simp]

theorem TauCeti.SpecialLinear.diagonalPermMulEquivWeylGroup_smul_apply {r : ℕ} (e : Equiv.Perm (Fin (r + 1))) (x : ULift.{u, 0} (Fin r) →₀ ℤ) (i : ULift.{u, 0} (Fin r)) :

((diagonalPermMulEquivWeylGroup r) e • x) i = x.sum fun (j : ULift.{u, 0} (Fin r)) (c : ℤ) => c * ((if (Equiv.symm e) i.down.castSucc ≤ j.down.castSucc then 1 else 0) - if (Equiv.symm e) i.down.succ ≤ j.down.castSucc then 1 else 0)

In fundamental-weight coordinates, the action of a permutation on a character is computed by pairing with the inverse images of the simple coroots.

source

noncomputable def TauCeti.SpecialLinear.diagonalNormalizerQuotientMulEquivWeylGroup {r : ℕ} {k : Type v} [Field k] (hsep : Matrix.SpecialLinearGroup.DiagonalTorusSeparatesCoordinates k (r + 1)) :

(Matrix.SpecialLinearGroup.diagonalTorus k (r + 1)).normalizerQuotient ≃* ↥(RootPairing.weylGroup (diagonalRootDatum r))

The normalizer quotient of the determinant-one diagonal torus is the Weyl group of the root datum of SL_{r+1}, whenever the torus separates coordinate lines.

Equations