The Weyl group of the diagonal torus of the symplectic group

The Weyl group of the type Cₘ root datum TauCeti.Symplectic.diagonalRootDatum of Sp₂ₘ is the hyperoctahedral group Sym(Bool) ≀ Sym(m) of signed permutations of the coordinates. This file constructs that identification integrally, for every rank m including m = 0.

The comparison goes through the signed basis characters ± eₐ of the character lattice. Every root reflection permutes them: the long reflections in ± 2eᵢ change the sign of eᵢ, the reflections in eᵢ - eⱼ exchange eᵢ and eⱼ, and those in ± (eᵢ + eⱼ) exchange eᵢ with -eⱼ. Hence every Weyl element permutes the 2m signed characters compatibly with negation, and it is determined by that permutation. Conversely the sign changes and the transpositions generate the hyperoctahedral group, so its imprimitive action on Fin m × Bool is exactly the image.

Over a field with a unit different from its inverse, the normalizer quotient of the diagonal torus in Sp₂ₘ(k) is the same hyperoctahedral group (TauCeti.GLSymplecticFin.diagonalNormalizerQuotientMulEquivWreathProduct). Composing the two identifications, the final section identifies the group-of-points Weyl group N(T)(k)/T(k) with the Weyl group of the root datum, the class of each Weyl representative n_α going to the reflection in α.

Main definitions

• TauCeti.Symplectic.diagonalWreathProductMulEquivWeylGroup: the multiplicative equivalence from Sym(Bool) ≀ Sym(m) to the Weyl group of diagonalRootDatum.
• TauCeti.Symplectic.diagonalNormalizerQuotientMulEquivWeylGroup: the multiplicative equivalence from the normalizer quotient of the diagonal torus in Sp₂ₘ(k) to the Weyl group of diagonalRootDatum.

Main results

• TauCeti.Symplectic.diagonalWreathProductMulEquivWeylGroup_smul_single: a signed permutation sends the character n • eₐ to ± n • e_{π a}, the sign being its sign change at π a; TauCeti.Symplectic.diagonalWreathProductMulEquivWeylGroup_smul_apply is the same action in coordinates.
• TauCeti.Symplectic.diagonalWreathProductMulEquivWeylGroup_inl_mulSingle_swap: the sign change of the i-th coordinate is the reflection in the long root 2eᵢ.
• TauCeti.Symplectic.diagonalWreathProductMulEquivWeylGroup_inr_swap: the transposition of the i-th and j-th coordinates is the reflection in the short root eᵢ - eⱼ.
• TauCeti.Symplectic.diagonalNormalizerQuotientMulEquivWeylGroup_smul_single: a normalizer class moving the coordinate line of eₐ to the line of ± e_b sends n • eₐ to ± n • e_b.
• TauCeti.Symplectic.diagonalNormalizerQuotientMulEquivWeylGroup_positiveLongRootWeylElement and TauCeti.Symplectic.diagonalNormalizerQuotientMulEquivWeylGroup_differenceShortRootWeylElement: the classes of the Weyl representatives n_{2eᵢ} and n_{eᵢ-eⱼ} are the reflections in 2eᵢ and eᵢ - eⱼ; the _symm_ofIdx_positiveLong and _symm_ofIdx_difference forms state the converse.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate III (the Weyl group of Cₘ).
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Section 12.1.
• J. S. Milne, Algebraic Groups (2017), Example 21.2 and Section 21.1.

The shape of the comparison follows TauCeti.SpecialLinear.diagonalPermMulEquivWeylGroup, and the hyperoctahedral group is TauCeti.WreathProduct with its imprimitive action.

noncomputable def TauCeti.Symplectic.diagonalWreathProductMulEquivWeylGroup (m : ℕ) : WreathProduct (Equiv.Perm Bool) (Fin m) ≃* ↥(RootPairing.weylGroup (diagonalRootDatum m))

The Weyl group of Sp₂ₘ. The Weyl group of the type Cₘ root datum of the diagonal torus of Sp₂ₘ is the hyperoctahedral group Sym(Bool) ≀ Sym(m) of signed permutations of the coordinates. A signed permutation acts on the character lattice by permuting the coordinate characters eₐ and changing their signs; see TauCeti.Symplectic.diagonalWreathProductMulEquivWeylGroup_smul_single.

