Finite-dimensional comodules generating a finite-type algebra-coalgebra

Let C be a coalgebra over a field which is also finitely generated as an algebra. Choose a finite algebra-generating set and place it in a finite-dimensional subcoalgebra D using the fundamental theorem of coalgebras. The regular coaction restricts to D, and every element of D is a matrix coefficient of this restricted comodule: pair it with the restriction of the counit. Consequently, the matrix coefficients of one finite-dimensional subcomodule generate the whole algebra C.

For a commutative Hopf algebra, this is the finite-dimensional construction at the heart of the affine-group embedding theorem. After choosing a basis, its coefficient matrix defines a map to GLₙ; the faithful-representation criterion identifies generation by its coefficients with a closed immersion.

Main declaration

• TauCeti.Comodule.exists_finite_subcomodule_matrixCoefficientSubalgebra_eq_top: a finite-type algebra-coalgebra over a field has a finite-dimensional subcomodule whose matrix coefficients generate the whole algebra.

References

This is the standard proof of the embedding theorem's finite-dimensional representation step; see J. S. Milne, Algebraic Groups (2017), Proposition 4.7 and Theorem 4.9. It advances Layer 1, "Embedding theorem (hard)", of the ReductiveGroups roadmap.

theorem TauCeti.Comodule.exists_finite_subcomodule_matrixCoefficientSubalgebra_eq_top {k : Type u} {C : Type v} [Field k] [Semiring C] [Algebra k C] [Coalgebra k C] [Algebra.FiniteType k C] : let x := Algebra.semiringToRing k; ∃ (M : Subcomodule k C C), Module.Finite k ↥M.toSubmodule ∧ matrixCoefficientSubalgebra = ⊤

A finite-type algebra-coalgebra over a field has a module-finite subcomodule of its regular comodule whose matrix coefficients generate the whole algebra. Over the field k, module-finite is finite-dimensional.