Borel subgroups of SLₙ

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

The proof views the subgroup inside GLₙ, where the Lie--Kolchin argument TauCeti.GeneralLinear.exists_map_inv_mul_mul_map_mem_upperTriangularGroup supplies a rational matrix P triangularizing the generic point of the subgroup. Rescaling one column of P by the inverse of its determinant keeps it triangularizing and makes it a rational point of SLₙ.

The upper-triangular subgroup is smooth, geometrically connected, and has solvable geometric points, so it is a Borel candidate. Combined with the containment above, it is a Borel subgroup, the Borel subgroups of SLₙ over an algebraically closed field are exactly its conjugates, and any two of them are conjugate. Its defining ideal commutes with base change, so it is a Borel subgroup of SLₙ over every commutative ring, smooth over the base with Borel geometric fibers, and in particular a Borel subgroup over every field.

Main declarations

• TauCeti.SpecialLinear.UpperTriangular.exists_conjugate_definingHopfIdeal_le: a reduced, connected, solvable closed subgroup of SLₙ is contained in a conjugate of the upper-triangular subgroup.
• TauCeti.SpecialLinear.UpperTriangular.isBorelCandidate_definingHopfIdeal: the upper-triangular subgroup is smooth, geometrically connected, and geometrically solvable.
• TauCeti.SpecialLinear.UpperTriangular.isBorelOverAlgClosed_iff_exists_eq_conjugate: over an algebraically closed field, the Borel subgroups of SLₙ are exactly the conjugates of the upper-triangular subgroup.
• TauCeti.SpecialLinear.UpperTriangular.exists_conjugate_eq_of_isBorelOverAlgClosed: any two Borel subgroups of SLₙ over an algebraically closed field are conjugate.
• TauCeti.SpecialLinear.UpperTriangular.map_baseChangeHopfIdeal_definingHopfIdeal: the upper-triangular ideal commutes with base change.
• TauCeti.SpecialLinear.UpperTriangular.isBorelOver_definingHopfIdeal: the upper-triangular subgroup is a Borel subgroup of SLₙ over every commutative ring.
• TauCeti.SpecialLinear.UpperTriangular.isBorel_definingHopfIdeal: the upper-triangular subgroup is a Borel subgroup of SLₙ over every field.

References

• A. Borel, Linear Algebraic Groups, 2nd ed. (1991), Corollary 10.5 and Theorem 11.1.
• J. S. Milne, Algebraic Groups (2017), Theorem 16.30 and Section 17.a.
• The argument follows the general-linear case in TauCeti.Algebra.AlgebraicGroup.GeneralLinear.UpperTriangular.Borel.

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

Every reduced, connected, solvable closed subgroup of SLₙ is contained in a conjugate of the upper-triangular subgroup, over an algebraically closed field. The inequality of Hopf ideals reverses subgroup containment.

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

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

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

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

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

The Borel subgroups of SLₙ 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.SpecialLinear.UpperTriangular.exists_conjugate_eq_of_isBorelOverAlgClosed {k : Type u} [Field k] {n : ℕ} [IsAlgClosed k] {I J : HopfIdeal k ↑(SpecialLinear.coordinateHopfAlgebra k n)} (hI : HopfIdeal.IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k ↑(SpecialLinear.coordinateHopfAlgebra k n)) I) (hJ : HopfIdeal.IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k ↑(SpecialLinear.coordinateHopfAlgebra k n)) J) : ∃ (g : WithConv (↑(SpecialLinear.coordinateHopfAlgebra k n) →ₐ[k] k)), I.conjugate g = J

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

@[simp]

theorem TauCeti.SpecialLinear.UpperTriangular.map_baseChangeHopfIdeal_definingHopfIdeal (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) : (CommHopfAlgCat.baseChangeHopfIdeal (definingHopfIdeal R n)).map (CommHopfAlgCat.Hom.hom (coordinateHopfAlgebraBaseChangeIso R K n).hom) = definingHopfIdeal K n

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

theorem TauCeti.SpecialLinear.UpperTriangular.isBorelOver_definingHopfIdeal (R : Type u) [CommRing R] (n : ℕ) : HopfIdeal.IsBorelOver R (SpecialLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n)

The upper-triangular subgroup of SLₙ is a Borel subgroup over every commutative ring: it is smooth over the base, and on every geometric fiber it is the upper-triangular Borel subgroup of SLₙ.

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

The upper-triangular subgroup of SLₙ 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.