Borel candidates under field extension

The three conditions defining a Borel candidate — smoothness, geometric connectedness and geometric solvability of the coordinate quotient — descend along field extensions. Consequently, a Borel subgroup over an arbitrary field, whose base change to an algebraic closure is a maximal Borel candidate, is in particular a Borel candidate over the ground field.

Each of the three conditions descends by its own mechanism. Smoothness descends along the faithfully flat field extension k → K, using Mathlib's Algebra.Smooth.of_smooth_tensorProduct_of_faithfullyFlat. Geometric connectedness and geometric solvability are stated in terms of geometric points, and are reflected by an arbitrary field extension. In all three cases the coordinate quotient of the base-changed ideal is identified with the base change of the coordinate quotient by CommHopfAlgCat.quotientBaseChangeIso.

Main declarations

• TauCeti.HopfIdeal.IsBorelCandidate.of_baseChange: Borel candidatehood descends along a field extension.
• TauCeti.HopfIdeal.IsBorel.isBorelCandidate: a Borel subgroup over an arbitrary field is a Borel candidate over that field.

References

• J. S. Milne, Algebraic Groups (2017), §§17.a and 1.h.
• A. Borel, Linear Algebraic Groups, 2nd ed. (1991), §11.21.

theorem TauCeti.HopfIdeal.IsBorelCandidate.of_baseChange {k K : Type u} [Field k] [Field K] [Algebra k K] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {I : HopfIdeal k ↑H} (hI : IsBorelCandidate K (FiniteTypeCommHopfAlgCat.baseChange { obj := H, property := ⋯ }) (CommHopfAlgCat.baseChangeHopfIdeal I)) : IsBorelCandidate k { obj := H, property := ⋯ } I

Borel candidatehood descends along a field extension.

theorem TauCeti.HopfIdeal.IsBorel.isBorelCandidate {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {I : HopfIdeal k ↑H} (hI : IsBorel k H I) : IsBorelCandidate k { obj := H, property := ⋯ } I

A Borel subgroup over an arbitrary field is a Borel candidate over that field: its quotient is smooth, geometrically connected, and geometrically solvable.