The symplectic diagonal normalizer acts faithfully modulo the torus

Over a field with a unit different from its inverse, the normalizer of the paired diagonal torus consists exactly of the symplectic monomial matrices. Its permutation action on the 2m coordinate lines has kernel the diagonal torus, and therefore induces an injective homomorphism from the normalizer quotient to the symmetric group.

This supplies the coordinate-line action used to compare the normalizer quotient with the type-C Weyl group. The image of the action is not computed here. The unit hypothesis separates the two weights in each symplectic plane; it holds over infinite fields in every characteristic, but cannot be dropped for rational points over small finite fields.

References

• J. E. Humphreys, Linear Algebraic Groups, Sections 16.1 and 26.3.
• J. S. Milne, Algebraic Groups (2017), Example 21.2.

The reduction to monomial matrices and the permutation construction follow TauCeti.LinearAlgebra.Matrix.SpecialLinearGroup.Diagonal.Normalizer, using the existing general-linear normalizer API and the symplectic coordinate-separation theorem.

theorem TauCeti.GLSymplecticFin.mem_normalizer_diagonalTorus_of_coe_mem {m : ℕ} {k : Type u_1} [CommRing k] {g : ↥(GLSymplecticFin m k)} (hg : ↑g ∈ Subgroup.normalizer ↑(TauCeti.diagonalTorus k (m + m))) : g ∈ Subgroup.normalizer ↑(diagonalTorus k m)

A symplectic matrix that normalizes the full diagonal torus also normalizes the paired diagonal torus.

theorem TauCeti.GLSymplecticFin.mem_normalizer_diagonalTorus_iff_coe_mem {m : ℕ} {k : Type u_1} [Field k] (u : kˣ) (hu : u ≠ u⁻¹) {g : ↥(GLSymplecticFin m k)} : g ∈ Subgroup.normalizer ↑(diagonalTorus k m) ↔ ↑g ∈ Subgroup.normalizer ↑(TauCeti.diagonalTorus k (m + m))

If a unit differs from its inverse, normalizing the symplectic diagonal torus is equivalent to normalizing the full diagonal torus in the ambient general linear group.

theorem TauCeti.GLSymplecticFin.mem_normalizer_diagonalTorus_iff_exists {m : ℕ} {k : Type u_1} [Field k] (u : kˣ) (hu : u ≠ u⁻¹) {g : ↥(GLSymplecticFin m k)} : g ∈ Subgroup.normalizer ↑(diagonalTorus k m) ↔ ∃ (d : Fin (m + m) → kˣ) (σ : Equiv.Perm (Fin (m + m))), ↑g = diagGL d * permutationGL σ

The normalizer of the paired diagonal torus consists exactly of symplectic monomial matrices. The diagonal and permutation factors are taken in the ambient general linear group; they need not separately be symplectic.

noncomputable def TauCeti.GLSymplecticFin.diagonalNormalizerPerm {m : ℕ} {k : Type u_1} [Field k] (u : kˣ) (hu : u ≠ u⁻¹) : ↥(Subgroup.normalizer ↑(diagonalTorus k m)) →* Equiv.Perm (Fin (m + m))

The permutation of the 2m coordinate lines induced by a symplectic matrix normalizing the paired diagonal torus.

Equations

• TauCeti.GLSymplecticFin.diagonalNormalizerPerm u hu = TauCeti.diagonalNormalizerPerm.comp (TauCeti.GLSymplecticFin.diagonalNormalizerToGL✝ u hu)

theorem TauCeti.GLSymplecticFin.diagonalNormalizerPerm_eq_of_eq_diagGL_mul_permutationGL {m : ℕ} {k : Type u_1} [Field k] (u : kˣ) (hu : u ≠ u⁻¹) (g : ↥(Subgroup.normalizer ↑(diagonalTorus k m))) (d : Fin (m + m) → kˣ) (σ : Equiv.Perm (Fin (m + m))) (h : ↑↑g = diagGL d * permutationGL σ) : (diagonalNormalizerPerm u hu) g = σ

Any monomial factorization reads off the permutation of a symplectic normalizer element.

theorem TauCeti.GLSymplecticFin.diagonalNormalizerPerm_eq {m : ℕ} {k : Type u_1} [Field k] (u : kˣ) (hu : u ≠ u⁻¹) (v : kˣ) (hv : v ≠ v⁻¹) : diagonalNormalizerPerm u hu = diagonalNormalizerPerm v hv

The coordinate permutation is independent of the unit used to separate coordinates.

@[simp]

theorem TauCeti.GLSymplecticFin.diagonalNormalizerPerm_eq_one_iff {m : ℕ} {k : Type u_1} [Field k] (u : kˣ) (hu : u ≠ u⁻¹) (g : ↥(Subgroup.normalizer ↑(diagonalTorus k m))) : (diagonalNormalizerPerm u hu) g = 1 ↔ ↑g ∈ diagonalTorus k m

A normalizer element acts trivially on coordinate lines exactly when it lies in the paired diagonal torus.

theorem TauCeti.GLSymplecticFin.coe_diagonalNormalizer_mul_diagonal_mul_inv {m : ℕ} {k : Type u_1} [Field k] (u : kˣ) (hu : u ≠ u⁻¹) (g : ↥(Subgroup.normalizer ↑(diagonalTorus k m))) (t : Fin m → kˣ) : ↑(↑g * diagonal t * (↑g)⁻¹) = diagGL fun (i : Fin (m + m)) => diagonalCoordinates t ((Equiv.symm ((diagonalNormalizerPerm u hu) g)) i)

Conjugation by a symplectic normalizer element permutes the paired diagonal entries by the inverse of its coordinate permutation.

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

The action of the symplectic diagonal normalizer quotient on coordinate lines.

Equations

• TauCeti.GLSymplecticFin.diagonalNormalizerQuotientPerm u hu = (TauCeti.GLSymplecticFin.diagonalTorus k m).normalizerQuotientLift (TauCeti.GLSymplecticFin.diagonalNormalizerPerm u hu) ⋯

@[simp]

theorem TauCeti.GLSymplecticFin.diagonalNormalizerQuotientPerm_mk {m : ℕ} {k : Type u_1} [Field k] (u : kˣ) (hu : u ≠ u⁻¹) (g : ↥(Subgroup.normalizer ↑(diagonalTorus k m))) : (diagonalNormalizerQuotientPerm u hu) ↑g = (diagonalNormalizerPerm u hu) g

On a quotient representative, the induced action is its coordinate permutation.

theorem TauCeti.GLSymplecticFin.diagonalNormalizerQuotientPerm_injective {m : ℕ} {k : Type u_1} [Field k] (u : kˣ) (hu : u ≠ u⁻¹) : Function.Injective ⇑(diagonalNormalizerQuotientPerm u hu)

The symplectic diagonal normalizer quotient acts faithfully on the coordinate lines.