The Lie--Kolchin theorem

Let H be the coordinate Hopf algebra of a reduced affine group of finite type over an algebraically closed field. This file proves the Lie--Kolchin theorem: if H has connected spectrum and its group of rational points is solvable, then every nonzero finite-dimensional H-comodule has a weight vector, and every finite-dimensional comodule is upper triangularizable with characters on the diagonal.

The file first proves the representation-theoretic reduction to the derived subgroup: if the derived closed subgroup has only unipotent points, the same conclusions hold. The abstract argument applies to a representation ρ and a normal subgroup N containing the commutator subgroup. Kolchin gives a nonzero vector fixed by N. The whole group preserves the space of N-fixed vectors, and its action there factors through the commutative quotient G/N. Simultaneous triangularization of commuting operators then gives a common eigenvector. For an affine group, take N to be the points of the scheme-theoretic derived subgroup. Point separation promotes the resulting point-stable eigenline to a one-dimensional subcomodule.

For a connected group, a nonzero joint weight of the abstract commutator subgroup also supplies an ambient weight vector: the joint weight is trivial, so the action on its weight space factors through a commutative quotient. The Lie--Kolchin theorem follows by induction on the derived length of the group of rational points. The derived closed subgroup of a reduced connected group is again reduced and connected, and its rational points have strictly smaller derived length (TauCeti.CommHopfAlgCat.derivedSeries_points_derived_eq_bot). A weight vector for the derived subgroup, supplied by induction, is a joint eigenvector of the abstract commutator subgroup, and hence yields an ambient weight vector.

Main declarations

• TauCeti.Comodule.hasNonzeroWeightVector_of_nonzeroJointWeight_commutator: a commutator joint weight supplies an ambient weight vector for a connected group.
• TauCeti.Comodule.hasNonzeroWeightVector_of_forall_isUnipotentPoint_derived: unipotence of the derived subgroup supplies a weight vector in every nonzero finite-dimensional comodule.
• TauCeti.Comodule.hasNonzeroWeightVector_of_geometricallyUnipotent_derived: the same conclusion phrased using the geometric-unipotence object property.
• exists_basis_coefficientMatrix_isUpperTriangular_of_forall_isUnipotentPoint_derived: the resulting Lie--Kolchin upper-triangular basis.
• exists_basis_coefficientMatrix_isUpperTriangular_of_geometricallyUnipotent_derived: the geometric-unipotence formulation of that basis theorem.
• TauCeti.Comodule.hasNonzeroWeightVector_of_isSolvable: every nonzero finite-dimensional representation of a connected solvable group has a weight vector.
• TauCeti.Comodule.hasNonzeroWeightVector_of_geometricallySolvable: the same conclusion stated with the geometric connectedness and solvability object properties.
• TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_isSolvable: the Lie--Kolchin theorem, every finite-dimensional representation of a connected solvable group is upper triangularizable.
• exists_basis_coefficientMatrix_isUpperTriangular_of_geometricallySolvable: the same theorem stated with the geometric connectedness and solvability object properties.

The corresponding declarations taking I and hID apply to any closed subgroup containing the derived subgroup.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, Theorem 6.3.1.
• A. Borel, Linear Algebraic Groups, Section 10.5.
• J. E. Humphreys, Linear Algebraic Groups, Section 17.6.

theorem TauCeti.Comodule.hasNonzeroWeightVector_of_nonzeroJointWeight_commutator {k : Type u} {H : Type v} {M : Type w} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [Module k M] [Comodule k H M] [FiniteDimensional k M] [ConnectedSpace (PrimeSpectrum H)] (χ : NonzeroJointWeight (commutator (WithConv (H →ₐ[k] k))) (basePointsRepresentation M)) : HasNonzeroWeightVector k H M

A nonzero joint weight for the commutator subgroup supplies a weight vector for the whole reduced connected affine group. This is the induction step from a commutator eigenvector to an ambient eigenline in Lie--Kolchin.

