The Weyl group of the diagonal torus in the general linear group

For a field k with a nontrivial unit group, the normalizer quotient of the diagonal torus in GL_n(k) is the permutation group of the coordinate lines. Independently, the Weyl group of the diagonal coordinate root datum is the permutation group of its universe-lifted coordinates. This file identifies those two groups and proves that the identification gives the same actions on the character lattice and on the roots.

Concretely, the class of a normalizing matrix g maps to the root-datum automorphism attached to diagonalNormalizerPerm g. The class of a permutation matrix for the transposition (i j) maps to reflection in the root e_i - e_j. Thus the group-of-points normalizer computation and the coordinate root datum describe the same Weyl group of the standard split torus in GL_n.

Main declarations

• TauCeti.GeneralLinear.diagonalNormalizerQuotientMulEquivWeylGroup: the canonical equivalence from the diagonal normalizer quotient to the Weyl group of diagonalRootDatum.
• TauCeti.GeneralLinear.diagonalNormalizerQuotientMulEquivWeylGroup_smul_apply: its action on the character lattice.
• TauCeti.GeneralLinear.diagonalNormalizerQuotientMulEquivWeylGroup_permutationGL_swap: a transposition matrix maps to the corresponding root reflection.

References

• J. S. Milne, Algebraic Groups (2017), Example 19.7 and Section 21.1.
• J. E. Humphreys, Linear Algebraic Groups (1975), Sections 16.1 and 26.3.

This advances Layer 7, "Root datum (G, T) with its Weyl group", of the ReductiveGroups roadmap through the group-of-points Weyl group of the standard split maximal torus of GL_n; the scheme-level identification is not addressed here.

noncomputable def TauCeti.GeneralLinear.diagonalWeylGroupMulEquivCoordinateWeylGroup (n : ℕ) : ↥(RootPairing.weylGroup (diagonalRootDatum n)) ≃* ↥(RootPairing.weylGroup (SplitTorus.coordinateRootDatum (ULift.{u, 0} (Fin n))))

Transport between the Weyl groups across the opaque diagonalRootDatum wrapper.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.GeneralLinear.diagonalNormalizerQuotientMulEquivWeylGroup (k : Type v) [Field k] [Nontrivial kˣ] (n : ℕ) : (TauCeti.diagonalTorus k n).normalizerQuotient ≃* ↥(RootPairing.weylGroup (diagonalRootDatum n))

The normalizer quotient of the diagonal torus is the Weyl group of its coordinate root datum. The intermediate permutation is transported from Fin n to the universe-lifted coordinate type used by diagonalRootDatum.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.GeneralLinear.diagonalNormalizerQuotientMulEquivWeylGroup_mk {k : Type v} [Field k] [Nontrivial kˣ] {n : ℕ} (g : ↥(Subgroup.normalizer ↑(TauCeti.diagonalTorus k n))) : (diagonalNormalizerQuotientMulEquivWeylGroup k n) ↑g = (diagonalWeylGroupMulEquivCoordinateWeylGroup n).symm (SplitTorus.coordinatePermMulEquivWeylGroup (Equiv.ulift.symm.permCongrHom (diagonalNormalizerPerm g)))

On a normalizer representative, the Weyl-group equivalence is the root-datum automorphism induced by its coordinate permutation.

@[simp]

theorem TauCeti.GeneralLinear.diagonalNormalizerQuotientMulEquivWeylGroup_permutationGL {k : Type v} [Field k] [Nontrivial kˣ] {n : ℕ} (e : Equiv.Perm (Fin n)) : (diagonalNormalizerQuotientMulEquivWeylGroup k n) ↑⟨permutationGL e, ⋯⟩ = (diagonalWeylGroupMulEquivCoordinateWeylGroup n).symm (SplitTorus.coordinatePermMulEquivWeylGroup (Equiv.ulift.symm.permCongrHom e))

A permutation matrix represents the Weyl element induced by the same coordinate permutation, transported to the universe-lifted root coordinates.

@[simp]

