ExampleConstruction: Literature-sourcedVerification: 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.

A rational representation of the multiplicative group from a graded comodule

Example

Assume the Axiom of Choice for the finite-type construction of $G_{m}$ . Let $k$ be a field, let $G = G_{m} = Spec k [t, t^{- 1}]$ and let $V$ be a finite-dimensional $k$ -vector space with a direct-sum decomposition $V = ⨁_{m \in Z} V_{m}$ into weight spaces (all but finitely many zero). Then $ρ ⁣ : V \to V \otimes_{k} k [t, t^{- 1}], ρ (v) = \sum_{m} v_{m} \otimes t^{m} for v = \sum_{m} v_{m}, v_{m} \in V_{m},$ is a comodule structure on $V$ over the coordinate Hopf algebra (Rational representations and comodules of an affine group scheme), and the corresponding rational representation (Rational representations of an affine group scheme are comodules of its coordinate Hopf algebra) is the homomorphism $r_{R} ⁣ : R^{\times} \to {GL}_{R} (V \otimes_{k} R)$ whose action on $V_{m} \otimes_{k} R$ is multiplication by the scalar $g^{m}$ . Conversely, every comodule structure on $V$ arises in this way: putting $V_{m} = {v : ρ (v) = v \otimes t^{m}}$ gives $ρ (V_{m}) \subseteq V_{m} \otimes k [t, t^{- 1}]$ and $V = ⨁_{m} V_{m}$ . If $e_{1}, \dots, e_{n}$ is a basis of weight vectors, the associated comorphism $O ({GL}_{n}) \to k [t, t^{- 1}]$ sends $x_{i j}$ to $δ_{i j} t^{m_{i}}$ , and the matrix coefficients satisfy the identities of Rational representations of an affine group scheme are comodules of its coordinate Hopf algebra.

Verification

Given: AC for the finite-type construction of $G_{m}$ , a field $k$ , the group $G = G_{m}$ with coordinate Hopf algebra $k [t, t^{- 1}]$ , a finite-dimensional $k$ -vector space $V$ with weight decomposition $V = ⨁_{m \in Z} V_{m}$ , and the coaction $ρ (v) = \sum_{m} v_{m} \otimes t^{m}$ .

[F1] The comultiplication, counit and antipode of $k [t, t^{- 1}]$ are determined by $Δ (t^{m}) = t^{m} \otimes t^{m}$ , $ε (t^{m}) = 1$ and $S (t^{m}) = t^{- m}$ for all $m \in Z$ , and the points of $G_{m}$ over a $k$ -algebra $R$ are the units $g \in R^{\times}$ , acting by $g \cdot t^{m} = g^{m}$ . (The general linear group scheme and its coordinate ring)

[F2] A rational representation corresponds to a comodule structure by $r_{R} (g) (v \otimes 1) = ({id}_{V} \otimes g) ρ (v)$ , and for a finite-dimensional comodule with coefficients $ρ (e_{j}) = \sum_{i} e_{i} \otimes a_{i j}$ the identities $Δ (a_{i j}) = \sum_{l} a_{i l} \otimes a_{l j}$ , $ε (a_{i j}) = δ_{i j}$ hold and the associated comorphism sends $x_{i j} \mapsto a_{i j}$ . (Rational representations of an affine group scheme are comodules of its coordinate Hopf algebra, Rational representations and comodules of an affine group scheme)

[F3] The Laurent polynomial ring has unique finite monomial expansions. For each integer $m$ , the coefficient map $c_{m} ⁣ : k [t, t^{- 1}] \to k$ is therefore linear, and ${id}_{X} \otimes c_{m}$ takes $\sum_{n} y_{n} \otimes t^{n}$ to $y_{m}$ . Hence a zero tensor expression has all $y_{m} = 0$ . (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis, The tensor product $M \otimes_{R} N$ from the additive group underlying the free $Z$ -module on $M \times N$ , elementary tensors, and finite tensor sums, Linear subspace of a vector space)

1.1F1F2algebra

The map $ρ$ is a comodule structure: by [F1], $(ρ \otimes id) ρ (v) = \sum_{m} v_{m} \otimes t^{m} \otimes t^{m} = (id \otimes Δ) ρ (v)$ and $(id \otimes ε) ρ (v) = \sum_{m} v_{m} \otimes 1 = v$ .

1.2F1F3algebra

Conversely, let $ρ$ be any comodule structure on the finite-dimensional space $V$ . Writing $ρ (v) = \sum_{m} v_{m} \otimes t^{m}$ with finitely many nonzero terms, coassociativity and [F1] give $\sum_{m} ρ (v_{m}) \otimes t^{m} = \sum_{m} v_{m} \otimes t^{m} \otimes t^{m}$ , so $\sum_{m} (ρ (v_{m}) - v_{m} \otimes t^{m}) \otimes t^{m} = 0$ ; by [F3] each $ρ (v_{m}) = v_{m} \otimes t^{m}$ , so $v_{m} \in V_{m}$ with $V_{m} = {v : ρ (v) = v \otimes t^{m}}$ . The counit identity gives $v = \sum_{m} v_{m}$ , so the $V_{m}$ span $V$ , and a relation $\sum_{m} u_{m} = 0$ with $u_{m} \in V_{m}$ gives $\sum_{m} u_{m} \otimes t^{m} = 0$ and hence $u_{m} = 0$ by [F3]; thus $V = ⨁_{m} V_{m}$ . Applying the construction to a finite basis of $V$ , the union of the finitely many supports of its coaction expressions spans $V$ by weight vectors; hence all other $V_{m}$ vanish. Each $V_{m}$ is a linear subspace because its defining condition is linear.

2.1F1F2step 1.1algebra

By [F2] the associated representation is $r_{R} (g) (v \otimes 1) = (id \otimes g) ρ (v) = \sum_{m} v_{m} \otimes g^{m}$ for $g \in R^{\times}$ ; since $(v \otimes r)$ is mapped to $r \cdot \sum_{m} v_{m} \otimes g^{m}$ , the action on each $V_{m} \otimes_{k} R$ is multiplication by the scalar $g^{m}$ , and $r_{R}$ is a group homomorphism because $g \mapsto g^{m}$ is multiplicative; hence $ρ$ defines the stated rational representation.

3.1F1F2step 1.2step 2.1∎

Let $e_{1}, \dots, e_{n}$ be a basis of weight vectors with $e_{i} \in V_{m_{i}}$ , so that $a_{i j} = δ_{i j} t^{m_{i}}$ ; by [F2] the matrix coefficients satisfy $Δ (a_{i j}) = \sum_{l} a_{i l} \otimes a_{l j}$ and $ε (a_{i j}) = δ_{i j}$ , and the associated comorphism sends $x_{i j}$ to $δ_{i j} t^{m_{i}}$ . For $V = 0$ , use ${GL}_{0} = Spec k$ with comorphism $k \to k [t, t^{- 1}]$ and no matrix entries. Together with steps 1.2 and 2.1 this proves both directions of the stated dictionary, using only the explicit monomial basis of $k [t, t^{- 1}]$ and finitely many weight spaces.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

56 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)