Scalar action of connected normal solvable subgroups #
A connected reduced solvable closed subgroup of a reduced connected affine group acts by scalars on each finite-dimensional simple rational representation, provided it is normal. Lie--Kolchin supplies a joint eigenvector for the subgroup. The ambient group's connectedness makes its joint weight space invariant, and simplicity makes that space the whole representation. This is the representation-theoretic step in eliminating solvable radicals of classical groups.
The proof combines Comodule.hasNonzeroWeightVector_of_isSolvable with
Comodule.normalWeightSubcomodule.
References #
- J. E. Humphreys, Linear Algebraic Groups, §§17.6 and 19.
- A. Borel, Linear Algebraic Groups, §10.5.
theorem
TauCeti.HopfIdeal.exists_basePointsRepresentation_eq_smul
{k : Type u_1}
{H : Type u_2}
{V : Type u_3}
[Field k]
[IsAlgClosed k]
[CommRing H]
[HopfAlgebra k H]
[Algebra.FiniteType k H]
[IsReduced H]
[ConnectedSpace (PrimeSpectrum H)]
[AddCommGroup V]
[Module k V]
[Comodule k H V]
[FiniteDimensional k V]
[Nontrivial V]
[IsSimpleOrder (Subcomodule k H V)]
(I : HopfIdeal k H)
(hI : I.IsNormal)
[IsReduced ↑(CommHopfAlgCat.quotient (↧H) I)]
[ConnectedSpace (PrimeSpectrum ↑(CommHopfAlgCat.quotient (↧H) I))]
[Group.IsSolvable (WithConv (↑(CommHopfAlgCat.quotient (↧H) I) →ₐ[k] k))]
(g : WithConv (↑(CommHopfAlgCat.quotient (↧H) I) →ₐ[k] k))
:
∃ (c : kˣ),
(Comodule.basePointsRepresentation V)
((AlgHom.mapDomain (CommHopfAlgCat.Hom.hom (CommHopfAlgCat.mkQuotient (↧H) I))) g) = ↑c • 1
A connected reduced normal solvable closed subgroup acts by scalars on a simple finite-dimensional rational representation of a reduced connected affine group.