Tori contained in Borel subgroups

Every torus in a finite-type affine group over an algebraically closed field is contained in a Borel subgroup. The coordinate-ring order is contravariant: if I defines the torus and J defines the Borel, containment is the inequality J ≤ I.

Over an arbitrary field, a Borel containing a given torus need not descend to the ground field. The geometric form therefore base-changes both the ambient group and the torus ideal to an algebraic closure, then constructs a Borel there.

Main declarations

• TauCeti.HopfIdeal.exists_isBorelOverAlgClosed_le_of_torus: every torus over an algebraically closed field is contained in a Borel subgroup.
• TauCeti.HopfIdeal.IsMaximalTorus.exists_isBorelOverAlgClosed_le: every maximal torus over an algebraically closed field is contained in a Borel subgroup.
• TauCeti.HopfIdeal.exists_geometricBorel_le_baseChangeHopfIdeal_of_torus: after passage to an algebraic closure, every torus is contained in a Borel subgroup of the geometric fibre.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 17.6 and §17.a.
• A. Borel, Linear Algebraic Groups, 2nd ed. (1991), §11.1.
• T. A. Springer, Linear Algebraic Groups, §6.2.

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

Every torus over an algebraically closed field is contained in a Borel subgroup.

In Hopf-ideal order, J ≤ I means that the closed subgroup cut out by J contains the torus cut out by I.

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

Every maximal torus over an algebraically closed field is contained in a Borel subgroup.

theorem TauCeti.HopfIdeal.exists_geometricBorel_le_baseChangeHopfIdeal_of_torus {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) {I : HopfIdeal k ↑H.obj} (hI : torusCommHopfAlgProperty k (H.quotient I)) : let K := AlgebraicClosure k; let H' := H.baseChange; have I' := CommHopfAlgCat.baseChangeHopfIdeal I; ∃ J ≤ I', IsBorelOverAlgClosed K H' J

After passage to an algebraic closure, every torus is contained in a Borel subgroup.

The returned ideal is a Borel subgroup of the geometric fibre and contains the base change of the given torus. No descent of that Borel to the ground field is asserted.