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.
Rational representations of an affine group scheme are comodules of its coordinate Hopf algebra
Statement
Let be a field, let be an affine group scheme of finite type over with coordinate Hopf algebra (The coordinate Hopf algebra of an affine group scheme), and let be a -vector space. The construction of Rational representations and comodules of an affine group scheme is a bijection, natural in and in , between -comodule structures and rational representations , and it maps subcomodules to subrepresentations. If is finite dimensional with basis and , then the matrix coefficients satisfy and the comorphism of the associated morphism is . No choice principle is used.
Facts & Assumptions
A rational representation is a natural family of group homomorphisms , and an -comodule structure is a -linear with and . (Rational representations and comodules of an affine group scheme, Commutative Hopf algebras over a field)
is a group under the convolution product , with identity the algebra map , and the universal points , the two tensor embeddings, satisfy . (Group schemes of finite type over a field, The functor of points of an affine scheme)
The Yoneda lemma identifies natural transformations on -algebras with elements of , naturally; for the functoriality is base change of -linear automorphisms along . (The Yoneda bijection is natural in both and , The functor of points of an affine scheme)
The choice-free coordinate and point constructions of the matrix supplier (without its finite-type conclusion) give the coordinate ring of is with and points the invertible matrices, and the antipode identity together with A positive-sized square matrix over a commutative ring is invertible if and only if its determinant is a unit makes a unit when arises from a comodule. (The general linear group scheme and its coordinate ring, A positive-sized square matrix over a commutative ring is invertible if and only if its determinant is a unit)
Ring homomorphisms correspond to morphisms of affine spectra contravariantly. (Affine schemes are contravariantly equivalent to commutative rings)
A finite basis of a vector space gives explicit coordinate functionals, and the tensor product is generated by elementary tensors subject to the universal property. (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis, Vector space over a field, Linear map between vector spaces over the same field, The tensor product from the additive group underlying the free -module on , elementary tensors, and finite tensor sums, Universal property of the tensor product for balanced maps into abelian groups)
Proof
Given: A field , an affine group scheme of finite type over with coordinate Hopf algebra , a -vector space , and the definitions [F1].
(From a comodule to a representation.) Let satisfy the comodule axioms. For a commutative unital -algebra and , define to be the -linear endomorphism of with . This is natural in . If , then by coassociativity and the convolution product of [F2], and by -linearity this proves multiplicativity; the counit identity gives , since factors through . Hence each is invertible with inverse and is a rational representation.
(From a representation to a comodule.) Let be a rational representation. By [F3] it corresponds to the element , and naturality at gives . Indeed by , so the base-changed automorphism sends to . Put ; then by -linearity, and . The identity element of is , so gives . For coassociativity, in by [F2], so , and evaluating at gives , that is, . Hence is a comodule structure.
(Matrix coefficients.) Let be finite dimensional with basis and . Comparing the components of under the finite coordinate functionals of in the coassociativity identity gives , and comparing them in gives .
(The two constructions are inverse.) If gives by step 1.1 and gives by step 1.2, then ; conversely if gives and gives , then and are -linear and agree on all by step 1.2, hence . For a linear map between two such structures, implies by evaluation; conversely the latter identities at , give the former. Pullback along a group morphism is on coactions and on actions. These formulas specify the asserted naturality.
(Subcomodules and subrepresentations.) If is a subcomodule, then for every and by step 1.1, so is a subrepresentation. Conversely, if is stable under every , then taking and in step 1.2 gives , so is a subcomodule. The correspondence preserves inclusions.
(The comorphism of the associated morphism.) If , both structures are unique and the associated morphism is , with comorphism the structure map ; the coefficient identities are empty. Otherwise . In the situation of step 1.3, the two antipode identities give , so the matrix over the commutative ring has two-sided inverse and therefore unit determinant by [F4]. Hence , , , is a well-defined -algebra homomorphism, and by [F5] it is the comorphism of a morphism . On -points this morphism sends to the matrix , which by step 1.1 and step 1.3 is exactly the matrix of in the basis ; by [F4] this identifies the morphism associated with under the basis with and its comorphism with . All constructions used the given coaction or point-action, explicit finite bases and the functorialities of [F3]-[F5]; no choice principle is used.
Depends on
- Commutative Hopf algebras over a field
- The coordinate Hopf algebra of an affine group scheme
- The functor of points of an affine scheme
- Group schemes of finite type over a field
- Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis
- Invertible linear maps, linear isomorphisms, and inverse linear maps
- Linear map between vector spaces over the same field
- Rational representations and comodules of an affine group scheme
- The tensor product $M\otimes_R N$ from the additive group underlying the free $\mathbb Z$-module on $M\times N$, elementary tensors, and finite tensor sums
- Vector space over a field
- A positive-sized square matrix over a commutative ring is invertible if and only if its determinant is a unit
- The general linear group scheme and its coordinate ring
- Affine schemes are contravariantly equivalent to commutative rings
- Universal property of the tensor product for balanced maps into abelian groups
- The Yoneda bijection $\operatorname{Nat}(\mathcal C(a,-),F)\cong F(a)$ is natural in both $a$ and $F$
Used by
- A rational representation of the multiplicative group from a graded comodule Example
- Coconnected Hopf algebras give fixed vectors in every nonzero comodule Lemma
- Representations of diagonalizable groups split into character eigenspaces Lemma
- Tensor products, exterior powers and Hom spaces of finite-dimensional rational representations are rational Lemma
- Unipotence is equivalent to unipotence of all finite-dimensional representations Lemma
- Primitive vectors of the induced coordinate module Proposition
- A finitely generated affine group scheme has a faithful finite-dimensional representation Theorem
- Chevalley: every closed subgroup is a line stabilizer Theorem
Cited to discharge well-definedness by Rational representations and comodules of an affine group scheme.
Dependency tree · two levels
68 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- J. S. Milne, Algebraic Groups (corrected 2022 printing, Cambridge University Press) (standard reference, not scraped)
- J. Swanson (notes), J. Pevtsova (lecturer), Algebraic Groups Lecture Notes, University of Washington, Fall 2014 (standard reference, not scraped)