Trigonalizing the representations of a commutative affine group

Let H be a reduced finite-type commutative Hopf algebra over an algebraically closed field k. If the points of H act on a finite-dimensional comodule by pairwise-commuting operators, that comodule has a nonzero weight vector: a joint eigenvector of the commuting operators spans a point-stable line, and point separation promotes that line to a subcomodule, whose weight is automatically a character.

Feeding this into the flag induction of TauCeti.Algebra.Coalgebra.Comodule.Flag.Triangular trigonalizes every finite-dimensional representation of a commutative affine group: over a cocommutative H the convolution group of points is commutative, so the hypothesis holds for every comodule at once.

This is the base case of the Lie--Kolchin induction, which reduces a connected solvable group to its commutative quotient by the derived subgroup. The induction step, which is where connectedness enters, is not proved here.

Main declarations

• TauCeti.Comodule.hasNonzeroWeightVector_of_basePointsRepresentation_stable: a nonzero vector spanning a point-stable line is a weight vector.
• TauCeti.Comodule.hasNonzeroWeightVector_of_pairwise_commute: commuting point actions produce a weight vector.
• TauCeti.Comodule.hasNonzeroWeightVector_of_isCocomm: every nonzero finite-dimensional representation of a commutative affine group has a weight vector.
• TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_isCocomm: every finite-dimensional representation of a commutative affine group has an upper-triangular basis with group-like diagonal.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, Theorem 6.3.1, whose commutative case is proved here.
• A. Borel, Linear Algebraic Groups, §10.5.

This advances the "Lie--Kolchin; solvable groups" milestone in Layer 5 of the ReductiveGroups roadmap.

theorem TauCeti.Comodule.hasNonzeroWeightVector_of_basePointsRepresentation_stable {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] (p : Submodule k M) (v : M) (hv : v ≠ 0) (hspan : p = k ∙ v) (hact : ∀ (g : WithConv (H →ₐ[k] k)) {m : M}, m ∈ p → ((basePointsRepresentation M) g) m ∈ p) : HasNonzeroWeightVector k H M

A nonzero vector spanning a submodule preserved by every base-valued point is a weight vector.

theorem TauCeti.Comodule.hasNonzeroWeightVector_of_pairwise_commute {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] [FiniteDimensional k M] [Nontrivial M] (hcomm : Pairwise fun (g h : WithConv (H →ₐ[k] k)) => Commute ((basePointsRepresentation M) g) ((basePointsRepresentation M) h)) : HasNonzeroWeightVector k H M

If the base-valued points of a reduced finite-type commutative Hopf algebra over an algebraically closed field act on a nonzero finite-dimensional comodule by pairwise-commuting operators, then that comodule has a nonzero weight vector.

theorem TauCeti.Comodule.hasNonzeroWeightVector_of_isCocomm {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] [FiniteDimensional k M] [Nontrivial M] : HasNonzeroWeightVector k H M

Every nonzero finite-dimensional representation of a commutative affine group, reduced and of finite type over an algebraically closed field, has a nonzero weight vector.

theorem TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_isCocomm {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] [FiniteDimensional k M] : ∃ (n : ℕ) (b : Module.Basis (Fin n) k M), (coefficientMatrix b).IsUpperTriangular ∧ ∀ (i : Fin n), IsGroupLikeElem k (coefficientMatrix b i i)

Every finite-dimensional representation of a commutative affine group is trigonalizable. For a reduced finite-type cocommutative Hopf algebra over an algebraically closed field, every finite-dimensional comodule has a basis whose coefficient matrix is upper triangular with group-like diagonal entries: the group acts by upper-triangular matrices whose diagonal entries are characters.