Conjugating diagonalizable subgroups of SL_{r+1} into the diagonal torus

Over a field k, every diagonalizable closed subgroup of SL_{r+1} is conjugate, by a rational point of SL_{r+1}, into the diagonal torus. In Hopf coordinates, a closed subgroup is diagonalizable when the group-like elements span its quotient coordinate Hopf algebra, and containment is reversed: the conclusion reads (diagonalTorusDefiningIdeal r k).conjugate g ≤ I.

The proof views the subgroup inside GL_{r+1}. The general-linear argument TauCeti.GeneralLinear.exists_mul_map_eq_map_mul_diagGL supplies a rational matrix P whose columns are weight vectors, so that the generic point M of the subgroup satisfies M P = P diag(t). Rescaling the first column of P by (det P)⁻¹ keeps it a matrix of weight vectors and makes its determinant one, so the conjugating matrix is a rational point of SL_{r+1}. After conjugation the generic point is diagonal, which is membership in the diagonal torus of SL_{r+1} on points.

As a consequence, every split maximal torus of SL_{r+1} is conjugate to the diagonal torus, and any two split maximal tori are conjugate over the base field. Over an algebraically closed field every torus is split, so the maximal tori are exactly the conjugates of the diagonal torus, and any two maximal tori are conjugate.

Main declarations

• TauCeti.SpecialLinear.exists_conjugate_diagonalTorusDefiningIdeal_le: a diagonalizable closed subgroup of SL_{r+1} is contained in a conjugate of the diagonal torus.
• TauCeti.SpecialLinear.exists_eq_conjugate_diagonalTorusDefiningIdeal_of_isMaximalTorus: a split maximal torus of SL_{r+1} is a conjugate of the diagonal torus.
• TauCeti.SpecialLinear.exists_conjugate_eq_of_isMaximalTorus_of_split: any two split maximal tori of SL_{r+1} over a field are conjugate.
• TauCeti.SpecialLinear.isMaximalTorus_iff_exists_eq_conjugate_diagonalTorusDefiningIdeal: over an algebraically closed field, the maximal tori are exactly those conjugates.
• TauCeti.SpecialLinear.exists_conjugate_eq_of_isMaximalTorus: any two maximal tori of SL_{r+1} over an algebraically closed field are conjugate.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 12.12 and Section 17.a.
• A. Borel, Linear Algebraic Groups, 2nd ed. (1991), Proposition 8.4.

theorem TauCeti.SpecialLinear.exists_conjugate_diagonalTorusDefiningIdeal_le {k : Type u} [Field k] {r : ℕ} (I : HopfIdeal k ↑(coordinateHopfAlgebra k (r + 1))) (hI : DiagonalizableGroup.groupLikeSpannedProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := coordinateHopfAlgebra k (r + 1), property := ⋯ } I)) : ∃ (g : WithConv (↑(coordinateHopfAlgebra k (r + 1)) →ₐ[k] k)), (diagonalTorusDefiningIdeal r k).conjugate g ≤ I

A diagonalizable closed subgroup of SL_{r+1} is conjugate into the diagonal torus.

If the quotient coordinate Hopf algebra of I is spanned by its group-like elements, then some rational point g of SL_{r+1} conjugates the diagonal torus to a closed subgroup containing the one cut out by I. Containment of closed subgroups is the reversed inequality of Hopf ideals.

theorem TauCeti.SpecialLinear.exists_eq_conjugate_diagonalTorusDefiningIdeal_of_isMaximalTorus {k : Type u} [Field k] {r : ℕ} {I : HopfIdeal k ↑(coordinateHopfAlgebra k (r + 1))} (hI : HopfIdeal.IsMaximalTorus k (coordinateHopfAlgebra k (r + 1)) I) (hsplit : splitTorusCommHopfAlgProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := coordinateHopfAlgebra k (r + 1), property := ⋯ } I)) : ∃ (g : WithConv (↑(coordinateHopfAlgebra k (r + 1)) →ₐ[k] k)), I = (diagonalTorusDefiningIdeal r k).conjugate g

Split maximal tori of SL_{r+1} are conjugate to the diagonal torus. A maximal torus of SL_{r+1} over k which is split over k is the conjugate of the diagonal torus by a rational point.

theorem TauCeti.SpecialLinear.exists_conjugate_eq_of_isMaximalTorus_of_split {k : Type u} [Field k] {r : ℕ} {I J : HopfIdeal k ↑(coordinateHopfAlgebra k (r + 1))} (hI : HopfIdeal.IsMaximalTorus k (coordinateHopfAlgebra k (r + 1)) I) (hJ : HopfIdeal.IsMaximalTorus k (coordinateHopfAlgebra k (r + 1)) J) (hsplitI : splitTorusCommHopfAlgProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := coordinateHopfAlgebra k (r + 1), property := ⋯ } I)) (hsplitJ : splitTorusCommHopfAlgProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := coordinateHopfAlgebra k (r + 1), property := ⋯ } J)) : ∃ (g : WithConv (↑(coordinateHopfAlgebra k (r + 1)) →ₐ[k] k)), I.conjugate g = J

Any two split maximal tori of SL_{r+1} over a field are conjugate by a rational point of SL_{r+1}.

theorem TauCeti.SpecialLinear.isMaximalTorus_iff_exists_eq_conjugate_diagonalTorusDefiningIdeal {k : Type u} [Field k] {r : ℕ} [IsAlgClosed k] (I : HopfIdeal k ↑(coordinateHopfAlgebra k (r + 1))) : HopfIdeal.IsMaximalTorus k (coordinateHopfAlgebra k (r + 1)) I ↔ ∃ (g : WithConv (↑(coordinateHopfAlgebra k (r + 1)) →ₐ[k] k)), I = (diagonalTorusDefiningIdeal r k).conjugate g

Maximal tori of SL_{r+1} over an algebraically closed field are exactly the conjugates of the diagonal torus. The equality is an equality of defining Hopf ideals, hence of closed subgroup schemes, rather than only of their rational points.

theorem TauCeti.SpecialLinear.exists_conjugate_eq_of_isMaximalTorus {k : Type u} [Field k] {r : ℕ} [IsAlgClosed k] {I J : HopfIdeal k ↑(coordinateHopfAlgebra k (r + 1))} (hI : HopfIdeal.IsMaximalTorus k (coordinateHopfAlgebra k (r + 1)) I) (hJ : HopfIdeal.IsMaximalTorus k (coordinateHopfAlgebra k (r + 1)) J) : ∃ (g : WithConv (↑(coordinateHopfAlgebra k (r + 1)) →ₐ[k] k)), I.conjugate g = J

Any two maximal tori of SL_{r+1} over an algebraically closed field are conjugate by a rational point of SL_{r+1}.