Maximality of the diagonal torus in the symplectic group

Over any field, the paired diagonal torus of Sp₂ₘ is a maximal torus. Over an algebraically closed field it is more: no reduced commutative closed subgroup scheme properly contains it. That is stronger than maximality among tori, because a competing subgroup here need not be a torus, or even connected.

The defining Hopf ideal and its split-torus quotient are the ones already attached to the diagonal torus in TauCeti.Algebra.AlgebraicGroup.Symplectic.DiagonalTorus.ClosedImmersion.

Main declarations

• TauCeti.Symplectic.quotientPointsSubgroup_diagonalTorusDefiningIdeal: the points cut out by the diagonal-torus ideal are the range of the diagonal-torus point morphism.
• TauCeti.Symplectic.eq_diagonalTorusDefiningIdeal_of_le_of_isCocomm: over an algebraically closed field, no larger reduced commutative closed subgroup contains the diagonal torus.
• TauCeti.Symplectic.isMaximalTorus_diagonalTorusDefiningIdeal: the diagonal torus of Sp₂ₘ is a maximal torus, over every field.

References

• J. S. Milne, Algebraic Groups (2017), §17 and §23.
• J. E. Humphreys, Linear Algebraic Groups (1975), §16.1 and §26.3.
• The Hopf-ideal organization and the point-subgroup comparison follow the formal template in TauCeti.Algebra.AlgebraicGroup.GeneralLinear.DiagonalTorus.Maximal, with which this module shares the maximality descent lemma TauCeti.HopfIdeal.isMaximalTorus_of_baseChange.
• The matrix centralizer input is TauCeti.GLSymplecticFin.centralizer_diagonalTorus.

@[simp]

theorem TauCeti.Symplectic.quotientPointsSubgroup_diagonalTorusDefiningIdeal (R : Type u) [CommRing R] (m : ℕ) (A : CommAlgCat R) : CommHopfAlgCat.quotientPointsSubgroup (coordinateHopfAlgebra R m) (diagonalTorusDefiningIdeal R m) A = (GrpCat.Hom.hom ((CommHopfAlgCat.mapPointsFunctor diagonalTorusCoordinateMap).app A)).range

The points cut out by diagonalTorusDefiningIdeal are exactly the diagonal-torus points.

theorem TauCeti.Symplectic.eq_diagonalTorusDefiningIdeal_of_le_of_isCocomm (k : Type u) [Field k] (m : ℕ) [IsAlgClosed k] (I : HopfIdeal k ↑(coordinateHopfAlgebra k m)) [IsReduced ↑(CommHopfAlgCat.quotient (coordinateHopfAlgebra k m) I)] [Coalgebra.IsCocomm k ↑(CommHopfAlgCat.quotient (coordinateHopfAlgebra k m) I)] (hI : I ≤ diagonalTorusDefiningIdeal k m) : I = diagonalTorusDefiningIdeal k m

The diagonal torus of Sp₂ₘ is maximal among reduced commutative closed subgroup schemes over an algebraically closed field.

If I cuts out a reduced commutative closed subgroup containing the diagonal torus, then I is the diagonal-torus defining ideal. Containment is written contravariantly as I ≤ diagonalTorusDefiningIdeal k m; commutativity is the cocommutativity of the quotient coordinate Hopf algebra.

theorem TauCeti.Symplectic.isMaximalTorus_diagonalTorusDefiningIdeal (k : Type u) [Field k] (m : ℕ) : HopfIdeal.IsMaximalTorus k (coordinateHopfAlgebra k m) (diagonalTorusDefiningIdeal k m)

The diagonal torus of Sp₂ₘ is a maximal torus over every field.