Borel subgroups of GLₙ

Over an algebraically closed field k, every smooth (indeed every reduced), connected, solvable closed subgroup of GLₙ is conjugate, by a rational point, into the upper-triangular subgroup. In Hopf coordinates containment of closed subgroups is reversed, so the conclusion reads (UpperTriangular.definingHopfIdeal k n).conjugate g ≤ I.

The proof restricts the standard representation of GLₙ to the subgroup and applies the Lie--Kolchin theorem: the restricted comodule has a basis b in which its coefficient matrix C is upper triangular. If P is the matrix with columns bⱼ and M is the generic point of the subgroup, the change of basis formula for the action of M on kⁿ reads P⁻¹ M P = C. Hence conjugating the generic point by P⁻¹ lands in the upper-triangular subgroup, which is the inclusion of closed subgroups to be proved.

Since the upper-triangular subgroup is itself smooth, connected, and solvable, the generic conjugacy results for Borel subgroups then show that it is a Borel subgroup, that the Borel subgroups of GLₙ over an algebraically closed field are exactly its conjugates, and that any two of them are conjugate. Base change to an algebraic closure shows that the upper-triangular subgroup is a Borel subgroup of GLₙ over every field.

Main declarations

• TauCeti.GeneralLinear.exists_map_inv_mul_mul_map_mem_upperTriangularGroup: a point of GLₙ with values in the coordinate algebra of a reduced connected solvable group is triangularized by a rational matrix.
• TauCeti.GeneralLinear.UpperTriangular.exists_conjugate_definingHopfIdeal_le: a reduced, connected, solvable closed subgroup of GLₙ is contained in a conjugate of the upper-triangular subgroup.
• TauCeti.GeneralLinear.UpperTriangular.isBorelOverAlgClosed_definingHopfIdeal and TauCeti.GeneralLinear.UpperTriangular.isBorel_definingHopfIdeal: the upper-triangular subgroup is a Borel subgroup of GLₙ, over an algebraically closed field and over every field.
• TauCeti.GeneralLinear.UpperTriangular.isBorelOverAlgClosed_iff_exists_eq_conjugate: over an algebraically closed field, the Borel subgroups of GLₙ are exactly the conjugates of the upper-triangular subgroup.
• TauCeti.GeneralLinear.UpperTriangular.exists_conjugate_eq_of_isBorelOverAlgClosed: any two Borel subgroups of GLₙ over an algebraically closed field are conjugate.
• TauCeti.GeneralLinear.UpperTriangular.map_baseChangeHopfIdeal_definingHopfIdeal: scalar extension preserves the upper-triangular defining ideal under the coordinate isomorphism.

References

• A. Borel, Linear Algebraic Groups, 2nd ed. (1991), Corollary 10.5 and Theorem 11.1.
• J. E. Humphreys, Linear Algebraic Groups, Sections 17.6 and 21.3.
• J. S. Milne, Algebraic Groups (2017), Theorem 16.30 and Section 17.a.
• TauCeti/Algebra/AlgebraicGroup/GeneralLinear/DiagonalTorus/Conjugacy.lean, for the analogous Hopf-coordinate proof of conjugacy in GLₙ.

theorem TauCeti.GeneralLinear.exists_map_inv_mul_mul_map_mem_upperTriangularGroup {k : Type u} [Field k] {n : ℕ} [IsAlgClosed k] {Q : Type v} [CommRing Q] [HopfAlgebra k Q] [Algebra.FiniteType k Q] [IsReduced Q] (hconn : geometricallyConnectedCommHopfAlgProperty k ↧Q) (hsolv : geometricallySolvablePointsCommHopfAlgProperty k ↧Q) (π : ↑(coordinateHopfAlgebra k n) →ₐc[k] Q) : ∃ (P : GL (Fin n) k), (Matrix.GeneralLinearGroup.map (algebraMap k Q)) P⁻¹ * (pointsMulEquiv n) (WithConv.toConv ↑π) * (Matrix.GeneralLinearGroup.map (algebraMap k Q)) P ∈ upperTriangularGroup (Fin n) Q

Lie--Kolchin for GLₙ-valued points.

Let Q be the coordinate algebra of a reduced, geometrically connected, geometrically solvable affine group of finite type over an algebraically closed field k. For every bialgebra morphism π : O(GLₙ) → Q some rational matrix P triangularizes the Q-valued point π: the matrix P⁻¹ π P is upper triangular. The columns of P form a Lie--Kolchin basis of the standard comodule corestricted along π.

