Weyl groups of coordinate-difference root data

For a finite coordinate type σ, the roots of SplitTorus.coordinateRootDatum σ are all differences e_i - e_j. Its root reflections are therefore exactly the transpositions of the coordinates. Since transpositions generate the finite symmetric group, the Weyl group of this root datum is canonically isomorphic to Equiv.Perm σ.

The equivalence constructed here is characterized both on reflections and on its actions on the character lattice and the root-index type.

Main declarations

• TauCeti.SplitTorus.coordinatePermMulEquivWeylGroup: the canonical multiplicative equivalence from coordinate permutations to the Weyl group.
• TauCeti.SplitTorus.coordinatePermMulEquivWeylGroup_swap and coordinatePermMulEquivWeylGroup_symm_ofIdx: coordinate transpositions correspond to root reflections in both directions.
• TauCeti.SplitTorus.coordinatePermMulEquivWeylGroup_smul_apply and coordinatePermMulEquivWeylGroup_indexEquiv_apply: the induced actions on characters and root indices.

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 the split Weyl-group part of Layer 7, "Root datum of (G, T)", of the ReductiveGroups roadmap.

noncomputable def TauCeti.SplitTorus.coordinatePermMulEquivWeylGroup {σ : Type u_1} [Finite σ] : Equiv.Perm σ ≃* ↥(RootPairing.weylGroup (coordinateRootDatum σ))

The Weyl group of the coordinate-difference root datum is canonically the permutation group of its coordinates. The equivalence sends a transposition to the reflection in the corresponding root.

Equations

• TauCeti.SplitTorus.coordinatePermMulEquivWeylGroup = MulEquiv.ofBijective TauCeti.SplitTorus.coordinatePermWeylGroupHom✝ ⋯

@[simp]

theorem TauCeti.SplitTorus.coordinatePermMulEquivWeylGroup_weightMap_apply {σ : Type u_1} [Finite σ] (e : Equiv.Perm σ) (x : σ →₀ ℤ) : (↑↑(coordinatePermMulEquivWeylGroup e)).weightMap x = (Finsupp.domLCongr e) x

The underlying root-datum automorphism pushes each character coordinate forward along the permutation; equivalently, its value at a is the original value at e.symm a.

@[simp]

theorem TauCeti.SplitTorus.coordinatePermMulEquivWeylGroup_coweightMap_apply {σ : Type u_1} [Finite σ] (e : Equiv.Perm σ) (x : σ → ℤ) (a : σ) : (↑↑(coordinatePermMulEquivWeylGroup e)).coweightMap x a = x (e a)

The underlying root-datum automorphism acts contravariantly on the cocharacter lattice.

@[simp]

theorem TauCeti.SplitTorus.coordinatePermMulEquivWeylGroup_smul_apply {σ : Type u_1} [Finite σ] (e : Equiv.Perm σ) (x : σ →₀ ℤ) (a : σ) : (coordinatePermMulEquivWeylGroup e • x) a = x ((Equiv.symm e) a)

A coordinate permutation acts on the character lattice by moving each coordinate through that permutation.

@[simp]

theorem TauCeti.SplitTorus.coordinatePermMulEquivWeylGroup_indexEquiv_apply {σ : Type u_1} [Finite σ] (e : Equiv.Perm σ) (p : CoordinateRootIndex σ) : (↑↑(coordinatePermMulEquivWeylGroup e)).indexEquiv p = (coordinatePermRootIndex e) p

The Weyl element attached to a coordinate permutation applies that permutation to both entries of every root index.

@[simp]

theorem TauCeti.SplitTorus.coordinatePermMulEquivWeylGroup_swap {σ : Type u_1} [Finite σ] [DecidableEq σ] (i j : σ) (hij : i ≠ j) : coordinatePermMulEquivWeylGroup (Equiv.swap i j) = RootPairing.weylGroup.ofIdx (coordinateRootDatum σ) ⟨(i, j), hij⟩

A coordinate transposition corresponds to the reflection in the associated root.

@[simp]

theorem TauCeti.SplitTorus.coordinatePermMulEquivWeylGroup_symm_ofIdx {σ : Type u_1} [Finite σ] [DecidableEq σ] (p : CoordinateRootIndex σ) : coordinatePermMulEquivWeylGroup.symm (RootPairing.weylGroup.ofIdx (coordinateRootDatum σ) p) = Equiv.swap (↑p).1 (↑p).2

The inverse Weyl-group equivalence sends a root reflection to the transposition of its two coordinates.