Detecting comodule fixed vectors on geometric points

Let H be a reduced commutative bialgebra of finite type over a field k, and let M be an H-comodule. A vector m : M is fixed by the coaction if and only if every point of H valued in an algebraically closed extension fixes 1 ⊗ m in the scalar extension.

The reverse implication is the substantive one. Evaluating the pointwise fixed-vector equation against every linear functional shows that every geometric point takes the corresponding matrix coefficient of m to its trivial-comodule value. Reduced finite-type point separation then identifies those coefficients in H. A finite-dimensional subspace containing the single tensor coact m - m ⊗ 1 has enough coordinate functionals to show that this tensor vanishes.

The representation-level restatements live in TauCeti.Algebra.AlgebraicGroup.Representation.PointsAction. This criterion is the bridge in the Kolchin induction for Layer 5 of the ReductiveGroups roadmap: a common fixed vector obtained from the geometric point representation is thereby promoted to a fixed vector of the comodule itself.

Main declarations

• TauCeti.Comodule.coact_eq_tmul_one_iff_forall_endOfPoint_tmul_eq: geometric-point detection of a fixed vector for a bialgebra comodule.

References

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

theorem TauCeti.Comodule.coact_eq_tmul_one_iff_forall_endOfPoint_tmul_eq {k : Type u} {H : Type v} {M : Type w} {K : Type x} [Field k] [CommRing H] [Bialgebra k H] [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [Module k M] [Comodule k H M] [Field K] [Algebra k K] [IsAlgClosed K] (m : M) : coact m = m ⊗ₜ[k] 1 ↔ ∀ (g : H →ₐ[k] K), (endOfPoint M g) (1 ⊗ₜ[k] m) = 1 ⊗ₜ[k] m

A vector in a comodule over a reduced finite-type bialgebra is fixed by the coaction exactly when every algebraically closed point fixes its scalar extension.