Equations

• TauCeti.Symplectic.diagonalWreathProductMulEquivWeylGroup m = ((MonoidHom.ofInjective ⋯).trans (MulEquiv.subgroupCongr ⋯)).trans (MonoidHom.ofInjective ⋯).symm

@[simp]

theorem TauCeti.Symplectic.diagonalWreathProductMulEquivWeylGroup_smul_single {m : ℕ} (w : WreathProduct (Equiv.Perm Bool) (Fin m)) (a : Fin m) (n : ℤ) : (diagonalWreathProductMulEquivWeylGroup m) w • Finsupp.single { down := a } n = Finsupp.single { down := w.right a } (if (w.left (w.right a)) false = true then -n else n)

A signed permutation w sends the character n • eₐ to ± n • e_{π a}, where π is the permutation w.right of the coordinates and the sign is negative exactly when w changes the sign of the coordinate π a.

@[simp]

theorem TauCeti.Symplectic.diagonalWreathProductMulEquivWeylGroup_smul_apply {m : ℕ} (w : WreathProduct (Equiv.Perm Bool) (Fin m)) (x : ULift.{u, 0} (Fin m) →₀ ℤ) (b : Fin m) : ((diagonalWreathProductMulEquivWeylGroup m) w • x) { down := b } = if (w.left b) false = true then -x { down := (Equiv.symm w.right) b } else x { down := (Equiv.symm w.right) b }

In coordinates, the b-th coordinate of a character moved by a signed permutation w is the π⁻¹ b-th coordinate of the character, where π is w.right, negated exactly when w changes the sign of b.

@[simp]

theorem TauCeti.Symplectic.diagonalWreathProductMulEquivWeylGroup_inl_mulSingle_swap {m : ℕ} (i : Fin m) : (diagonalWreathProductMulEquivWeylGroup m) (SemidirectProduct.inl (Pi.mulSingle i (Equiv.swap false true))) = RootPairing.weylGroup.ofIdx (diagonalRootDatum m) (GLSymplecticFin.RootSubgroupIndex.positiveLong i)

The sign change of the i-th coordinate is the reflection in the long root 2eᵢ.

@[simp]

theorem TauCeti.Symplectic.diagonalWreathProductMulEquivWeylGroup_inr_swap {m : ℕ} {i j : Fin m} (hij : i ≠ j) : (diagonalWreathProductMulEquivWeylGroup m) (SemidirectProduct.inr (Equiv.swap i j)) = RootPairing.weylGroup.ofIdx (diagonalRootDatum m) (GLSymplecticFin.RootSubgroupIndex.difference i j hij)

The transposition of the i-th and j-th coordinates is the reflection in the short root eᵢ - eⱼ.

@[simp]

theorem TauCeti.Symplectic.diagonalWreathProductMulEquivWeylGroup_symm_ofIdx_positiveLong {m : ℕ} (i : Fin m) : (diagonalWreathProductMulEquivWeylGroup m).symm (RootPairing.weylGroup.ofIdx (diagonalRootDatum m) (GLSymplecticFin.RootSubgroupIndex.positiveLong i)) = SemidirectProduct.inl (Pi.mulSingle i (Equiv.swap false true))

The reflection in the long root 2eᵢ is the sign change of the i-th coordinate.

@[simp]

theorem TauCeti.Symplectic.diagonalWreathProductMulEquivWeylGroup_symm_ofIdx_difference {m : ℕ} {i j : Fin m} (hij : i ≠ j) : (diagonalWreathProductMulEquivWeylGroup m).symm (RootPairing.weylGroup.ofIdx (diagonalRootDatum m) (GLSymplecticFin.RootSubgroupIndex.difference i j hij)) = SemidirectProduct.inr (Equiv.swap i j)

The reflection in the short root eᵢ - eⱼ is the transposition of the i-th and j-th coordinates.

The normalizer quotient of the diagonal torus

noncomputable def TauCeti.Symplectic.diagonalNormalizerQuotientMulEquivWeylGroup (m : ℕ) {k : Type u_1} [Field k] (c : kˣ) (hc : c ≠ c⁻¹) : (GLSymplecticFin.diagonalTorus k m).normalizerQuotient ≃* ↥(RootPairing.weylGroup (diagonalRootDatum m))