theorem TauCeti.Comodule.hasNonzeroWeightVector_of_forall_isUnipotentPoint_of_le_derivedDefiningIdeal {k : Type u} {H : Type v} {M : Type w} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [Module k M] [Comodule k H M] [FiniteDimensional k M] [Nontrivial M] (I : HopfIdeal k H) (hID : I ≤ CommHopfAlgCat.derivedDefiningIdeal H) (hI : ∀ (g : WithConv (↑(CommHopfAlgCat.quotient (↧H) I) →ₐ[k] k)), HopfAlgebra.IsUnipotentPoint g) : HasNonzeroWeightVector k H M

If a closed subgroup containing the derived subgroup acts unipotently, then every nonzero finite-dimensional representation has a nonzero weight vector.

theorem TauCeti.Comodule.hasNonzeroWeightVector_of_forall_isUnipotentPoint_derived {k : Type u} {H : Type v} {M : Type w} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [Module k M] [Comodule k H M] [FiniteDimensional k M] [Nontrivial M] (hderived : ∀ (g : WithConv (↑(CommHopfAlgCat.quotient (↧H) (CommHopfAlgCat.derivedDefiningIdeal H)) →ₐ[k] k)), HopfAlgebra.IsUnipotentPoint g) : HasNonzeroWeightVector k H M

If every point of the derived closed subgroup acts unipotently, then every nonzero finite-dimensional representation has a nonzero weight vector.

This is the representation-theoretic reduction in Lie--Kolchin. The hypothesis concerns the coordinate algebra H / derivedDefiningIdeal H of the scheme-theoretic derived subgroup, not merely the abstract commutator subgroup of H(k).

theorem TauCeti.Comodule.hasNonzeroWeightVector_of_geometricallyUnipotent_of_le_derivedDefiningIdeal {k : Type u} {H : Type v} {M : Type w} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [Module k M] [Comodule k H M] [FiniteDimensional k M] [Nontrivial M] (I : HopfIdeal k H) (hID : I ≤ CommHopfAlgCat.derivedDefiningIdeal H) (hI : geometricallyUnipotentPointsCommHopfAlgProperty k (CommHopfAlgCat.quotient (↧H) I)) : HasNonzeroWeightVector k H M

If a geometrically unipotent closed subgroup contains the derived subgroup, then every nonzero finite-dimensional representation has a nonzero weight vector.

theorem TauCeti.Comodule.hasNonzeroWeightVector_of_geometricallyUnipotent_derived {k : Type u} {H : Type v} {M : Type w} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [Module k M] [Comodule k H M] [FiniteDimensional k M] [Nontrivial M] (hderived : geometricallyUnipotentPointsCommHopfAlgProperty k (CommHopfAlgCat.quotient (↧H) (CommHopfAlgCat.derivedDefiningIdeal H))) : HasNonzeroWeightVector k H M

If the derived closed subgroup is geometrically unipotent, then every nonzero finite-dimensional representation has a nonzero weight vector.

theorem TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_unipotentPoints_of_le_derived {k : Type u} {H : Type v} {M : Type w} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [Module k M] [Comodule k H M] [FiniteDimensional k M] (I : HopfIdeal k H) (hID : I ≤ CommHopfAlgCat.derivedDefiningIdeal H) (hI : ∀ (g : WithConv (↑(CommHopfAlgCat.quotient (↧H) I) →ₐ[k] k)), HopfAlgebra.IsUnipotentPoint g) : ∃ (n : ℕ) (b : Module.Basis (Fin n) k M), (coefficientMatrix b).IsUpperTriangular ∧ ∀ (i : Fin n), IsGroupLikeElem k (coefficientMatrix b i i)

If a unipotent closed subgroup contains the derived subgroup, then every finite-dimensional representation admits an upper-triangular basis with characters on the diagonal.

