Conjugating diagonalizable subgroups of GLₙ into the diagonal torus

Over a field k, every diagonalizable closed subgroup of GLₙ is conjugate, by a rational point, 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 k n).conjugate g ≤ I.

The proof restricts the standard representation of GLₙ to the subgroup. The restricted comodule is spanned by weight vectors, so kⁿ has a basis w of weight vectors with weights χⱼ. If P is the matrix with columns wⱼ and M is the generic point of the subgroup, the weight equations say M P = P diag(χ). Hence conjugating the generic point by P⁻¹ lands in the diagonal torus, which is the inclusion of closed subgroups to be proved.

As a consequence, every split maximal torus of GLₙ 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.GeneralLinear.exists_mul_map_eq_map_mul_diagGL: a point of GLₙ with values in a Hopf algebra spanned by its group-like elements is diagonalized by a rational matrix.
• TauCeti.GeneralLinear.exists_conjugate_diagonalTorusDefiningIdeal_le: a diagonalizable closed subgroup of GLₙ is contained in a conjugate of the diagonal torus.
• TauCeti.GeneralLinear.exists_eq_conjugate_diagonalTorusDefiningIdeal_of_isMaximalTorus: a split maximal torus of GLₙ is a conjugate of the diagonal torus.
• TauCeti.GeneralLinear.exists_conjugate_eq_of_isMaximalTorus_of_split: any two split maximal tori of GLₙ over a field are conjugate.
• TauCeti.GeneralLinear.isMaximalTorus_iff_exists_eq_conjugate_diagonalTorusDefiningIdeal: over an algebraically closed field, the maximal tori are exactly those conjugates.
• TauCeti.GeneralLinear.exists_conjugate_eq_of_isMaximalTorus: any two maximal tori of GLₙ 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.GeneralLinear.exists_mul_map_eq_map_mul_diagGL {k : Type u} [Field k] {n : ℕ} {Q : Type u} [CommRing Q] [HopfAlgebra k Q] (hQ : Subcoalgebra.groupLikeSetSpan Set.univ = ⊤) (π : ↑(coordinateHopfAlgebra k n) →ₐc[k] Q) : ∃ (P : GL (Fin n) k) (t : Fin n → Qˣ), (pointsMulEquiv n) (WithConv.toConv ↑π) * (Matrix.GeneralLinearGroup.map (algebraMap k Q)) P = (Matrix.GeneralLinearGroup.map (algebraMap k Q)) P * diagGL t

Simultaneous diagonalization over a diagonalizable Hopf algebra.

If the group-like elements of Q span it, then for every bialgebra morphism π : O(GLₙ) → Q some rational matrix P diagonalizes the Q-valued point π: π P = P diag(t). The columns of P are weight vectors of the standard comodule corestricted along π, and the entries of t are their weights.

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

A diagonalizable closed subgroup of GLₙ 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 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.GeneralLinear.exists_eq_conjugate_diagonalTorusDefiningIdeal_of_isMaximalTorus {k : Type u} [Field k] {n : ℕ} {I : HopfIdeal k ↑(coordinateHopfAlgebra k n)} (hI : HopfIdeal.IsMaximalTorus k (coordinateHopfAlgebra k n) I) (hsplit : splitTorusCommHopfAlgProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := coordinateHopfAlgebra k n, property := ⋯ } I)) : ∃ (g : WithConv (↑(coordinateHopfAlgebra k n) →ₐ[k] k)), I = (diagonalTorusDefiningIdeal k n).conjugate g

Split maximal tori of GLₙ are conjugate to the diagonal torus. A maximal torus of GLₙ over k which is split over k is the conjugate of the diagonal torus by a rational point.

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

Any two split maximal tori of GLₙ over a field are conjugate by a rational point of GLₙ.

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

Maximal tori of GLₙ 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.GeneralLinear.exists_conjugate_eq_of_isMaximalTorus {k : Type u} [Field k] {n : ℕ} [IsAlgClosed k] {I J : HopfIdeal k ↑(coordinateHopfAlgebra k n)} (hI : HopfIdeal.IsMaximalTorus k (coordinateHopfAlgebra k n) I) (hJ : HopfIdeal.IsMaximalTorus k (coordinateHopfAlgebra k n) J) : ∃ (g : WithConv (↑(coordinateHopfAlgebra k n) →ₐ[k] k)), I.conjugate g = J

Any two maximal tori of GLₙ over an algebraically closed field are conjugate by a rational point of GLₙ.