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.

Distinct characters are linearly independent and eigenspace sums are direct

Statement

Let $k$ be a field and let $G = D_{k} (M)$ be a diagonalizable group over $k$ with coordinate ring $O (G) = k [M]$ and character group $M$ (Diagonalizable groups and their character modules). Distinct characters of $G$ are linearly independent as functions on $G$ : if $χ_{1}, \dots, χ_{r} \in M$ are pairwise distinct and $c_{1}, \dots, c_{r} \in k$ satisfy $\sum_{i} c_{i} χ_{i} = 0$ as elements of $k [M]$ , then $c_{1} = \dots = c_{r} = 0$ .

Consequently, if a rational representation $V$ of an affine algebraic group $G$ (Rational representations and comodules of an affine group scheme) over $k$ is written as a sum $V = \sum_{χ} V_{χ}$ of eigenspaces for pairwise distinct characters $χ$ , where $V_{χ} = {v \in V : r_{R} (g) (v \otimes 1) = χ_{R} (g) (v \otimes 1) for every R and g \in G (R)}$ , then the sum is direct: every family $(v_{χ})$ with $v_{χ} \in V_{χ}$ and $\sum_{χ} v_{χ} = 0$ has $v_{χ} = 0$ for all $χ$ .

Facts & Assumptions

Given: A field $k$ , a diagonalizable group $G = D_{k} (M)$ with $O (G) = k [M]$ , and pairwise distinct characters $χ_{1}, \dots, χ_{r} \in M$ .

[F1]

For an abelian group $M$ the group algebra $k [M]$ has $k$ -basis the elements $e_{m}$ for $m \in M$ , with $e_{m} e_{n} = e_{m + n}$ , unit $e_{0}$ , and Hopf maps $Δ (e_{m}) = e_{m} \otimes e_{m}$ , $ε (e_{m}) = 1$ , $S (e_{m}) = e_{- m}$ ; the character group of $D_{k} (M)$ is identified with $M$ via $m \leftrightarrow e_{m}$ , and $D_{k} (M) (R) = Hom (M, R^{\times})$ for every $k$ -algebra $R$ . (Diagonalizable groups and their character modules)

[F2]

A rational representation of an affine algebraic group $G$ is a $k$ -vector space $V$ with a linear action of $G$ , equivalently a comodule structure; for a character $χ$ the eigenspace $V_{χ}$ is the set of $v$ with $g \cdot v = χ (g) v$ for all $R$ -points $g$ and all $R$ . (Rational representations and comodules of an affine group scheme)

[F3]

A sum $\sum_{χ} V_{χ}$ inside $V$ is direct exactly when every relation $\sum_{χ} v_{χ} = 0$ with $v_{χ} \in V_{χ}$ forces all $v_{χ} = 0$ . (Linear subspace of a vector space)

Proof

Given: A field $k$ , a diagonalizable group $D_{k} (M)$ with character group $M$ , pairwise distinct characters $χ_{1}, \dots, χ_{r} \in M$ , and coefficients $c_{1}, \dots, c_{r} \in k$ .

1.1F1

By [F1] each $χ_{i}$ corresponds to the group-like element $e_{χ_{i}} \in k [M]$ : its comultiplication is $Δ (e_{χ_{i}}) = e_{χ_{i}} \otimes e_{χ_{i}}$ and its counit is $ε (e_{χ_{i}}) = 1$ , and the map $M \to k [M]$ , $m \mapsto e_{m}$ , is injective because the $e_{m}$ form a $k$ -basis indexed by $M$ .

1.2F1algebra

I claim that distinct group-like elements of a $k$ -coalgebra are linearly independent. Suppose not; choose a shortest relation $\sum_{i \in S} c_{i} e_{i} = 0$ with all $c_{i} \neq 0$ , the $e_{i}$ group-like and pairwise distinct, and $∣ S ∣ \geq 2$ minimal. Applying $Δ$ and subtracting the tensor product of the relation with $e_{s}$ for a fixed $s \in S$ gives $\sum_{i \in S ∖ {s}} c_{i} e_{i} \otimes (e_{i} - e_{s}) = 0$ . By minimality of $∣ S ∣$ , the elements $e_{i}$ for $i \neq s$ are linearly independent, so each $e_{i} - e_{s} = 0$ , contradicting distinctness. Hence $r \leq 1$ , and then $c_{1} e_{1} = 0$ gives $c_{1} = 0$ because $e_{1} \neq 0$ .

2.1step 1.1step 1.2

By [step 1.1] the characters $χ_{1}, \dots, χ_{r}$ are distinct group-like elements of $k [M] = O (G)$ , so the relation $\sum_{i} c_{i} χ_{i} = 0$ is a linear relation among distinct group-like elements and forces $c_{1} = \dots = c_{r} = 0$ by [step 1.2]. This proves the independence statement.

3.1F2F3step 1.2algebra∎

For the second assertion, let $G$ now be any affine algebraic group and let $\sum_{i = 1}^{r} v_{i} = 0$ be a finite relation with $v_{i} \in V_{χ_{i}}$ and distinct characters. Applying the coaction gives $\sum_{i} v_{i} \otimes χ_{i} = 0$ in $V \otimes O (G)$ . Each character is group-like in $O (G)$ , so step 1.2 makes the $χ_{i}$ linearly independent. Finite tensor coefficient comparison therefore gives $v_{i} = 0$ for every $i$ : the character span has basis $(χ_{i})$ , and the coefficient equations can be checked in finite-dimensional spans of the vectors involved in a tensor relation. This uses no separation by the dual of an arbitrary-dimensional space. By [F3] the eigenspace sum is direct.

Depends on

Used by

Dependency tree · two levels

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