The subgroup character of a Chevalley line

Every closed subgroup with finitely generated defining ideal is the stabilizer of a line in an exterior power of a finite regular subcomodule. The line is a subrepresentation after restriction to the subgroup, so the subgroup acts on it by a unique character. Here characters are group-like elements of the quotient coordinate Hopf algebra; no reducedness, smoothness, or algebraic closure is needed.

The character places the Chevalley line inside the sum of the subgroup's weight spaces. For a normal subgroup this sum is an ambient subrepresentation under the hypotheses of HopfIdeal.IsNormal.iSupWeightSpaceSubcomodule. Its block-diagonal endomorphisms are the next representation used to realize the normal subgroup as a kernel.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 4.27 and Lemma 4.28.
• J. E. Humphreys, Linear Algebraic Groups, §11.5.

The exterior-line construction uses Subcomodule.exists_line_corestrict_exteriorPower and HopfIdeal.definingSubcomodule; its stabilizer is detected by HopfIdeal.mem_quotientPointsSubgroup_iff_map_baseChange_range_exteriorPowerMap_eq.

theorem TauCeti.HopfIdeal.existsUnique_topExteriorLine_le_weightSpace {k : Type u} [Field k] {H : CommHopfAlgCat k} (I : HopfIdeal k ↑H) (V : Subcomodule k ↑H ↑H) (hW : Module.Finite k ↥(I.definingSubspace V)) : ∃! χ : GroupLike k (↑H ⧸ I.toIdeal), (exteriorPower.map (Module.finrank k ↥(I.definingSubspace V)) (I.definingSubspace V).subtype).range ≤ I.weightSpace (↥(⋀[k]^(Module.finrank k ↥(I.definingSubspace V)) ↥V)) χ

The top exterior line of the defining subspace of a closed subgroup transforms by a unique character of that subgroup. Only the defining subspace must be finite-dimensional.

theorem TauCeti.HopfIdeal.exists_finite_subcomodule_exteriorPower_line_stabilizer {k : Type u} [Field k] {H : CommHopfAlgCat k} (I : HopfIdeal k ↑H) (hI : I.toIdeal.FG) : ∃ (V : Subcomodule k ↑H ↑H) (n : ℕ), Module.Finite k ↥V.toSubmodule ∧ let this := Module.addCommMonoidToAddCommGroup k; ∃ (L : Submodule k ↥(⋀[k]^n ↥V)), Module.finrank k ↥L = 1 ∧ (∃! χ : GroupLike k (↑H ⧸ I.toIdeal), L ≤ I.weightSpace (↥(⋀[k]^n ↥V)) χ) ∧ ∀ (A : CommAlgCat k) (g : ↑(HopfAlgebra.points A)), g ∈ CommHopfAlgCat.quotientPointsSubgroup H I A ↔ Submodule.map (Comodule.endOfPoint (↥(⋀[k]^n ↥V)) g.ofConv) (Submodule.baseChange (↑A) L) = Submodule.baseChange (↑A) L

Chevalley's theorem with the subgroup character. A closed subgroup with finitely generated defining ideal is the stabilizer, over every commutative value algebra, of a line in a finite-dimensional exterior-power representation. The line lies in the weight space of a unique character of the subgroup, including when the subgroup is nonreduced.