Conjugating diagonalizable subgroups of Sp₂ₘ into the diagonal torus

Over a field k, every diagonalizable closed subgroup of Sp₂ₘ is conjugate, by a rational point of Sp₂ₘ, into the paired 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 m).conjugate g ≤ I.

As a consequence, every split maximal torus of Sp₂ₘ 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.Symplectic.exists_conjugate_diagonalTorusDefiningIdeal_le: a diagonalizable closed subgroup of Sp₂ₘ is contained in a conjugate of the diagonal torus.
• TauCeti.Symplectic.exists_eq_conjugate_diagonalTorusDefiningIdeal_of_isMaximalTorus: a split maximal torus of Sp₂ₘ is a conjugate of the diagonal torus.
• TauCeti.Symplectic.exists_conjugate_eq_of_isMaximalTorus_of_split: any two split maximal tori of Sp₂ₘ over a field are conjugate.
• TauCeti.Symplectic.isMaximalTorus_iff_exists_eq_conjugate_diagonalTorusDefiningIdeal: over an algebraically closed field, the maximal tori are exactly those conjugates.
• TauCeti.Symplectic.exists_conjugate_eq_of_isMaximalTorus: any two maximal tori of Sp₂ₘ 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.
• The Hopf-ideal argument follows the general-linear and special-linear cases, TauCeti.GeneralLinear.exists_conjugate_diagonalTorusDefiningIdeal_le and TauCeti.SpecialLinear.exists_conjugate_diagonalTorusDefiningIdeal_le.

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

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

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

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

Any two split maximal tori of Sp₂ₘ over a field are conjugate by a rational point of Sp₂ₘ.

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

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

Any two maximal tori of Sp₂ₘ over an algebraically closed field are conjugate by a rational point of Sp₂ₘ.