Existence of Borel subgroups

A Borel subgroup of an affine algebraic group over an algebraically closed field is a maximal smooth, geometrically connected, geometrically solvable closed subgroup. This file proves existence by maximizing Lie dimension. More precisely, every Borel candidate is contained in a maximal one. Applying this on the geometric fibre of a group over an arbitrary field constructs a Borel subgroup there.

The identity subgroup makes the family of candidates nonempty. For the relative statement, a candidate containing a prescribed one is again a nonempty family. Lie dimensions of closed subgroups are bounded by the ambient Lie dimension, and equality of Lie dimensions detects equality for an inclusion of smooth connected closed subgroups. This is exactly the general maximal-dimension argument in HopfIdeal.exists_minimal_of_smooth_of_connected.

The resulting Borel lives over the algebraic closure. It need not descend to the original field: the existence of a Borel defined over a non-algebraically-closed field is an additional condition on the group. No conjugacy statement is proved here.

Main declarations

• TauCeti.HopfIdeal.exists_minimal_isBorelCandidate_le: every Borel candidate is contained in a maximal Borel candidate.
• TauCeti.HopfIdeal.exists_minimal_isBorelCandidate: every finite-type affine group over a field has a maximal Borel candidate.
• TauCeti.HopfIdeal.exists_geometricBorel: the geometric fibre of every finite-type affine group has a Borel subgroup.
• TauCeti.HopfIdeal.torusCommHopfAlgProperty.isBorelCandidate: every torus is a Borel candidate.

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.IsSolvableRadicalCandidate.isBorelCandidate {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsSolvableRadicalCandidate H I) : IsBorelCandidate k H I

A solvable-radical candidate is in particular a Borel candidate after forgetting normality.

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

The identity subgroup is a Borel candidate.

theorem TauCeti.HopfIdeal.exists_minimal_isBorelCandidate_le {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) {I : HopfIdeal k ↑H.obj} (hI : IsBorelCandidate k H I) : ∃ J ≤ I, Minimal (IsBorelCandidate k H) J

Every smooth, geometrically connected, geometrically solvable closed subgroup is contained in a maximal one.

In Hopf-ideal order the inequality J ≤ I says that the closed subgroup cut out by J contains the one cut out by I. Thus the returned minimal Borel candidate is a maximal smooth, geometrically connected, geometrically solvable subgroup containing the prescribed candidate.

theorem TauCeti.HopfIdeal.exists_minimal_isBorelCandidate {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : ∃ (I : HopfIdeal k ↑H.obj), Minimal (IsBorelCandidate k H) I

Every finite-type affine group over a field has a maximal smooth geometrically connected geometrically solvable closed subgroup.

Over an algebraically closed field this is a Borel subgroup. Over a general field it is only maximal among candidates defined over that field; exists_geometricBorel below applies the result after extension to an algebraic closure.

theorem TauCeti.HopfIdeal.exists_geometricBorel {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : let K := AlgebraicClosure k; let H' := H.baseChange; ∃ (I : HopfIdeal K ↑H'.obj), IsBorelOverAlgClosed K H' I

The geometric fibre of every finite-type affine group has a Borel subgroup.

The conclusion is stated directly on the base-changed coordinate Hopf algebra. Since the base field there is algebraically closed, IsBorelOverAlgClosed is precisely minimality among smooth, geometrically connected, geometrically solvable closed subgroups.

theorem TauCeti.HopfIdeal.torusCommHopfAlgProperty.isBorelCandidate {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : torusCommHopfAlgProperty k (H.quotient I)) : IsBorelCandidate k H I

Every torus closed subgroup is a Borel candidate.