Lie--Kolchin reduction to the derived subgroup

Let H be the coordinate Hopf algebra of a reduced affine group of finite type over an algebraically closed field. This file proves the representation-theoretic reduction at the heart of Lie--Kolchin: if the derived closed subgroup has only unipotent points, then every nonzero finite-dimensional H-comodule has a weight vector, and every finite-dimensional comodule is upper triangularizable.

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.

The remaining geometric step in the general Lie--Kolchin theorem is to prove that the derived subgroup of a connected solvable affine group is unipotent.

Main declarations

• 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.

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.

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 { X := H, commRing := inst✝, hopfAlgebra := inst✝¹ } 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 { X := H, commRing := inst✝, hopfAlgebra := inst✝¹ } (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 { X := H, commRing := inst✝, hopfAlgebra := inst✝¹ } 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 { X := H, commRing := inst✝, hopfAlgebra := inst✝¹ } (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 { X := H, commRing := inst✝, hopfAlgebra := inst✝¹ } 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 { X := H, commRing := inst✝, hopfAlgebra := inst✝¹ } (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 { X := H, commRing := inst✝, hopfAlgebra := inst✝¹ } 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 { X := H, commRing := inst✝, hopfAlgebra := inst✝¹ } (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.