The centralizer of the symplectic diagonal torus

The diagonal symplectic matrices are exactly the image of the paired diagonal homomorphism. Over a domain with a unit different from its inverse, this image is its own centralizer, hence maximal among commutative subgroups. In particular these conclusions hold over every infinite field, in all characteristics and in every rank.

This pointwise centralizer calculation supplies the matrix comparison used to prove maximality of the diagonal torus as a closed subgroup scheme. The unit hypothesis distinguishes the two weights on each symplectic plane; it cannot simply be omitted over small finite fields.

References

• The general-linear centralizer formalization in TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Diagonal.Basic.
• J. E. Humphreys, Linear Algebraic Groups, §16.1 and §26.3.

theorem TauCeti.GLSymplecticFin.exists_diagonalCoordinates_ne {m : ℕ} {R : Type u_1} [Monoid R] (u : Rˣ) (hu : u ≠ u⁻¹) {i j : Fin (m + m)} (hij : i ≠ j) : ∃ (t : Fin m → Rˣ), diagonalCoordinates t i ≠ diagonalCoordinates t j

A unit different from its inverse lets paired diagonal coordinates separate any two positions.

theorem TauCeti.GLSymplecticFin.centralizer_diagonalTorus {m : ℕ} {R : Type u_1} [CommRing R] [IsCancelMulZero R] (u : Rˣ) (hu : u ≠ u⁻¹) : Subgroup.centralizer ↑(diagonalTorus R m) = diagonalTorus R m

The paired diagonal torus is its own centralizer whenever the domain has a unit different from its inverse.

theorem TauCeti.GLSymplecticFin.eq_diagonalTorus_of_le_of_isMulCommutative {m : ℕ} {R : Type u_1} [CommRing R] [IsCancelMulZero R] (u : Rˣ) (hu : u ≠ u⁻¹) (H : Subgroup ↥(GLSymplecticFin m R)) [IsMulCommutative ↥H] (hH : diagonalTorus R m ≤ H) : H = diagonalTorus R m

If the domain has a unit different from its inverse, every commutative subgroup containing the paired diagonal torus is that torus.

theorem TauCeti.GLSymplecticFin.centralizer_diagonalTorus_of_infinite {m : ℕ} {R : Type u_1} [Field R] [Infinite R] : Subgroup.centralizer ↑(diagonalTorus R m) = diagonalTorus R m

Over an infinite field, the paired diagonal torus in the symplectic group is its own centralizer.

theorem TauCeti.GLSymplecticFin.eq_diagonalTorus_of_le_of_isMulCommutative_of_infinite {m : ℕ} {R : Type u_1} [Field R] [Infinite R] (H : Subgroup ↥(GLSymplecticFin m R)) [IsMulCommutative ↥H] (hH : diagonalTorus R m ≤ H) : H = diagonalTorus R m

Over an infinite field, every commutative subgroup containing the paired diagonal torus is that torus.