The Weyl group of the symplectic diagonal torus is the hyperoctahedral group

Over a field k with a unit different from its inverse, the normalizer quotient N(T)/T of the paired diagonal torus T in Sp₂ₘ(k) acts faithfully on the 2m coordinate lines (TauCeti.GLSymplecticFin.diagonalNormalizerQuotientPerm_injective). This file computes the image of that action: it consists exactly of the signed permutations. Hence N(T)/T is the hyperoctahedral group Sym(Bool) ≀ Sym(m).

The coordinate lines are labelled by Fin m × Bool through signedCoordinateEquiv: the line (i, false) is the i-th line of the first block, on which the torus acts by tᵢ, and (i, true) is the i-th line of the second block, on which it acts by tᵢ⁻¹. A normalizer element conjugates diag(t) to another element of the torus, so it must carry the two lines of each symplectic plane, on which the torus acts by mutually inverse characters, to the two lines of a single plane; this is the commutation with the flip of Bool. Conversely the long-root Weyl representative n_{2eᵢ} exchanges the two lines of the i-th plane and the short-root Weyl representative n_{eᵢ-eⱼ} exchanges the i-th and j-th planes, and these generate the hyperoctahedral group.

Main definitions

• TauCeti.GLSymplecticFin.signedCoordinateEquiv: the labelling of the coordinates of Fin (m + m) by Fin m × Bool.
• TauCeti.GLSymplecticFin.diagonalNormalizerQuotientMulEquivWreathProduct: the normalizer quotient of the paired diagonal torus is the hyperoctahedral group.

Main results

All in the namespace TauCeti.GLSymplecticFin:

• signedCoordinateEquiv_diagonalNormalizerQuotientMulEquivWreathProduct_apply: the equivalence is compatible with the actions on the coordinate lines.
• diagonalNormalizerQuotientMulEquivWreathProduct_positiveLongRootWeylElement: the long-root Weyl representative n_{2eᵢ} is the sign change of the i-th coordinate.
• diagonalNormalizerQuotientMulEquivWreathProduct_differenceShortRootWeylElement: the short-root Weyl representative n_{eᵢ-eⱼ} is the transposition of the i-th and j-th coordinates.

References

• J. E. Humphreys, Linear Algebraic Groups (1975), Section 26.3 and the table of Weyl groups in Appendix A.
• J. S. Milne, Algebraic Groups (2017), Example 21.2 and Section 21.1.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate III.

def TauCeti.GLSymplecticFin.signedCoordinateEquiv (m : ℕ) : Fin m × Bool ≃ Fin (m + m)

The labelling of the coordinates of Fin (m + m) by Fin m × Bool: (i, false) is the i-th coordinate of the first block and (i, true) is the i-th coordinate of the second block. On these, the paired diagonal torus acts by tᵢ and tᵢ⁻¹ respectively.

Equations

• TauCeti.GLSymplecticFin.signedCoordinateEquiv m = ((Equiv.prodComm (Fin m) Bool).trans (Equiv.boolProdEquivSum (Fin m))).trans finSumFinEquiv

@[simp]

theorem TauCeti.GLSymplecticFin.signedCoordinateEquiv_false {m : ℕ} (i : Fin m) : (signedCoordinateEquiv m) (i, false) = Fin.castAdd m i

@[simp]

theorem TauCeti.GLSymplecticFin.signedCoordinateEquiv_true {m : ℕ} (i : Fin m) : (signedCoordinateEquiv m) (i, true) = i.addNat m

@[simp]

theorem TauCeti.GLSymplecticFin.diagonalCoordinates_signedCoordinateEquiv {m : ℕ} {R : Type u_1} [Monoid R] (t : Fin m → Rˣ) (x : Fin m × Bool) : diagonalCoordinates t ((signedCoordinateEquiv m) x) = if x.2 = true then (t x.1)⁻¹ else t x.1

The diagonal entry of a paired diagonal matrix on the line (i, s) is tᵢ or tᵢ⁻¹ according to whether s is false or true.

noncomputable def TauCeti.GLSymplecticFin.diagonalNormalizerQuotientMulEquivWreathProduct {m : ℕ} {k : Type u_1} [Field k] (u : kˣ) (hu : u ≠ u⁻¹) : (diagonalTorus k m).normalizerQuotient ≃* WreathProduct (Equiv.Perm Bool) (Fin m)

The Weyl group of the symplectic diagonal torus. Over a field with a unit different from its inverse, the normalizer quotient N(T)/T of the paired diagonal torus T in Sp₂ₘ(k) is the hyperoctahedral group Sym(Bool) ≀ Sym(m) of signed permutations. The class of a normalizer element acts on Fin m × Bool as its coordinate permutation does on the coordinate lines; see signedCoordinateEquiv_diagonalNormalizerQuotientMulEquivWreathProduct_apply.

Equations

• TauCeti.GLSymplecticFin.diagonalNormalizerQuotientMulEquivWreathProduct u hu = ((MonoidHom.ofInjective ⋯).trans (MulEquiv.subgroupCongr ⋯)).trans (MonoidHom.ofInjective ⋯).symm

@[simp]

theorem TauCeti.GLSymplecticFin.signedCoordinateEquiv_diagonalNormalizerQuotientMulEquivWreathProduct_apply {m : ℕ} {k : Type u_1} [Field k] (u : kˣ) (hu : u ≠ u⁻¹) (q : (diagonalTorus k m).normalizerQuotient) (x : Fin m × Bool) : (signedCoordinateEquiv m) (((diagonalNormalizerQuotientMulEquivWreathProduct u hu) q).right x.1, (((diagonalNormalizerQuotientMulEquivWreathProduct u hu) q).left (((diagonalNormalizerQuotientMulEquivWreathProduct u hu) q).right x.1)) x.2) = ((diagonalNormalizerQuotientPerm u hu) q) ((signedCoordinateEquiv m) x)

The hyperoctahedral element attached to a class moves the labelled coordinate lines as the class moves the coordinate lines of Fin (m + m).

@[simp]

theorem TauCeti.GLSymplecticFin.diagonalNormalizerQuotientMulEquivWreathProduct_positiveLongRootWeylElement {m : ℕ} {k : Type u_1} [Field k] (u : kˣ) (hu : u ≠ u⁻¹) (i : Fin m) : (diagonalNormalizerQuotientMulEquivWreathProduct u hu) ↑⟨positiveLongRootWeylElement i, ⋯⟩ = SemidirectProduct.inl (Pi.mulSingle i (Equiv.swap false true))

The class of the long-root Weyl representative n_{2eᵢ} is the sign change of the i-th coordinate.

@[simp]

theorem TauCeti.GLSymplecticFin.diagonalNormalizerQuotientMulEquivWreathProduct_differenceShortRootWeylElement {m : ℕ} {k : Type u_1} [Field k] (u : kˣ) (hu : u ≠ u⁻¹) {i j : Fin m} (hij : i ≠ j) : (diagonalNormalizerQuotientMulEquivWreathProduct u hu) ↑⟨differenceShortRootWeylElement hij, ⋯⟩ = SemidirectProduct.inr (Equiv.swap i j)

The class of the short-root Weyl representative n_{eᵢ-eⱼ} is the transposition of the i-th and j-th coordinates.