Upper triangular embeddings from weight vectors

If every nonzero finite-dimensional representation of an affine group has a weight vector, then a finite-type group embeds as a closed subgroup of an upper triangular general linear group. A finite-dimensional subcomodule of the regular comodule generates the coordinate algebra by its coefficients. The weight-vector hypothesis triangularizes this comodule, so its faithful coordinate morphism factors through the upper triangular quotient.

This combines Comodule.exists_finite_subcomodule_matrixCoefficientSubalgebra_eq_top with Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_weight_vectors. It applies both to Lie--Kolchin triangularization and to triangularization of the differentiated action.

References

• J. S. Milne, Algebraic Groups (2017), Chapters 4 and 16.

theorem TauCeti.exists_upperTriangular_surjective_of_weight_vectors {k : Type u} [Field k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] (hweight : ∀ (V : Type u) [inst : AddCommGroup V] [inst_1 : Module k V] [inst_2 : Comodule k H V] [FiniteDimensional k V] [Nontrivial V], Comodule.HasNonzeroWeightVector k H V) : ∃ (n : ℕ) (f : GeneralLinear.UpperTriangular.coordinateHopfAlgebra k n ⟶ ↧H), Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)

If every nonzero finite-dimensional comodule has a weight vector, the represented finite-type affine group is a closed subgroup of some upper triangular general linear group. The surjection runs in the contravariant coordinate direction.