theorem TauCeti.GeneralLinear.UpperTriangular.exists_conjugate_definingHopfIdeal_le {k : Type u} [Field k] {n : ℕ} [IsAlgClosed k] (I : HopfIdeal k ↑(GeneralLinear.coordinateHopfAlgebra k n)) [IsReduced ↑(CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra k n) I)] (hconn : geometricallyConnectedCommHopfAlgProperty k (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra k n) I)) (hsolv : geometricallySolvablePointsCommHopfAlgProperty k (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra k n) I)) : ∃ (g : WithConv (↑(GeneralLinear.coordinateHopfAlgebra k n) →ₐ[k] k)), (definingHopfIdeal k n).conjugate g ≤ I

A reduced connected solvable closed subgroup of GLₙ is conjugate into the upper-triangular subgroup.

Over an algebraically closed field, if the quotient coordinate Hopf algebra of I is reduced, geometrically connected, and geometrically solvable, then some rational point g conjugates the upper-triangular subgroup to a closed subgroup containing the one cut out by I. Containment of closed subgroups is the reversed inequality of Hopf ideals.

theorem TauCeti.GeneralLinear.UpperTriangular.isBorelCandidate_definingHopfIdeal (k : Type u) [Field k] (n : ℕ) : HopfIdeal.IsBorelCandidate k (FiniteTypeCommHopfAlgCat.of k ↑(GeneralLinear.coordinateHopfAlgebra k n)) (definingHopfIdeal k n)

The upper-triangular subgroup of GLₙ is a Borel candidate over every field: it is smooth, geometrically connected, and geometrically solvable.

theorem TauCeti.GeneralLinear.UpperTriangular.isBorelOverAlgClosed_definingHopfIdeal (k : Type u) [Field k] (n : ℕ) [IsAlgClosed k] : HopfIdeal.IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k ↑(GeneralLinear.coordinateHopfAlgebra k n)) (definingHopfIdeal k n)

The upper-triangular subgroup of GLₙ is a Borel subgroup over an algebraically closed field: it is maximal among smooth, connected, solvable closed subgroups.

theorem TauCeti.GeneralLinear.UpperTriangular.isBorelOverAlgClosed_iff_exists_eq_conjugate {k : Type u} [Field k] {n : ℕ} [IsAlgClosed k] (I : HopfIdeal k ↑(GeneralLinear.coordinateHopfAlgebra k n)) : HopfIdeal.IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k ↑(GeneralLinear.coordinateHopfAlgebra k n)) I ↔ ∃ (g : WithConv (↑(GeneralLinear.coordinateHopfAlgebra k n) →ₐ[k] k)), I = (definingHopfIdeal k n).conjugate g

The Borel subgroups of GLₙ over an algebraically closed field are exactly the conjugates of the upper-triangular subgroup. The equality is an equality of defining Hopf ideals, hence of closed subgroup schemes, rather than only of their rational points.

theorem TauCeti.GeneralLinear.UpperTriangular.exists_conjugate_eq_of_isBorelOverAlgClosed {k : Type u} [Field k] {n : ℕ} [IsAlgClosed k] {I J : HopfIdeal k ↑(GeneralLinear.coordinateHopfAlgebra k n)} (hI : HopfIdeal.IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k ↑(GeneralLinear.coordinateHopfAlgebra k n)) I) (hJ : HopfIdeal.IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k ↑(GeneralLinear.coordinateHopfAlgebra k n)) J) : ∃ (g : WithConv (↑(GeneralLinear.coordinateHopfAlgebra k n) →ₐ[k] k)), I.conjugate g = J

Any two Borel subgroups of GLₙ over an algebraically closed field are conjugate by a rational point of GLₙ.

@[simp]

theorem TauCeti.GeneralLinear.UpperTriangular.map_baseChangeHopfIdeal_definingHopfIdeal {n : ℕ} (k K : Type u) [Field k] [Field K] [Algebra k K] : (CommHopfAlgCat.baseChangeHopfIdeal (definingHopfIdeal k n)).map (CommHopfAlgCat.Hom.hom (coordinateHopfAlgebraBaseChangeIso k K n).hom) = definingHopfIdeal K n

The general-linear base-change isomorphism carries the scalar extension of the upper-triangular defining ideal to the upper-triangular defining ideal over the new field.

theorem TauCeti.GeneralLinear.UpperTriangular.isBorel_definingHopfIdeal (k : Type u) [Field k] (n : ℕ) : HopfIdeal.IsBorel k (GeneralLinear.coordinateHopfAlgebra k n) (definingHopfIdeal k n)

The upper-triangular subgroup of GLₙ is a Borel subgroup over every field. Its base change to an algebraic closure is smooth, connected, solvable, and maximal among closed subgroups with those properties.