How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Affine finite-type group schemes have faithful finite-dimensional representations
Statement
Let be an affine finite-type group scheme over an arbitrary field . Every right comodule over its coordinate Hopf algebra is the filtered union of its finite-dimensional subcomodules. The right regular representation of on contains a finite-dimensional subrepresentation such that is a closed immersion. These assertions allow nonreduced .
Facts & Assumptions
A group scheme has multiplication, identity and inversion morphisms; for affine their comorphisms are the coproduct , counit and antipode. The group identities become the Hopf identities. (Abelian varieties over a field)
Proof
Given: , , and a right -comodule , meaning and .
Fix and write with the linearly independent. Let be the finite-dimensional space containing the and every second-factor coefficient of the finitely many . Choose linear functionals with by extending this finite independent list to a basis of . Apply to coassociativity. It gives . Thus is a finite-dimensional subcomodule. The counit gives . Finite sums of subcomodules are subcomodules, proving the filtered-union assertion. Both sides lie in , so all these contractions are defined on finite coefficient spaces and require only finite choices.
Apply step 1.1 to the comodule and to a finite algebra-generating list for . Taking the sum gives a finite-dimensional subcomodule containing that list. In a basis of , write . Coassociativity and counit give and . The antipode gives an inverse for the matrix . Hence these entries define a homomorphism : for any -algebra and point , its matrix is . This is the right regular action , formulated on all algebras.
The image of contains every . Applying to gives , so that image contains , hence the algebra generators of . The ring map is onto and therefore the group morphism is a closed immersion. In particular it is injective on -points for every , including nonreduced algebras.