Detecting a subgroup by endomorphisms preserving each character space

Suppose a representation is spanned by the character spaces of a closed subgroup, and the subgroup is the stabilizer of a line inside one character space. A point belongs to the subgroup if and only if it commutes with the scalar extensions of all endomorphisms preserving each character space.

The forward implication uses the subgroup's scalar action on each character space. For the reverse implication, independence of the character spaces supplies a projection onto the line preserving each character space. Commuting with its scalar extension forces the point to stabilize the line. All coefficient algebras are allowed, so the criterion detects scheme-theoretic subgroups, including nonreduced ones.

For the normal-subgroup kernel argument, the representation is the sum of the subgroup weight spaces containing a Chevalley line. This file proves the centralizer criterion from the spanning and line-stabilizer properties; it does not construct that representation or its line.

The character-space API is HopfIdeal.weightSpace; the linear-algebra argument is Submodule.map_baseChange_eq_of_forall_commute_familyInvariant.

References

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

theorem TauCeti.HopfIdeal.commute_baseChange_of_mem_quotientPointsSubgroup {R : Type u} [CommRing R] {H : CommHopfAlgCat R} (I : HopfIdeal R ↑H) (V : Type w) [AddCommMonoid V] [Module R V] [Comodule R (↑H) V] (hV : ⨆ (χ : GroupLike R (↑H ⧸ I.toIdeal)), I.weightSpace V χ = ⊤) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) (hg : g ∈ CommHopfAlgCat.quotientPointsSubgroup H I A) {p : Module.End R V} (hp : p ∈ Submodule.familyInvariant (I.weightSpace V)) : Commute (Comodule.endOfPoint V g.ofConv) (LinearMap.baseChange (↑A) p)

If subgroup character spaces span a representation, every subgroup point commutes with the scalar extensions of the endomorphisms preserving each character space. This assertion needs neither normality, finite type, reducedness, nor algebraic closure.

theorem TauCeti.HopfIdeal.mem_quotientPointsSubgroup_iff_forall_commute_familyInvariant_of_subspace_stabilizer {k : Type u} [Field k] {H : CommHopfAlgCat k} (I : HopfIdeal k ↑H) (V : Type w) [AddCommGroup V] [Module k V] [Comodule k (↑H) V] (hV : ⨆ (χ : GroupLike k (↑H ⧸ I.toIdeal)), I.weightSpace V χ = ⊤) (χ : GroupLike k (↑H ⧸ I.toIdeal)) (L : Submodule k V) (hL : L ≤ I.weightSpace V χ) (A : CommAlgCat k) (g : ↑(HopfAlgebra.points A)) (hstab : Submodule.map (Comodule.endOfPoint V g.ofConv) (Submodule.baseChange (↑A) L) = Submodule.baseChange (↑A) L → g ∈ CommHopfAlgCat.quotientPointsSubgroup H I A) : g ∈ CommHopfAlgCat.quotientPointsSubgroup H I A ↔ ∀ p ∈ Submodule.familyInvariant (I.weightSpace V), Commute (Comodule.endOfPoint V g.ofConv) (LinearMap.baseChange (↑A) p)

A subgroup that stabilizes a subspace inside one character space of a representation spanned by its character spaces is detected by centralizing the endomorphisms preserving each character space, over the whole coefficient algebra. The implication from stabilizing the subspace to subgroup membership is an explicit input.