Point actions and coefficient matrices

Let M be a finite free comodule over a coalgebra C. In a basis b, the matrix of the endomorphism induced by an algebra-valued point g : C →ₐ[R] A is obtained by applying g entrywise to the coefficient matrix of M. Thus the coefficient matrix records all point actions simultaneously.

When C is a reduced finite-type commutative algebra over a field, its points valued in an algebraically closed extension separate elements. It follows that the coefficient matrix is upper triangular, or upper unitriangular, exactly when every point-action matrix has the corresponding property. The reverse implications are the important ones: they lift a common invariant flag found on geometric points to an actual flag by subcomodules.

Main declarations

• TauCeti.Comodule.toMatrix_endOfPoint: the matrix of a point action is the evaluated coefficient matrix.
• TauCeti.Comodule.charpoly_endOfPoint_comp: characteristic polynomials of point actions commute with scalar extension.
• TauCeti.Comodule.isUnipotent_pointsAction_of_coefficientMatrix_charpoly_eq: a universal characteristic-polynomial identity makes every point action unipotent.
• TauCeti.Comodule.coefficientMatrix_isUpperTriangular_iff_forall_toMatrix_endOfPoint: pointwise detection of upper triangularity.
• TauCeti.Comodule.coefficientMatrix_isUpperUnitriangular_iff_forall_toMatrix_endOfPoint: pointwise detection of upper unitriangularity.

References

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

This is the point-separation bridge in Layer 5, "Lie–Kolchin; solvable groups", of the ReductiveGroups roadmap. Lie–Kolchin produces a basis in which every geometric point acts triangularly; for a unipotent group the diagonal characters are trivial, and the results here turn that pointwise statement into the upper-unitriangular comodule flag used to embed the group in Uₙ.

@[simp]

theorem TauCeti.Comodule.toMatrix_endOfPoint {R : Type u} {C : Type v} {M : Type w} {A : Type x} {i : Type y} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [CommSemiring A] [Algebra R A] [Fintype i] [DecidableEq i] (b : Module.Basis i R M) (g : C →ₐ[R] A) : (LinearMap.toMatrix (Module.Basis.baseChange A b) (Module.Basis.baseChange A b)) (endOfPoint M g) = (coefficientMatrix b).map ⇑g

The matrix of the endomorphism induced by an algebra-valued point is obtained by applying that point entrywise to the comodule's coefficient matrix. The bases on the scalar extension are the base changes of the chosen basis of the comodule.

@[simp]

theorem TauCeti.Comodule.charpoly_endOfPoint_comp {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [Module.Free R M] [Module.Finite R M] {B : Type u_1} {D : Type u_2} [CommRing B] [Algebra R B] [CommRing D] [Algebra R D] (g : C →ₐ[R] B) (f : B →ₐ[R] D) : (endOfPoint M (f.comp g)).charpoly = Polynomial.map (↑f) (endOfPoint M g).charpoly

Composing a point with a morphism of value algebras maps the characteristic polynomial of its action along that morphism.

theorem TauCeti.Comodule.isUnipotent_pointsAction_of_coefficientMatrix_charpoly_eq {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] {M : Type w} [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Free k M] [Module.Finite k M] {L : Type x} [CommRing L] [Algebra k L] (g : WithConv (H →ₐ[k] L)) {ι : Type y} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι k M) (hCcharpoly : (coefficientMatrix b).charpoly = Polynomial.map (algebraMap k H) ((Polynomial.X - 1) ^ Module.finrank k M)) : (LinearMap.GeneralLinearGroup.ofLinearEquiv ((pointsAction M) g)).IsUnipotent

A universal X - 1 characteristic-polynomial identity makes the action of every point on the comodule unipotent.

theorem TauCeti.Comodule.coefficientMatrix_isUpperTriangular_iff_forall_toMatrix_endOfPoint {k : Type u} {C : Type v} {M : Type w} {K : Type x} {i : Type y} [Field k] [CommRing C] [Algebra k C] [Coalgebra k C] [Algebra.FiniteType k C] [IsReduced C] [AddCommGroup M] [Module k M] [Comodule k C M] [Field K] [Algebra k K] [IsAlgClosed K] [Fintype i] [LinearOrder i] (b : Module.Basis i k M) : (coefficientMatrix b).IsUpperTriangular ↔ ∀ (g : C →ₐ[k] K), ((LinearMap.toMatrix (Module.Basis.baseChange K b) (Module.Basis.baseChange K b)) (endOfPoint M g)).IsUpperTriangular

Over a reduced finite-type coordinate algebra, a coefficient matrix is upper triangular if and only if every algebraically closed point-action matrix is upper triangular.

theorem TauCeti.Comodule.coefficientMatrix_isUpperUnitriangular_iff_forall_toMatrix_endOfPoint {k : Type u} {C : Type v} {M : Type w} {K : Type x} {i : Type y} [Field k] [CommRing C] [Algebra k C] [Coalgebra k C] [Algebra.FiniteType k C] [IsReduced C] [AddCommGroup M] [Module k M] [Comodule k C M] [Field K] [Algebra k K] [IsAlgClosed K] [Fintype i] [LinearOrder i] (b : Module.Basis i k M) : (coefficientMatrix b).IsUpperUnitriangular ↔ ∀ (g : C →ₐ[k] K), ((LinearMap.toMatrix (Module.Basis.baseChange K b) (Module.Basis.baseChange K b)) (endOfPoint M g)).IsUpperUnitriangular

Over a reduced finite-type coordinate algebra, a coefficient matrix is upper unitriangular if and only if every algebraically closed point-action matrix is upper unitriangular.