theorem TauCeti.GeneralLinear.diagonalNormalizerQuotientMulEquivWeylGroup_smul_apply {k : Type v} [Field k] [Nontrivial kˣ] {n : ℕ} (q : (TauCeti.diagonalTorus k n).normalizerQuotient) (x : ULift.{u, 0} (Fin n) →₀ ℤ) (a : ULift.{u, 0} (Fin n)) : ((diagonalNormalizerQuotientMulEquivWeylGroup k n) q • x) a = x { down := (Equiv.symm (diagonalNormalizerQuotientMulEquivPerm q)) a.down }

The Weyl element represented by a normalizer class acts on the character lattice by moving each coordinate through its associated permutation; equivalently, its value at a coordinate is the original value at the inverse image of that coordinate.

@[simp]

theorem TauCeti.GeneralLinear.diagonalNormalizerQuotientMulEquivWeylGroup_weightMap_apply {k : Type v} [Field k] [Nontrivial kˣ] {n : ℕ} (q : (TauCeti.diagonalTorus k n).normalizerQuotient) (x : ULift.{u, 0} (Fin n) →₀ ℤ) : (↑↑((diagonalNormalizerQuotientMulEquivWeylGroup k n) q)).weightMap x = (Finsupp.domLCongr (Equiv.ulift.symm.permCongrHom (diagonalNormalizerQuotientMulEquivPerm q))) x

The underlying root-datum automorphism moves character coordinates by the associated permutation.

@[simp]

theorem TauCeti.GeneralLinear.diagonalNormalizerQuotientMulEquivWeylGroup_coweightMap_apply {k : Type v} [Field k] [Nontrivial kˣ] {n : ℕ} (q : (TauCeti.diagonalTorus k n).normalizerQuotient) (x : ULift.{u, 0} (Fin n) → ℤ) (a : ULift.{u, 0} (Fin n)) : (↑↑((diagonalNormalizerQuotientMulEquivWeylGroup k n) q)).coweightMap x a = x { down := (diagonalNormalizerQuotientMulEquivPerm q) a.down }

The underlying root-datum automorphism acts contravariantly on cocharacters through the associated coordinate permutation.

@[simp]

theorem TauCeti.GeneralLinear.diagonalNormalizerQuotientMulEquivWeylGroup_indexEquiv_apply {k : Type v} [Field k] [Nontrivial kˣ] {n : ℕ} (q : (TauCeti.diagonalTorus k n).normalizerQuotient) (p : DiagonalRootIndex n) : (↑↑((diagonalNormalizerQuotientMulEquivWeylGroup k n) q)).indexEquiv p = (SplitTorus.coordinatePermRootIndex (Equiv.ulift.symm.permCongrHom (diagonalNormalizerQuotientMulEquivPerm q))) p

The Weyl element represented by a normalizer class applies the associated coordinate permutation simultaneously to both entries of a root index.

@[simp]

theorem TauCeti.GeneralLinear.diagonalNormalizerQuotientMulEquivWeylGroup_permutationGL_swap {k : Type v} [Field k] [Nontrivial kˣ] {n : ℕ} (i j : Fin n) (hij : i ≠ j) : (diagonalNormalizerQuotientMulEquivWeylGroup k n) ↑⟨permutationGL (Equiv.swap i j), ⋯⟩ = RootPairing.weylGroup.ofIdx (diagonalRootDatum n) ⟨({ down := i }, { down := j }), ⋯⟩

A transposition matrix maps to reflection in the corresponding diagonal root.

@[simp]

theorem TauCeti.GeneralLinear.diagonalNormalizerQuotientMulEquivWeylGroup_symm_ofIdx {k : Type v} [Field k] [Nontrivial kˣ] {n : ℕ} (p : DiagonalRootIndex n) : (diagonalNormalizerQuotientMulEquivWeylGroup k n).symm (RootPairing.weylGroup.ofIdx (diagonalRootDatum n) p) = ↑⟨permutationGL (Equiv.swap (↑p).1.down (↑p).2.down), ⋯⟩

Conversely, a diagonal-root reflection corresponds to the normalizer class of the transposition matrix swapping its two coordinate lines.