A Chevalley line in the weight-sum representation

Let N be a normal closed subgroup of a reduced affine group of finite type over an algebraically closed field. Chevalley's theorem realizes N as the stabilizer of a line in a finite-dimensional representation. That line lies in one character space of N, hence in the subrepresentation spanned by all its character spaces. Restricting to this subrepresentation preserves the line and its stabilizer over every commutative value algebra, including nonreduced ones.

The resulting representation is spanned by its N-weight spaces and contains a line whose stabilizer is exactly N. These are the inputs to the construction of a representation with kernel N, by conjugation on block-diagonal endomorphisms.

The construction uses HopfIdeal.exists_finite_subcomodule_exteriorPower_line_stabilizer and HopfIdeal.IsNormal.iSupWeightSpaceSubcomodule.

References

• J. E. Humphreys, Linear Algebraic Groups, §11.5.
• A. Borel, Linear Algebraic Groups, §5.5.

theorem TauCeti.HopfIdeal.IsNormal.exists_finite_weightSum_line_stabilizer {k : Type u} [Field k] [IsAlgClosed k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] [IsReduced ↑H] {I : HopfIdeal k ↑H} (hI : I.IsNormal) : ∃ (V : FGComoduleCat k ↑H), ⨆ (χ : GroupLike k (↑H ⧸ I.toIdeal)), I.weightSpace (↑V) χ = ⊤ ∧ ∃ (χ : GroupLike k (↑H ⧸ I.toIdeal)) (L : Submodule k ↑V), Module.finrank k ↥L = 1 ∧ L ≤ I.weightSpace (↑V) χ ∧ ∀ (A : CommAlgCat k) (g : ↑(HopfAlgebra.points A)), g ∈ CommHopfAlgCat.quotientPointsSubgroup H I A ↔ Submodule.map (Comodule.endOfPoint (↑V) g.ofConv) (Submodule.baseChange (↑A) L) = Submodule.baseChange (↑A) L

A normal closed subgroup is the stabilizer of a line in a finite-dimensional representation spanned by its subgroup weight spaces. The line lies in a single weight space, and the stabilizer equality holds over every commutative value algebra.