Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)
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 k be a field, let G be an affine group scheme of finite type over k with coordinate Hopf algebra A=O(G) (The coordinate Hopf algebra of an affine group scheme), and let V be a k-vector space. The construction of Rational representations and comodules of an affine group scheme is a bijection, natural in V and in G, between A-comodule structures ρ ⁣:V→V⊗kA and rational representations r ⁣:G→GL⁡V, and it maps subcomodules to subrepresentations. If V is finite dimensional with basis e1,…,en and ρ(ej)=∑iei⊗aij, then the matrix coefficients satisfy Δ(aij)=∑kaik⊗akj,ε(aij)=δij, and the comorphism of the associated morphism G→GL⁡n is xij↦aij. No choice principle is used.

Facts & Assumptions

[F1]

A rational representation is a natural family of group homomorphisms rR ⁣:G(R)→Aut⁡R(V⊗kR), and an A-comodule structure is a k-linear ρ ⁣:V→V⊗kA with (ρ⊗id⁡A)ρ=(id⁡V⊗Δ)ρ and (id⁡V⊗ε)ρ=id⁡V. (Rational representations and comodules of an affine group scheme, Commutative Hopf algebras over a field)

[F2]

G(R)=Hom⁡k-alg(A,R) is a group under the convolution product g∗h=mR∘(g⊗h)∘Δ, with identity the algebra map A→εk→R, and the universal points p1,p2 ⁣:A→A⊗kA, pi(a)= the two tensor embeddings, satisfy p1∗p2=Δ. (Group schemes of finite type over a field, The functor of points of an affine scheme)

[F3]

The Yoneda lemma identifies natural transformations hA→F on k-algebras with elements of F(A), naturally; for F=GL⁡V the functoriality is base change of A-linear automorphisms along A→R. (The Yoneda bijection Nat⁡(C(a,−),F)≅F(a) is natural in both a and F, The functor of points of an affine scheme)

[F4]

The choice-free coordinate and point constructions of the matrix supplier (without its finite-type conclusion) give the coordinate ring of GL⁡n is k[xij,d−1] with d=det⁡(xij) 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 det⁡(aij) a unit when (aij) 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)

[F5]

Ring homomorphisms correspond to morphisms of affine spectra contravariantly. (Affine schemes are contravariantly equivalent to commutative rings)

Proof

Given: A field k, an affine group scheme G of finite type over k with coordinate Hopf algebra A=O(G), a k-vector space V, and the definitions [F1].

1.1F1F2algebra

(From a comodule to a representation.) Let ρ ⁣:V→V⊗kA satisfy the comodule axioms. For a commutative unital k-algebra R and g∈G(R), define rR(g) to be the R-linear endomorphism of V⊗kR with rR(g)(v⊗x)=(id⁡V⊗g)ρ(v)⋅x. This is natural in R. If ρ(v)=∑ivi⊗ai, then rR(g)rR(h)(v⊗1)=∑i(id⁡V⊗g)ρ(vi)⋅h(ai)=(id⁡V⊗(gh))ρ(v)=rR(gh)(v⊗1) by coassociativity and the convolution product of [F2], and by R-linearity this proves multiplicativity; the counit identity gives rR(eR)=id⁡, since eR factors through ε. Hence each rR(g) is invertible with inverse rR(g−1) and r is a rational representation.

1.2F1F2F3algebra

(From a representation to a comodule.) Let r ⁣:G→GL⁡V be a rational representation. By [F3] it corresponds to the element φ=rA(id⁡A)∈GL⁡V(A)=Aut⁡A(V⊗kA), and naturality at g ⁣:A→R gives rR(g)(v⊗1)=(id⁡V⊗g)φ(v⊗1). Indeed (V⊗kA)⊗AR≅V⊗kR by (v⊗a)⊗x↦v⊗g(a)x, so the base-changed automorphism sends v⊗1 to (id⁡V⊗g)φ(v⊗1). Put ρ(v)=φ(v⊗1); then φ(v⊗a)=ρ(v)a by A-linearity, and rR(g)(v⊗1)=(id⁡V⊗g)ρ(v). The identity element of G(k) is ε, so rk(ε)=id⁡ gives (id⁡V⊗ε)ρ=id⁡V. For coassociativity, p1∗p2=Δ in G(A⊗kA) by [F2], so rA⊗kA(Δ)=rA⊗kA(p1)rA⊗kA(p2), and evaluating at v⊗1 gives ∑iρ(vi)⊗ai=∑ivi⊗Δ(ai), that is, (ρ⊗id⁡A)ρ=(id⁡V⊗Δ)ρ. Hence ρ is a comodule structure.

1.3F1F6algebra

(Matrix coefficients.) Let V be finite dimensional with basis e1,…,en and ρ(ej)=∑iei⊗aij. Comparing the components of ei under the finite coordinate functionals of V in the coassociativity identity gives Δ(aij)=∑lail⊗alj, and comparing them in (id⁡V⊗ε)ρ(ej)=ej gives ε(aij)=δij.

2.1F1F3step 1.1step 1.2

(The two constructions are inverse.) If ρ gives r by step 1.1 and r gives ρ′ by step 1.2, then ρ′(v)=rA(id⁡A)(v⊗1)=(id⁡V⊗id⁡A)ρ(v)=ρ(v); conversely if r gives ρ and ρ gives r′, then rR′(g) and rR(g) are R-linear and agree on all v⊗1 by step 1.2, hence r′=r. For a linear map T ⁣:V→W between two such structures, (T⊗id⁡A)ρV=ρWT implies (T⊗id⁡R)rV,R(g)=rW,R(g)(T⊗id⁡R) by evaluation; conversely the latter identities at R=A, g=id⁡A give the former. Pullback along a group morphism f ⁣:H→G is (id⁡V⊗O(f))ρ on coactions and r∘f on actions. These formulas specify the asserted naturality.

2.2F1step 1.1step 1.2

(Subcomodules and subrepresentations.) If N⊆V is a subcomodule, then rR(g)(N⊗kR)=(id⁡V⊗g)ρ(N)⋅R⊆N⊗kR for every R and g by step 1.1, so N is a subrepresentation. Conversely, if N is stable under every rR(g), then taking R=A and g=id⁡A in step 1.2 gives ρ(N)=rA(id⁡A)(N⊗1)⊆N⊗kA, so N is a subcomodule. The correspondence preserves inclusions.

3.1F3F4F5step 1.1step 1.3∎

(The comorphism of the associated morphism.) If V=0, both structures are unique and the associated morphism is G→GL⁡0=Spec⁡k, with comorphism the structure map k→A; the coefficient identities are empty. Otherwise n≥1. In the situation of step 1.3, the two antipode identities give ∑lS(ail)alj=δij=∑lailS(alj), so the matrix (aij) over the commutative ring A has two-sided inverse (S(aij)) and therefore unit determinant by [F4]. Hence φ ⁣:k[xij,d−1]→A, xij↦aij, d−1↦det⁡(aij)−1, is a well-defined k-algebra homomorphism, and by [F5] it is the comorphism of a morphism G→GL⁡n. On R-points this morphism sends g to the matrix (φ(xij)(g))=(g(aij)), which by step 1.1 and step 1.3 is exactly the matrix of rR(g) in the basis e1,…,en; by [F4] this identifies the morphism associated with r under the basis with GL⁡n and its comorphism with xij↦aij. 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

Used by

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