Existence of maximal tori

Every finite-type affine group over a field has a maximal torus, and more precisely every torus closed subgroup is contained in a maximal one. The argument is the standard dimension count: tori are smooth and connected, so a torus of maximal Lie dimension among those containing a given one cannot be enlarged.

Two ingredients make the count work. The identity subgroup, cut out by the augmentation ideal, is the rank-zero split torus, so the family of tori is never empty; for a group with no nontrivial torus the maximal torus obtained is the identity subgroup. And the Lie dimensions of closed subgroups are bounded by the Lie dimension of the ambient group, so a maximal-dimensional torus exists.

No conjugacy statement is proved here: even over an algebraically closed field, conjugacy of maximal tori is a separate theorem. Likewise, the maximal torus produced is maximal among tori defined over the ground field, which is a priori weaker than maximality after base change to an algebraic closure; comparing the two is again a separate theorem.

Main declarations

• TauCeti.HopfIdeal.torusCommHopfAlgProperty_quotient_augmentation: the identity subgroup of a finite-type affine group is a torus.
• TauCeti.HopfIdeal.exists_isMaximalTorus_le: every torus closed subgroup is contained in a maximal torus.
• TauCeti.HopfIdeal.exists_isMaximalTorus: every finite-type affine group over a field has a maximal torus.

References

• J. S. Milne, Algebraic Groups (2017), §17.a.
• A. Borel, Linear Algebraic Groups, 2nd ed. (1991), §8.4.
• T. A. Springer, Linear Algebraic Groups, §6.3.

theorem TauCeti.HopfIdeal.torusCommHopfAlgProperty_quotient_augmentation {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : torusCommHopfAlgProperty k (H.quotient (augmentation k ↑H.obj))

The identity subgroup of a finite-type affine group is a torus.

Contravariantly, the augmentation ideal cuts out the identity subgroup, and the quotient by it is the base field, the coordinate ring of the rank-zero split torus.

theorem TauCeti.HopfIdeal.exists_isMaximalTorus_le {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) {I : HopfIdeal k ↑H.obj} (hI : torusCommHopfAlgProperty k (H.quotient I)) : ∃ J ≤ I, IsMaximalTorus k H.obj J

Every torus closed subgroup is contained in a maximal torus.

Because Hopf ideals reverse inclusion of closed subgroups, the conclusion J ≤ I says that the maximal torus cut out by J contains the torus cut out by I.

theorem TauCeti.HopfIdeal.exists_isMaximalTorus {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : ∃ (J : HopfIdeal k ↑H.obj), IsMaximalTorus k H.obj J

Every finite-type affine group over a field has a maximal torus.

The identity subgroup is a torus, so the previous theorem applies to it. The maximal torus produced may well be the identity subgroup, for instance for a unipotent group.