Building upper-triangular bases from weight vectors

Suppose every nonzero finite-dimensional comodule over a coalgebra has a nonzero weight vector with weight drawn from a prescribed set S, that is, a vector v with coaction v ↦ v ⊗ c for some c ∈ S. Repeatedly choose such a vector and pass to the quotient by its span. Induction on dimension, together with the extension basis from TauCeti.Algebra.Coalgebra.Comodule.Flag.Extension, gives a basis whose coefficient matrix is upper triangular with diagonal entries in S.

This is the formal induction step behind both Kolchin arguments in Layer 5 of the ReductiveGroups roadmap. Taking S = {1} recovers the unitriangular statement used for unipotent groups, where Kolchin's theorem supplies genuine fixed vectors; taking S to be the set of group-like elements gives the triangular statement Lie--Kolchin needs for solvable groups, where only eigenvectors are available and group-like elements survive on the diagonal. When C is the coordinate Hopf algebra of an affine group, these group-like elements are its diagonal characters.

Main declarations

• TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_diag_mem_of_weight_vectors: the induction, with the weights confined to a prescribed set.
• TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_weight_vectors: its group-like specialization, with group-like diagonal coefficients.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, §§2.4 and 6.3.

theorem TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_diag_mem_of_weight_vectors {k : Type u} {C : Type v} {M : Type w} [Field k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] (S : Set C) [FiniteDimensional k M] (hweight : ∀ (V : Type w) [inst : AddCommGroup V] [inst_1 : Module k V] [inst_2 : Comodule k C V] [FiniteDimensional k V] [Nontrivial V], ∃ (v : V) (c : C), v ≠ 0 ∧ c ∈ S ∧ coact v = v ⊗ₜ[k] c) : ∃ (n : ℕ) (b : Module.Basis (Fin n) k M), (coefficientMatrix b).IsUpperTriangular ∧ ∀ (i : Fin n), coefficientMatrix b i i ∈ S

If every nonzero finite-dimensional C-comodule has a nonzero weight vector whose weight lies in S, then every finite-dimensional C-comodule has a basis whose coefficient matrix is upper triangular with diagonal entries in S.

The hypothesis is deliberately uniform in the comodule: the induction applies it to successive quotients. The conclusion allows an arbitrary finite index n; the exhibited basis itself certifies that n is the dimension of M.

theorem TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_weight_vectors {k : Type u} {C : Type v} {M : Type w} [Field k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] [FiniteDimensional k M] (hweight : ∀ (V : Type w) [inst : AddCommGroup V] [inst_1 : Module k V] [inst_2 : Comodule k C V] [FiniteDimensional k V] [Nontrivial V], HasNonzeroWeightVector k C V) : ∃ (n : ℕ) (b : Module.Basis (Fin n) k M), (coefficientMatrix b).IsUpperTriangular ∧ ∀ (i : Fin n), IsGroupLikeElem k (coefficientMatrix b i i)

If every nonzero finite-dimensional C-comodule has a nonzero weight vector, then every finite-dimensional C-comodule has a basis whose coefficient matrix is upper triangular with group-like diagonal entries.