theorem TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_forall_isUnipotentPoint_derived {k : Type u} {H : Type v} {M : Type w} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [Module k M] [Comodule k H M] [FiniteDimensional k M] (hderived : ∀ (g : WithConv (↑(CommHopfAlgCat.quotient (↧H) (CommHopfAlgCat.derivedDefiningIdeal H)) →ₐ[k] k)), HopfAlgebra.IsUnipotentPoint g) : ∃ (n : ℕ) (b : Module.Basis (Fin n) k M), (coefficientMatrix b).IsUpperTriangular ∧ ∀ (i : Fin n), IsGroupLikeElem k (coefficientMatrix b i i)

Lie--Kolchin under unipotence of the derived subgroup. If every point of the derived closed subgroup of a reduced finite-type affine group over an algebraically closed field is unipotent, then every finite-dimensional representation admits a basis in which its coefficient matrix is upper triangular, with characters on the diagonal.

theorem TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_geometricallyUnipotent_of_le_derived {k : Type u} {H : Type v} {M : Type w} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [Module k M] [Comodule k H M] [FiniteDimensional k M] (I : HopfIdeal k H) (hID : I ≤ CommHopfAlgCat.derivedDefiningIdeal H) (hI : geometricallyUnipotentPointsCommHopfAlgProperty k (CommHopfAlgCat.quotient (↧H) I)) : ∃ (n : ℕ) (b : Module.Basis (Fin n) k M), (coefficientMatrix b).IsUpperTriangular ∧ ∀ (i : Fin n), IsGroupLikeElem k (coefficientMatrix b i i)

If a geometrically unipotent closed subgroup contains the derived subgroup, then every finite-dimensional representation admits an upper-triangular basis with characters on the diagonal.

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

Geometric Lie--Kolchin reduction. If the derived closed subgroup of a reduced finite-type affine group over an algebraically closed field is geometrically unipotent, then every finite-dimensional representation admits an upper-triangular basis with characters on the diagonal.

theorem TauCeti.Comodule.hasNonzeroWeightVector_of_isSolvable {k : Type u} {H : Type v} {M : Type w} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [Module k M] [Comodule k H M] [FiniteDimensional k M] [Nontrivial M] [ConnectedSpace (PrimeSpectrum H)] [Group.IsSolvable (WithConv (H →ₐ[k] k))] : HasNonzeroWeightVector k H M

Lie--Kolchin, weight-vector form. If the rational points of a reduced connected affine group of finite type over an algebraically closed field form a solvable group, every nonzero finite-dimensional representation has a nonzero weight vector: a line on which the group acts through a character.

theorem TauCeti.Comodule.hasNonzeroWeightVector_of_geometricallySolvable {k : Type u} {H : Type v} {M : Type w} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [Module k M] [Comodule k H M] [FiniteDimensional k M] [Nontrivial M] (hconn : geometricallyConnectedCommHopfAlgProperty k ↧H) (hsolv : geometricallySolvablePointsCommHopfAlgProperty k ↧H) : HasNonzeroWeightVector k H M

Lie--Kolchin, geometric weight-vector form. Over an algebraically closed field, every nonzero finite-dimensional representation of a reduced, geometrically connected, geometrically solvable affine group of finite type has a nonzero weight vector.

theorem TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_isSolvable {k : Type u} {H : Type v} {M : Type w} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [Module k M] [Comodule k H M] [FiniteDimensional k M] [ConnectedSpace (PrimeSpectrum H)] [Group.IsSolvable (WithConv (H →ₐ[k] k))] : ∃ (n : ℕ) (b : Module.Basis (Fin n) k M), (coefficientMatrix b).IsUpperTriangular ∧ ∀ (i : Fin n), IsGroupLikeElem k (coefficientMatrix b i i)

The Lie--Kolchin theorem. If the rational points of a reduced connected affine group of finite type over an algebraically closed field form a solvable group, every finite-dimensional representation admits a basis in which its coefficient matrix is upper triangular, with characters on the diagonal.

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

The Lie--Kolchin theorem for the geometric object properties. Over an algebraically closed field, every finite-dimensional representation of a reduced, geometrically connected, geometrically solvable affine group of finite type admits a basis in which its coefficient matrix is upper triangular, with characters on the diagonal.

These are the connectedness and solvability conditions in the definition of a Borel candidate.