The Weyl group of Sp₂ₘ as a normalizer quotient. Over a field with a unit c ≠ c⁻¹, the normalizer quotient N(T)(k)/T(k) of the diagonal torus of Sp₂ₘ(k) is the Weyl group of the type Cₘ root datum diagonalRootDatum. Both are identified with the hyperoctahedral group Sym(Bool) ≀ Sym(m).

Equations

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

theorem TauCeti.Symplectic.diagonalNormalizerQuotientMulEquivWeylGroup_smul_single {m : ℕ} {k : Type u_1} [Field k] (c : kˣ) (hc : c ≠ c⁻¹) (q : (GLSymplecticFin.diagonalTorus k m).normalizerQuotient) {a b : Fin m} {s : Bool} (h : ((GLSymplecticFin.diagonalNormalizerQuotientPerm c hc) q) (Fin.castAdd m a) = (GLSymplecticFin.signedCoordinateEquiv m) (b, s)) (n : ℤ) : (diagonalNormalizerQuotientMulEquivWeylGroup m c hc) q • Finsupp.single { down := a } n = Finsupp.single { down := b } (if s = true then -n else n)

If the class q moves the coordinate line of the character eₐ to the line of e_b (for s = false) or of -e_b (for s = true), then its Weyl element sends n • eₐ to n • e_b or -n • e_b respectively.

@[simp]

theorem TauCeti.Symplectic.diagonalNormalizerQuotientMulEquivWeylGroup_positiveLongRootWeylElement {m : ℕ} {k : Type u_1} [Field k] (c : kˣ) (hc : c ≠ c⁻¹) (i : Fin m) : (diagonalNormalizerQuotientMulEquivWeylGroup m c hc) ↑⟨GLSymplecticFin.positiveLongRootWeylElement i, ⋯⟩ = RootPairing.weylGroup.ofIdx (diagonalRootDatum m) (GLSymplecticFin.RootSubgroupIndex.positiveLong i)

The class of the long-root Weyl representative n_{2eᵢ} is the reflection in 2eᵢ.

@[simp]

theorem TauCeti.Symplectic.diagonalNormalizerQuotientMulEquivWeylGroup_differenceShortRootWeylElement {m : ℕ} {k : Type u_1} [Field k] (c : kˣ) (hc : c ≠ c⁻¹) {i j : Fin m} (hij : i ≠ j) : (diagonalNormalizerQuotientMulEquivWeylGroup m c hc) ↑⟨GLSymplecticFin.differenceShortRootWeylElement hij, ⋯⟩ = RootPairing.weylGroup.ofIdx (diagonalRootDatum m) (GLSymplecticFin.RootSubgroupIndex.difference i j hij)

The class of the short-root Weyl representative n_{eᵢ-eⱼ} is the reflection in eᵢ - eⱼ.

@[simp]

theorem TauCeti.Symplectic.diagonalNormalizerQuotientMulEquivWeylGroup_symm_ofIdx_positiveLong {m : ℕ} {k : Type u_1} [Field k] (c : kˣ) (hc : c ≠ c⁻¹) (i : Fin m) : (diagonalNormalizerQuotientMulEquivWeylGroup m c hc).symm (RootPairing.weylGroup.ofIdx (diagonalRootDatum m) (GLSymplecticFin.RootSubgroupIndex.positiveLong i)) = ↑⟨GLSymplecticFin.positiveLongRootWeylElement i, ⋯⟩

The reflection in the long root 2eᵢ is the class of the Weyl representative n_{2eᵢ}.

@[simp]

theorem TauCeti.Symplectic.diagonalNormalizerQuotientMulEquivWeylGroup_symm_ofIdx_difference {m : ℕ} {k : Type u_1} [Field k] (c : kˣ) (hc : c ≠ c⁻¹) {i j : Fin m} (hij : i ≠ j) : (diagonalNormalizerQuotientMulEquivWeylGroup m c hc).symm (RootPairing.weylGroup.ofIdx (diagonalRootDatum m) (GLSymplecticFin.RootSubgroupIndex.difference i j hij)) = ↑⟨GLSymplecticFin.differenceShortRootWeylElement hij, ⋯⟩

The reflection in the short root eᵢ - eⱼ is the class of the Weyl representative n_{eᵢ-eⱼ}.