Maximality of the diagonal torus in the special linear group

Over any field, the diagonal torus of SL_{r+1} is a maximal torus. Over an algebraically closed field it is moreover maximal among reduced commutative closed subgroup schemes: a competing subgroup need not be a torus, or even connected.

The points of the closed subgroup TauCeti.SpecialLinear.diagonalTorusDefiningIdeal are exactly the points with diagonal matrix. Maximality is proved on algebraically closed points. A reduced commutative closed subgroup containing the diagonal torus has commutative point group containing all determinant-one diagonal matrices. Transported into the standard type A_r carrier, the maximality of its weight torus among commutative subgroups shows that every point of the subgroup is diagonal, and therefore already a point of the torus. Reduced finite-type point separation turns this equality of point groups into an equality of defining Hopf ideals, and maximality over an arbitrary field descends from an algebraic closure.

Main declarations

• TauCeti.SpecialLinear.quotientPointsSubgroup_diagonalTorusDefiningIdeal: the points of the diagonal torus are the range of the diagonal-torus point morphism.
• TauCeti.SpecialLinear.mem_quotientPointsSubgroup_diagonalTorusDefiningIdeal_iff: a point lies in the diagonal torus exactly when its matrix is diagonal.
• TauCeti.SpecialLinear.eq_diagonalTorusDefiningIdeal_of_le_of_isCocomm: over an algebraically closed field, no larger reduced commutative closed subgroup contains the diagonal torus.
• TauCeti.SpecialLinear.isMaximalTorus_diagonalTorusDefiningIdeal: the diagonal torus of SL_{r+1} is a maximal torus, over every field.

References

• J. S. Milne, Algebraic Groups (2017), Chapters 17 and 21.
• J. E. Humphreys, Linear Algebraic Groups (1975), §§15.3 and 26.3.
• The argument follows TauCeti.Algebra.AlgebraicGroup.GeneralLinear.DiagonalTorus.Maximal and TauCeti.Algebra.AlgebraicGroup.Symplectic.DiagonalTorus.Maximal.

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

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

@[simp]

theorem TauCeti.SpecialLinear.mem_quotientPointsSubgroup_diagonalTorusDefiningIdeal_iff (r : ℕ) (R : Type u) [CommRing R] (A : Type w) [CommRing A] [Algebra R A] (g : ↑(HopfAlgebra.points ↧A)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (coordinateHopfAlgebra R (r + 1)) (diagonalTorusDefiningIdeal r R) ↧A ↔ (↑(Matrix.SpecialLinearGroup.toGL ((pointsMulEquiv R (r + 1)) g))).IsDiag

Membership in the diagonal torus of SL_{r+1} on points. A point lies in the torus exactly when its matrix is diagonal.

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

The diagonal torus of SL_{r+1} 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 r k; commutativity is the cocommutativity of the quotient coordinate Hopf algebra.

theorem TauCeti.SpecialLinear.isMaximalTorus_diagonalTorusDefiningIdeal (r : ℕ) (k : Type u) [Field k] : HopfIdeal.IsMaximalTorus k (coordinateHopfAlgebra k (r + 1)) (diagonalTorusDefiningIdeal r k)

The diagonal torus of SL_{r+1} is a maximal torus over every field.